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

fix proof production wrt conflict minimization

Browse source
This commit is contained in:
Simon Cruanes 2021-11-28 18:10:15 -05:00
parent 1bf05d51ce
commit f909e6bc9e
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
1 changed files with 9 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/sat/Solver.ml
View file

@ -1266,9 +1266,17 @@ module Make(Plugin : PLUGIN)
(* check that all the other lits of [c] are marked or redundant *) (* check that all the other lits of [c] are marked or redundant *)
for i = 1 to Array.length c_atoms - 1 do for i = 1 to Array.length c_atoms - 1 do
let v2 = Atom.var c_atoms.(i) in let v2 = Atom.var c_atoms.(i) in
if not (Var.marked store v2) && Var.level store v2 > 0 then ( let lvl_v2 = Var.level store v2 in
if not (Var.marked store v2) then (
match Var.reason store v2 with match Var.reason store v2 with
| None -> assert false | None -> assert false
| _ when lvl_v2 = 0 ->
(* can always remove literals at level 0, but got
to update proof properly *)
if Proof.enabled self.proof then (
let p = proof_of_atom_lvl0_ self (Atom.neg c_atoms.(i)) in
Step_vec.push steps p;
)
| Some (Bcp _ | Bcp_lazy _) | Some (Bcp _ | Bcp_lazy _)
when (abstract_level_ self v2 land abstract_levels) <> 0 -> when (abstract_level_ self v2 land abstract_levels) <> 0 ->
(* possibly removable, its level may comprise an atom in learnt clause *) (* possibly removable, its level may comprise an atom in learnt clause *)