From 672b5945ceeaccb1c261a6aff060349f146394f7 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 29 Jul 2016 17:07:54 +0200 Subject: [PATCH] expose `true_at_level0` in `Solver_intf` --- src/core/external.ml | 6 ++++++ src/core/solver_intf.ml | 4 ++++ 2 files changed, 10 insertions(+) diff --git a/src/core/external.ml b/src/core/external.ml index 56720429..386e5f5d 100644 --- a/src/core/external.ml +++ b/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 diff --git a/src/core/solver_intf.ml b/src/core/solver_intf.ml index ea2ee415..c70b1392 100644 --- a/src/core/solver_intf.ml +++ b/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 *)