expose true_at_level0 in Solver_intf

src/core/external.ml

@@ -85,6 +85,12 @@ module Make
 
   let unsat_core = S.Proof.unsat_core
 
+  let true_at_level0 a =
+    try
+      let b, lev = S.eval_level a in
+      b && lev = 0
+    with S.UndecidedLit -> false
+
   let get_tag cl = St.(cl.tag)
 
 end

src/core/solver_intf.ml

@@ -62,6 +62,10 @@ module type S = sig
   val unsat_core : Proof.proof -> St.clause list
   (** Returns the unsat core of a given proof. *)
 
+  val true_at_level0 : atom -> bool
+  (** [true_at_level0 a] returns [true] if [a] was proved at level0, i.e.
+      it must hold in all models *)
+
   val get_tag : St.clause -> int option
   (** Recover tag from a clause, if any *)