simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-29 04:44:52 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

feat(solver): eager checking of proofs for theory propagation

Browse source 
bugs where a literal is propagated "too late" (at current level)
when the cause stems from previous levels, thus leading to invalid
clause learning (non UIP clauses) since some literals are not resolved
away as they're "too low", are hard to debug.
so we just check that propagation level coincides with current level.
This commit is contained in:
Simon Cruanes 2022-01-11 12:21:17 -05:00
parent a33029129e
commit 1ffe778951
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
1 changed files with 22 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

36
src/sat/Solver.ml
View file

@ -1738,10 +1738,10 @@ module Make(Plugin : PLUGIN)
(Clause.debug self.store) c); (Clause.debug self.store) c);
raise_notrace (Th_conflict c) raise_notrace (Th_conflict c)
let check_consequence_lits_false_ self l : unit = let check_consequence_lits_false_ self l p : unit =
let store = self.store in let store = self.store in
Log.debugf 50 (fun k->k "(@[sat.check-consequence-lits: %a@])" Log.debugf 50 (fun k->k "(@[sat.check-consequence-lits: %a@ :for %a@])"
(Util.pp_list (Atom.debug store)) l); (Util.pp_list (Atom.debug store)) l (Atom.debug store) p);
match List.find (fun a -> Atom.is_true store a) l with match List.find (fun a -> Atom.is_true store a) l with
| a -> | a ->
invalid_argf invalid_argf
@ -1761,24 +1761,32 @@ module Make(Plugin : PLUGIN)
else if Atom.is_false store p then ( else if Atom.is_false store p then (
let lits, proof = mk_expl() in let lits, proof = mk_expl() in
let guard = List.rev_map (fun f -> Atom.neg @@ make_atom_ self f) lits in let guard = List.rev_map (fun f -> Atom.neg @@ make_atom_ self f) lits in
check_consequence_lits_false_ self guard; check_consequence_lits_false_ self guard p;
let c = Clause.make_l store ~removable:true (p::guard) proof in let c = Clause.make_l store ~removable:true (p::guard) proof in
raise_notrace (Th_conflict c) raise_notrace (Th_conflict c)
) else ( ) else (
insert_var_order self (Atom.var p); insert_var_order self (Atom.var p);
let c = lazy ( let level = decision_level self in
let c = (
(* Check literals + proof eagerly, as it's safer.
We could check invariants in a [lazy] block,
as conflict analysis would run in an environment where
the literals should be true anyway, since it's an extension of the
current trail.
(otherwise the propagated lit would have been backtracked and
discarded already.)
However it helps catching propagation bugs to verify truthiness
of the guard (and level) eagerly.
*)
let lits, proof = mk_expl () in let lits, proof = mk_expl () in
let guard = List.rev_map (fun f -> Atom.neg @@ make_atom_ self f) lits in let guard = List.rev_map (fun f -> Atom.neg @@ make_atom_ self f) lits in
(* note: we can check that invariant here in the [lazy] block, check_consequence_lits_false_ self guard p;
as conflict analysis will run in an environment where assert (List.fold_left (fun l a -> max l (Atom.level store a)) 0 guard = level);
the literals should be true anyway, since it's an extension of the (* delay creating the actual clause. *)
current trail lazy (Clause.make_l store ~removable:true (p::guard) proof)
(otherwise the propagated lit would have been backtracked and
discarded already.) *)
check_consequence_lits_false_ self guard;
Clause.make_l store ~removable:true (p::guard) proof
) in ) in
let level = decision_level self in
Stat.incr self.n_propagations; Stat.incr self.n_propagations;
enqueue_bool self p ~level (Bcp_lazy c) enqueue_bool self p ~level (Bcp_lazy c)
) )