Massive doc upgrade for .mli

src/backend/backend_intf.ml

@@ -1,6 +1,27 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+(** Backend interface
+
+    This modules defines the interface of the modules providing
+    export of proofs.
+*)
 
 module type S = sig
+  (** Proof exporting
+
+      Currently, exporting a proof means printing it into a file
+      according to the conventions of a given format.
+  *)
+
   type t
+  (** The type of proofs. *)
+
   val print : Format.formatter -> t -> unit
+  (** A function for printing proofs in the desired format. *)
+
 end
 

src/backend/dot.ml

@@ -1,3 +1,8 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
 
 module type S = Backend_intf.S
 

src/backend/dot.mli

@@ -1,14 +1,50 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+(** Dot backend for proofs
+
+    This modules provides functions to export proofs into the dot graph format.
+    Graphs in dot format can be used to generates images using the graphviz tool.
+*)
 
 module type S = Backend_intf.S
+(** Interface for exporting proofs. *)
 
 module type Arg = sig
+  (** Term printing for DOT
+
+      This module defines what functions are required in order to export
+      a proof to the DOT format.
+  *)
+
   type atom
+  (** The type of atomic formuals *)
+
   type lemma
+  (** The type of theory-specifi proofs (also called lemmas). *)
 
   val print_atom : Format.formatter -> atom -> unit
+  (** Print the contents of the given atomic formulas.
+      WARNING: this function should take care to esapce and/or not output special
+      reserved characters for the dot format (such as quotes and so on). *)
+
   val lemma_info : lemma -> string * string option * (Format.formatter -> unit -> unit) list
+  (** Generate some information about a theory specific lemmas. This backend does not
+      support printing of proper proofs in DOT format, so all proofs are printed as leafs
+      of the resolution tree. This function should return a triplet [(rule, color, l)],
+      such that:
+      - [rule] is a name for the proof (arbitrary, does not need to be unique, but
+        should rather be descriptive)
+      - [color] is a color name (optional) understood by DOT
+      - [l] is a list of printers that will be called to print some additional information
+  *)
+
 end
 
 module Make(S : Res.S)(A : Arg with type atom := S.atom and type lemma := S.lemma) :
   S with type t := S.proof
+(** Functor for making a module to export proofs to the DOT format. *)
 

src/core/expr_intf.ml

@@ -4,9 +4,16 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
+(** Mcsat expressions
+
+    This modules defines the required implementation of expressions for Mcsat.
+*)
+
 type negated = Formula_intf.negated =
-  | Negated (* changed sign *)
+  | Negated     (** changed sign *)
-  | Same_sign (* kept sign *)
+  | Same_sign   (** kept sign *)
+(** This type is used during the normalisation of formulas.
+    See {!val:Expr_intf.S.norm} for more details. *)
 
 module type S = sig
   (** Signature of formulas that parametrises the Mcsat Solver Module. *)
@@ -15,29 +22,41 @@ module type S = sig
   (** An abstract type for proofs *)
 
   module Term : sig
+    (** McSat Terms *)
 
     type t
     (** The type of terms *)
 
-    val hash : t -> int
     val equal : t -> t -> bool
+    (** Equality over terms. *)
+
+    val hash : t -> int
+    (** Hashing function for terms. Should be such that two terms equal according
+        to {!val:Expr_intf.S.equal} have the same hash. *)
+
     val print : Format.formatter -> t -> unit
-    (** Common functions *)
+    (** Printing function used among other for debugging. *)
 
   end
 
   module Formula : sig
+    (** McSat formulas *)
 
     type t
     (** The type of atomic formulas over terms. *)
 
-    val hash : t -> int
     val equal : t -> t -> bool
+    (** Equality over formulas. *)
+
+    val hash : t -> int
+    (** Hashing function for formulas. Should be such that two formulas equal according
+        to {!val:Expr_intf.S.equal} have the same hash. *)
+
     val print : Format.formatter -> t -> unit
-    (** Common functions *)
+    (** Printing function used among other thing for debugging.  *)
 
     val dummy : t
-    (** Formula constants. A valid formula should never be physically equal to [dummy] *)
+    (** Constant formula. A valid formula should never be physically equal to [dummy] *)
 
     val neg : t -> t
     (** Formula negation *)

src/core/formula_intf.ml

@@ -4,12 +4,20 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
+(** SMT formulas
+
+    This module defines the required implementation of formulas for
+    an SMT solver.
+*)
+
 type negated =
-  | Negated (* changed sign *)
+  | Negated     (** changed sign *)
-  | Same_sign (* kept sign *)
+  | Same_sign   (** kept sign *)
+(** This type is used during the normalisation of formulas.
+    See {!val:Expr_intf.S.norm} for more details. *)
 
 module type S = sig
