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

fix(sat): resolution at level 0 is not recursive

Browse source 
recursion is implicit in the structure of the proof of the clause
that is unit at level 0, and thus responsible for propagating the
level-0 atom in the first place.
This commit is contained in:
Simon Cruanes 2021-11-14 22:50:12 -05:00
parent 7d70994758
commit 5d18086e53
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
1 changed files with 3 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/sat/Solver.ml
View file

@ -2141,7 +2141,7 @@ module Make(Plugin : PLUGIN)
assert (AVec.is_empty to_unmark); assert (AVec.is_empty to_unmark);
(* resolve against the root cause of [a] being false *) (* resolve against the root cause of [a] being false *)
let rec resolve_with_a (a:atom) : unit = let resolve_with_a (a:atom) : unit =
assert (Atom.is_false self.store a); assert (Atom.is_false self.store a);
if not (Var.marked self.store (Atom.var a)) then ( if not (Var.marked self.store (Atom.var a)) then (
AVec.push to_unmark a; AVec.push to_unmark a;
@ -2152,11 +2152,8 @@ module Make(Plugin : PLUGIN)
| Some Decision -> res := a :: !res (* keep assumption *) | Some Decision -> res := a :: !res (* keep assumption *)
| Some (Bcp c2 | Bcp_lazy (lazy c2)) -> | Some (Bcp c2 | Bcp_lazy (lazy c2)) ->
lvl0 := Clause.proof_step self.store c2 :: !lvl0; lvl0 := Clause.proof_step self.store c2 :: !lvl0;
(* recursively explain other literals of [c2] *) (* NOTE: no need to recurse, we just need to depend on [c2]
Clause.iter self.store c2 and its proof will be required later *)
~f:(fun a2 ->
let na2 = Atom.neg a2 in
if not (Atom.equal a na2) then resolve_with_a a2)
) )
in in