From 5d18086e53cd9077c5c8c8916f576fbc283e71f5 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 14 Nov 2021 22:50:12 -0500 Subject: [PATCH] fix(sat): resolution at level 0 is not recursive 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. --- src/sat/Solver.ml | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml index 74d14c20..8c9cc5f7 100644 --- a/src/sat/Solver.ml +++ b/src/sat/Solver.ml @@ -2141,7 +2141,7 @@ module Make(Plugin : PLUGIN) assert (AVec.is_empty to_unmark); (* 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); if not (Var.marked self.store (Atom.var a)) then ( AVec.push to_unmark a; @@ -2152,11 +2152,8 @@ module Make(Plugin : PLUGIN) | 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) + (* NOTE: no need to recurse, we just need to depend on [c2] + and its proof will be required later *) ) in