-  (** Signature of formulas that parametrises the SAT/SMT Solver Module. *)
+  (** SMT formulas *)
 
   type t
   (** The type of atomic formulas. *)
@@ -17,13 +25,18 @@ module type S = sig
   type proof
   (** An abstract type for proofs *)
 
-  val hash : t -> int
   val equal : t -> t -> bool
+  (** Equality over formulas. *)
+
+  val hash : t -> int
+    (** Hashing function for formulas. Should be such that two formulas equal according
+        to {!val:Expr_intf.S.equal} have the same hash. *)
+
   val print : Format.formatter -> t -> unit
-  (** Common functions *)
+  (** Printing function used among other thing for debugging.  *)
 
   val dummy : t
-  (** Formula constants. A valid formula should never be physically equal to [dummy] *)
+  (** Formula constant. A valid formula should never be physically equal to [dummy] *)
 
   val neg : t -> t
   (** Formula negation *)

src/core/plugin_intf.ml

@@ -12,38 +12,54 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(** McSat Theory
+
+    This module defines what a theory must implement in order to
+    be sued in a McSat solver.
+*)
+
 type 'term eval_res =
-  | Unknown
+  | Unknown                       (** The given formula does not have an evaluation *)
-  | Valued of bool * ('term list)
+  | Valued of bool * ('term list) (** The given formula can be evaluated to the given bool.
-(** The type of evaluation results, either the given formula cannot be
+                                      The list of terms to give is the list of terms that
-    evaluated, or it can thanks to assignment. In that case, the level
+                                      were effectively used for the evaluation.
-    of the evaluation is the maximum of levels of assignemnts needed
+                                      *)
-    to evaluate the given formula. *)
+(** The type of evaluation results for a given formula.
+    For instance, let's suppose we want to evaluate the formula [x * y = 0], the
+    following result are correct:
+    - [Unknown] if neither [x] nor [y] are assigned to a value
+    - [Valued (true, [x])] if [x] is assigned to [0]
+    - [Valued (true, [y])] if [y] is assigned to [0]
+    - [Valued (false, [x; y])] if [x] and [y] are assigned to 1 (or any non-zero number)
+  *)
 
 type ('formula, 'proof) res =
   | Sat
+    (** The current set of assumptions is satisfiable. *)
   | Unsat of 'formula list * 'proof
-(** Type returned by the theory, either the current set of assumptions is satisfiable,
+    (** The current set of assumptions is *NOT* satisfiable, and here is a
-    or it is not, in which case a tautological clause (hopefully minimal) is returned.
+        theory tautology (with its proof), for which every litteral is false
-    Formulas in the unsat clause must come from the current set of assumptions, i.e
+        under the current assumptions. *)
-    must have been encountered in a slice. *)
+(** Type returned by the theory. Formulas in the unsat clause must come from the
+    current set of assumptions, i.e must have been encountered in a slice. *)
 
 type ('term, 'formula) assumption =
-  | Lit of 'formula
+  | Lit of 'formula         (** The given formula is asserted true by the solver *)
-  | Assign of 'term * 'term
+  | Assign of 'term * 'term (** The first term is assigned to the second *)
-(** Asusmptions made by the core SAT solver. Can be either a formula, or an assignment.
+(** Asusmptions made by the core SAT solver. *)
-    Assignemnt are given a level. *)
 
 type ('term, 'formula, 'proof) slice = {
-  start : int;
+  start : int;                                (** Start of the slice *)
-  length : int;
+  length : int;                               (** Length of the slice *)
-  get : int -> ('term, 'formula) assumption;
+  get : int -> ('term, 'formula) assumption;  (** Accessor for the assertions in the slice.
-  push : 'formula list -> 'proof -> unit;
+                                                  Should only be called on integers [i] s.t.
-  propagate : 'formula -> 'term list -> unit;
+                                                  [start <= i < start + length] *)
+  push : 'formula list -> 'proof -> unit;     (** Add a clause to the solver. *)
+  propagate : 'formula -> 'term list -> unit; (** Propagate a formula, i.e. the theory can
+                                                  evaluate the formula to be true (see the
+                                                  definition of {!type:eval_res} *)
 }
-(** The type for a slice of litterals to assume/propagate in the theory.
+(** The type for a slice of assertions to assume/propagate in the theory. *)
-    [get] operations should only be used for integers [ start <= i < start + length].
-    [push clause proof] allows to add a tautological clause to the sat solver. *)
 
 module type S = sig
   (** Signature for theories to be given to the Model Constructing Solver. *)

src/core/res.mli

@@ -4,7 +4,14 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
+(** Resolution proofs
+
+    This modules defines functions to create and manipulate resolution proofs.
+*)
+
 module type S = Res_intf.S
+(** Interface for a module manipulating resolution proofs. *)
 
 module Make : functor (St : Solver_types.S) -> S with module St = St
 (** Functor to create a module building proofs from a sat-solver unsat trace. *)
+

src/core/res_intf.ml

@@ -4,6 +4,8 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
+(** Interface for proofs *)
+
 module type S = sig
   (** Signature for a module handling proof by resolution from sat solving traces *)
 
@@ -21,19 +23,28 @@ module type S = sig
   (** Abstract types for atoms, clauses and theory-specific lemmas *)
 
   type proof
-  and proof_node = {
-    conclusion : clause;
-    step : step;
-  }
-  and step =
-    | Hypothesis
-    | Assumption
-    | Lemma of lemma
-    | Resolution of proof * proof * atom
   (** Lazy type for proof trees. Proofs are persistent objects, and can be
       extended to proof nodes using functions defined later. *)
+  and proof_node = {
+    conclusion : clause;  (** The conclusion of the proof *)
+    step : step;          (** The reasoning step used to prove the conclusion *)
+  }
+  (** A proof can be expanded into a proof node, which show the first step of the proof. *)
+  and step =
+    | Hypothesis
+      (** The conclusion is a user-provided hypothesis *)
+    | Assumption
+      (** The conclusion has been locally assumed by the user *)
+    | Lemma of lemma
+      (** The conclusion is a tautology provided by the theory, with associated proof *)
+    | Resolution of proof * proof * atom
+      (** The conclusion can be deduced by performing a resolution between the conclusions
+          of the two given proofs. The atom on which to perform the resolution is also given. *)
+  (** The type of reasoning steps allowed in a proof. *)
+
 
   (** {3 Resolution helpers} *)
+
   val to_list : clause -> atom list
   (** Returns the sorted list of atoms of a clause. *)
 
@@ -45,6 +56,7 @@ module type S = sig
       [resolve (List.merge l1 l2)] where [l1] and [l2] are sorted atom lists should return the pair
       [\[a\], l'], where [l'] is the result of the resolution of [l1] and [l2] over [a]. *)
 
+
   (** {3 Proof building functions} *)
 
   val prove : clause -> proof
@@ -58,6 +70,7 @@ module type S = sig
   val prove_atom : atom -> proof option
   (** Given an atom [a], returns a proof of the clause [\[a\]] if [a] is true at level 0 *)
 
+
   (** {3 Proof Manipulation} *)
 
   val expand : proof -> proof_node
@@ -72,6 +85,7 @@ module type S = sig
   (** Returns the unsat_core of the given proof, i.e the lists of conclusions of all leafs of the proof.
       More efficient than using the [fold] function since it has access to the internal representation of proofs *)
 
+
   (** {3 Misc} *)
 
   val check : proof -> unit

src/core/solver_intf.ml

@@ -4,6 +4,11 @@ Copyright 2016 Guillaume Bury
 Copyright 2016 Simon Cruanes
 *)
 
