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

fix(sat): when theory-propagating a literal below current level, backtrack

Browse source 
it can be triggered by local clause addition (in DT for example), which
is hard to avoid.
This commit is contained in:
Simon Cruanes 2022-01-11 12:35:03 -05:00
parent 1ffe778951
commit 8b263d4d46
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 9 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/sat/Solver.ml
View file

@ -1176,6 +1176,10 @@ module Make(Plugin : PLUGIN)
assert (not (Atom.is_true store a) && assert (not (Atom.is_true store a) &&
Atom.level store a < 0 && Atom.level store a < 0 &&
Atom.reason store a == None && lvl >= 0); Atom.reason store a == None && lvl >= 0);
(* backtrack if required *)
if lvl < decision_level self then (
cancel_until self lvl;
);
Atom.set_is_true store a true; Atom.set_is_true store a true;
Var.set_level store (Atom.var a) lvl; Var.set_level store (Atom.var a) lvl;
Var.set_reason store (Atom.var a) (Some reason); Var.set_reason store (Atom.var a) (Some reason);
@ -1766,8 +1770,7 @@ module Make(Plugin : PLUGIN)
raise_notrace (Th_conflict c) raise_notrace (Th_conflict c)
) else ( ) else (
insert_var_order self (Atom.var p); insert_var_order self (Atom.var p);
let level = decision_level self in let c, level = (
let c = (
(* Check literals + proof eagerly, as it's safer. (* Check literals + proof eagerly, as it's safer.
We could check invariants in a [lazy] block, We could check invariants in a [lazy] block,
@ -1783,11 +1786,13 @@ module Make(Plugin : PLUGIN)
let lits, proof = mk_expl () in let lits, proof = mk_expl () in
let guard = List.rev_map (fun f -> Atom.neg @@ make_atom_ self f) lits in let guard = List.rev_map (fun f -> Atom.neg @@ make_atom_ self f) lits in
check_consequence_lits_false_ self guard p; check_consequence_lits_false_ self guard p;
assert (List.fold_left (fun l a -> max l (Atom.level store a)) 0 guard = level); let level = List.fold_left (fun l a -> max l (Atom.level store a)) 0 guard in
assert (level <= decision_level self);
(* delay creating the actual clause. *) (* delay creating the actual clause. *)
lazy (Clause.make_l store ~removable:true (p::guard) proof) lazy (Clause.make_l store ~removable:true (p::guard) proof), level
) in ) in
Stat.incr self.n_propagations; Stat.incr self.n_propagations;
Log.debugf 40 (fun k->k "(@[sat.propagation-level %d@])" level);
enqueue_bool self p ~level (Bcp_lazy c) enqueue_bool self p ~level (Bcp_lazy c)
) )