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

fix(cc): polarity error in conflicts

Browse source
This commit is contained in:
Simon Cruanes 2019-02-01 21:12:08 -06:00
parent e6de1de949
commit a2e177abe8
1 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/smt/Congruence_closure.ml
View file

@ -184,7 +184,8 @@ let raise_conflict (cc:t) (acts:sat_actions) (e:conflict): _ =
Vec.iter (N.set_field N.field_is_pending false) cc.pending;
Vec.clear cc.pending;
Vec.clear cc.combine;
acts.Msat.acts_raise_conflict e Proof_default
let c = List.map Lit.neg e in
acts.Msat.acts_raise_conflict c Proof_default
let[@inline] all_classes cc : repr Sequence.t =
Term.Tbl.values cc.tbl
@ -585,9 +586,10 @@ let[@inline] push_level (self:t) : unit =
Backtrack_stack.push_level self.undo
let pop_levels (self:t) n : unit =
Backtrack_stack.pop_levels self.undo n ~f:(fun f -> f());
Vec.iter (N.set_field N.field_is_pending false) self.pending;
Vec.clear self.pending;
Vec.clear self.combine;
Backtrack_stack.pop_levels self.undo n ~f:(fun f -> f());
()
(* TODO: if a lit is [= a b], merge [a] and [b];
@ -655,7 +657,7 @@ let[@inline] find_t cc t : repr =
find cc n
let[@inline] check cc acts : unit =
Log.debug 5 "(CC.check)";
Log.debug 5 "(cc.check)";
update_tasks cc acts
(* model: map each uninterpreted equiv class to some ID *)