+(** Interface for Solvers
+    This modules defines the safe external interface for solvers.
+    Solvers that implements this interface can be obtained using the [Make]
+    functor in {!Solver} or {!Mcsolver}. *)
+
 type ('term, 'form) sat_state = {
   eval: 'form -> bool;
   (** Returns the valuation of a formula in the current state
@@ -21,6 +26,7 @@ type ('term, 'form) sat_state = {
   model: unit -> ('term * 'term) list;
   (** Returns the model found if the formula is satisfiable. *)
 }
+(** The type of values returned when the solver reaches a SAT state. *)
 
 type ('clause, 'proof) unsat_state = {
   unsat_conflict : unit -> 'clause;
@@ -28,7 +34,10 @@ type ('clause, 'proof) unsat_state = {
   get_proof : unit -> 'proof;
   (** returns a persistent proof of the empty clause from the Unsat result. *)
 }
+(** The type of values returned when the solver reaches an UNSAT state. *)
 
+(** The external interface implemented by safe solvers, such as the one
+    created by the {!Solver.Make} and {!Mcsolver.Make} functors. *)
 module type S = sig
 
   (** {2 Internal modules}
@@ -36,8 +45,11 @@ module type S = sig
       if you're not familiar with the internals of mSAT. *)
 
   module St : Solver_types.S
+  (** WARNING: Very dangerous module that expose the internal representation used
+      by the solver. *)
 
   module Proof : Res.S with module St = St
+  (** A module to manipulate proofs. *)
 
   (** {2 Types} *)
 
@@ -46,7 +58,7 @@ module type S = sig
 
   type res =
     | Sat of (St.term,St.formula) sat_state
-    | Unsat of (St.clause,Proof.proof) unsat_state
+    | Unsat of (St.clause,Proof.proof) unsat_state (**)
   (** Result type for the solver *)
 
   exception UndecidedLit

src/core/theory_intf.ml

@@ -12,23 +12,33 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(** SMT Theory
+
+    This module defines what a theory must implement in order to
+    be used in an SMT solver.
+*)
+
 type ('formula, 'proof) res = ('formula, 'proof) Plugin_intf.res =
   | Sat
+    (** The current set of assumptions is satisfiable. *)
   | Unsat of 'formula list * 'proof
-(** Type returned by the theory, either the current set of assumptions is satisfiable,
+    (** The current set of assumptions is *NOT* satisfiable, and here is a
-    or it is not, in which case a tautological clause (hopefully minimal) is returned.
+        theory tautology (with its proof), for which every litteral is false
-    Formulas in the unsat clause must come from the current set of assumptions, i.e
+        under the current assumptions. *)
-    must have been encountered in a slice. *)
+(** Type returned by the theory. Formulas in the unsat clause must come from the
+    current set of assumptions, i.e must have been encountered in a slice. *)
 
 type ('form, 'proof) slice = {
-  start : int;
+  start : int;                        (** Start of the slice *)
-  length : int;
+  length : int;                       (** Length of the slice *)
-  get : int -> 'form;
+  get : int -> 'form;                 (** Accesor for the formuals in the slice.
-  push : 'form list -> 'proof -> unit;
+                                          Should only be called on integers [i] s.t.
+                                          [start <= i < start + length] *)
+  push : 'form list -> 'proof -> unit; (** Allows to add to the solver a clause. *)
 }
-(** The type for a slice of literals to assume/propagate in the theory.
+(** The type for a slice. Slices are some kind of view of the current
-    [get] operations should only be used for integers [ start <= i < start + length].
+    propagation queue. They allow to look at the propagated literals,
-    [push clause proof] allows to add a tautological clause to the sat solver. *)
+    and to add new clauses to the solver. *)
 
 module type S = sig
   (** Signature for theories to be given to the Solver. *)

src/doc.txt

@@ -6,10 +6,10 @@ This code is free, under the Apache 2.0 license.
 
 {2 Contents}
 
-mSAT is an ocaml library provinding SAT/SMT/McSat solvers. More precisely,
+mSAT is an ocaml library providing SAT/SMT/McSat solvers. More precisely,
 what mSAT provides are functors to easily create such solvers. Indeed, the core
 of a sat solver does not need much information about neither the exact representation
-of terms nor the innner workings of a theory.
+of terms nor the inner workings of a theory.
 
 {4 Solver creation}
 
@@ -18,6 +18,7 @@ simply an SMT solver with an empty theory).
 
 {!modules:
 Solver
+Solver_intf
 Formula_intf
 Theory_intf
 }
@@ -26,6 +27,7 @@ The following modules allow the creation of a McSat solver (Model Constructing s
 
 {!modules:
 Mcsolver
+Solver_intf
 Expr_intf
 Plugin_intf
 }

src/msat.odocl

@@ -27,17 +27,17 @@ backend/Dedukti
 backend/Backend_intf
 
 # SAT solver frontend
-sat/Sat
+#sat/Sat
-sat/Expr_sat
+#sat/Expr_sat
-sat/Type_sat
+#sat/Type_sat
 
 # SMT solver frontend
-smt/Smt
+#smt/Smt
-smt/Expr_smt
+#smt/Expr_smt
-smt/Type_smt
+#smt/Type_smt
-smt/Unionfind
+#smt/Unionfind
 
 # MCsat solver frontend
-mcsat/Mcsat
+#mcsat/Mcsat
-mcsat/Eclosure
+#mcsat/Eclosure
-mcsat/Plugin_mcsat
+#mcsat/Plugin_mcsat

src/solver/mcsolver.mli

@@ -4,7 +4,11 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
+(** Create McSat solver
+    This module provides a functor to create an McSAt solver. *)
+
 module type S = Solver_intf.S
+(** The interface exposed by the solver. *)
 
 module Make (E : Expr_intf.S)
     (Th : Plugin_intf.S with type term = E.Term.t

src/solver/solver.mli

@@ -4,12 +4,18 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
-module type S = Solver_intf.S
+(** Create SAT/SMT Solvers
+    This module provides a functor to create an SMT solver. Additionally, it also
+    gives a functor that produce an adequate empty theory that can be given to the [Make]
+    functor in order to create a pure SAT solver. *)
+
+module type S = Solver_intf.S
+(** The interface of instantiated solvers. *)
 
-(** Simple case where the proof type is [unit] and the theory is empty *)
 module DummyTheory(F : Formula_intf.S) :
   Theory_intf.S with type formula = F.t
                  and type proof = F.proof
+(** Simple case where the proof type is [unit] and the theory is empty *)
 
 module Make (F : Formula_intf.S)
     (Th : Theory_intf.S with type formula = F.t
@@ -17,6 +23,6 @@ module Make (F : Formula_intf.S)
     (Dummy: sig end) :
   S with type St.formula = F.t
      and type St.proof = F.proof
-  (** Functor to create a SMT Solver parametrised by the atomic
+(** Functor to create a SMT Solver parametrised by the atomic
-      formulas and a theory. *)
+    formulas and a theory. *)
 

src/solver/tseitin.mli

@@ -4,8 +4,19 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
+(** Tseitin CNF conversion
+
+    This modules implements Tseitin's Conjunctive Normal Form conversion, i.e.
+    the ability to transform an arbitrary boolean formula into an equi-satisfiable
+    CNF, that can then be fed to a SAT/SMT/McSat solver.
+*)
+
+module type Arg = Tseitin_intf.Arg
+(** The implementation of formulas required to implement Tseitin's CNF conversion. *)
+
 module type S = Tseitin_intf.S
+(** The exposed interface of Tseitin's CNF conversion. *)
 
-module Make : functor
+module Make : functor (F : Arg) -> S with type atom = F.t
-  (F : Tseitin_intf.Arg) -> S with type atom = F.t
+(** This functor provides an implementation of Tseitin's CNF conversion. *)
 

src/solver/tseitin_intf.ml

@@ -10,46 +10,75 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(** Interfaces for Tseitin's CNF conversion *)
+
 module type Arg = sig
+  (** Formulas
+
+      This defines what is needed of formulas in order to implement
+      Tseitin's CNF conversion.
+  *)
 
   type t
-  (** Type of atomic formulas *)
+  (** Type of atomic formulas. *)
 
   val neg : t -> t
-  (** Negation of atomic formulas *)
+  (** Negation of atomic formulas. *)
 
   val fresh : unit -> t
-  (** Generate fresh formulas *)
+  (** Generate fresh formulas (that are different from any other). *)
 
   val print : Format.formatter -> t -> unit
-  (** Print the given formula *)
+  (** Print the given formula. *)
 
 end
 
 module type S = sig
+  (** CNF conversion
+
+      This modules allows to convert arbitrary boolean formulas
+      into CNF.
+  *)
 
-  (** The type of ground formulas *)
-  type t
   type atom
+  (** The type of atomic formulas. *)
+
+  type t
+  (** The type of arbitrary boolean formulas. Arbitrary boolean formulas
+      can be built using functions in this module, and then converted
+      to a CNF, which is a list of clauses that only use atomic formulas. *)
 
   val f_true : t
+  (** The [true] formula, i.e a formula that is always satisfied. *)
+
   val f_false : t
+  (** The [false] formula, i.e a formula that cannot be satisfied. *)
 
   val make_atom : atom -> t
-  (** [make_pred p] builds the atomic formula [p = true].
+  (** [make_atom p] builds the boolean formula equivalent to the atomic formula [p]. *)
-      @param sign the polarity of the atomic formula *)
 
   val make_not : t -> t
+  (** Creates the negation of a boolean formula. *)
+
   val make_and : t list -> t
+  (** Creates the conjunction of a list of formulas. An empty conjunction is always satisfied. *)
+
   val make_or : t list -> t
-  val make_imply : t -> t -> t
+  (** Creates the disjunction of a list of formulas. An empty disjunction is never satisfied. *)
-  val make_equiv : t -> t -> t
+
   val make_xor : t -> t -> t
+  (** [make_xor p q] creates the boolean formula "[p] xor [q]". *)
+
+  val make_imply : t -> t -> t
+  (** [make_imply p q] creates the boolean formula "[p] implies [q]". *)
+
+  val make_equiv : t -> t -> t
+  (** [make_equiv p q] creates the boolena formula "[p] is equivalent to [q]". *)
 
   val make_cnf : t -> atom list list
   (** [make_cnf f] returns a conjunctive normal form of [f] under the form: a
       list (which is a conjunction) of lists (which are disjunctions) of
-      literals. *)
+      atomic formulas. *)
 
   val print : Format.formatter -> t -> unit
   (** [print fmt f] prints the formula on the formatter [fmt].*)