From 99a6aaa79043dbd745406c2a16f4e3df386753b8 Mon Sep 17 00:00:00 2001
From: "Hichem R. A" <hichem.ait-el-hara@ocamlpro.com>
Date: Tue, 11 Apr 2023 14:20:59 +0200
Subject: [PATCH] [Array] Added memoization of some RW rules
---
colibri2/theories/array/Id.ml | 12 +-
colibri2/theories/array/RWRules.ml | 407 +++++++++++++++++++----------
colibri2/theories/array/WEGraph.ml | 208 +++++++--------
colibri2/theories/array/common.ml | 165 +++++++++---
colibri2/theories/array/common.mli | 49 +++-
5 files changed, 524 insertions(+), 317 deletions(-)
diff --git a/colibri2/theories/array/Id.ml b/colibri2/theories/array/Id.ml
index d082659bf..b77cf3420 100644
--- a/colibri2/theories/array/Id.ml
+++ b/colibri2/theories/array/Id.ml
@@ -20,19 +20,13 @@
(*************************************************************************)
module Array = Common.MkIdDom (struct
- let n1 = "Array.Id.Array.merge_hooks"
- let n2 = "Array.Id"
- let n3 = "Array.Id.Array.new_id_hooks"
+ let name = "Array.Id"
end)
module Index = Common.MkIdDom (struct
- let n1 = "Array.Id.Index.merge_hooks"
- let n2 = "Array.Index_id"
- let n3 = "Array.Id.Index.new_id_hooks"
+ let name = "Array.Index.Id"
end)
module Value = Common.MkIdDom (struct
- let n1 = "Array.Id.Value.merge_hooks"
- let n2 = "Array.Value_id"
- let n3 = "Array.Id.Value.new_id_hooks"
+ let name = "Array.Value.Id"
end)
diff --git a/colibri2/theories/array/RWRules.ml b/colibri2/theories/array/RWRules.ml
index 0f791f261..5a67c8d58 100644
--- a/colibri2/theories/array/RWRules.ml
+++ b/colibri2/theories/array/RWRules.ml
@@ -27,6 +27,63 @@ open Colibri2_theories_quantifiers
module GHT = Datastructure.Hashtbl (Ground)
module GTHT = Datastructure.Hashtbl (Ground.Ty)
+(** disjunction 1: (a,b,i,j) -> (i = j) \/ (a[j] = b[j]) *)
+module D1db =
+ SHT
+ (struct
+ include I4
+
+ let sort (a, b, i, j, ty1, ty2) =
+ let a, b = if a <= b then (a, b) else (b, a) in
+ let i, j = if i <= j then (i, j) else (j, i) in
+ (a, b, i, j, ty1, ty2)
+ end)
+ (struct
+ type t = unit
+
+ let name = "D1db"
+ let pp = Pp.unit
+ end)
+
+(** disjunction 2: (a,b) -> (a = b) ⋠(a[k] ≠b[k]) *)
+module D2db =
+ SHT
+ (struct
+ include I2
+
+ let sort (a, b, ty1, ty2) =
+ let a, b = if a <= b then (a, b) else (b, a) in
+ (a, b, ty1, ty2)
+ end)
+ (struct
+ type t = unit
+
+ let name = "D2db"
+ let pp = Pp.unit
+ end)
+
+let get_ss_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
+ 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
+ let a_n =
+ try Expr.Term.Var.M.find STV.va subst.term
+ with Not_found ->
+ let v_n = Expr.Term.Var.M.find STV.vv subst.term in
+ ground_apply env Expr.Term.Const.Array.store [ ind_gty; val_gty ]
+ [ b_n; i_n; v_n ]
+ 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) *)
+
type size = Inf | Finite of { num : int; size : int } [@@deriving show]
let check_gty_num_size =
@@ -52,24 +109,40 @@ let check_gty_num_size =
(* ⇓: a ≡ b[i <- v], a[j] |> (i = j) \/ a[j] = b[j] *)
let adown_pattern, adown_run =
- let a = mk_store_term STV.tb STV.ti STV.tv in
- let term = mk_select_term a STV.tj in
+ (* (a,b,i,j) *)
+ let a_term = mk_store_term STV.tb STV.ti STV.tv in
+ let term = mk_select_term a_term STV.tj in
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 n = convert ~subst env term in
- let v =
- convert ~subst env
- (Expr.Term._or
- [
- Expr.Term.eq STV.ti STV.tj;
- Expr.Term.eq (mk_select_term a STV.tj)
- (mk_select_term STV.tb STV.tj);
- ])
- in
- Egraph.register env n;
- Egraph.register env v;
- Boolean.set_true env v
+ 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) ()
in
(adown_pattern, adown_run)
@@ -85,19 +158,36 @@ let aup_pattern, aup_run =
let aup_pattern_bis = Pattern.of_term_exn ~subst term_bis in
let aup_run_bis env subst_bis =
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 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
+ 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) ()
in
InvertedPath.add_callback env aup_pattern_bis aup_run_bis
in
@@ -105,6 +195,7 @@ let aup_pattern, aup_run =
(* ⇑ᵣ: a ≡ b[i <- v], b[j], b ∈ non-linear |> (i = j) \/ a[j] = b[j] *)
let raup_pattern, raup_run =
+ (* (a,b,i,j) *)
let term = mk_store_term STV.tb STV.ti STV.tv in
let raup_pattern = Pattern.of_term_exn ~subst:Ground.Subst.empty term in
let raup_run env subst =
@@ -116,25 +207,41 @@ 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 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
- | _ ->
- Debug.dprintf2 debug "Do not apply raup2: %a is not non-linear"
- Node.pp bn
+ 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)
in
InvertedPath.add_callback env raup_pattern_bis raup_run_bis
in
@@ -152,84 +259,93 @@ let const_read_pattern, const_read_run =
in
(const_read_pattern, const_read_run)
-let apply_res_ext_1_1_aux _env ind_gty val_gty l tyvt =
+let apply_res_ext_1_1_aux env ind_gty val_gty l =
Debug.dprintf2 debug "Application of the res-ext-1-1 rule on %a"
(Fmt.list ~sep:Fmt.comma Node.pp)
l;
- let rec aux tnl =
- match tnl with
- | (nterm, _) :: t ->
- let nterms =
- List.fold_left
- (fun acc (oterm, _) -> distinct_arrays_term nterm oterm :: acc)
- [] t
- in
- List.rev_append nterms (aux t)
- | [] -> []
- in
- let _, tsubst, tnl =
- List.fold_left
- (fun (cnt, tsubst, tns) node ->
- let anv = Expr.Term.Var.mk (Format.sprintf "a%d" cnt) tyvt in
- let anvt = Expr.Term.of_var anv in
- (cnt + 1, (anv, node) :: tsubst, (anvt, node) :: tns))
- (0, [], []) l
+ let rec aux l =
+ match l with
+ | [] -> ()
+ | n1 :: t ->
+ 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) ())
+ t;
+ aux t
in
- let tysubst = [ (STV.ind_ty_var, ind_gty); (STV.val_ty_var, val_gty) ] in
- let subst = mk_subst tsubst tysubst in
- (aux tnl, subst)
+ aux l
-let apply_res_ext_1_2_aux env ind_gty val_gty l tyvt =
+let apply_res_ext_1_2_aux env ind_gty val_gty l =
Debug.dprintf2 debug "Application of the res-ext-1-2 rule on %a"
(Fmt.list ~sep:Fmt.comma Node.pp)
l;
- let rec aux (tnl : (Expr.term * int) list) =
- match tnl with
- | (nterm, idn) :: t -> (
- match WEGraph.WEG.find_opt env idn with
+ let rec aux2 l =
+ match l with
+ | [] -> ()
+ | (n1, id1) :: t -> (
+ match WEGraph.WEG.find_opt env id1 with
+ | None -> aux2 t
| Some (_, m) ->
- let nterms =
- List.fold_left
- (fun acc (oterm, oid) ->
- if DInt.M.mem oid m then
- distinct_arrays_term nterm oterm :: acc
- else acc)
- [] t
- in
- List.rev_append nterms (aux t)
- | None -> aux t)
- | [] -> []
+ List.iter
+ (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) ())
+ t)
in
- let _, tsubst, tnl =
- List.fold_left
- (fun (cnt, tsubst, tns) node ->
- let anv = Expr.Term.Var.mk (Format.sprintf "a%d" cnt) tyvt in
- let anvt = Expr.Term.of_var anv in
- (cnt + 1, (anv, node) :: tsubst, (anvt, Id.Array.get_id env node) :: tns))
- (0, [], []) l
+ let rec aux1 l =
+ match l with
+ | [] -> ()
+ | n1 :: t -> (
+ let id1 = Id.Array.get_id env n1 in
+ match WEGraph.WEG.find_opt env id1 with
+ | Some (_, m) ->
+ let t' =
+ 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) ());
+ (n2, id2))
+ t
+ in
+ aux2 t'
+ | None -> aux1 t)
in
- let tysubst = [ (STV.ind_ty_var, ind_gty); (STV.val_ty_var, val_gty) ] in
- let subst = mk_subst tsubst tysubst in
- (aux tnl, subst)
+ aux1 l
(* (a = b) ≡ false |> (a[k] ≠b[k]) *)
let apply_res_ext_1_1, apply_res_ext_1_2 =
let apply_res_ext_1 f env s =
let l = Node.S.elements s in
match get_array_gty_args env (List.hd l) with
- | ind_gty, val_gty -> (
- let tyvt = Expr.Ty.array STV.ind_ty STV.val_ty in
- let l, subst = f env ind_gty val_gty l tyvt in
- match l with
- | [] -> ()
- | [ t ] ->
- let n = convert ~subst env t in
- Egraph.register env n;
- Boolean.set_true env n
- | l ->
- let n = convert ~subst env (Expr.Term._and l) in
- Egraph.register env n;
- Boolean.set_true env n)
+ | ind_gty, val_gty -> f env ind_gty val_gty l
| exception Not_An_Array _ -> ()
in
let apply_res_ext_1_1 = apply_res_ext_1 apply_res_ext_1_1_aux in
@@ -248,34 +364,38 @@ let get_foreign_neighbours env a arr_set =
else acc)
arr_set Node.S.empty
-let apply_ext env a b =
- let ind_gty, val_gty = array_gty_args (get_array_gty env a) in
- 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);
- ]);
- }
+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 =
@@ -300,14 +420,27 @@ let apply_res_ext_2_1, apply_res_ext_2_2 =
let apply_res_ext_2_1 env aty a =
Debug.dprintf2 debug "Application of the res-ext-2-1 rule on %a" Node.pp a;
apply_res_ext_2
- (fun env a fa_set -> Node.S.iter (apply_ext env a) fa_set)
+ (fun env a fa_set ->
+ let ind_gty, val_gty = array_gty_args (get_array_gty env a) in
+ let id1 = Id.Array.get_id env a in
+ 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)
+ fa_set)
env aty a
in
let apply_res_ext_2_2 env aty a =
Debug.dprintf2 debug "Application of the res-ext-2-2 rule on %a" Node.pp a;
apply_res_ext_2
(fun env a fa_set ->
- Node.S.iter (apply_ext env a) (get_foreign_neighbours env a fa_set))
+ let ind_gty, val_gty = array_gty_args (get_array_gty env a) in
+ let id1 = Id.Array.get_id env a in
+ 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)
+ (get_foreign_neighbours env a fa_set))
env aty a
in
(apply_res_ext_2_1, apply_res_ext_2_2)
diff --git a/colibri2/theories/array/WEGraph.ml b/colibri2/theories/array/WEGraph.ml
index 5f5f64d37..8a1946443 100644
--- a/colibri2/theories/array/WEGraph.ml
+++ b/colibri2/theories/array/WEGraph.ml
@@ -24,39 +24,15 @@ open Colibri2_popop_lib
open Popop_stdlib
open Common
-module EHT = MkIHT (struct
+module ITN = MkIHT (struct
type t = Node.t
let pp = Node.pp
- let name = "WEGraph.Edges.Nodes"
+ let name = "WEGraph.IdsToNodes"
end)
-module VHT = MkIHT (struct
- type t = Node.t
-
- let pp = Node.pp
- let name = "WEGraph.Vertices.Nodes"
-end)
-
-module ValHT = MkIHT (struct
- type t = Node.t
-
- let pp = Node.pp
- let name = "WEGraph.Values.Nodes"
-end)
-
-let pp_eid env fmt i =
- match EHT.find_opt env i with
- | Some n -> Format.fprintf fmt "%a{id = %d}" Node.pp n i
- | None -> Format.fprintf fmt "Not_found{id = %d}" i
-
-let pp_vid env fmt i =
- match VHT.find_opt env i with
- | Some n -> Format.fprintf fmt "%a{id = %d}" Node.pp n i
- | None -> Format.fprintf fmt "Not_found{id = %d}" i
-
-let pp_val_id env fmt i =
- match ValHT.find_opt env i with
+let pp_nid env fmt i =
+ match ITN.find_opt env i with
| Some n -> Format.fprintf fmt "%a{id = %d}" Node.pp n i
| None -> Format.fprintf fmt "Not_found{id = %d}" i
@@ -152,26 +128,26 @@ module Values = struct
let check_store env a b i v =
Debug.dprintf8 debug "WEGraph.Values.check_store: a=%a b=%a i=%a v=%a"
- (pp_eid env) a (pp_eid env) b (pp_vid env) i (pp_val_id env) v;
+ (pp_nid env) a (pp_nid env) b (pp_nid env) i (pp_nid env) v;
Option.iter
(fun (_, s2) ->
if a <> b && IDS.mem (v, b) s2 then (
Debug.dprintf8 debug "WEGraph.Values.do_mk_eq1: a=%a b=%a (v=%a i=%a)"
- (pp_eid env) a (pp_eid env) b (pp_val_id env) v (pp_vid env) i;
- do_mk_eq env (EHT.find env a) (EHT.find env b)))
+ (pp_nid env) a (pp_nid env) b (pp_nid env) v (pp_nid env) i;
+ do_mk_eq env (ITN.find env a) (ITN.find env b)))
(VIHT.find_opt env i)
let check_select env u c j =
Debug.dprintf6 debug "WEGraph.Values.check_select: u=%a c=%a j=%a"
- (pp_val_id env) u (pp_eid env) c (pp_vid env) j;
+ (pp_nid env) u (pp_nid env) c (pp_nid env) j;
Option.iter
(fun (s1, _) ->
ITS.iter (* find a way not to iterate *)
(fun (a, b, i) ->
if a <> b && b = c && a = c && j = i then (
Debug.dprintf8 debug "WEGraph.Values.do_mk_eq2: %a %a (%a %a)"
- (pp_eid env) a (pp_eid env) b (pp_val_id env) u (pp_vid env) j;
- do_mk_eq env (EHT.find env a) (EHT.find env b)))
+ (pp_nid env) a (pp_nid env) b (pp_nid env) u (pp_nid env) j;
+ do_mk_eq env (ITN.find env a) (ITN.find env b)))
s1)
(VHT.find_opt env u)
@@ -180,11 +156,11 @@ module Values = struct
| Some (s, _) when ITS.mem (a, i, v) s ->
Debug.dprintf8 debug
"WEGraph.Values.add_store: a=%a b=%a i=%a v=%a (Already present)"
- (pp_eid env) a (pp_eid env) b (pp_vid env) i (pp_val_id env) v;
+ (pp_nid env) a (pp_nid env) b (pp_nid env) i (pp_nid env) v;
()
| _ ->
Debug.dprintf8 debug "WEGraph.Values.add_store: a=%a b=%a i=%a v=%a"
- (pp_eid env) a (pp_eid env) b (pp_vid env) i (pp_val_id env) v;
+ (pp_nid env) a (pp_nid env) b (pp_nid env) i (pp_nid env) v;
A1HT.add_store env b (a, i, v);
VHT.add_store env v (a, b, i);
VIHT.add_store env i (a, b, v);
@@ -196,11 +172,11 @@ module Values = struct
| Some (_, s) when IDS.mem (u, j) s ->
Debug.dprintf6 debug
"WEGraph.Values.add_select: u=%a c=%a j=%a (Already present)"
- (pp_val_id env) u (pp_eid env) c (pp_vid env) j;
+ (pp_nid env) u (pp_nid env) c (pp_nid env) j;
()
| _ ->
Debug.dprintf6 debug "WEGraph.Values.add_select: u=%a c=%a j=%a"
- (pp_val_id env) u (pp_eid env) c (pp_vid env) j;
+ (pp_nid env) u (pp_nid env) c (pp_nid env) j;
A1HT.add_select env c (u, j);
VHT.add_select env u (c, j);
VIHT.add_select env j (u, c);
@@ -209,8 +185,8 @@ module Values = struct
let subst_kr kid rid aid = if aid = rid then Some kid else None
let eq_arrays_norm env kid rid =
- Debug.dprintf4 debug "WEGraph.Values.eq_arrays_norm: %a %a " (pp_eid env)
- kid (pp_eid env) rid;
+ Debug.dprintf4 debug "WEGraph.Values.eq_arrays_norm: %a %a " (pp_nid env)
+ kid (pp_nid env) rid;
(* res-arrays *)
Option.iter
(fun rm ->
@@ -290,8 +266,8 @@ module Values = struct
(A1HT.find_opt env rid)
let eq_indices_norm env kid rid =
- Debug.dprintf4 debug "WEGraph.Values.eq_indices_norm: %a %a " (pp_vid env)
- kid (pp_vid env) rid;
+ Debug.dprintf4 debug "WEGraph.Values.eq_indices_norm: %a %a " (pp_nid env)
+ kid (pp_nid env) rid;
Option.iter
(fun (rsto, rsel) ->
let ksto, ksel =
@@ -339,8 +315,8 @@ module Values = struct
(VIHT.find_opt env rid)
let eq_values_norm env kid rid =
- Debug.dprintf4 debug "WEGraph.Values.eq_values_norm: %a %a " (pp_val_id env)
- kid (pp_val_id env) rid;
+ Debug.dprintf4 debug "WEGraph.Values.eq_values_norm: %a %a " (pp_nid env)
+ kid (pp_nid env) rid;
Option.iter
(fun (rsto, rsel) ->
let ksto, ksel =
@@ -455,20 +431,20 @@ module WEG = struct
let rec aux (m : DInt.t DInt.M.t DInt.M.t) =
match DInt.M.min_binding m with
| nid, mnp when DInt.M.is_empty mnp ->
- Format.fprintf fmt " \"%a\";@." Node.pp (EHT.find env nid);
+ Format.fprintf fmt " \"%a\";@." Node.pp (ITN.find env nid);
aux (DInt.M.remove nid m)
| nid, mnp ->
- let nidn = EHT.find env nid in
+ let nidn = ITN.find env nid in
aux
@@ DInt.M.fold
(fun inid (kid : DInt.t) (nm : DInt.t DInt.M.t DInt.M.t) ->
- let inidn = EHT.find env inid in
- let k = VHT.find env kid in
+ let inidn = ITN.find env inid in
+ let k = ITN.find env kid in
match DInt.M.find_opt inid nm with
| Some inpm -> (
match DInt.M.find_opt nid inpm with
| Some kid' ->
- let k' = VHT.find env kid' in
+ let k' = ITN.find env kid' in
if Egraph.is_equal env k k' then (
pp_arrow fmt nidn inidn k
~options:[ ("dir", "both") ];
@@ -653,7 +629,7 @@ module KnownValues = struct
Debug.dprintf6 debug
"Adding (%a) the known values of %a (and its neighbours excluding \
%a)"
- (DInt.M.pp Node.pp) ppg (pp_eid env) src_id (Opt.pp DInt.pp) except;
+ (DInt.M.pp Node.pp) ppg (pp_nid env) src_id (Opt.pp DInt.pp) except;
let new_ppg = add_kvs env src_id ppg in
ppg_neighbours env ?except src_id new_ppg
@@ -663,18 +639,18 @@ module KnownValues = struct
let ns = match except with Some e -> DInt.M.remove e ns | None -> ns in
Debug.dprintf8 debug
"Propagating (%a) over the neighbours (%a) of %a (excluding %a)"
- (DInt.M.pp Node.pp) ppg (DInt.M.pp DInt.pp) ns (pp_eid env) src_id
+ (DInt.M.pp Node.pp) ppg (DInt.M.pp DInt.pp) ns (pp_nid env) src_id
(Opt.pp DInt.pp) except;
DInt.M.iter
(fun dest_id dest_ind_id ->
- let n_vrt = VHT.find env dest_ind_id in
+ let n_vrt = ITN.find env dest_ind_id in
let dest_ppg =
DInt.M.filter
(fun ppg_ind ppg_val ->
if is_nppg env dest_ind_id ppg_ind then false
else if
(not (is_already_ppg env dest_id ppg_ind ppg_val))
- && Equality.is_disequal env (VHT.find env ppg_ind) n_vrt
+ && Equality.is_disequal env (ITN.find env ppg_ind) n_vrt
then true
else (
add_nppg env dest_ind_id ppg_ind;
@@ -712,10 +688,10 @@ module KnownValues = struct
| None, None -> ()
let split_nppgs env ind s =
- let indn = VHT.find env ind in
+ let indn = ITN.find env ind in
DInt.S.fold
(fun iid (acc1, acc2) ->
- let iidn = VHT.find env iid in
+ let iidn = ITN.find env iid in
if Equality.is_disequal env indn iidn then (DInt.S.add iid acc1, acc2)
else (acc1, DInt.S.add iid acc2))
s
@@ -819,7 +795,7 @@ module KnownValues = struct
let ppg_s =
match (NP.find_opt env ind1, NP.find_opt env ind2) with
| Some nps1, Some nps2 ->
- let ind1n, ind2n = (VHT.find env ind1, VHT.find env ind2) in
+ let ind1n, ind2n = (ITN.find env ind1, ITN.find env ind2) in
let ppg_s, nnps =
DInt.S.fold
(fun iid (acc1, acc2) ->
@@ -828,7 +804,7 @@ module KnownValues = struct
(acc1, acc2))
else if DInt.S.mem iid nps2 then (acc1, DInt.S.add iid acc2)
else
- let iidn = VHT.find env iid in
+ let iidn = ITN.find env iid in
if Equality.is_disequal env ind2n iidn then (
rm_np_id env iid ind1;
(DInt.S.add iid acc1, acc2))
@@ -844,7 +820,7 @@ module KnownValues = struct
else if DInt.S.mem iid nps1 then
(* it was already added in the fold over nps1 *) (acc1, acc2)
else
- let iidn = VHT.find env iid in
+ let iidn = ITN.find env iid in
if Equality.is_disequal env ind1n iidn then
(DInt.S.add iid acc1, acc2)
else (
@@ -856,12 +832,12 @@ module KnownValues = struct
NP.remove env ind2;
ppg_s
| None, Some nps2 ->
- let ind1n = VHT.find env ind1 in
+ let ind1n = ITN.find env ind1 in
let ppg_s, _nnps =
DInt.S.fold
(fun iid (acc1, acc2) ->
rm_np_id env iid ind2;
- let iidn = VHT.find env iid in
+ let iidn = ITN.find env iid in
if Equality.is_disequal env ind1n iidn then
(DInt.S.add iid acc1, acc2)
else (
@@ -873,11 +849,11 @@ module KnownValues = struct
NP.remove env ind2;
ppg_s
| Some nps1, None ->
- let ind2n = VHT.find env ind2 in
+ let ind2n = ITN.find env ind2 in
let ppg_s, _nnps =
DInt.S.fold
(fun iid (acc1, acc2) ->
- let iidn = VHT.find env iid in
+ let iidn = ITN.find env iid in
if Equality.is_disequal env ind2n iidn then (
rm_np_id env iid ind1;
(DInt.S.add iid acc1, acc2))
@@ -925,7 +901,7 @@ let are_neighbours env id1 id2 =
| Some (_, m) -> DInt.M.mem id2 m
let rm_neighbour env (kid, knode) (rid, rnode) iid =
- let ind = VHT.find env iid in
+ let ind = ITN.find env iid in
WEG.change env kid ~f:(function
| None -> raise (Not_a_neighbour (knode, rnode, ind))
| Some (m1, m2) ->
@@ -943,7 +919,7 @@ let rm_neighbour env (kid, knode) (rid, rnode) iid =
DInt.M.change
(function
| Some iid' ->
- let ind' = VHT.find env iid' in
+ let ind' = ITN.find env iid' in
assert (Egraph.is_equal env ind ind');
None
| None -> raise (Not_a_neighbour (knode, rnode, ind)))
@@ -979,15 +955,15 @@ let add_neighbour vid aid = function
DInt.M.add aid vid m2 )
let add_edge_aux env (a, aid) (b, bid) (i, iid) ind_gty val_gty =
- Debug.dprintf6 debug "WEGraph: add_edge_aux %a between %a and %a" (pp_vid env)
- iid (pp_eid env) aid (pp_eid env) bid;
+ Debug.dprintf6 debug "WEGraph: add_edge_aux %a between %a and %a" (pp_nid env)
+ iid (pp_nid env) aid (pp_nid env) bid;
match DInt.M.find_opt bid (snd (WEG.find env aid)) with
| Some jid when iid = jid -> ()
| None ->
WEG.change env aid ~f:(add_neighbour iid bid);
WEG.change env bid ~f:(add_neighbour iid aid)
| Some jid ->
- let j = VHT.find env jid in
+ let j = ITN.find env jid in
let ij_eq = Equality.equality env [ i; j ] in
let ij_neq = Equality.disequality env [ i; j ] in
Egraph.register env ij_eq;
@@ -1052,20 +1028,20 @@ let add_edge ?from_merge env aid bid iid =
as a neighbour to all the nodes in the complete graph formed by all the
array nodes which differ on the same index k. *)
Debug.dprintf6 debug "WEGraph: adding the edge %a between %a and %a"
- (pp_vid env) iid (pp_eid env) aid (pp_eid env) bid;
+ (pp_nid env) iid (pp_nid env) aid (pp_nid env) bid;
if aid <> bid (* && not (are_k_neighbours env aid bid iid) *) then (
let ind_gty, val_gty =
- array_gty_args (get_node_ty env (EHT.find env aid))
+ array_gty_args (get_node_ty env (ITN.find env aid))
in
let ank = get_k_neighbours env aid iid in
let bnk = get_k_neighbours env bid iid in
- let ind = VHT.find env iid in
+ let ind = ITN.find env iid in
DInt.S.iter
(fun id1 ->
DInt.S.iter
(fun id2 ->
- let n1 = EHT.find env id1 in
- let n2 = EHT.find env id2 in
+ let n1 = ITN.find env id1 in
+ let n2 = ITN.find env id2 in
if (not (are_neighbours env id1 id2)) && id1 <> id2 then (
Vertices.change env iid ~f:(function
| Some s -> Some (Vertex.S.add (id1, id2) s)
@@ -1080,22 +1056,22 @@ let add_edge ?from_merge env aid bid iid =
~msg:
(Fmt.str
"_merge_neighbours %a %a\\n add edge between %a and %a with %a"
- (pp_eid env) kid (pp_eid env) rid (pp_eid env) aid (pp_eid env)
- bid Node.pp (VHT.find env iid))
+ (pp_nid env) kid (pp_nid env) rid (pp_nid env) aid (pp_nid env)
+ bid Node.pp (ITN.find env iid))
env ()
| None ->
WEG.pp_dot_wegraph
~msg:
- (Fmt.str "Add edge between %a and %a with %a" (pp_eid env) aid
- (pp_eid env) bid Node.pp (VHT.find env iid))
+ (Fmt.str "Add edge between %a and %a with %a" (pp_nid env) aid
+ (pp_nid env) bid Node.pp (ITN.find env iid))
env ())
let rm_edge ?from_merge env aid bid iid =
- Debug.dprintf6 debug "WEGraph: rm_edge %a between %a and %a" (pp_vid env) iid
- (pp_eid env) aid (pp_eid env) bid;
+ Debug.dprintf6 debug "WEGraph: rm_edge %a between %a and %a" (pp_nid env) iid
+ (pp_nid env) aid (pp_nid env) bid;
if aid <> bid then (
- let an = EHT.find env aid in
- let bn = EHT.find env bid in
+ let an = ITN.find env aid in
+ let bn = ITN.find env bid in
Vertices.change env iid ~f:(function
| Some s -> Some (Vertex.S.remove (aid, bid) s)
| None -> None (* should be unreachable *));
@@ -1109,28 +1085,28 @@ let rm_edge ?from_merge env aid bid iid =
(Fmt.str
"_merge_neighbours %a to %a\\n remove the edge %a between %a \
and %a"
- (pp_eid env) kid (pp_eid env) rid (pp_vid env) iid (pp_eid env)
- aid (pp_eid env) bid)
+ (pp_nid env) kid (pp_nid env) rid (pp_nid env) iid (pp_nid env)
+ aid (pp_nid env) bid)
env ()
| None ->
WEG.pp_dot_wegraph
~msg:
- (Fmt.str " remove the edge %a between %a and %a" (pp_vid env) iid
- (pp_eid env) aid (pp_eid env) bid)
+ (Fmt.str " remove the edge %a between %a and %a" (pp_nid env) iid
+ (pp_nid env) aid (pp_nid env) bid)
env ())
let merge_neigbours_aux env (a, aid) (_, bid) nid kk_opt kr_opt () =
match (kk_opt, kr_opt) with
| Some iid, Some jid ->
- let i = VHT.find env iid in
- let j = VHT.find env jid in
+ let i = ITN.find env iid in
+ let j = ITN.find env jid in
Debug.dprintf6 debug
"WEGraph: _merge_neigbours_aux: iter1: found the neighbour %a through \
%a and %a"
- (pp_eid env) nid (pp_vid env) iid (pp_vid env) jid;
+ (pp_nid env) nid (pp_nid env) iid (pp_nid env) jid;
if not (Egraph.is_equal env i j) then (
let ijeq = Equality.equality env [ i; j ] in
- let aneq = Equality.equality env [ a; EHT.find env nid ] in
+ let aneq = Equality.equality env [ a; ITN.find env nid ] in
Egraph.register env ijeq;
Egraph.register env aneq;
Choice.register_global env
@@ -1153,14 +1129,14 @@ let merge_neigbours_aux env (a, aid) (_, bid) nid kk_opt kr_opt () =
Debug.dprintf4 debug
"WEGraph: _merge_neigbours_aux: iter2: found the neighbour %a through \
%a"
- (pp_eid env) nid (pp_vid env) iid;
+ (pp_nid env) nid (pp_nid env) iid;
rm_edge ~from_merge:(aid, bid) env nid bid iid;
add_edge ~from_merge:(aid, bid) env nid aid iid
| _ -> ()
let merge_neighbours env (kn, kid) (rn, rid) b =
Debug.dprintf5 debug "WEGraph: _merge_neighbours %b [kn=%a; rn=%a]" b
- (pp_eid env) kid (pp_eid env) rid;
+ (pp_nid env) kid (pp_nid env) rid;
(* Add all the neighbours of rnode to knp, removes rnode as a neighbour from the
others and adds knp as a neighbour to them if it isn't already. *)
(match (WEG.find_opt env kid, WEG.find_opt env rid) with
@@ -1178,7 +1154,7 @@ let merge_neighbours env (kn, kid) (rn, rid) b =
WEG.pp_dot_wegraph
~msg:
(Fmt.str "_merge_neighbours %b | %a | %a\\n remove %a" b
- (pp_eid env) kid (pp_eid env) rid (pp_eid env) rid)
+ (pp_nid env) kid (pp_nid env) rid (pp_nid env) rid)
env ()
| None, Some (_, rnm) ->
let rnm = DInt.M.remove kid rnm in
@@ -1187,34 +1163,34 @@ let merge_neighbours env (kn, kid) (rn, rid) b =
Debug.dprintf4 debug
"WEGraph: _merge_neighbours: iter3: found the neighbour %a through \
%a"
- (pp_eid env) nid (pp_vid env) iid;
+ (pp_nid env) nid (pp_nid env) iid;
rm_edge ~from_merge:(kid, rid) env nid rid iid;
add_edge ~from_merge:(kid, rid) env nid kid iid)
rnm
| _ -> ());
if not b then (
- EHT.set env kid rn;
+ ITN.set env kid rn;
if Debug.test_flag WEG.wegraph_opt then
WEG.pp_dot_wegraph
~msg:
(Fmt.str "_merge_neighbours %b | %a | %a\\n replace %a <- %a" b
- (pp_eid env) kid (pp_eid env) rid (pp_eid env) kid (pp_eid env) rid)
+ (pp_nid env) kid (pp_nid env) rid (pp_nid env) kid (pp_nid env) rid)
env ())
let eq_arrays_norm env (kn, kid) (rn, rid) b =
- Debug.dprintf4 debug "WEGraph: eq_arrays_norm_ %a %a" (pp_eid env) kid
- (pp_eid env) rid;
+ Debug.dprintf4 debug "WEGraph: eq_arrays_norm_ %a %a" (pp_nid env) kid
+ (pp_nid env) rid;
Values.eq_arrays_norm env kid rid;
KnownValues.eq_arrays_norm env kid rid;
merge_neighbours env (kn, kid) (rn, rid) b;
if Debug.test_flag WEG.wegraph_opt then
WEG.pp_dot_wegraph
- ~msg:(Fmt.str "eq_arrays_norm_ %a %a" (pp_eid env) kid (pp_eid env) rid)
+ ~msg:(Fmt.str "eq_arrays_norm_ %a %a" (pp_nid env) kid (pp_nid env) rid)
env ()
let eq_indices_norm env (_kn, kid) (rn, rid) b =
- Debug.dprintf4 debug "WEGraph: eq_indices_norm_ %a %a" (pp_vid env) kid
- (pp_vid env) rid;
+ Debug.dprintf4 debug "WEGraph: eq_indices_norm_ %a %a" (pp_nid env) kid
+ (pp_nid env) rid;
Values.eq_indices_norm env kid rid;
let ppg_s = KnownValues.eq_indices_norm env kid rid in
(match (Vertices.find_opt env kid, Vertices.find_opt env rid) with
@@ -1225,23 +1201,23 @@ let eq_indices_norm env (_kn, kid) (rn, rid) b =
add_edge env aid bid kid)
sr
| _ -> ());
- VHT.remove env rid;
- if not b then VHT.set env kid rn;
+ ITN.remove env rid;
+ if not b then ITN.set env kid rn;
DInt.S.iter (KnownValues.reppg env kid) ppg_s;
if Debug.test_flag WEG.wegraph_opt then
WEG.pp_dot_wegraph
- ~msg:(Fmt.str "_eq_indices_norm %a %a" (pp_vid env) kid (pp_vid env) rid)
+ ~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 =
- Debug.dprintf4 debug "WEGraph: eq_values_norm_ %a %a" (pp_val_id env) kid
- (pp_val_id env) rid;
+ 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 ValHT.set env kid (ValHT.find env rid);
- ValHT.remove env rid
+ if not _b then ITN.set env kid (ITN.find env rid);
+ ITN.remove env rid
let ineq_indices_norm env s =
- Debug.dprintf2 debug "WEGraph: ineq_indices_norm_: %a" KnownValues.HT.pp env;
+ Debug.dprintf2 debug "WEGraph: ineq_indices_norm_: %a" Node.S.pp s;
let ns =
List.filter_map
(fun n ->
@@ -1257,15 +1233,15 @@ let new_store env a b ind v =
let bid = Id.Array.get_id env b in
let iid = Id.Index.get_id env ind in
let vid = Id.Value.get_id env v in
- Debug.dprintf8 debug "WEGraph.new_store: %a %a %a %a" (pp_eid env) aid
- (pp_eid env) bid (pp_vid env) iid (pp_val_id env) vid;
+ Debug.dprintf8 debug "WEGraph.new_store: %a %a %a %a" (pp_nid env) aid
+ (pp_nid env) bid (pp_nid env) iid (pp_nid env) vid;
Values.add_store env aid bid iid vid;
add_edge env aid bid iid;
KnownValues.directed_ppg env aid (DInt.M.singleton iid v);
if Debug.test_flag WEG.wegraph_opt then
WEG.pp_dot_wegraph
~msg:
- (Fmt.str "WEGraph.update: %a %a %a" (pp_eid env) aid (pp_eid env) bid
+ (Fmt.str "WEGraph.update: %a %a %a" (pp_nid env) aid (pp_nid env) bid
Node.pp ind)
env ()
@@ -1273,8 +1249,8 @@ let new_select env r a i =
let aid = Id.Array.get_id env a in
let iid = Id.Index.get_id env i in
let rid = Id.Value.get_id env r in
- Debug.dprintf6 debug "WEGraph.new_select: %a %a %a" (pp_val_id env) rid
- (pp_eid env) aid (pp_vid env) iid;
+ Debug.dprintf6 debug "WEGraph.new_select: %a %a %a" (pp_nid env) rid
+ (pp_nid env) aid (pp_nid env) iid;
Values.add_select env rid aid iid;
match KnownValues.HT.find_opt env aid with
| None -> ()
@@ -1301,20 +1277,20 @@ let get_neighbours env nid =
let new_id_hook env id n =
WEG.set env id (DInt.M.empty, DInt.M.empty);
- EHT.set env id n
+ ITN.set env id n
let new_index_id_hook env id n =
Vertices.set env id Vertex.S.empty;
- VHT.set env id n
+ 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 ->
DInt.M.fold
(fun i v acc ->
- let indn = VHT.find env i in
+ let indn = ITN.find env i in
Node.M.add indn v acc)
kv Node.M.empty
| None -> Node.M.empty
-let new_value_id_hook env id n = ValHT.set env id n
+let new_value_id_hook env id n = ITN.set env id n
diff --git a/colibri2/theories/array/common.ml b/colibri2/theories/array/common.ml
index 4e35ab627..0596c8286 100644
--- a/colibri2/theories/array/common.ml
+++ b/colibri2/theories/array/common.ml
@@ -81,6 +81,29 @@ exception NoIdFound of string * Node.t
exception Not_a_neighbour of (Node.t * Node.t * Node.t)
exception Empty_neighbour_set of (Node.t * Node.t * Node.t)
+let () =
+ Printexc.register_printer (function
+ | Not_An_Array n -> Some (Fmt.str "%a is not an array!" Node.pp n)
+ | Not_An_Array_gty gty ->
+ Some (Fmt.str "%a is not an array ground type!" Ground.Ty.pp gty)
+ | Not_An_Array_ty ty ->
+ Some (Fmt.str "%a is not an array type!" Expr.Ty.pp ty)
+ | Type_Not_Set n ->
+ Some (Fmt.str "the type of the node %a was not set!" Node.pp n)
+ | NoIdFound (s, n) ->
+ Some (Fmt.str "get_id(%s) of %a: No Id found!" s Node.pp n)
+ | Not_a_neighbour (kn, rn, k) ->
+ Some
+ (Fmt.str "%a was expected to be a neighbour of %a through %a" Node.pp
+ rn Node.pp kn Node.pp k)
+ | Empty_neighbour_set (kn, rn, k) ->
+ Some
+ (Fmt.str
+ "%a was expected to be a neighbour of %a through %a, but %a's \
+ neighbour set is empty"
+ Node.pp rn Node.pp kn Node.pp k Node.pp kn)
+ | _ -> None)
+
module STV = struct
let ind_ty_var = Expr.Ty.Var.mk "ind_ty"
let val_ty_var = Expr.Ty.Var.mk "val_ty"
@@ -351,16 +374,16 @@ let do_mk_eq_if_neq env a b =
if not (Egraph.is_equal env a b) then do_mk_eq env a b
module type HTS = sig
+ type key
type t
- val set : Egraph.wt -> int -> t -> unit
- val find : Egraph.wt -> int -> t
- val find_opt : Egraph.wt -> int -> t option
- val change : f:(t option -> t option) -> Egraph.wt -> int -> unit
- val remove : Egraph.wt -> int -> unit
- val iter : f:(int -> t -> unit) -> Egraph.wt -> unit
- val fold : (int -> t -> 'a -> 'a) -> Egraph.wt -> 'a -> 'a
- val filter_map_inplace : (int -> t -> t option) -> 'a Egraph.t -> unit
+ val set : Egraph.wt -> key -> t -> unit
+ val find : Egraph.wt -> key -> t
+ val find_opt : Egraph.wt -> key -> t option
+ val change : f:(t option -> t option) -> Egraph.wt -> key -> unit
+ val remove : Egraph.wt -> key -> unit
+ val iter : f:(key -> t -> unit) -> Egraph.wt -> unit
+ val fold : (key -> t -> 'a -> 'a) -> Egraph.wt -> 'a -> 'a
val pp : Format.formatter -> Egraph.wt -> unit
end
@@ -369,7 +392,8 @@ module MkIHT (V : sig
val pp : t Pp.pp
val name : string
-end) : HTS with type t = V.t = struct
+end) : HTS with type key = int and type t = V.t = struct
+ type key = int
type t = V.t
let db = HT.create V.pp V.name
@@ -380,7 +404,6 @@ end) : HTS with type t = V.t = struct
let remove (env : Egraph.wt) i = HT.remove db env i
let iter = HT.iter db
let fold f env acc = HT.fold f db env acc
- let filter_map_inplace f env = HT.filter_map_inplace f db env
let pp fmt env =
Fmt.pf fmt "%s:[%a]" V.name
@@ -402,35 +425,13 @@ module type IdDomSig = sig
val get_id : Egraph.wt -> Node.t -> int
end
-let () =
- Printexc.register_printer (function
- | Not_An_Array n -> Some (Fmt.str "%a is not an array!" Node.pp n)
- | Not_An_Array_gty gty ->
- Some (Fmt.str "%a is not an array ground type!" Ground.Ty.pp gty)
- | Not_An_Array_ty ty ->
- Some (Fmt.str "%a is not an array type!" Expr.Ty.pp ty)
- | Type_Not_Set n ->
- Some (Fmt.str "the type of the node %a was not set!" Node.pp n)
- | NoIdFound (s, n) ->
- Some (Fmt.str "get_id(%s) of %a: No Id found!" s Node.pp n)
- | Not_a_neighbour (kn, rn, k) ->
- Some
- (Fmt.str "%a was expected to be a neighbour of %a through %a" Node.pp
- rn Node.pp kn Node.pp k)
- | Empty_neighbour_set (kn, rn, k) ->
- Some
- (Fmt.str
- "%a was expected to be a neighbour of %a through %a, but %a's \
- neighbour set is empty"
- Node.pp rn Node.pp kn Node.pp k Node.pp kn)
- | _ -> None)
+(** Global Id counter *)
+let id_counter = ref 0
module MkIdDom (N : sig
- val n1 : string
- val n2 : string
- val n3 : string
+ val name : string
end) : IdDomSig = struct
- let merge_hooks = Datastructure.Push.create Fmt.nop N.n1
+ let merge_hooks = Datastructure.Push.create Fmt.nop (N.name ^ ".merge_hooks")
let register_merge_hook env (f : Egraph.wt -> 'a -> 'a -> bool -> unit) =
Datastructure.Push.push merge_hooks env f
@@ -448,7 +449,7 @@ end) : IdDomSig = struct
(module struct
type nonrec t = t
- let name = N.n2
+ let name = N.name ^ ".DOM"
end)
let inter _ v _ = Some v
@@ -469,28 +470,108 @@ end) : IdDomSig = struct
end
let () = Dom.register (module D)
- let new_id_hooks = Datastructure.Push.create Fmt.nop N.n3
+ let new_id_hooks = Datastructure.Push.create Fmt.nop (N.name ^ ".new_id_hooks")
let register_new_id_hook env (f : Egraph.wt -> int -> Node.t -> unit) =
Datastructure.Push.push new_id_hooks env f
let set_id, get_id =
- let id_counter = ref 0 in
let set_id env n =
match Egraph.get_dom env D.key n with
| None ->
incr id_counter;
- Debug.dprintf4 debug "set_id(%s) of %a: none -> %d" N.n2 Node.pp n
+ Debug.dprintf4 debug "set_id(%s) of %a: none -> %d" N.name Node.pp n
!id_counter;
D.set_dom env n !id_counter;
Datastructure.Push.iter new_id_hooks env ~f:(fun new_id_hook ->
new_id_hook env !id_counter n)
- | Some id -> Debug.dprintf4 debug "set_id(%s) of %a: %d" N.n2 Node.pp n id
+ | Some id ->
+ Debug.dprintf4 debug "set_id(%s) of %a: %d" N.name Node.pp n id
in
+
let get_id env n =
match Egraph.get_dom env D.key n with
| Some id -> id
- | None -> raise (NoIdFound (N.n2, n))
+ | None -> raise (NoIdFound (N.name, n))
in
(set_id, get_id)
end
+
+module SHT (K : sig
+ include Datatype
+
+ val sort : t -> t
+ val pp : t Pp.pp
+end) (V : sig
+ type t
+
+ val name : string
+ val pp : t Pp.pp
+end) : HTS with type key = K.t and type t = V.t = struct
+ type key = K.t
+ type t = V.t
+
+ module HT = Datastructure.Hashtbl (K)
+
+ let db = HT.create V.pp V.name
+ let aux f env k = f db env (K.sort k)
+ let remove = aux HT.remove
+ let set = aux HT.set
+ let find = aux HT.find
+ let find_opt = aux HT.find_opt
+ let mem = aux HT.mem
+ let change ~f = aux (HT.change f)
+ let iter = HT.iter db
+ let fold f env acc = HT.fold f db env acc
+
+ let pp fmt env =
+ Fmt.pf fmt "%s:[%a]" V.name
+ (fun fmt () ->
+ iter env ~f:(fun i v -> Fmt.pf fmt "(%a -> %a);@ " K.pp i V.pp v))
+ ()
+end
+
+module I4 = struct
+ module T = struct
+ type t = DInt.t * DInt.t * DInt.t * DInt.t * Ground.Ty.t * Ground.Ty.t
+ [@@deriving eq, ord, hash, show]
+ end
+
+ include T
+ include MkDatatype (T)
+end
+
+module I3 = struct
+ module T = struct
+ type t = DInt.t * DInt.t * DInt.t * Ground.Ty.t * Ground.Ty.t
+ [@@deriving eq, ord, hash, show]
+ end
+
+ include T
+ include MkDatatype (T)
+end
+
+module I2 = struct
+ module T = struct
+ type t = DInt.t * DInt.t * Ground.Ty.t * Ground.Ty.t
+ [@@deriving eq, ord, hash, show]
+ end
+
+ include T
+ include MkDatatype (T)
+end
+
+module I1 = struct
+ module T = struct
+ type t = DInt.t * Ground.Ty.t * Ground.Ty.t [@@deriving eq, ord, hash, show]
+ end
+
+ include T
+ include MkDatatype (T)
+end
+
+(* (id1,id2,id3,id4,ty1,ty2) *)
+(* (id1,id2,ty1,ty2) *)
+
+(* id1 -> (id2,id3,id4,ty1,ty2) *)
+(* id1 -> (id2,ty1,ty2) *)
diff --git a/colibri2/theories/array/common.mli b/colibri2/theories/array/common.mli
index 101a6a0ef..81fc6144d 100644
--- a/colibri2/theories/array/common.mli
+++ b/colibri2/theories/array/common.mli
@@ -19,6 +19,9 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
+open Colibri2_popop_lib
+open Popop_stdlib
+
val no_wegraph : bool Options.t
val no_res_ext : bool Options.t
val no_res_aup : bool Options.t
@@ -140,25 +143,25 @@ val do_mk_eq : Egraph.wt -> Node.t -> Node.t -> unit
val do_mk_eq_if_neq : Egraph.wt -> Node.t -> Node.t -> unit
module type HTS = sig
+ type key
type t
- val set : Egraph.wt -> int -> t -> unit
- val find : Egraph.wt -> int -> t
- val find_opt : Egraph.wt -> int -> t option
- val change : f:(t option -> t option) -> Egraph.wt -> int -> unit
- val remove : Egraph.wt -> int -> unit
- val iter : f:(int -> t -> unit) -> Egraph.wt -> unit
- val fold : (int -> t -> 'a -> 'a) -> Egraph.wt -> 'a -> 'a
- val filter_map_inplace : (int -> t -> t option) -> 'a Egraph.t -> unit
+ val set : Egraph.wt -> key -> t -> unit
+ val find : Egraph.wt -> key -> t
+ val find_opt : Egraph.wt -> key -> t option
+ val change : f:(t option -> t option) -> Egraph.wt -> key -> unit
+ val remove : Egraph.wt -> key -> unit
+ val iter : f:(key -> t -> unit) -> Egraph.wt -> unit
+ val fold : (key -> t -> 'a -> 'a) -> Egraph.wt -> 'a -> 'a
val pp : Format.formatter -> Egraph.wt -> unit
end
module MkIHT (V : sig
type t
- val pp : t Colibri2_popop_lib.Pp.pp
+ val pp : t Pp.pp
val name : string
-end) : HTS with type t = V.t
+end) : HTS with type key = int and type t = V.t
module type IdDomSig = sig
val register_merge_hook :
@@ -174,7 +177,27 @@ module type IdDomSig = sig
end
module MkIdDom (_ : sig
- val n1 : string
- val n2 : string
- val n3 : string
+ val name : string
end) : IdDomSig
+
+module SHT (K : sig
+ include Datatype
+
+ val sort : t -> t
+ val pp : t Pp.pp
+end) (V : sig
+ type t
+
+ val name : string
+ val pp : t Pp.pp
+end) : HTS with type key = K.t and type t = V.t
+
+module I4 :
+ Datatype
+ 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
+
+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
--
GitLab