simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2026-01-28 12:24:50 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

cc: remove new_merges

Browse source
This commit is contained in:
Simon Cruanes 2022-02-17 22:03:33 -05:00
parent cdc5d160a7
commit a388c96fe3
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
3 changed files with 1 additions and 13 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/cc/Sidekick_cc.ml
View file

@ -308,7 +308,6 @@ module Make (A: CC_ARG)
mutable on_conflict: ev_on_conflict list; mutable on_conflict: ev_on_conflict list;
mutable on_propagate: ev_on_propagate list; mutable on_propagate: ev_on_propagate list;
mutable on_is_subterm : ev_on_is_subterm list; mutable on_is_subterm : ev_on_is_subterm list;
mutable new_merges: bool;
stat: Stat.t; stat: Stat.t;
count_conflict: int Stat.counter; count_conflict: int Stat.counter;
count_props: int Stat.counter; count_props: int Stat.counter;
@ -768,7 +767,6 @@ module Make (A: CC_ARG)
and[@inline] task_combine_ cc acts = function and[@inline] task_combine_ cc acts = function
| CT_merge (a,b,e_ab) -> | CT_merge (a,b,e_ab) ->
cc.new_merges <- true;
task_merge_ cc acts a b e_ab task_merge_ cc acts a b e_ab
| CT_set_val (n, v) -> | CT_set_val (n, v) ->
@ -1055,14 +1053,12 @@ module Make (A: CC_ARG)
(* run [f] in a local congruence closure level *) (* run [f] in a local congruence closure level *)
let with_model_mode cc f = let with_model_mode cc f =
assert (not cc.model_mode); assert (not cc.model_mode);
assert (not cc.new_merges);
cc.model_mode <- true; cc.model_mode <- true;
push_level cc; push_level cc;
CCFun.protect f CCFun.protect f
~finally:(fun() -> ~finally:(fun() ->
pop_levels cc 1; pop_levels cc 1;
cc.model_mode <- false; cc.model_mode <- false;
cc.new_merges <- false;
) )
(* assert that this boolean literal holds. (* assert that this boolean literal holds.
@ -1160,7 +1156,6 @@ module Make (A: CC_ARG)
true_; true_;
false_; false_;
stat; stat;
new_merges=false;
field_marked_explain; field_marked_explain;
count_conflict=Stat.mk_int stat "cc.conflicts"; count_conflict=Stat.mk_int stat "cc.conflicts";
count_props=Stat.mk_int stat "cc.propagations"; count_props=Stat.mk_int stat "cc.propagations";
@ -1182,11 +1177,8 @@ module Make (A: CC_ARG)
let[@inline] check cc acts : unit = let[@inline] check cc acts : unit =
Log.debug 5 "(cc.check)"; Log.debug 5 "(cc.check)";
cc.new_merges <- false;
update_tasks cc acts update_tasks cc acts
let new_merges cc = cc.new_merges
let check_inv_enabled_ = true (* XXX NUDGE *) let check_inv_enabled_ = true (* XXX NUDGE *)
(* check some internal invariants *) (* check some internal invariants *)

4
src/core/Sidekick_core.ml
View file

@ -739,10 +739,6 @@ module type CC_S = sig
(** Perform all pending operations done via {!assert_eq}, {!assert_lit}, etc. (** Perform all pending operations done via {!assert_eq}, {!assert_lit}, etc.
Will use the {!actions} to propagate literals, declare conflicts, etc. *) Will use the {!actions} to propagate literals, declare conflicts, etc. *)
val new_merges : t -> bool
(** Called after {!check}, returns [true] if some pairs of classes
were merged. *)
val push_level : t -> unit val push_level : t -> unit
(** Push backtracking level *) (** Push backtracking level *)

2
src/smt-solver/Sidekick_smt_solver.ml
View file

@ -608,7 +608,7 @@ module Make(A : ARG)
List.iter (fun f -> f self acts lits) self.on_final_check; List.iter (fun f -> f self acts lits) self.on_final_check;
CC.check cc acts; CC.check cc acts;
let new_work = CC.new_merges cc || has_delayed_actions self in let new_work = has_delayed_actions self in
(* do actual theory combination if nothing changed by pure "final check" *) (* do actual theory combination if nothing changed by pure "final check" *)
if not new_work then ( if not new_work then (
match check_th_combination_ self acts with match check_th_combination_ self acts with