simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-10 05:03:59 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix: only push atoms that don't have a value into next_decisions

Browse source
This commit is contained in:
Simon Cruanes 2019-10-29 14:35:26 -05:00
parent 2286a72437
commit 919c1e6011
1 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/core/Internal.ml
View file

@ -246,6 +246,7 @@ module Make(Plugin : PLUGIN)
let[@inline] id a = a.aid let[@inline] id a = a.aid
let[@inline] is_true a = a.is_true let[@inline] is_true a = a.is_true
let[@inline] is_false a = a.neg.is_true let[@inline] is_false a = a.neg.is_true
let has_value a = is_true a || is_false a
let[@inline] seen a = let[@inline] seen a =
if sign a if sign a
@ -1700,8 +1701,10 @@ module Make(Plugin : PLUGIN)
let acts_add_decision_lit (st:t) (f:formula) : unit = let acts_add_decision_lit (st:t) (f:formula) : unit =
let a = create_atom st f in let a = create_atom st f in
if not (Atom.has_value a) then (
Log.debugf 10 (fun k->k "(@[sat.th.add-decision-lit@ %a@])" Atom.debug a); Log.debugf 10 (fun k->k "(@[sat.th.add-decision-lit@ %a@])" Atom.debug a);
st.next_decisions <- a :: st.next_decisions st.next_decisions <- a :: st.next_decisions
)
let acts_raise st (l:formula list) proof : 'a = let acts_raise st (l:formula list) proof : 'a =
let atoms = List.rev_map (create_atom st) l in let atoms = List.rev_map (create_atom st) l in