From 6dbaa2d335d87dd09c74f3848948f0033c917374 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Fri, 1 Feb 2019 19:44:02 -0600
Subject: [PATCH] feat: expose `eval_atom`

---
 src/core/Internal.ml    | 9 +++++++--
 src/core/Solver_intf.ml | 3 +++
 2 files changed, 10 insertions(+), 2 deletions(-)

diff --git a/src/core/Internal.ml b/src/core/Internal.ml
index 5b98b9b3..2ce6dfe9 100644
--- a/src/core/Internal.ml
+++ b/src/core/Internal.ml
@@ -1667,12 +1667,15 @@ module Make(Plugin : PLUGIN)
       f e
     done
 
-  let acts_eval_lit st (f:formula) : Solver_intf.lbool =
-    let a = create_atom st f in
+  let eval_atom_ a =
     if Atom.is_true a then Solver_intf.L_true
     else if Atom.is_false a then Solver_intf.L_false
     else Solver_intf.L_undefined
 
+  let[@inline] acts_eval_lit st (f:formula) : Solver_intf.lbool =
+    let a = create_atom st f in
+    eval_atom_ a
+
   let[@inline] acts_mk_lit st f : unit =
     ignore (create_atom st f : atom)
 
@@ -2088,6 +2091,8 @@ module Make(Plugin : PLUGIN)
       b && lev = 0
     with UndecidedLit -> false
 
+  let[@inline] eval_atom _st a : Solver_intf.lbool = eval_atom_ a
+
   let export (st:t) : clause Solver_intf.export =
     let hyps = hyps st in
     let history = history st in
diff --git a/src/core/Solver_intf.ml b/src/core/Solver_intf.ml
index 2a005f21..4f50a6e7 100644
--- a/src/core/Solver_intf.ml
+++ b/src/core/Solver_intf.ml
@@ -468,6 +468,9 @@ module type S = sig
   (** [true_at_level0 a] returns [true] if [a] was proved at level0, i.e.
       it must hold in all models *)
 
+  val eval_atom : t -> atom -> lbool
+  (** Evaluate atom in current state *)
+
   val export : t -> clause export
 end