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(sat): level-0 resolution needs to be recursive

Browse source
This commit is contained in:
Simon Cruanes 2021-11-10 13:20:00 -05:00
parent 72d79d7c0a
commit f500704905
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
1 changed files with 26 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

34
src/sat/Solver.ml
View file

@ -2137,14 +2137,32 @@ module Make(Plugin : PLUGIN)
let resolve_with_lvl0 (self:t) (c:clause) : clause =
let lvl0 = ref [] in
let res = ref [] in
Clause.iter self.store c
~f:(fun a ->
assert (Atom.is_false self.store a);
match Atom.reason self.store a with
| None -> assert false
| Some Decision -> res := a :: !res (* keep assumption *)
| Some (Bcp c2 | Bcp_lazy (lazy c2)) ->
lvl0 := Clause.proof_step self.store c2 :: !lvl0);
let to_unmark = self.temp_atom_vec in
assert (AVec.is_empty to_unmark);
(* resolve against the root cause of [a] being false *)
let rec resolve_with_a (a:atom) : unit =
assert (Atom.is_false self.store a);
if not (Var.marked self.store (Atom.var a)) then (
AVec.push to_unmark a;
Var.mark self.store (Atom.var a);
match Atom.reason self.store a with
| None -> assert false
| Some Decision -> res := a :: !res (* keep assumption *)
| Some (Bcp c2 | Bcp_lazy (lazy c2)) ->
lvl0 := Clause.proof_step self.store c2 :: !lvl0;
(* recursively explain other literals of [c2] *)
Clause.iter self.store c2
~f:(fun a2 ->
let na2 = Atom.neg a2 in
if not (Atom.equal a na2) then resolve_with_a a2)
)
in
Clause.iter self.store c ~f:resolve_with_a;
AVec.iter to_unmark ~f:(fun a -> Var.unmark self.store (Atom.var a));
AVec.clear to_unmark;
if !lvl0 = [] then (
c (* no resolution happened *)