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

refactor(cc): simple renaming

Browse source
This commit is contained in:
Simon Cruanes 2021-09-09 08:57:03 -04:00
parent 86512dbed0
commit acc682c5af
No known key found for this signature in database
GPG key ID: 4AC01D0849AA62B6
1 changed files with 14 additions and 14 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
src/cc/Sidekick_cc.ml
View file

@ -443,25 +443,25 @@ module Make (A: CC_ARG)
| Some (App_fun (f1, a1)), Some (App_fun (f2, a2)) ->
assert (Fun.equal f1 f2);
assert (List.length a1 = List.length a2);
List.fold_left2 (explain_equal cc ~th) acc a1 a2
List.fold_left2 (explain_equal_rec_ cc ~th) acc a1 a2
| Some (App_ho (f1, a1)), Some (App_ho (f2, a2)) ->
let acc = explain_equal cc ~th acc f1 f2 in
explain_equal cc ~th acc a1 a2
let acc = explain_equal_rec_ cc ~th acc f1 f2 in
explain_equal_rec_ cc ~th acc a1 a2
| Some (If (a1,b1,c1)), Some (If (a2,b2,c2)) ->
let acc = explain_equal cc ~th acc a1 a2 in
let acc = explain_equal cc ~th acc b1 b2 in
explain_equal cc ~th acc c1 c2
let acc = explain_equal_rec_ cc ~th acc a1 a2 in
let acc = explain_equal_rec_ cc ~th acc b1 b2 in
explain_equal_rec_ cc ~th acc c1 c2
| _ ->
assert false
end
| E_lit lit -> lit :: acc
| E_theory e' ->
th := true; explain_decompose_expl cc ~th acc e'
| E_merge (a,b) -> explain_equal cc ~th acc a b
| E_merge (a,b) -> explain_equal_rec_ cc ~th acc a b
| E_merge_t (a,b) ->
(* find nodes for [a] and [b] on the fly *)
begin match T_tbl.find cc.tbl a, T_tbl.find cc.tbl b with
| a, b -> explain_equal cc ~th acc a b
| a, b -> explain_equal_rec_ cc ~th acc a b
| exception Not_found ->
Error.errorf "expl: cannot find node(s) for %a, %a" Term.pp a Term.pp b
end
@ -469,7 +469,7 @@ module Make (A: CC_ARG)
let acc = explain_decompose_expl cc ~th acc a in
explain_decompose_expl cc ~th acc b
and explain_equal (cc:t) ~th (acc:lit list) (a:node) (b:node) : _ list =
and explain_equal_rec_ (cc:t) ~th (acc:lit list) (a:node) (b:node) : _ list =
Log.debugf 5
(fun k->k "(@[cc.explain_loop.at@ %a@ =?= %a@])" N.pp a N.pp b);
assert (N.equal (find_ a) (find_ b));
@ -654,8 +654,8 @@ module Make (A: CC_ARG)
C3: r1 C1 C2
*)
let lits = explain_decompose_expl cc ~th [] e_ab in
let lits = explain_equal cc ~th lits a ra in
let lits = explain_equal cc ~th lits b rb in
let lits = explain_equal_rec_ cc ~th lits a ra in
let lits = explain_equal_rec_ cc ~th lits b rb in
let emit_proof p =
let p_lits = Iter.of_list lits |> Iter.map Lit.neg in
P.lemma_cc p_lits p in
@ -754,7 +754,7 @@ module Make (A: CC_ARG)
let half_expl = lazy (
let th = ref false in
let lits = explain_decompose_expl cc ~th [] e_12 in
th, explain_equal cc ~th lits r2 t2
th, explain_equal_rec_ cc ~th lits r2 t2
) in
(* TODO: flag per class, `or`-ed on merge, to indicate if the class
contains at least one lit *)
@ -773,7 +773,7 @@ module Make (A: CC_ARG)
let reason =
let e = lazy (
let lazy (th, acc) = half_expl in
let lits = explain_equal cc ~th acc u1 t1 in
let lits = explain_equal_rec_ cc ~th acc u1 t1 in
let emit_proof p =
(* make a tautology, not a true guard *)
let p_lits = Iter.cons lit (Iter.of_list lits |> Iter.map Lit.neg) in
@ -863,7 +863,7 @@ module Make (A: CC_ARG)
let explain_eq cc n1 n2 : lit list =
let th = ref true in
explain_equal cc ~th [] n1 n2
explain_equal_rec_ cc ~th [] n1 n2
let on_pre_merge cc f = cc.on_pre_merge <- f :: cc.on_pre_merge
let on_post_merge cc f = cc.on_post_merge <- f :: cc.on_post_merge