From 5bef85ce54a067129a30065f1e665fb7a15e8a3b Mon Sep 17 00:00:00 2001
From: hra687261 <hichem.ait-el-hara@ocamlpro.com>
Date: Tue, 7 Feb 2023 21:19:27 +0100
Subject: [PATCH] [Array] Use integers for vertices, added eq_indices_norm
---
colibri2/theories/array/DiffGraph.ml | 378 +++++++++++++-------
colibri2/theories/array/DiffGraph.mli | 36 +-
colibri2/theories/array/SharingIsCaring.ml | 49 ---
colibri2/theories/array/SharingIsCaring.mli | 23 --
colibri2/theories/array/array.ml | 27 +-
colibri2/theories/array/common.ml | 17 +-
colibri2/theories/array/common.mli | 22 +-
7 files changed, 307 insertions(+), 245 deletions(-)
delete mode 100644 colibri2/theories/array/SharingIsCaring.ml
delete mode 100644 colibri2/theories/array/SharingIsCaring.mli
diff --git a/colibri2/theories/array/DiffGraph.ml b/colibri2/theories/array/DiffGraph.ml
index 5ee8fb152..184099176 100644
--- a/colibri2/theories/array/DiffGraph.ml
+++ b/colibri2/theories/array/DiffGraph.ml
@@ -25,18 +25,52 @@ open Popop_stdlib
open Common
module HT = Datastructure.Hashtbl (DInt)
-module NHT = MkIHT (struct
+module EHT = MkIHT (struct
type t = Node.t
let pp = Node.pp
- let name = "diffgraph_nodes"
+ let name = "diffgraph_edges"
+end)
+
+module VHT = MkIHT (struct
+ type t = Node.t
+
+ let pp = Node.pp
+ let name = "diffgraph_indices"
+end)
+
+module Vertex = struct
+ let sort (a, b) = if DInt.compare a b <= 0 then (a, b) else (b, a)
+
+ include MkDatatype (struct
+ type t = DInt.t * DInt.t
+
+ let hash (a, b) = Hashcons.combine (DInt.hash a) (DInt.hash b)
+
+ let compare (a1, b1) (a2, b2) =
+ match (sort (a1, b1), sort (a2, b2)) with
+ | (a1, b1), (a2, b2) ->
+ let r = DInt.compare a1 a2 in
+ if r = 0 then DInt.compare b1 b2 else r
+
+ let equal a b = compare a b = 0
+ let pp fmt (a, b) = Fmt.pf fmt "(%d, %d)" a b
+ let hash_fold_t s (a, b) = DInt.hash_fold_t s (hash (a, b))
+ end)
+end
+
+module Vertices = MkIHT (struct
+ type t = Vertex.S.t
+
+ let pp = Vertex.S.pp
+ let name = "index_vertices"
end)
module DG = struct
include MkIHT (struct
- type t = DInt.S.t Node.M.t * Node.t DInt.M.t
+ type t = DInt.S.t DInt.M.t * DInt.t DInt.M.t
- let pp fmt (m, (_ : Node.t DInt.M.t)) = Node.M.pp DInt.S.pp fmt m
+ let pp fmt (m, (_ : DInt.t DInt.M.t)) = DInt.M.pp DInt.S.pp fmt m
let name = "diffgraph_nodes"
end)
@@ -69,29 +103,32 @@ module DG = struct
in
let update_nm np inp inpm nm = DInt.M.add inp (DInt.M.remove np inpm) nm in
let pp_maps_aux env fmt () =
- let rec aux (m : Node.t DInt.M.t DInt.M.t) =
+ 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 (NHT.find env nid);
+ Format.fprintf fmt " \"%a\";@." Node.pp (EHT.find env nid);
aux (DInt.M.remove nid m)
| nid, mnp ->
- let nidn = NHT.find env nid in
+ let nidn = EHT.find env nid in
aux
@@ DInt.M.fold
- (fun inid k nm ->
- let inidn = NHT.find env inid in
+ (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
match DInt.M.find_opt inid nm with
| Some inpm -> (
match DInt.M.find_opt nid inpm with
- | Some k' when Egraph.is_equal env k k' ->
- pp_arrow fmt nidn inidn k
- ~options:[ ("dir", "both") ];
- update_nm nid inid inpm nm
- | Some k' ->
- pp_arrow fmt nidn inidn k ~k'
- ~options:
- [ ("dir", "both"); ("color", "turquoise") ];
- update_nm nid inid inpm nm
+ | Some kid' ->
+ let k' = VHT.find env kid' in
+ if Egraph.is_equal env k k' then (
+ pp_arrow fmt nidn inidn k
+ ~options:[ ("dir", "both") ];
+ update_nm nid inid inpm nm)
+ else (
+ pp_arrow fmt nidn inidn k ~k'
+ ~options:
+ [ ("dir", "both"); ("color", "turquoise") ];
+ update_nm nid inid inpm nm)
| None ->
pp_arrow fmt nidn inidn k
~options:[ ("color", "red") ];
@@ -114,6 +151,13 @@ module DG = struct
| Some msg -> Fmt.pf fmt " label = \"%s\"@." msg
| None -> ())
msg)
+
+ let pp env fmt id =
+ match find_opt env id with
+ | Some (m1, m2) ->
+ Fmt.pf fmt "%d{%a;%a}" id (DInt.M.pp DInt.S.pp) m1 (DInt.M.pp DInt.pp)
+ m2
+ | None -> Fmt.pf fmt "%d{}" id
end
module Id_dom = struct
@@ -125,15 +169,36 @@ module Id_dom = struct
let new_id_hook env id n b =
if b then (
- DG.set env id (Node.M.empty, DInt.M.empty);
- NHT.set env id n)
+ DG.set env id (DInt.M.empty, DInt.M.empty);
+ EHT.set env id n)
+
+ let set_id env n = set_id ~new_id_hook env n
+ let get_id env n = get_id ~new_id_hook env n
+end
+
+module Index_Id_dom = struct
+ include MkIdDom (struct
+ let n1 = "Array.Index_Id.value"
+ let n2 = "Array.Index_Id_dom.merge_hooks"
+ let n3 = "Array.Index_id"
+ end)
+
+ let new_id_hook env id n b =
+ if b then (
+ Vertices.set env id Vertex.S.empty;
+ VHT.set env id n)
let set_id env n = set_id ~new_id_hook env n
let get_id env n = get_id ~new_id_hook env n
end
-let pp_nid env fmt i =
- match NHT.find_opt env i with
+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
@@ -145,7 +210,7 @@ let s_remove_opt s_opt v =
| None -> raise Not_found
let are_linked env id1 id2 =
- let rec aux (seen : DInt.S.t) (m : Node.t DInt.M.t) =
+ let rec aux (seen : DInt.S.t) (m : DInt.t DInt.M.t) =
DInt.M.fold
(fun id _ (seen, b) ->
if b then (seen, b)
@@ -163,37 +228,40 @@ let are_neighbours env id1 id2 =
| None -> false
| Some (_, m) -> DInt.M.mem id2 m
-let add_neighbour env (srcid, srcn) (destid, destn) k ind_gty val_gty =
- Debug.dprintf6 debug "DiffGraph: adding %a as a neighbour to %a through %a"
- Node.pp srcn Node.pp destn Node.pp k;
+let add_neighbour env (srcid, srcn) (destid, destn) ind ind_gty val_gty =
+ let iid = Index_Id_dom.get_id env ind in
+ Debug.dprintf6 debug "DiffGraph: add_neighbour %a to %a through %a"
+ (pp_eid env) srcid (pp_eid env) destid (pp_vid env) iid;
DG.change env destid ~f:(function
| None ->
Some
- (Node.M.singleton k (DInt.S.singleton srcid), DInt.M.singleton srcid k)
+ ( DInt.M.singleton iid (DInt.S.singleton srcid),
+ DInt.M.singleton srcid iid )
| Some (m1, m2) ->
Some
- ( Node.M.change
+ ( DInt.M.change
(function
| Some nps -> Some (DInt.S.add srcid nps)
| None -> Some (DInt.S.singleton srcid))
- k m1,
+ iid m1,
DInt.M.change
(function
- | Some k' ->
- if not (Egraph.is_equal env k k') then (
+ | Some iid' ->
+ let ind' = VHT.find env iid' in
+ if not (Egraph.is_equal env ind ind') then (
(* if a and b are already neighbours and k and k' are not
equal then set (k = k' \/ a[k] = b[k] \/ a[k'] = b[k']) to true *)
- let eq1 = mk_eq env k k' ind_gty in
+ let eq1 = mk_eq env ind ind' ind_gty in
let eq2 =
mk_eq env
- (mk_select env srcn k ind_gty val_gty)
- (mk_select env destn k ind_gty val_gty)
+ (mk_select env srcn ind ind_gty val_gty)
+ (mk_select env destn ind ind_gty val_gty)
(Ground.Ty.array ind_gty val_gty)
in
let eq3 =
mk_eq env
- (mk_select env srcn k' ind_gty val_gty)
- (mk_select env destn k' ind_gty val_gty)
+ (mk_select env srcn ind' ind_gty val_gty)
+ (mk_select env destn ind' ind_gty val_gty)
(Ground.Ty.array ind_gty val_gty)
in
let disj = mk_or env eq1 (mk_or env eq2 eq3) in
@@ -201,8 +269,7 @@ let add_neighbour env (srcid, srcn) (destid, destn) k ind_gty val_gty =
if Options.get env use_choice then
Choice.register_global env
{
- Choice.print_cho =
- "Decision from DiffGraph.add_neighbour.";
+ Choice.print_cho = "Decision from add_neighbour.";
Choice.prio = 1;
choice =
(fun env ->
@@ -221,13 +288,13 @@ let add_neighbour env (srcid, srcn) (destid, destn) k ind_gty val_gty =
Debug.dprintf10 debug
"DiffGraph: adding %a as a neighbour to %a through %a: \
setting %a = %a to true"
- Node.pp srcn Node.pp destn Node.pp k Node.pp k Node.pp
- k');
+ Node.pp srcn Node.pp destn Node.pp ind Node.pp ind
+ Node.pp ind');
(* Don't do anything right away, assume that the
activation of the equality hook will take care of
normalizing the graph. *)
- Some k
- | None -> Some k)
+ Some iid
+ | None -> Some iid)
srcid m2 ))
exception Not_a_neighbour of string
@@ -247,98 +314,121 @@ let empty_neighbour_set kn rn k =
neighbour set is empty"
Node.pp rn Node.pp kn Node.pp k Node.pp kn))
-let rm_neighbour env (kid, knode) (rid, rnode) k =
- Debug.dprintf6 debug "DiffGraph: rm_neighbour %a of %a through %a" Node.pp
- rnode Node.pp knode Node.pp k;
+let rm_neighbour env (kid, knode) (rid, rnode) iid =
+ let ind = VHT.find env iid in
+ Debug.dprintf6 debug "DiffGraph: rm_neighbour %a of %a through %a"
+ (pp_eid env) rid (pp_eid env) kid (pp_vid env) iid;
DG.change env kid ~f:(function
- | None -> empty_neighbour_set knode rnode k
+ | None -> empty_neighbour_set knode rnode ind
| Some (m1, m2) ->
- Some
- ( Node.M.change
- (fun s_opt ->
- match s_remove_opt s_opt rid with
- | s -> s
- | exception Not_found -> not_a_neighbour 1 knode rnode k)
- k m1,
- DInt.M.change
- (function
- | Some k' ->
- Debug.dprintf4 debug
- "DiffGraph: rm_neighbour found %a (should be equal to %a)"
- Node.pp k' Node.pp k;
- assert (Egraph.is_equal env k k');
- None
- | None -> not_a_neighbour 2 knode rnode k)
- rid m2 ))
-
-let get_k_neighbours env np k =
+ let nm1 =
+ DInt.M.change
+ (fun s_opt ->
+ match s_remove_opt s_opt rid with
+ | s -> s
+ | exception Not_found -> not_a_neighbour 1 knode rnode ind)
+ iid m1
+ in
+ let nm2 =
+ DInt.M.change
+ (function
+ | Some iid' ->
+ let ind' = VHT.find env iid' in
+ Debug.dprintf4 debug
+ "DiffGraph: rm_neighbour found %a (should be equal to %a)"
+ (pp_vid env) iid' (pp_vid env) iid;
+ assert (Egraph.is_equal env ind ind');
+ None
+ | None -> not_a_neighbour 2 knode rnode ind)
+ rid m2
+ in
+ Some (nm1, nm2))
+
+let get_k_neighbours env np iid =
match DG.find_opt env np with
| None -> DInt.S.empty
| Some (m, _) -> (
- match Node.M.find_opt k m with None -> DInt.S.empty | Some s -> s)
+ match DInt.M.find_opt iid m with None -> DInt.S.empty | Some s -> s)
-let add_edge env aid bid k =
+let add_edge env aid bid iid =
(* when adding a node dest as a neighbour to a node src, dest is also added
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.dprintf4 debug "DiffGraph: adding the edge %d between %d and %a" aid bid
- Node.pp k;
- let ind_gty, val_gty = array_gty_args (get_node_ty env (NHT.find env aid)) in
- let ank = DInt.S.add aid (get_k_neighbours env aid k) in
- let bnk = DInt.S.add bid (get_k_neighbours env bid k) in
- DInt.S.iter
- (fun id1 ->
- DInt.S.iter
- (fun id2 ->
- let n1 = NHT.find env id1 in
- let n2 = NHT.find env id2 in
- if (not (are_neighbours env id1 id2)) && id1 <> id2 then (
- add_neighbour env (id1, n1) (id2, n2) k ind_gty val_gty;
- add_neighbour env (id2, n2) (id1, n1) k ind_gty val_gty))
- bnk)
- ank
-
-let rm_edge_k env aid bid k =
- let an = NHT.find env aid in
- let bn = NHT.find env bid in
- rm_neighbour env (aid, an) (bid, bn) k;
- rm_neighbour env (bid, bn) (aid, an) k
-
-let add_edge_aux knp rnode env aid bid k =
- add_edge env aid bid k;
+ Debug.dprintf6 debug "DiffGraph: adding the edge %a between %a and %a"
+ (pp_vid env) iid (pp_eid env) aid (pp_eid env) bid;
+ if aid <> bid then
+ let ind_gty, val_gty =
+ array_gty_args (get_node_ty env (EHT.find env aid))
+ in
+ let ank = DInt.S.add aid (get_k_neighbours env aid iid) in
+ let bnk = DInt.S.add bid (get_k_neighbours env bid iid) in
+ let ind = VHT.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
+ 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)
+ | None -> Some (Vertex.S.singleton (id1, id2)));
+ add_neighbour env (id1, n1) (id2, n2) ind ind_gty val_gty;
+ add_neighbour env (id2, n2) (id1, n1) ind ind_gty val_gty))
+ bnk)
+ ank
+
+let rm_edge env aid bid iid =
+ Debug.dprintf6 debug "DiffGraph: rm_edge %a between %a and %a" (pp_vid env)
+ iid (pp_eid env) aid (pp_eid env) bid;
+ if aid <> bid then (
+ let an = EHT.find env aid in
+ let bn = EHT.find env bid in
+ Vertices.change env iid ~f:(function
+ | Some s -> Some (Vertex.S.remove (aid, bid) s)
+ | None -> None (* should be unreachable *));
+ rm_neighbour env (aid, an) (bid, bn) iid;
+ rm_neighbour env (bid, bn) (aid, an) iid)
+
+let add_edge_aux knp rnode env aid bid iid =
+ add_edge env aid bid iid;
if Debug.test_flag DG.diffgraph_opt then
DG.pp_dot_diffgraph
~msg:
(Fmt.str
"_merge_neighbours %a to %a\\n add edge between %a and %a with %a"
- Node.pp rnode Node.pp knp (pp_nid env) aid (pp_nid env) bid Node.pp k)
+ Node.pp rnode Node.pp knp (pp_eid env) aid (pp_eid env) bid Node.pp
+ (VHT.find env iid))
env ()
-let rm_edge_aux knp rnode env aid bid k =
- rm_edge_k env aid bid k;
+let rm_edge_aux env aid bid iid =
+ rm_edge env aid bid iid;
if Debug.test_flag DG.diffgraph_opt then
DG.pp_dot_diffgraph
~msg:
(Fmt.str
"_merge_neighbours %a -> %a\\n rm_edge between %a and %a linked \
with %a"
- Node.pp rnode Node.pp knp (pp_nid env) aid (pp_nid env) bid Node.pp k)
+ (pp_eid env) aid (pp_eid env) bid (pp_eid env) aid (pp_eid env) bid
+ (pp_vid env) iid)
env ()
let merge_neigbours_aux env (kn, kid) (rn, rid) nid kk_opt kr_opt () =
match (kk_opt, kr_opt) with
- | Some k1, Some k2 ->
+ | Some iid1, Some iid2 ->
+ let ind1 = VHT.find env iid1 in
+ let ind2 = VHT.find env iid2 in
Debug.dprintf6 debug
"DiffGraph: _merge_neigbours_aux: iter1: found the neighbour %a \
through %a and %a"
- (pp_nid env) nid Node.pp k1 Node.pp k2;
+ (pp_eid env) nid (pp_vid env) iid1 (pp_vid env) iid2;
(* if a node X is a neighbour of both A and B through the edges
- k1 and k2 (resp.) then (k1 = k2) must be set to true, and
- only the k1 edge should be kept. *)
- if not (Egraph.is_equal env k1 k2) then (
- let nidn = NHT.find env nid in
+ ind1 and ind2 (resp.) then (ind1 = ind2) must be set to true, and
+ only the ind1 edge should be kept. *)
+ if not (Egraph.is_equal env ind1 ind2) then (
+ let nidn = EHT.find env nid in
let ind_gty, val_gty = array_gty_args (get_node_ty env nidn) in
- let eq1 = mk_eq env k1 k2 ind_gty in
+ let eq1 = mk_eq env ind1 ind2 ind_gty in
let eq2 = mk_eq env kn nidn (Ground.Ty.array ind_gty val_gty) in
let disj = mk_or env eq1 eq2 in
Egraph.register env disj;
@@ -360,71 +450,111 @@ let merge_neigbours_aux env (kn, kid) (rn, rid) nid kk_opt kr_opt () =
]);
}
else Boolean.set_true env disj);
- rm_edge_aux kn rn env nid rid k2
- | None, Some k ->
+ rm_edge_aux env nid rid iid2
+ | None, Some iid ->
Debug.dprintf4 debug
"DiffGraph: _merge_neigbours_aux: iter2: found the neighbour %a \
through %a"
- (pp_nid env) nid Node.pp k;
- rm_edge_aux kn rn env nid rid k;
- add_edge_aux kn rn env nid kid k
+ (pp_eid env) nid (pp_vid env) iid;
+ rm_edge_aux env nid rid iid;
+ add_edge_aux kn rn env nid kid iid
| _ -> ()
let merge_neighbours env (kn, kid) (rn, rid) b =
Debug.dprintf5 debug "DiffGraph: _merge_neighbours %b [kn=%a; rn=%a]" b
- (pp_nid env) kid (pp_nid env) rid;
+ (pp_eid env) kid (pp_eid 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 (DG.find_opt env kid, DG.find_opt env rid) with
| Some (_, knm), Some (_, rnm) ->
- DInt.M.fold2_union
- (merge_neigbours_aux env (kn, kid) (rn, rid))
- (DInt.M.remove rid knm) (DInt.M.remove kid rnm) ();
+ let m1 = DInt.M.remove rid knm in
+ let m2 = DInt.M.remove kid rnm in
+ DInt.M.fold2_union (merge_neigbours_aux env (kn, kid) (rn, rid)) m1 m2 ();
(try
match DInt.M.find_opt rid knm with
| None -> ()
- | Some k -> rm_edge_aux kn rn env kid rid k
+ | Some iid -> rm_edge_aux env kid rid iid
with Not_a_neighbour _ -> ());
DG.remove env rid;
if Debug.test_flag DG.diffgraph_opt then
DG.pp_dot_diffgraph
~msg:
(Fmt.str "_merge_neighbours %b | %a | %a\\n remove %a" b
- (pp_nid env) rid (pp_nid env) kid Node.pp rn)
+ (pp_eid env) rid (pp_eid env) kid (pp_eid env) rid)
env ()
| None, Some (_, rnm) ->
let rnm = DInt.M.remove kid rnm in
DInt.M.iter
- (fun nid k ->
+ (fun nid iid ->
Debug.dprintf4 debug
"DiffGraph: _merge_neighbours: iter3: found the neighbour %a \
through %a"
- (pp_nid env) nid Node.pp k;
- rm_edge_aux kn rn env nid rid k;
- add_edge_aux kn rn env nid kid k)
+ (pp_eid env) nid (pp_vid env) iid;
+ rm_edge_aux env nid rid iid;
+ add_edge_aux kn rn env nid kid iid)
rnm
| _ -> ());
if not b then (
- NHT.set env kid rn;
+ EHT.set env kid rn;
if Debug.test_flag DG.diffgraph_opt then
DG.pp_dot_diffgraph
~msg:
- (Fmt.str "_merge_neighbours %b | %a | %a\\n replace %d <- %a" b
- (pp_nid env) rid (pp_nid env) kid kid (pp_nid env) rid)
+ (Fmt.str "_merge_neighbours %b | %a | %a\\n replace %a <- %a" b
+ (pp_eid env) rid (pp_eid env) kid (pp_eid env) kid (pp_eid env) rid)
env ())
+let eq_arrays_norm env (kn, kid) (rn, rid) b =
+ Debug.dprintf4 debug "DiffGraph: eq_arrays_norm %a %a" (pp_eid env) kid
+ (pp_eid env) rid;
+ merge_neighbours env (kn, kid) (rn, rid) b;
+ if Debug.test_flag DG.diffgraph_opt then
+ DG.pp_dot_diffgraph
+ ~msg:(Fmt.str "eq_arrays_norm %a %a" (pp_eid env) kid (pp_eid env) rid)
+ env ()
+
+let eq_indices_norm env (_kn, kid) (rn, rid) b =
+ Debug.dprintf4 debug "DiffGraph: eq_indices_norm %a %a" (pp_eid env) kid
+ (pp_eid env) rid;
+ (match (Vertices.find_opt env kid, Vertices.find_opt env rid) with
+ | Some _, Some sr | None, Some sr ->
+ Vertex.S.iter
+ (fun (aid, bid) ->
+ rm_edge env aid bid rid;
+ add_edge env aid bid kid)
+ sr
+ | _ -> ());
+ VHT.remove env rid;
+ if not b then VHT.set env kid rn;
+ if Debug.test_flag DG.diffgraph_opt then
+ DG.pp_dot_diffgraph
+ ~msg:(Fmt.str "eq_indices_norm %a %a" (pp_eid env) kid (pp_eid env) rid)
+ env ()
+
+let update env a b k _v =
+ let aid = Id_dom.get_id env a in
+ let bid = Id_dom.get_id env b in
+ Debug.dprintf6 debug "DiffGraph.update: %a %a %a" (pp_eid env) aid
+ (pp_eid env) bid Node.pp k;
+ add_edge env aid bid (Index_Id_dom.get_id env k);
+ if Debug.test_flag DG.diffgraph_opt then
+ DG.pp_dot_diffgraph
+ ~msg:
+ (Fmt.str "DiffGraph.update: %a %a %a" (pp_eid env) aid (pp_eid env) bid
+ Node.pp k)
+ env ()
+
let get_neighbours env nid =
- let rec aux (k : Node.t) inp acc =
+ let rec aux (k : DInt.t) inp acc =
if DInt.S.mem inp acc then acc
else
let nacc = DInt.S.add inp acc in
match DG.find_opt env inp with
| None -> nacc
| Some (m, _) -> (
- match Node.M.find_opt k m with
+ match DInt.M.find_opt k m with
| None -> nacc
| Some s -> DInt.S.fold (aux k) s nacc)
in
match DG.find_opt env nid with
| None -> DInt.S.empty
- | Some (m, _) -> Node.M.fold (fun k -> DInt.S.fold (aux k)) m DInt.S.empty
+ | Some (m, _) -> DInt.M.fold (fun k -> DInt.S.fold (aux k)) m DInt.S.empty
diff --git a/colibri2/theories/array/DiffGraph.mli b/colibri2/theories/array/DiffGraph.mli
index b776f0f55..2d551184e 100644
--- a/colibri2/theories/array/DiffGraph.mli
+++ b/colibri2/theories/array/DiffGraph.mli
@@ -23,34 +23,22 @@ open Colibri2_core
open Colibri2_popop_lib
open Popop_stdlib
-module NHT : sig
- val set : Egraph.wt -> int -> Node.t -> unit
- val find : Egraph.wt -> int -> Node.t
- val find_opt : Egraph.wt -> int -> Node.t option
- val change : f:(Node.t option -> Node.t option) -> Egraph.wt -> int -> unit
- val remove : Egraph.wt -> int -> unit
-end
-
module DG : sig
- val set : Egraph.wt -> int -> DInt.S.t Node.M.t * Node.t DInt.M.t -> unit
-
val find_opt :
- Egraph.wt -> int -> (DInt.S.t Node.M.t * Node.t DInt.M.t) option
+ Egraph.wt -> int -> (DInt.S.t DInt.M.t * DInt.t DInt.M.t) option
+end
+
+module Id_dom : sig
+ val set_id : Egraph.wt -> Node.t -> unit
+ val get_id : Egraph.wt -> Node.t -> int
- val change :
- f:
- ((DInt.S.t Node.M.t * Node.t DInt.M.t) option ->
- (DInt.S.t Node.M.t * Node.t DInt.M.t) option) ->
+ val register_merge_hook :
Egraph.wt ->
- int ->
+ (Egraph.wt -> Node.t * int -> Node.t * int -> bool -> unit) ->
unit
-
- val remove : Egraph.wt -> int -> unit
- val diffgraph_opt : Colibri2_stdlib.Debug.flag
- val pp_dot_diffgraph : Egraph.wt -> ?msg:string -> unit -> unit
end
-module Id_dom : sig
+module Index_Id_dom : sig
val set_id : Egraph.wt -> Node.t -> unit
val get_id : Egraph.wt -> Node.t -> int
@@ -60,7 +48,7 @@ module Id_dom : sig
unit
end
-val pp_nid : Egraph.wt -> Format.formatter -> int -> unit
-val add_edge : Egraph.wt -> int -> int -> Node.t -> unit
-val merge_neighbours : Egraph.wt -> Node.t * int -> Node.t * int -> bool -> 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
+val update : Egraph.wt -> Node.t -> Node.t -> Node.t -> Node.t -> unit
val get_neighbours : Egraph.wt -> int -> DInt.S.t
diff --git a/colibri2/theories/array/SharingIsCaring.ml b/colibri2/theories/array/SharingIsCaring.ml
deleted file mode 100644
index d4cebc3ce..000000000
--- a/colibri2/theories/array/SharingIsCaring.ml
+++ /dev/null
@@ -1,49 +0,0 @@
-(*************************************************************************)
-(* 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). *)
-(*************************************************************************)
-
-open Common
-module NHT = DiffGraph.NHT
-module DG = DiffGraph.DG
-
-(* if _b is true then kn is the representative, otherwise, it's rid *)
-let eq_arrays_norm env (kn, kid) (rn, rid) b =
- Debug.dprintf4 debug "DiffGraph: eq_arrays_norm %a %a" (DiffGraph.pp_nid env)
- kid (DiffGraph.pp_nid env) rid;
- DiffGraph.merge_neighbours env (kn, kid) (rn, rid) b;
- if Debug.test_flag DG.diffgraph_opt then
- DG.pp_dot_diffgraph
- ~msg:
- (Fmt.str "eq_arrays_norm %a{%d} %a{%d} " Node.pp (NHT.find env kid) kid
- Node.pp (NHT.find env rid) rid)
- env ()
-
-let update_np_dp env a b k =
- let aid = DiffGraph.Id_dom.get_id env a in
- let bid = DiffGraph.Id_dom.get_id env b in
- Debug.dprintf6 debug "DiffGraph: update_np_dp %a %a %a" (DiffGraph.pp_nid env)
- aid (DiffGraph.pp_nid env) bid Node.pp k;
- DiffGraph.add_edge env aid bid k;
- if Debug.test_flag DG.diffgraph_opt then
- DG.pp_dot_diffgraph
- ~msg:
- (Fmt.str "update_np_dp %a %a %a" (DiffGraph.pp_nid env) aid
- (DiffGraph.pp_nid env) bid Node.pp k)
- env ()
diff --git a/colibri2/theories/array/SharingIsCaring.mli b/colibri2/theories/array/SharingIsCaring.mli
deleted file mode 100644
index c7bb7be51..000000000
--- a/colibri2/theories/array/SharingIsCaring.mli
+++ /dev/null
@@ -1,23 +0,0 @@
-(*************************************************************************)
-(* 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 update_np_dp : Egraph.wt -> Node.t -> Node.t -> Node.t -> unit
diff --git a/colibri2/theories/array/array.ml b/colibri2/theories/array/array.ml
index b12c5d297..212964210 100644
--- a/colibri2/theories/array/array.ml
+++ b/colibri2/theories/array/array.ml
@@ -24,21 +24,18 @@ open Colibri2_popop_lib
open Common
open Colibri2_theories_quantifiers
open GE_Array_DP
-open SharingIsCaring
(*
Command line options:
- "None": uses RW1(adown), RW2(aup), idx and extensionality
- GE_Array_DP:
- - "--array-res-ext": restricts the extrensionality rule using the foreign
- domain
- - "--array-res-aup": restricts the RW2 rule using the linearity domain
- - "--array-ext-comb": to support additional combinators
- (const, map, def_ind, def_val)
- - "--array-blast-rule": uses the blast rule when it suits
- - "--array-def-values": suppots the rules on the default values
- SharingIsCaring:
- - "--array-diff-graph": uses the diff graph
+ - "--array-res-ext": restricts the extrensionality rule using the foreign
+ domain
+ - "--array-res-aup": restricts the RW2 rule using the linearity domain
+ - "--array-ext-comb": to support additional combinators
+ (const, map, def_ind, def_val)
+ - "--array-blast-rule": uses the blast rule when it suits
+ - "--array-def-values": suppots the rules on the default values
+ - "--array-diff-graph": uses the diff graph
*)
let converter env (f : Ground.t) =
@@ -134,6 +131,7 @@ let converter env (f : Ground.t) =
add_array_gty env b ind_gty val_gty;
DiffGraph.Id_dom.set_id env a;
DiffGraph.Id_dom.set_id env b;
+ DiffGraph.Index_Id_dom.set_id env k;
(* update of the Linearity domain *)
if Options.get env restrict_aup then
Linearity_dom.upd_dom env fn (Linear b);
@@ -165,7 +163,7 @@ let converter env (f : Ground.t) =
let eqn = mk_eq env a b (Ground.Ty.array ind_gty val_gty) in
Egraph.register env eqn;
Boolean.set_true env eqn)
- else update_np_dp env a b k)
+ else DiffGraph.update env a b k v)
| {
app = { builtin = Builtin.Array_diff; _ };
args;
@@ -223,8 +221,9 @@ let init env =
Array_value.init_ty env;
Array_value.init_check env;
Ground.register_converter env converter;
- if Options.get env use_diff_graph then
- DiffGraph.Id_dom.register_merge_hook env eq_arrays_norm;
+ if Options.get env use_diff_graph then (
+ DiffGraph.Id_dom.register_merge_hook env DiffGraph.eq_arrays_norm;
+ DiffGraph.Index_Id_dom.register_merge_hook env DiffGraph.eq_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 576c4507e..e46769b79 100644
--- a/colibri2/theories/array/common.ml
+++ b/colibri2/theories/array/common.ml
@@ -338,13 +338,26 @@ let distinct_arrays_term a b =
let diff = Builtin.apply_array_diff a b in
Expr.Term.distinct [ mk_select_term a diff; mk_select_term b diff ]
+module type HTS = sig
+ 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
+end
+
module MkIHT (V : sig
type t
val pp : t Pp.pp
val name : string
-end) =
-struct
+end) : HTS with type t = V.t = struct
+ type t = V.t
+
let db = HT.create V.pp V.name
let set (env : Egraph.wt) = HT.set db env
let find (env : Egraph.wt) = HT.find db env
diff --git a/colibri2/theories/array/common.mli b/colibri2/theories/array/common.mli
index 1b17f37df..a4efe23ae 100644
--- a/colibri2/theories/array/common.mli
+++ b/colibri2/theories/array/common.mli
@@ -134,20 +134,24 @@ val mk_distinct_arrays :
val mk_array_const : 'a Egraph.t -> Node.t -> Ground.Ty.t -> Node.t
val distinct_arrays_term : Expr.term -> Expr.term -> Expr.term
+module type HTS = sig
+ 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
+end
+
module MkIHT (V : sig
type t
val pp : t Colibri2_popop_lib.Pp.pp
val name : string
-end) : sig
- val set : Egraph.wt -> int -> V.t -> unit
- val find : Egraph.wt -> int -> V.t
- val find_opt : Egraph.wt -> int -> V.t option
- val change : f:(V.t option -> V.t option) -> Egraph.wt -> int -> unit
- val remove : Egraph.wt -> int -> unit
- val iter : f:(int -> V.t -> unit) -> Egraph.wt -> unit
- val fold : (int -> V.t -> 'a -> 'a) -> Egraph.wt -> 'a -> 'a
-end
+end) : HTS with type t = V.t
module MkIdDom (_ : sig
val n1 : string
--
GitLab