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

bugfix in CC explanations

Browse source
This commit is contained in:
Simon Cruanes 2022-01-05 10:31:33 -05:00
parent 0afdb06f6c
commit 78df8252dc
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
2 changed files with 7 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/cc/Sidekick_cc.ml
View file

@ -856,9 +856,12 @@ module Make (A: CC_ARG)
let e = lazy ( let e = lazy (
let lazy st = half_expl_and_pr in let lazy st = half_expl_and_pr in
explain_equal_rec_ cc st u1 t1; explain_equal_rec_ cc st u1 t1;
(* assert that [guard /\ ¬lit] is absurd, to propagate [lit] *) (* true literals explaining why t1=t2 *)
let guard = st.lits in
(* get a proof of [guard /\ ¬lit] being absurd, to propagate [lit] *)
Expl_state.add_lit st (Lit.neg lit); Expl_state.add_lit st (Lit.neg lit);
lits_and_proof_of_expl cc st let _, pr = lits_and_proof_of_expl cc st in
guard, pr
) in ) in
fun () -> Lazy.force e fun () -> Lazy.force e
in in

3
src/sat/Solver.ml
View file

@ -1743,7 +1743,8 @@ module Make(Plugin : PLUGIN)
match List.find (Atom.is_true store) l with match List.find (Atom.is_true store) l with
| a -> | a ->
invalid_argf invalid_argf
"slice.acts_propagate:@ Consequence should contain only true literals, but %a isn't" "slice.acts_propagate:@ Consequence should contain only false literals,@ \
but @[%a@] is true"
(Atom.debug store) (Atom.neg a) (Atom.debug store) (Atom.neg a)
| exception Not_found -> () | exception Not_found -> ()