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

minor refactoring, removing useless field in nodes

Browse source
This commit is contained in:
Simon Cruanes 2018-02-22 21:19:54 -06:00
parent 77af72e739
commit f21d373620
3 changed files with 0 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/smt/Congruence_closure.ml
View file

@ -294,15 +294,12 @@ and update_combine cc =
begin
let r_from = (r_from :> node) in
let r_into = (r_into :> node) in
let rb_old_class = r_into.n_class in
let rb_old_parents = r_into.n_parents in
cc.acts.on_backtrack
(fun () ->
r_from.n_root <- r_from;
r_into.n_class <- rb_old_class;
r_into.n_parents <- rb_old_parents);
r_from.n_root <- r_into;
r_from.n_class <- Bag.append rb_old_class r_from.n_class;
r_from.n_parents <- Bag.append rb_old_parents r_from.n_parents;
end;
(* update explanations (a -> b), arbitrarily *)

3
src/smt/Equiv_class.ml
View file

@ -22,14 +22,11 @@ let make (t:term) : t =
let rec n = {
n_term=t;
n_bits=Node_bits.empty;
n_class=Bag.empty;
n_parents=Bag.empty;
n_root=n;
n_expl=E_none;
n_payload=[];
} in
(* set [class(t) = {t}] *)
n.n_class <- Bag.return n;
n
let set_payload ?(can_erase=fun _->false) n e =

1
src/smt/Solver_types.ml
View file

@ -84,7 +84,6 @@ and solve_result =
and cc_node = {
n_term: term;
mutable n_bits: Node_bits.t; (* bitfield for various properties *)
mutable n_class: cc_node Bag.t; (* terms in the same equiv class *)
mutable n_parents: cc_node Bag.t; (* parent terms of the whole equiv class *)
mutable n_root: cc_node; (* representative of congruence class (itself if a representative) *)
mutable n_expl: explanation_forest_link; (* the rooted forest for explanations *)