simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-29 04:44:52 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

feat: expose eval_atom

Browse source
This commit is contained in:
Simon Cruanes 2019-02-01 19:44:02 -06:00 • committed by Guillaume Bury
parent c89a99e82b
commit 6dbaa2d335
2 changed files with 10 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/core/Internal.ml
View file

@ -1667,12 +1667,15 @@ module Make(Plugin : PLUGIN)
f e f e
done done
let acts_eval_lit st (f:formula) : Solver_intf.lbool = let eval_atom_ a =
let a = create_atom st f in
if Atom.is_true a then Solver_intf.L_true if Atom.is_true a then Solver_intf.L_true
else if Atom.is_false a then Solver_intf.L_false else if Atom.is_false a then Solver_intf.L_false
else Solver_intf.L_undefined 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 = let[@inline] acts_mk_lit st f : unit =
ignore (create_atom st f : atom) ignore (create_atom st f : atom)
@ -2088,6 +2091,8 @@ module Make(Plugin : PLUGIN)
b && lev = 0 b && lev = 0
with UndecidedLit -> false with UndecidedLit -> false
let[@inline] eval_atom _st a : Solver_intf.lbool = eval_atom_ a
let export (st:t) : clause Solver_intf.export = let export (st:t) : clause Solver_intf.export =
let hyps = hyps st in let hyps = hyps st in
let history = history st in let history = history st in

3
src/core/Solver_intf.ml
View file

@ -468,6 +468,9 @@ module type S = sig
(** [true_at_level0 a] returns [true] if [a] was proved at level0, i.e. (** [true_at_level0 a] returns [true] if [a] was proved at level0, i.e.
it must hold in all models *) it must hold in all models *)
val eval_atom : t -> atom -> lbool
(** Evaluate atom in current state *)
val export : t -> clause export val export : t -> clause export
end end