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

fix(sat): emit proofs where needed

Browse source
This commit is contained in:
Simon Cruanes 2021-08-23 00:08:09 -04:00
parent fa04cb7997
commit bb682b8080
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
1 changed files with 10 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/sat/Solver.ml
View file

@ -940,6 +940,8 @@ module Make(Plugin : PLUGIN)
| US_false c -> | US_false c ->
self.unsat_at_0 <- Some c; self.unsat_at_0 <- Some c;
(match self.on_learnt with Some f -> f self c | None -> ()); (match self.on_learnt with Some f -> f self c | None -> ());
Proof.with_proof self.proof
(Proof.emit_redundant_clause (Clause.lits_iter self.store c));
US_false c US_false c
| _ -> us | _ -> us
in in
@ -1206,6 +1208,8 @@ module Make(Plugin : PLUGIN)
let uclause = let uclause =
Clause.make_a store ~removable:true cr.cr_learnt in Clause.make_a store ~removable:true cr.cr_learnt in
(match self.on_learnt with Some f -> f self uclause | None -> ()); (match self.on_learnt with Some f -> f self uclause | None -> ());
Proof.with_proof self.proof
(Proof.emit_redundant_clause (Clause.lits_iter self.store uclause));
(* no need to attach [uclause], it is true at level 0 *) (* no need to attach [uclause], it is true at level 0 *)
enqueue_bool self fuip ~level:0 (Bcp uclause) enqueue_bool self fuip ~level:0 (Bcp uclause)
) )
@ -1218,6 +1222,8 @@ module Make(Plugin : PLUGIN)
attach_clause self lclause; attach_clause self lclause;
clause_bump_activity self lclause; clause_bump_activity self lclause;
(match self.on_learnt with Some f -> f self lclause | None -> ()); (match self.on_learnt with Some f -> f self lclause | None -> ());
Proof.with_proof self.proof
(Proof.emit_redundant_clause (Clause.lits_iter self.store lclause));
assert (cr.cr_is_uip); assert (cr.cr_is_uip);
enqueue_bool self fuip ~level:cr.cr_backtrack_lvl (Bcp lclause) enqueue_bool self fuip ~level:cr.cr_backtrack_lvl (Bcp lclause)
end; end;
@ -1650,6 +1656,8 @@ module Make(Plugin : PLUGIN)
(match self.on_gc with (match self.on_gc with
| Some f -> let lits = Clause.lits_a store c in f self lits | Some f -> let lits = Clause.lits_a store c in f self lits
| None -> ()); | None -> ());
Proof.with_proof self.proof
(Proof.del_clause (Clause.lits_iter store c));
in in
(* find clauses to GC *) (* find clauses to GC *)
@ -1943,6 +1951,8 @@ module Make(Plugin : PLUGIN)
solve_ self; solve_ self;
Sat (mk_sat self) Sat (mk_sat self)
with E_unsat us -> with E_unsat us ->
(* emit empty clause *)
Proof.with_proof self.proof (Proof.emit_redundant_clause Iter.empty);
Unsat (mk_unsat self us) Unsat (mk_unsat self us)
let true_at_level0 (self:t) (lit:lit) : bool = let true_at_level0 (self:t) (lit:lit) : bool =