add eval_level in the API of the SAT solver

sat/sat.ml

@@ -146,6 +146,7 @@ module Make(Log : Log_intf.S) = struct
     with SatSolver.Unsat -> ()
 
   let eval = SatSolver.eval
+  let eval_level = SatSolver.eval_level
 
   let get_proof () =
     (* SatSolver.Proof.learn (SatSolver.history ()); *)

sat/sat.mli

@@ -57,6 +57,12 @@ module Make(Log: Log_intf.S) : sig
   val eval : atom -> bool
   (** Return the current assignement of the literals. *)
 
+  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. *)
+
   val assume : ?tag:int -> atom list list -> unit
   (** Add a list of clauses to the set of assumptions. *)
 

solver/internal.ml

@@ -941,11 +941,14 @@ module Make
     let cnf = List.rev_map (List.rev_map atom) cnf in
     init_solver ?tag cnf
 
-  let eval lit =
+  let eval_level lit =
     let var, negated = make_boolean_var lit in
     assert (var.pa.is_true || var.na.is_true);
     let truth = var.pa.is_true in
-    if negated then not truth else truth
+    let value = if negated then not truth else truth in
+    value, var.level
+
+  let eval lit = fst (eval_level lit)
 
   let hyps () = env.clauses_hyps
 

solver/internal.mli

@@ -31,6 +31,12 @@ module Make
   (** Returns the valuation of a formula in the current state
       of the sat solver. *)
 
+  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. *)
+
   val hyps : unit -> St.clause Vec.t
   (** Returns the vector of assumptions used by the solver. May be slightly different
       from the clauses assumed because of top-level simplification of clauses. *)

solver/solver.mli

@@ -38,6 +38,12 @@ module Make (L : Log_intf.S)(F : Formula_intf.S)
   (** Returns the valuation of a formula in the current state
       of the sat solver. *)
 
+  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. *)
+
   val hyps : unit -> St.clause Vec.t
   (** Returns the vector of assumptions used by the solver. May be slightly different
       from the clauses assumed because of top-level simplification of clauses. *)