add UndecidedLit for eval, eval_level

sat/sat.ml

@@ -66,6 +66,7 @@ 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

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.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
@@ -43,13 +44,15 @@ module Make (F : Formula_intf.S)
 
   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