Merge branch 'master' of github.com:Gbury/mSAT

sat/sat.ml

@@ -66,12 +66,13 @@ module Make(Dummy : sig end) = struct
   module SatSolver = Solver.Make(Fsat)(Tsat)
 
   exception Bad_atom
+  exception UndecidedLit = SatSolver.UndecidedLit
 
   type atom = Fsat.t
   type clause = SatSolver.St.clause
   type proof = SatSolver.Proof.proof
 
-  let tag_clause cl = SatSolver.St.(cl.tag)
+  let tag_clause = SatSolver.tag_clause
 
   type res =
     | Sat

sat/sat.mli

@@ -11,6 +11,8 @@ module Tseitin : Tseitin.S with type atom = Fsat.t
 module Make(Dummy : sig end) : sig
   (** Fonctor to make a pure SAT Solver module with built-in literals. *)
 
+  exception UndecidedLit
+
   exception Bad_atom
   (** Exception raised when a problem with atomic formula encoding is detected. *)
 
@@ -55,13 +57,15 @@ module Make(Dummy : sig end) : sig
   (** Returns the satisfiability status of the current set of assumptions. *)
 
   val eval : atom -> bool
-  (** Return the current assignement of the literals. *)
+  (** Return the current assignement of the literal.
+      @raise UndecidedLit if the literal is not decided *)
 
   val eval_level : atom -> bool * int
   (** Return the current assignement of the literals, as well as its
       decision level. If the level is 0, then it is necessary for
       the atom to have this value; otherwise it is due to choices
-      that can potentially be backtracked. *)
+      that can potentially be backtracked.
+      @raise UndecidedLit if the literal is not decided *)
 
   val assume : ?tag:int -> atom list list -> unit
   (** Add a list of clauses to the set of assumptions. *)

solver/internal.ml

@@ -15,6 +15,7 @@ module Make
 
   exception Sat
   exception Unsat
+  exception UndecidedLit
   exception Restart
   exception Conflict of clause
 
@@ -970,7 +971,9 @@ module Make
 
   let eval_level lit =
     let var, negated = make_boolean_var lit in
-    assert (var.pa.is_true || var.na.is_true);
+    if not var.pa.is_true && not var.na.is_true
+      then raise UndecidedLit
+      else assert (var.level >= 0);
     let truth = var.pa.is_true in
     let value = if negated then not truth else truth in
     value, var.level

solver/internal.mli

@@ -13,6 +13,7 @@ module Make
   (** {2 Solving facilities} *)
 
   exception Unsat
+  exception UndecidedLit
 
   module Proof : Res.S with module St = St
 
@@ -28,13 +29,15 @@ module Make
 
   val eval : St.formula -> bool
   (** Returns the valuation of a formula in the current state
-      of the sat solver. *)
+      of the sat solver.
+      @raise UndecidedLit if the literal is not decided *)
 
   val eval_level : St.formula -> bool * int
   (** Return the current assignement of the literals, as well as its
       decision level. If the level is 0, then it is necessary for
       the atom to have this value; otherwise it is due to choices
-      that can potentially be backtracked. *)
+      that can potentially be backtracked.
+      @raise UndecidedLit if the literal is not decided *)
 
   val hyps : unit -> St.clause Vec.t
   (** Returns the vector of assumptions used by the solver. May be slightly different

solver/solver.ml

@@ -101,5 +101,6 @@ module Make (E : Formula_intf.S)
 
   include S
 
+  let tag_clause cl = St.(cl.tag)
 end
 

solver/solver.mli

@@ -21,6 +21,7 @@ module Make (F : Formula_intf.S)
       formulas and a theory. *)
 
   exception Unsat
+  exception UndecidedLit
 
   module St : Solver_types.S
     with type formula = F.t
@@ -38,15 +39,20 @@ module Make (F : Formula_intf.S)
       Modifies the sat solver state in place.
       @raise Unsat if a conflict is detect when adding the clauses *)
 
+  val tag_clause : St.clause -> int option
+  (** Recover tag from a clause, if any *)
+
   val eval : F.t -> bool
   (** Returns the valuation of a formula in the current state
-      of the sat solver. *)
+      of the sat solver.
+      @raise UndecidedLit if the literal is not decided *)
 
   val eval_level : F.t -> bool * int
   (** Return the current assignement of the literals, as well as its
       decision level. If the level is 0, then it is necessary for
       the atom to have this value; otherwise it is due to choices
-      that can potentially be backtracked. *)
+      that can potentially be backtracked.
+      @raise UndecidedLit if the literal is not decided *)
 
   val hyps : unit -> St.clause Vec.t
   (** Returns the vector of assumptions used by the solver. May be slightly different