Added some documentation.

msat.odocl

@@ -1,7 +1,10 @@
 sat/Formula_intf
 sat/Explanation
+sat/Explanation_intf
+sat/Sat
 sat/Solver
 sat/Solver_types
+sat/Solver_types_intf
 sat/Theory_intf
 
 #smt/Arith

sat/explanation.mli

@@ -15,3 +15,4 @@
 module type S = Explanation_intf.S
 
 module Make : functor (St : Solver_types.S) -> S with type atom = St.atom
+(** Functor to create the types of explanations used in the Solver Module. *)

sat/explanation_intf.ml

@@ -13,6 +13,7 @@
 (**************************************************************************)
 
 module type S = sig
+  (** Signature for explanations. To be modified to allow passing bulks of assumptions to the theories. *)
 
   type t
   type exp

sat/formula_intf.ml

@@ -14,6 +14,7 @@
 (**************************************************************************)
 
 module type S = sig
+  (** Signature of formulas that parametrises the SMT Solver Module. *)
 
   type t
   (** The type of atomic formulas. *)
@@ -21,15 +22,14 @@ module type S = sig
   val true_ : t
   val false_ : t
   val dummy : t
-  (** Formula constants. [dummy] should be different from any other formula. *)
+  (** Formula constants. A valid formula should never be physically equal to [dummy] *)
 
   val neg : t -> t
   (** Formula negation *)
 
   val norm : t -> t * bool
   (** Returns a 'normalized' form of the formula, possibly negated (in which case return true).
-      WARNING: for the solver to cork correctly, the normalisation function must be so that
-      [a] and  [neg a] normalises to the same formula. *)
+      [norm] must be so that [a] and [neg a] normalises to the same formula. *)
 
   val hash : t -> int
   val equal : t -> t -> bool

sat/sat.mli

@@ -1,22 +1,39 @@
 (* Copyright 2014 Guillaume Bury *)
 
 module Make(Dummy: sig end) : sig
+    (** Fonctor to make a pure SAT Solver module with built-in literals. *)
+
     type atom
-    type state
+    (** Abstract type for atoms, i.e boolean literals. *)
+
     type res = Sat | Unsat
+    (** Type of results returned by the solve function. *)
 
     val new_atom : unit -> atom
+    (** [new_atom ()] returns a fresh literal. *)
+
     val neg : atom -> atom
+    (** [neg a] returns the negation of a literal. Involutive, i.e [neg (neg a) = a]. *)
 
     val hash : atom -> int
     val equal : atom -> atom -> bool
     val compare : atom -> atom -> int
+    (** Usual hash and comparison functions. For now, directly uses Pervasives and Hashtbl builtins. *)
 
     val print_atom : Format.formatter -> atom -> unit
+    (** Print the atom on the given formatter. *)
+
     val iter_atoms : (atom -> unit) -> unit
+    (** Allows iteration over all atoms created (even if unused). *)
 
     val solve : unit -> res
+    (** Returns the satisfiability status of the current set of assumptions. *)
+
     val eval : atom -> bool
+    (** Return the current assignement of the literals. *)
+
     val assume : atom list list -> unit
+    (** Add a list of clauses to the set of assumptions. *)
+
 end
 

sat/solver.ml

@@ -917,11 +917,10 @@ module Make (F : Formula_intf.S)
     env.model <- Vec.make 0 dummy_var;
     env.trail <- Vec.make 601 dummy_atom;
     env.trail_lim <- Vec.make 601 (-105);
-    env.tenv_queue <- Vec.make 100 (empty_theory);
+    env.tenv_queue <- Vec.make 100 Th.dummy;
     env.tatoms_queue <- Queue.create ();
     St.clear ()
 
-
   let copy (v : 'a) : 'a = Marshal.from_string (Marshal.to_string v []) 0
 
   let save () =

sat/solver.mli

@@ -15,19 +15,33 @@ module Make (F : Formula_intf.S)
     (St : Solver_types.S with type formula = F.t)
     (Ex : Explanation.S with type atom = St.atom)
     (Th : Theory_intf.S with type formula = F.t and type explanation = Ex.t) : sig
+  (** Functor to create a SMT Solver parametrised by the atomic formulas and a theory. *)
 
   exception Sat
   exception Unsat of St.clause list
+  (** Exceptions raised by the [solve] function to return the nature of the current set of assummtions.
+      Once the [Unsat] exception is raised, the solver needs to be cleared before anything else is done. *)
 
   type t
+  (** The type of the state of the sat solver. Mutable.*)
 
   val solve : unit -> unit
+  (** Try and solves the current set of assumptions.
+      @raise Sat if the current set of assummptions is satisfiable.
+      @raise Unsat if the current set of assumptions is unsatisfiable *)
+
   val assume : F.t list list -> cnumber : int -> unit
+  (** Add the list of clauses to the current set of assumptions. Modifies the sat solver state in place. *)
+
   val clear : unit -> unit
+  (** Resets everything done. Basically returns the solver to a state similar to when the module was created. *)
 
   val eval : F.t -> bool
+  (** Returns the valuation of a formula in the current state of the sat solver. *)
+
   val save : unit -> t
   val restore : t -> unit
+  (** Functions to be replaced by push&pop functions. *)
 
 end
 

sat/solver_types.mli

@@ -14,3 +14,4 @@
 module type S = Solver_types_intf.S
 
 module Make : functor (F : Formula_intf.S) -> S with type formula = F.t
+(** Functor to instantiate the types of clauses for the Solver. *)

sat/solver_types_intf.ml

@@ -12,6 +12,8 @@
 (**************************************************************************)
 
 module type S = sig
+  (** The signatures of clauses used in the Solver. *)
+
   type formula
 
   type var = {

sat/theory_intf.ml

@@ -13,16 +13,30 @@
 (**************************************************************************)
 
 module type S = sig
+  (** Singature for theories to be given to the Solver. *)
+
   type t
+  (** The type of states of the theory. Preferably not mutable. *)
+
   type formula
+  (** The type of formulas. Should be compatble with Formula_intf.S *)
+
   type explanation
+  (** The type of explanations. Should be compatible with
+      Explanations.S.t with module St = Solver_types.S with type formula = fomula *)
 
   exception Inconsistent of explanation
+  (** Exception raised by the theory when assuming an incoherent set of formulas. *)
 
   val dummy : t
+  (** A dummy theory state. Should be physically different from any valid theory state. *)
+
   val empty : unit -> t
+  (** A function to create an empty theory. *)
+
   val assume : cs:bool -> formula -> explanation -> t -> t
-  (** Any valid theory, either the empty one, or one returned by assume, should
-      be different from the dummy one. *)
+  (** Return a new theory state with the formula as assumption.
+      @raise Inconsistent if the new state would be inconsistent. *)
+
 end