Added Sat module to the lib. Updated README

README.md

@@ -37,12 +37,12 @@ as shown in the following code :
 
 ```ocaml
     (* Module initialization *)
-    module F = Msat.Sat.Tseitin
     module Sat = Msat.Sat.Make()
+    module F = Msat.Tseitin.Make(Msat.Sat.Expr)
 
     (* We create here two distinct atoms *)
-    let a = Msat.Sat.Fsat.fresh ()    (* A 'new_atom' is always distinct from any other atom *)
+    let a = Msat.Sat.Expr.fresh ()    (* A 'new_atom' is always distinct from any other atom *)
-    let b = Msat.Sat.Fsat.make 1      (* Atoms can be created from integers *)
+    let b = Msat.Sat.Expr.make 1      (* Atoms can be created from integers *)
 
     (* Let's create some formulas *)
     let p = F.make_atom a
@@ -52,12 +52,12 @@ as shown in the following code :
 
     (* We can try and check the satisfiability of the given formulas *)
     Sat.assume (F.make_cnf r)
-    let _ = Sat.solve ()        (* Should return Sat.Sat *)
+    let _ = Sat.solve ()        (* Should return (Sat.Sat _) *)
 
     (* The Sat solver has an incremental mutable state, so we still have
      * the formula 'r' in our assumptions *)
     Sat.assume (F.make_cnf s)
-    let _ = Sat.solve ()        (* Should return Sat.Unsat *)
+    let _ = Sat.solve ()        (* Should return (Sat.Unsat _) *)
 ```
 
 ## INSTALLATION

_tags

@@ -19,6 +19,8 @@ true: inline(100), optimize(3), unbox_closures, unbox_closures_factor(20)
 <src/solver/*.cmx>: for-pack(Msat)
 <src/backend/*.cmx>: for-pack(Msat)
 <src/util/*.cmx>: for-pack(Msat)
+<src/sat/sat.cmx>: for-pack(Msat)
+<src/sat/expr_sat.cmx>: for-pack(Msat)
 
 # Testing dependencies
 <src/main.*>: package(dolmen)

src/doc.txt

@@ -32,6 +32,15 @@ Expr_intf
 Plugin_intf
 }
 
+{4 Useful tools}
+
+An instanciation of a pure sat solver is also provided:
+
+{!modules:
+Sat
+Expr_sat
+}
+
 Lastly, mSAT also provides an implementation of Tseitin's CNF conversion:
 
 {!modules:

src/msat.mlpack

@@ -26,3 +26,8 @@ Dedukti
 
 # Auxiliary modules
 Tseitin
+
+# Pure Sat solver
+Sat
+Expr_sat
+

src/msat.odocl

@@ -27,8 +27,8 @@ backend/Dedukti
 backend/Backend_intf
 
 # SAT solver frontend
-#sat/Sat
+sat/Sat
-#sat/Expr_sat
+sat/Expr_sat
 #sat/Type_sat
 
 # SMT solver frontend

src/sat/expr_sat.mli

@@ -4,7 +4,15 @@ Copyright 2016 Guillaume Bury
 Copyright 2016 Simon Cruanes
 *)
 
+(** SAT Formulas
+
+    This modules implements formuals adequate for use in a pure SAT Solver.
+    Atomic formuals are represented using integers, that should allow
+    near optimal efficiency (both in terms of space and time).
+*)
+
 include Formula_intf.S
+(** This modules implements the requirements for implementing an SAT Solver. *)
 
 val make : int -> t
 (** Make a proposition from an integer. *)

src/sat/sat.ml

@@ -1,9 +1,10 @@
 (*
 MSAT is free software, using the Apache license, see file LICENSE
-Copyright 2014 Guillaume Bury
+Copyright 2016 Guillaume Bury
-Copyright 2014 Simon Cruanes
 *)
 
-module Make(Dummy : sig end) =
+module Expr = Expr_sat
-  Solver.Make(Expr_sat)(Solver.DummyTheory(Expr_sat))(struct end)
+
+module Make(Dummy : sig end) =
+  Solver.Make(Expr)(Solver.DummyTheory(Expr))(struct end)
 

src/sat/sat.mli

@@ -1,9 +1,17 @@
 (*
 MSAT is free software, using the Apache license, see file LICENSE
-Copyright 2014 Guillaume Bury
+Copyright 2016 Guillaume Bury
-Copyright 2014 Simon Cruanes
 *)
 
+(** Sat solver
+
+    This modules instanciates a pure sat solver using integers to represent
+    atomic propositions.
+*)
+
+module Expr = Expr_sat
+(** The module defining formulas *)
+
 module Make(Dummy : sig end) : Solver.S with type St.formula = Expr_sat.t
-
+(** A functor that can generate as many solvers as needed. *)
 

src/sat/type_sat.ml

@@ -1,3 +1,8 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
 
 (* Log&Module Init *)
 (* ************************************************************************ *)
@@ -5,7 +10,7 @@
 module Id = Dolmen.Id
 module Ast = Dolmen.Term
 module H = Hashtbl.Make(Id)
-module Formula = Tseitin.Make(Expr_sat)
+module Formula = Tseitin.Make(Sat.Expr)
 
 (* Exceptions *)
 (* ************************************************************************ *)
@@ -21,7 +26,7 @@ let find_id id =
   try
     H.find symbols id
   with Not_found ->
-    let res = Expr_sat.fresh () in
+    let res = Sat.Expr.fresh () in
     H.add symbols id res;
     res
 

src/sat/type_sat.mli

@@ -1,7 +1,12 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
 
 (** Typechecking of terms from Dolmen.Term.t
     This module provides functions to parse terms from the untyped syntax tree
     defined in Dolmen, and generate formulas as defined in the Expr_sat module. *)
 
-include Type.S with type atom := Expr_sat.t
+include Type.S with type atom := Sat.Expr.t