Added Instanciated Sat Solver.

msat.mlpack

@@ -1,5 +1,6 @@
 Explanation
 Formula_intf
+Sat
 Solver
 Solver_types
 Theory_intf

sat/formula_intf.ml

@@ -16,23 +16,30 @@
 module type S = sig
 
   type t
+  (** The type of atomic formulas. *)
 
   val true_ : t
   val false_ : t
   val dummy : t
+  (** Formula constants. [dummy] should be different from any other formula. *)
 
   val neg : t -> t
+  (** Formula negation *)
 
   val norm : t -> t * bool
-  (** Returns a 'normalized' form of the formula, possibly negated *)
+  (** Returns a 'normalized' form of the formula, possibly negated (in which case return true).
+      Note : [fun a -> a, false] is a perfectly reasonnable implementation. *)
 
   val hash : t -> int
   val equal : t -> t -> bool
   val compare : t -> t -> int
+  (** Usual hash and comparison functions. Given to Map and Hash functors. *)
 
   val label : t -> Hstring.t
   val add_label : Hstring.t -> t -> unit
+  (** Optional. Not yet used in Solver. *)
 
   val print : Format.formatter -> t -> unit
+  (** Printing function used for debugging. *)
 end
 

sat/sat.ml

@@ -0,0 +1,74 @@
+(* Copyright 2014 Guillaume Bury *)
+
+module Fsat = struct
+    exception Out_of_int
+
+    type t = {
+        (* Invariant : var >= 0 *)
+        var : int;
+        pos : bool;
+    }
+
+    let max_index = ref 0
+
+    let true_ = { var = 0; pos = true }
+    let false_ = { var = 0; pos = false }
+    let dummy = { var = -1; pos = true }
+
+    let unsafe_make i = { var = i; pos = true }
+    let make i = if i > 0 then unsafe_make i else dummy
+
+    let neg a = { a with pos = not a.pos }
+    let norm a = a, false
+
+    let hash = Hashtbl.hash
+    let equal = (=)
+    let compare = Pervasives.compare
+
+    let label a = Hstring.make ""
+    let add_label _ _ = ()
+
+    let create, iter =
+        let create () =
+            if !max_index <> max_int then
+                (incr max_index; unsafe_make !max_index)
+            else
+                raise Out_of_int
+        in
+        let iter: (t -> unit) -> unit = fun f ->
+            for j = 1 to !max_index do
+                f (unsafe_make j)
+            done
+        in
+        create, iter
+
+    let print fmt a =
+        Format.fprintf fmt "%s%d" (if not a.pos then "~" else "") a.var
+
+end
+
+module Stypes = Solver_types.Make(Fsat)
+
+module Exp = Explanation.Make(Stypes)
+
+module Tsat = struct
+    (* We don't have anything to do since the SAT Solver already
+     * does propagation and conflict detection *)
+
+    type t = unit
+    type formula = Fsat.t
+    type explanation = Exp.t
+
+    exception Inconsistent of explanation
+
+    let empty () = ()
+    let assume ~cs:_ _ _ _ = ()
+end
+
+module Sat = struct
+    module SatSolver = Solver.Make(Fsat)(Stypes)(Exp)(Tsat)
+
+    type atom = Fsat.t
+    type state = SatSolver.t
+
+end

sat/solver.ml

@@ -98,6 +98,8 @@ module Make (F : Formula_intf.S)
     st_ma : varmap;
   }
 
+  type t = state
+
   let env = {
     is_unsat = false;
     unsat_core = [] ;

sat/solver.mli

@@ -19,15 +19,15 @@ module Make (F : Formula_intf.S)
   exception Sat
   exception Unsat of St.clause list
 
-  type state
+  type t
 
   val solve : unit -> unit
   val assume : F.t list list -> cnumber : int -> unit
   val clear : unit -> unit
 
   val eval : F.t -> bool
-  val save : unit -> state
+  val save : unit -> t
-  val restore : state -> unit
+  val restore : t -> unit
 
 end