From facfe336a1c03cf6255a224f21193979d9b27435 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Wed, 20 Jan 2016 20:06:56 +0100
Subject: [PATCH] add `eval_level` in the API of the SAT solver

---
 sat/sat.ml          | 1 +
 sat/sat.mli         | 6 ++++++
 solver/internal.ml  | 7 +++++--
 solver/internal.mli | 6 ++++++
 solver/solver.mli   | 6 ++++++
 5 files changed, 24 insertions(+), 2 deletions(-)

diff --git a/sat/sat.ml b/sat/sat.ml
index 6348ffe4..c1c6b2a8 100644
--- a/sat/sat.ml
+++ b/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 ()); *)
diff --git a/sat/sat.mli b/sat/sat.mli
index c1adecf0..986d7682 100644
--- a/sat/sat.mli
+++ b/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. *)
 
diff --git a/solver/internal.ml b/solver/internal.ml
index 194ec234..0e0c857b 100644
--- a/solver/internal.ml
+++ b/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
 
diff --git a/solver/internal.mli b/solver/internal.mli
index 99bc6c0e..b391a343 100644
--- a/solver/internal.mli
+++ b/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. *)
diff --git a/solver/solver.mli b/solver/solver.mli
index 629f5eba..12c6d2e8 100644
--- a/solver/solver.mli
+++ b/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. *)