From 5ee49bdcb9c2b89abc5165f8105ce60c54a61fb5 Mon Sep 17 00:00:00 2001
From: "Hichem R. A" <hichem.ait-el-hara@ocamlpro.com>
Date: Wed, 12 Apr 2023 21:23:52 +0200
Subject: [PATCH] [Array] Add nomalization of the memoization data structures
---
colibri2/theories/array/RWRules.ml | 423 ++++++++++++++--------
colibri2/theories/array/RWRules.mli | 2 +
colibri2/theories/array/WEGraph.ml | 24 +-
colibri2/theories/array/array.ml | 8 +-
colibri2/theories/array/common.ml | 5 +-
colibri2/theories/array/common.mli | 5 +-
colibri2/theories/array/normalization.ml | 33 ++
colibri2/theories/array/normalization.mli | 25 ++
8 files changed, 344 insertions(+), 181 deletions(-)
create mode 100644 colibri2/theories/array/normalization.ml
create mode 100644 colibri2/theories/array/normalization.mli
diff --git a/colibri2/theories/array/RWRules.ml b/colibri2/theories/array/RWRules.ml
index 5a67c8d58..b8e448f56 100644
--- a/colibri2/theories/array/RWRules.ml
+++ b/colibri2/theories/array/RWRules.ml
@@ -62,7 +62,49 @@ module D2db =
let pp = Pp.unit
end)
-let get_ss_nodes env (subst : Ground.Subst.t) =
+(** (a,b,i,j):
+ a -> (true,b,i,j) | b -> (false,a,i,j) |
+ i -> (true,a,b,j) | j -> (false,a,b,i) *)
+module D1ids = struct
+ include MkIHT (struct
+ include I3.S
+
+ let name = "D1Ids"
+ end)
+
+ let add env (id1, id2, id3, id4, ty1, ty2) =
+ let aux env id v =
+ change
+ ~f:(function
+ | Some s -> Some (I3.S.add v s) | None -> Some (I3.S.singleton v))
+ env id
+ in
+ aux env id1 (true, id2, id3, id4, ty1, ty2);
+ aux env id2 (false, id1, id3, id4, ty1, ty2);
+ aux env id3 (true, id1, id2, id4, ty1, ty2);
+ aux env id4 (false, id1, id2, id3, ty1, ty2)
+end
+
+(** (a,b): a -> (true,b) | b -> (false,a) *)
+module D2ids = struct
+ include MkIHT (struct
+ include I1.S
+
+ let name = "D2Ids"
+ end)
+
+ let add env (id1, id2, ty1, ty2) =
+ let aux env id v =
+ change
+ ~f:(function
+ | Some s -> Some (I1.S.add v s) | None -> Some (I1.S.singleton v))
+ env id
+ in
+ aux env id1 (true, id2, ty1, ty2);
+ aux env id2 (false, id1, ty1, ty2)
+end
+
+let get_disj1_nodes env (subst : Ground.Subst.t) =
let b_n = Expr.Term.Var.M.find STV.vb subst.term in
let i_n = Expr.Term.Var.M.find STV.vi subst.term in
let j_n = Expr.Term.Var.M.find STV.vj subst.term in
@@ -77,12 +119,212 @@ let get_ss_nodes env (subst : Ground.Subst.t) =
in
(a_n, b_n, i_n, j_n, ind_gty, val_gty)
-(* let get_ext_nodes (subst : Ground.Subst.t) =
- let a_n = Expr.Term.Var.M.find STV.va subst.term in
- let b_n = Expr.Term.Var.M.find STV.vb subst.term in
- let ind_gty = Expr.Ty.Var.M.find STV.ind_ty_var subst.ty in
- let val_gty = Expr.Ty.Var.M.find STV.val_ty_var subst.ty in
- (a_n, b_n, ind_gty, val_gty) *)
+let new_disj1_aux env subst a_n b_n i_n j_n ind_gty val_gty =
+ match
+ let a_id = Id.Array.get_id env a_n in
+ let b_id = Id.Array.get_id env b_n in
+ let i_id = Id.Index.get_id env i_n in
+ let j_id = Id.Index.get_id env j_n in
+ D1db.find_opt env (a_id, b_id, i_id, j_id, ind_gty, val_gty)
+ with
+ | Some () -> ()
+ | None | (exception NoIdFound _) ->
+ let v =
+ convert ~subst env
+ (Expr.Term._or
+ [
+ Expr.Term.eq STV.ti STV.tj;
+ Expr.Term.eq
+ (mk_select_term (mk_store_term STV.tb STV.ti STV.tv) STV.tj)
+ (mk_select_term STV.tb STV.tj);
+ ])
+ in
+ Egraph.register env v;
+ Boolean.set_true env v;
+ Id.Array.set_id env a_n;
+ let a_id = Id.Array.get_id env a_n in
+ let b_id = Id.Array.get_id env b_n in
+ let i_id = Id.Index.get_id env i_n in
+ let j_id = Id.Index.get_id env j_n in
+ D1db.set env (a_id, b_id, i_id, j_id, ind_gty, val_gty) ();
+ D1ids.add env (a_id, b_id, i_id, j_id, ind_gty, val_gty)
+
+let new_disj1 env subst =
+ let a_n, b_n, i_n, j_n, ind_gty, val_gty = get_disj1_nodes env subst in
+ new_disj1_aux env subst a_n b_n i_n j_n ind_gty val_gty
+
+let new_disj1_raup2 env subst =
+ let a_n, b_n, i_n, j_n, ind_gty, val_gty = get_disj1_nodes env subst in
+ match Egraph.get_dom env Linearity_dom.key b_n with
+ | Some NonLinear ->
+ Debug.dprintf2 debug "Apply raup2 with %a" Ground.Subst.pp subst;
+ new_disj1_aux env subst a_n b_n i_n j_n ind_gty val_gty
+ | _ ->
+ Debug.dprintf2 debug "Do not apply raup2: %a is not non-linear" Node.pp
+ b_n
+
+let new_dist_arrays env (a_n, a_id) (b_n, b_id) ind_gty val_gty =
+ match D2db.find_opt env (a_id, b_id, ind_gty, val_gty) with
+ | Some () -> ()
+ | None ->
+ let diseq = mk_distinct_arrays env a_n b_n ind_gty val_gty in
+ Egraph.register env diseq;
+ Boolean.set_true env diseq;
+ D2db.set env (a_id, b_id, ind_gty, val_gty) ();
+ D2ids.add env (a_id, b_id, ind_gty, val_gty)
+
+let new_disj2 env (a, a_id) (b, b_id) ind_gty val_gty =
+ match D2db.find_opt env (a_id, b_id, ind_gty, val_gty) with
+ | Some () -> ()
+ | None ->
+ let eq = Equality.equality env [ a; b ] in
+ let diseq = mk_distinct_arrays env a b ind_gty val_gty in
+ Debug.dprintf4 debug "Application of the extensionality rule on %a and %a"
+ Node.pp a Node.pp b;
+ Egraph.register env eq;
+ Egraph.register env diseq;
+ Choice.register_global env
+ {
+ print_cho = "Decision from extensionality application.";
+ prio = 1;
+ choice =
+ (fun env ->
+ match (Boolean.is env eq, Boolean.is env diseq) with
+ | Some true, _ -> DecNo
+ | _, Some true -> DecNo
+ | _ ->
+ DecTodo
+ [
+ (fun env ->
+ Boolean.set_true env eq;
+ Boolean.set_false env diseq);
+ (fun env ->
+ Boolean.set_false env eq;
+ Boolean.set_true env diseq);
+ ]);
+ };
+ D2db.set env (a_id, b_id, ind_gty, val_gty) ();
+ D2ids.add env (a_id, b_id, ind_gty, val_gty)
+
+let eq_arrays_norm env (_, kid) (_, rid) _ =
+ (match D1ids.find_opt env rid with
+ | None -> ()
+ | Some s ->
+ let ns =
+ I3.S.fold
+ (fun (b, oid, iid, jid, ty1, ty2) s ->
+ let ns, (ofst, osnd, nfst, nsnd) =
+ if oid = rid then
+ ( I3.S.add
+ (b, kid, iid, jid, ty1, ty2)
+ (I3.S.remove (b, oid, iid, jid, ty1, ty2) s),
+ if b then (rid, oid, kid, kid) else (oid, rid, kid, kid) )
+ else (s, if b then (rid, oid, kid, oid) else (oid, rid, oid, kid))
+ in
+ D1db.remove env (ofst, osnd, iid, jid, ty1, ty2);
+ D1db.set env (nfst, nsnd, iid, jid, ty1, ty2) ();
+ D1ids.change env iid ~f:(function
+ | None -> assert false
+ | Some s ->
+ Some
+ (I3.S.add
+ (true, nfst, nsnd, jid, ty1, ty2)
+ (I3.S.remove (true, ofst, osnd, jid, ty1, ty2) s)));
+ D1ids.change env jid ~f:(function
+ | None -> assert false
+ | Some s ->
+ Some
+ (I3.S.add
+ (false, nfst, nsnd, iid, ty1, ty2)
+ (I3.S.remove (false, ofst, osnd, iid, ty1, ty2) s)));
+ D1ids.change env oid ~f:(function
+ | None -> assert false
+ | Some s ->
+ Some
+ (I3.S.add
+ (not b, kid, iid, jid, ty1, ty2)
+ (I3.S.remove (not b, rid, iid, jid, ty1, ty2) s)));
+ ns)
+ s s
+ in
+ D1ids.change env kid ~f:(function
+ | None -> Some ns
+ | Some s' -> Some (I3.S.union ns s')));
+ (match D2ids.find_opt env rid with
+ | None -> ()
+ | Some s ->
+ let ns =
+ I1.S.fold
+ (fun (b, oid, ty1, ty2) s ->
+ let ns, (ofst, osnd, nfst, nsnd) =
+ if oid = rid then
+ ( I1.S.add (b, kid, ty1, ty2) (I1.S.remove (b, oid, ty1, ty2) s),
+ if b then (rid, oid, kid, kid) else (oid, rid, kid, kid) )
+ else (s, if b then (rid, oid, kid, oid) else (oid, rid, oid, kid))
+ in
+ D2db.remove env (ofst, osnd, ty1, ty2);
+ D2db.set env (nfst, nsnd, ty1, ty2) ();
+ D2ids.change env oid ~f:(function
+ | None -> assert false
+ | Some s ->
+ Some
+ (I1.S.add (not b, kid, ty1, ty2)
+ (I1.S.remove (not b, rid, ty1, ty2) s)));
+ ns)
+ s s
+ in
+ D2ids.change env kid ~f:(function
+ | None -> Some ns
+ | Some s' -> Some (I1.S.union ns s')));
+ D2ids.remove env rid;
+ D1ids.remove env rid
+
+let eq_indices_norm env (_, kid) (_, rid) _ =
+ (match D1ids.find_opt env rid with
+ | None -> ()
+ | Some s ->
+ let ns =
+ I3.S.fold
+ (fun (b, aid, bid, oid, ty1, ty2) s ->
+ let ns, (ofst, osnd, nfst, nsnd) =
+ if oid = rid then
+ ( I3.S.add
+ (b, aid, bid, kid, ty1, ty2)
+ (I3.S.remove (b, aid, bid, oid, ty1, ty2) s),
+ if b then (rid, oid, kid, kid) else (oid, rid, kid, kid) )
+ else (s, if b then (rid, oid, kid, oid) else (oid, rid, oid, kid))
+ in
+ D1db.remove env (aid, bid, ofst, osnd, ty1, ty2);
+ D1db.set env (aid, bid, nfst, nsnd, ty1, ty2) ();
+ D1ids.change env aid ~f:(function
+ | None -> assert false
+ | Some s ->
+ Some
+ (I3.S.add
+ (true, bid, nfst, nsnd, ty1, ty2)
+ (I3.S.remove (true, bid, ofst, osnd, ty1, ty2) s)));
+ D1ids.change env bid ~f:(function
+ | None -> assert false
+ | Some s ->
+ Some
+ (I3.S.add
+ (false, aid, nfst, nsnd, ty1, ty2)
+ (I3.S.remove (false, aid, ofst, osnd, ty1, ty2) s)));
+ D1ids.change env oid ~f:(function
+ | None -> assert false
+ | Some s ->
+ Some
+ (I3.S.add
+ (not b, aid, bid, kid, ty1, ty2)
+ (I3.S.remove (not b, aid, bid, rid, ty1, ty2) s)));
+ ();
+ ns)
+ s s
+ in
+ D1ids.change env kid ~f:(function
+ | None -> Some ns
+ | Some s' -> Some (I3.S.union ns s')));
+ D1ids.remove env rid
type size = Inf | Finite of { num : int; size : int } [@@deriving show]
@@ -115,34 +357,7 @@ let adown_pattern, adown_run =
let adown_pattern = Pattern.of_term_exn ~subst:Ground.Subst.empty term in
let adown_run env subst =
Debug.dprintf2 debug "Found adown with %a" Ground.Subst.pp subst;
- let a_n, b_n, i_n, j_n, ind_gty, val_gty = get_ss_nodes env subst in
- match
- let a_id = Id.Array.get_id env a_n in
- let b_id = Id.Array.get_id env b_n in
- let i_id = Id.Index.get_id env i_n in
- let j_id = Id.Index.get_id env j_n in
- D1db.find_opt env (a_id, b_id, i_id, j_id, ind_gty, val_gty)
- with
- | Some () -> ()
- | None | (exception NoIdFound _) ->
- let v =
- convert ~subst env
- (Expr.Term._or
- [
- Expr.Term.eq STV.ti STV.tj;
- Expr.Term.eq
- (mk_select_term a_term STV.tj)
- (mk_select_term STV.tb STV.tj);
- ])
- in
- Egraph.register env v;
- Boolean.set_true env v;
- Id.Array.set_id env a_n;
- let a_id = Id.Array.get_id env a_n in
- let b_id = Id.Array.get_id env b_n in
- let i_id = Id.Index.get_id env i_n in
- let j_id = Id.Index.get_id env j_n in
- D1db.set env (a_id, b_id, i_id, j_id, ind_gty, val_gty) ()
+ new_disj1 env subst
in
(adown_pattern, adown_run)
@@ -160,34 +375,7 @@ let aup_pattern, aup_run =
let subst = Ground.Subst.distinct_union subst_bis subst in
(* (a,b,i,j) *)
Debug.dprintf2 debug "Found aup2 with %a" Ground.Subst.pp subst;
- let a_n, b_n, i_n, j_n, ind_gty, val_gty = get_ss_nodes env subst in
- match
- let a_id = Id.Array.get_id env a_n in
- let b_id = Id.Array.get_id env b_n in
- let i_id = Id.Index.get_id env i_n in
- let j_id = Id.Index.get_id env j_n in
- D1db.find_opt env (a_id, b_id, i_id, j_id, ind_gty, val_gty)
- with
- | Some () -> ()
- | None | (exception NoIdFound _) ->
- let v =
- convert ~subst env
- (Expr.Term._or
- [
- Expr.Term.eq STV.ti STV.tj;
- Expr.Term.eq
- (mk_select_term term STV.tj)
- (mk_select_term STV.tb STV.tj);
- ])
- in
- Egraph.register env v;
- Boolean.set_true env v;
- Id.Array.set_id env a_n;
- let a_id = Id.Array.get_id env a_n in
- let b_id = Id.Array.get_id env b_n in
- let i_id = Id.Index.get_id env i_n in
- let j_id = Id.Index.get_id env j_n in
- D1db.set env (a_id, b_id, i_id, j_id, ind_gty, val_gty) ()
+ new_disj1 env subst
in
InvertedPath.add_callback env aup_pattern_bis aup_run_bis
in
@@ -207,41 +395,7 @@ let raup_pattern, raup_run =
let raup_run_bis env subst_bis =
let subst = Ground.Subst.distinct_union subst_bis subst in
Debug.dprintf2 debug "Found raup2 with %a" Ground.Subst.pp subst;
- let a_n, b_n, i_n, j_n, ind_gty, val_gty = get_ss_nodes env subst in
- match
- let a_id = Id.Array.get_id env a_n in
- let b_id = Id.Array.get_id env b_n in
- let i_id = Id.Index.get_id env i_n in
- let j_id = Id.Index.get_id env j_n in
- D1db.find_opt env (a_id, b_id, i_id, j_id, ind_gty, val_gty)
- with
- | Some () -> ()
- | None | (exception NoIdFound _) -> (
- let bn = convert ~subst env STV.tb in
- match Egraph.get_dom env Linearity_dom.key bn with
- | Some NonLinear ->
- let v =
- convert ~subst env
- (Expr.Term._or
- [
- Expr.Term.eq STV.ti STV.tj;
- Expr.Term.eq
- (mk_select_term term STV.tj)
- (mk_select_term STV.tb STV.tj);
- ])
- in
- Debug.dprintf2 debug "Apply raup2: set %a to true" Node.pp v;
- Egraph.register env v;
- Boolean.set_true env v;
- Id.Array.set_id env a_n;
- let a_id = Id.Array.get_id env a_n in
- let b_id = Id.Array.get_id env b_n in
- let i_id = Id.Index.get_id env i_n in
- let j_id = Id.Index.get_id env j_n in
- D1db.set env (a_id, b_id, i_id, j_id, ind_gty, val_gty) ()
- | _ ->
- Debug.dprintf2 debug "Do not apply raup2: %a is not non-linear"
- Node.pp bn)
+ new_disj1_raup2 env subst
in
InvertedPath.add_callback env raup_pattern_bis raup_run_bis
in
@@ -267,18 +421,12 @@ let apply_res_ext_1_1_aux env ind_gty val_gty l =
match l with
| [] -> ()
| n1 :: t ->
+ let id1 = Id.Array.get_id env n1 in
List.iter
(fun n2 ->
(* (a,b) *)
- let id1 = Id.Array.get_id env n1 in
let id2 = Id.Array.get_id env n2 in
- match D2db.find_opt env (id1, id2, ind_gty, val_gty) with
- | Some () -> ()
- | None ->
- let diseq = mk_distinct_arrays env n1 n2 ind_gty val_gty in
- Egraph.register env diseq;
- Boolean.set_true env diseq;
- D2db.set env (id1, id2, ind_gty, val_gty) ())
+ new_dist_arrays env (n1, id1) (n2, id2) ind_gty val_gty)
t;
aux t
in
@@ -299,15 +447,7 @@ let apply_res_ext_1_2_aux env ind_gty val_gty l =
(fun (n2, id2) ->
if DInt.M.mem id2 m then
(* (a,b) *)
- match D2db.find_opt env (id1, id2, ind_gty, val_gty) with
- | Some () -> ()
- | None ->
- let diseq =
- mk_distinct_arrays env n1 n2 ind_gty val_gty
- in
- Egraph.register env diseq;
- Boolean.set_true env diseq;
- D2db.set env (id1, id2, ind_gty, val_gty) ())
+ new_dist_arrays env (n1, id1) (n2, id2) ind_gty val_gty)
t)
in
let rec aux1 l =
@@ -321,17 +461,9 @@ let apply_res_ext_1_2_aux env ind_gty val_gty l =
List.rev_map
(fun n2 ->
let id2 = Id.Array.get_id env n2 in
- (if DInt.M.mem id2 m then
- (* (a,b) *)
- match D2db.find_opt env (id1, id2, ind_gty, val_gty) with
- | Some () -> ()
- | None ->
- let diseq =
- mk_distinct_arrays env n1 n2 ind_gty val_gty
- in
- Egraph.register env diseq;
- Boolean.set_true env diseq;
- D2db.set env (id1, id2, ind_gty, val_gty) ());
+ if DInt.M.mem id2 m then
+ (* (a,b) *)
+ new_dist_arrays env (n1, id1) (n2, id2) ind_gty val_gty;
(n2, id2))
t
in
@@ -364,39 +496,6 @@ let get_foreign_neighbours env a arr_set =
else acc)
arr_set Node.S.empty
-let apply_ext env (a, id1) (b, id2) ind_gty val_gty =
- (* (a,b) *)
- match D2db.find_opt env (id1, id2, ind_gty, val_gty) with
- | Some () -> ()
- | None ->
- let eq = Equality.equality env [ a; b ] in
- let diseq = mk_distinct_arrays env a b ind_gty val_gty in
- Debug.dprintf4 debug "Application of the extensionality rule on %a and %a"
- Node.pp a Node.pp b;
- Egraph.register env eq;
- Egraph.register env diseq;
- Choice.register_global env
- {
- print_cho = "Decision from extensionality application.";
- prio = 1;
- choice =
- (fun env ->
- match (Boolean.is env eq, Boolean.is env diseq) with
- | Some true, _ -> DecNo
- | _, Some true -> DecNo
- | _ ->
- DecTodo
- [
- (fun env ->
- Boolean.set_true env eq;
- Boolean.set_false env diseq);
- (fun env ->
- Boolean.set_false env eq;
- Boolean.set_true env diseq);
- ]);
- };
- D2db.set env (id1, id2, ind_gty, val_gty) ()
-
(* a, b, {a,b} ⊆ foreign |> (a = b) ⋠(a[k] ≠b[k]) *)
let apply_res_ext_2_1, apply_res_ext_2_2 =
let foreign_array_db = GTHT.create Node.S.pp "foreign_array_db" in
@@ -426,7 +525,8 @@ let apply_res_ext_2_1, apply_res_ext_2_2 =
Node.S.iter
(fun b ->
let id2 = Id.Array.get_id env b in
- apply_ext env (a, id1) (b, id2) ind_gty val_gty)
+ (* (a, b) *)
+ new_disj2 env (a, id1) (b, id2) ind_gty val_gty)
fa_set)
env aty a
in
@@ -439,7 +539,8 @@ let apply_res_ext_2_1, apply_res_ext_2_2 =
Node.S.iter
(fun b ->
let id2 = Id.Array.get_id env b in
- apply_ext env (a, id1) (b, id2) ind_gty val_gty)
+ (* (a, b) *)
+ new_disj2 env (a, id1) (b, id2) ind_gty val_gty)
(get_foreign_neighbours env a fa_set))
env aty a
in
diff --git a/colibri2/theories/array/RWRules.mli b/colibri2/theories/array/RWRules.mli
index 1066dc707..49d89536e 100644
--- a/colibri2/theories/array/RWRules.mli
+++ b/colibri2/theories/array/RWRules.mli
@@ -50,3 +50,5 @@ val add_array_map_hook :
val new_map : Egraph.rw Egraph.t -> Ground.t -> unit
val apply_blast_rule : Egraph.wt -> Node.t -> Ground.Ty.t -> Ground.Ty.t -> unit
+val eq_arrays_norm : Egraph.wt -> Node.t * int -> Node.t * int -> bool -> unit
+val eq_indices_norm : Egraph.wt -> Node.t * int -> Node.t * int -> bool -> unit
diff --git a/colibri2/theories/array/WEGraph.ml b/colibri2/theories/array/WEGraph.ml
index 8a1946443..adf5f481c 100644
--- a/colibri2/theories/array/WEGraph.ml
+++ b/colibri2/theories/array/WEGraph.ml
@@ -1209,11 +1209,11 @@ let eq_indices_norm env (_kn, kid) (rn, rid) b =
~msg:(Fmt.str "_eq_indices_norm %a %a" (pp_nid env) kid (pp_nid env) rid)
env ()
-let eq_values_norm env (_, kid) (_, rid) _b =
+let eq_values_norm env (_, kid) (_, rid) b =
Debug.dprintf4 debug "WEGraph: eq_values_norm_ %a %a" (pp_nid env) kid
(pp_nid env) rid;
Values.eq_values_norm env kid rid;
- if not _b then ITN.set env kid (ITN.find env rid);
+ if not b then ITN.set env kid (ITN.find env rid);
ITN.remove env rid
let ineq_indices_norm env s =
@@ -1259,6 +1259,16 @@ let new_select env r a i =
| None -> ()
| Some v -> do_mk_eq_if_neq env v r)
+let new_id_hook env id n =
+ WEG.set env id (DInt.M.empty, DInt.M.empty);
+ ITN.set env id n
+
+let new_index_id_hook env id n =
+ Vertices.set env id Vertex.S.empty;
+ ITN.set env id n
+
+let new_value_id_hook env id n = ITN.set env id n
+
let get_neighbours env nid =
let rec aux (k : DInt.t) inp acc =
if DInt.S.mem inp acc then acc
@@ -1275,14 +1285,6 @@ let get_neighbours env nid =
| None -> DInt.S.empty
| Some (m, _) -> DInt.M.fold (fun k -> DInt.S.fold (aux k)) m DInt.S.empty
-let new_id_hook env id n =
- WEG.set env id (DInt.M.empty, DInt.M.empty);
- ITN.set env id n
-
-let new_index_id_hook env id n =
- Vertices.set env id Vertex.S.empty;
- ITN.set env id n
-
let get_array_kvs env n =
match KnownValues.HT.find_opt env (Id.Array.get_id env n) with
| Some kv ->
@@ -1292,5 +1294,3 @@ let get_array_kvs env n =
Node.M.add indn v acc)
kv Node.M.empty
| None -> Node.M.empty
-
-let new_value_id_hook env id n = ITN.set env id n
diff --git a/colibri2/theories/array/array.ml b/colibri2/theories/array/array.ml
index 9d643e41a..5e972171b 100644
--- a/colibri2/theories/array/array.ml
+++ b/colibri2/theories/array/array.ml
@@ -219,12 +219,12 @@ let init env =
Ground.register_converter env converter;
if not (Options.get env no_wegraph) then (
Id.Array.register_new_id_hook env WEGraph.new_id_hook;
- Id.Array.register_merge_hook env WEGraph.eq_arrays_norm;
Id.Index.register_new_id_hook env WEGraph.new_index_id_hook;
- Id.Index.register_merge_hook env WEGraph.eq_indices_norm;
Id.Value.register_new_id_hook env WEGraph.new_value_id_hook;
- Id.Value.register_merge_hook env WEGraph.eq_values_norm;
- Equality.register_hook_new_disequality env WEGraph.ineq_indices_norm);
+ Id.Array.register_merge_hook env Normalization.eq_arrays_norm;
+ Id.Index.register_merge_hook env Normalization.eq_indices_norm;
+ Id.Value.register_merge_hook env Normalization.eq_values_norm;
+ Equality.register_hook_new_disequality env Normalization.ineq_indices_norm);
(* extáµ£ (restricted extensionality):
- (a = b) ≡ false |> (a[k] ≠b[k])
- a, b, {a,b} ⊆ foreign |> (a = b) ⋠(a[k] ≠b[k]) *)
diff --git a/colibri2/theories/array/common.ml b/colibri2/theories/array/common.ml
index 0596c8286..392544c76 100644
--- a/colibri2/theories/array/common.ml
+++ b/colibri2/theories/array/common.ml
@@ -543,7 +543,7 @@ end
module I3 = struct
module T = struct
- type t = DInt.t * DInt.t * DInt.t * Ground.Ty.t * Ground.Ty.t
+ type t = DBool.t * DInt.t * DInt.t * DInt.t * Ground.Ty.t * Ground.Ty.t
[@@deriving eq, ord, hash, show]
end
@@ -563,7 +563,8 @@ end
module I1 = struct
module T = struct
- type t = DInt.t * Ground.Ty.t * Ground.Ty.t [@@deriving eq, ord, hash, show]
+ type t = DBool.t * DInt.t * Ground.Ty.t * Ground.Ty.t
+ [@@deriving eq, ord, hash, show]
end
include T
diff --git a/colibri2/theories/array/common.mli b/colibri2/theories/array/common.mli
index 81fc6144d..a1a808676 100644
--- a/colibri2/theories/array/common.mli
+++ b/colibri2/theories/array/common.mli
@@ -197,7 +197,8 @@ module I4 :
with type t = DInt.t * DInt.t * DInt.t * DInt.t * Ground.Ty.t * Ground.Ty.t
module I3 :
- Datatype with type t = DInt.t * DInt.t * DInt.t * Ground.Ty.t * Ground.Ty.t
+ Datatype
+ with type t = DBool.t * DInt.t * DInt.t * DInt.t * Ground.Ty.t * Ground.Ty.t
module I2 : Datatype with type t = DInt.t * DInt.t * Ground.Ty.t * Ground.Ty.t
-module I1 : Datatype with type t = DInt.t * Ground.Ty.t * Ground.Ty.t
+module I1 : Datatype with type t = DBool.t * DInt.t * Ground.Ty.t * Ground.Ty.t
diff --git a/colibri2/theories/array/normalization.ml b/colibri2/theories/array/normalization.ml
new file mode 100644
index 000000000..9eb9efa5b
--- /dev/null
+++ b/colibri2/theories/array/normalization.ml
@@ -0,0 +1,33 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* OCamlPro *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
+let eq_arrays_norm env (kn, kid) (rn, rid) b =
+ (* RWRules.eq_arrays_norm env (kn, kid) (rn, rid) b; *)
+ WEGraph.eq_arrays_norm env (kn, kid) (rn, rid) b
+
+let eq_indices_norm env (kn, kid) (rn, rid) b =
+ (* RWRules.eq_indices_norm env (kn, kid) (rn, rid) b; *)
+ WEGraph.eq_indices_norm env (kn, kid) (rn, rid) b
+
+let eq_values_norm env (kn, kid) (rn, rid) b =
+ WEGraph.eq_values_norm env (kn, kid) (rn, rid) b
+
+let ineq_indices_norm env s = WEGraph.ineq_indices_norm env s
diff --git a/colibri2/theories/array/normalization.mli b/colibri2/theories/array/normalization.mli
new file mode 100644
index 000000000..59d4a65d1
--- /dev/null
+++ b/colibri2/theories/array/normalization.mli
@@ -0,0 +1,25 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* OCamlPro *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(*************************************************************************)
+
+val eq_arrays_norm : Egraph.wt -> Node.t * int -> Node.t * int -> bool -> unit
+val eq_indices_norm : Egraph.wt -> Node.t * int -> Node.t * int -> bool -> unit
+val ineq_indices_norm : Egraph.wt -> Node.S.t -> unit
+val eq_values_norm : Egraph.wt -> Node.t * int -> Node.t * int -> bool -> unit
--
GitLab