diff --git a/colibri2/core/colibri2_core.mli b/colibri2/core/colibri2_core.mli
index b3cca4eec2d3270d4ba7723b6a2fe7350dd1cb1e..54edf8848d5b3eb8f632d7044fa6bf95b1aab817 100644
--- a/colibri2/core/colibri2_core.mli
+++ b/colibri2/core/colibri2_core.mli
@@ -769,6 +769,9 @@ module Datastructure : sig
val change : ('a option -> 'a option) -> 'a t -> _ Egraph.t -> key -> unit
val iter : f:(key -> 'a -> unit) -> 'a t -> _ Egraph.t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> _ Egraph.t -> 'b -> 'b
+
+ val filter_map_inplace :
+ (key -> 'a -> 'a option) -> 'a t -> _ Egraph.t -> unit
end
module Hashtbl (S : Colibri2_popop_lib.Popop_stdlib.Datatype) :
diff --git a/colibri2/core/datastructure.ml b/colibri2/core/datastructure.ml
index cdddee3d52d867b3129b547b3f5cefa81bb0d478..155a9298f898fe4f42558b4964d106989dad7a16 100644
--- a/colibri2/core/datastructure.ml
+++ b/colibri2/core/datastructure.ml
@@ -32,6 +32,7 @@ module type Sig = sig
val change : ('a option -> 'a option) -> 'a t -> _ Egraph.t -> key -> unit
val iter : f:(key -> 'a -> unit) -> 'a t -> _ Egraph.t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> _ Egraph.t -> 'b -> 'b
+ val filter_map_inplace: (key -> 'a -> 'a option) -> 'a t -> _ Egraph.t -> unit
end
module Hashtbl(S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Sig with type key := S.t = struct
@@ -112,6 +113,13 @@ module Hashtbl(S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Sig with type key :
| Some r -> f k r acc
) h acc
+ let filter_map_inplace (f : S.t -> 'a -> 'a option)
+ (t : 'a option Context.Ref.t S.H.t Env.Unsaved.t) (d : _ Egraph.t) =
+ let h = Egraph.get_unsaved_env d t in
+ S.H.iter
+ (fun k _ -> change (function Some v -> f k v | None -> None) t d k)
+ h
+
end
module type Sig2 = sig
diff --git a/colibri2/core/datastructure.mli b/colibri2/core/datastructure.mli
index 0f7320de07c6b1497af4a4742eddca5ee6c025bb..323a3e53dab8c204832731f9ec00cf65ab8a00fa 100644
--- a/colibri2/core/datastructure.mli
+++ b/colibri2/core/datastructure.mli
@@ -34,6 +34,7 @@ module type Sig = sig
val change : ('a option -> 'a option) -> 'a t -> _ Egraph.t -> key -> unit
val iter : f:(key -> 'a -> unit) -> 'a t -> _ Egraph.t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> _ Egraph.t -> 'b -> 'b
+ val filter_map_inplace: (key -> 'a -> 'a option) -> 'a t -> _ Egraph.t -> unit
end
module Hashtbl (S:Colibri2_popop_lib.Popop_stdlib.Datatype) : Sig with type key := S.t
diff --git a/colibri2/theories/array/Array_Id_dom.mli b/colibri2/theories/array/Array_Id_dom.mli
index 5c580537e680ae6ec1c16c4dfbb4362c1e0de068..438f2ca30fc18e2b273e75c03e0bf2f4bbc8f44c 100644
--- a/colibri2/theories/array/Array_Id_dom.mli
+++ b/colibri2/theories/array/Array_Id_dom.mli
@@ -19,13 +19,4 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-val register_merge_hook :
- Egraph.wt ->
- (Egraph.wt -> Node.t * int -> Node.t * int -> bool -> unit) ->
- unit
-
-val register_new_id_hook :
- Egraph.wt -> (Egraph.wt -> int -> Node.t -> unit) -> unit
-
-val set_id : Egraph.wt -> Node.t -> unit
-val get_id : Egraph.wt -> Node.t -> int
+include Common.IdDomSig
diff --git a/colibri2/theories/array/Index_Id_dom.mli b/colibri2/theories/array/Index_Id_dom.mli
index 5c580537e680ae6ec1c16c4dfbb4362c1e0de068..438f2ca30fc18e2b273e75c03e0bf2f4bbc8f44c 100644
--- a/colibri2/theories/array/Index_Id_dom.mli
+++ b/colibri2/theories/array/Index_Id_dom.mli
@@ -19,13 +19,4 @@
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
-val register_merge_hook :
- Egraph.wt ->
- (Egraph.wt -> Node.t * int -> Node.t * int -> bool -> unit) ->
- unit
-
-val register_new_id_hook :
- Egraph.wt -> (Egraph.wt -> int -> Node.t -> unit) -> unit
-
-val set_id : Egraph.wt -> Node.t -> unit
-val get_id : Egraph.wt -> Node.t -> int
+include Common.IdDomSig
diff --git a/colibri2/theories/array/RWRules.ml b/colibri2/theories/array/RWRules.ml
index a7a60b5054a68dc6d833c4ef78955cefee5b7354..ab7ced4ba272617b05a589fec742bce01d7af3fa 100644
--- a/colibri2/theories/array/RWRules.ml
+++ b/colibri2/theories/array/RWRules.ml
@@ -316,21 +316,21 @@ let new_array =
(* Extensionality rule ext: a, b ⇒ (a = b) ⋠(a[k] ≠b[k]) *)
let agty = Ground.Ty.array ind_gty val_gty in
(if not (Options.get env restrict_ext) then
- match GHT.find_opt db_gty env agty with
- | Some s ->
- Ground.S.iter
- (fun f2 ->
- let a = Ground.node f in
- let b = Ground.node f2 in
- let adist = mk_distinct_arrays env a b ind_gty val_gty in
- let aeq = mk_eq env a b (Ground.Ty.array ind_gty val_gty) in
- let n = mk_or env adist aeq in
- Debug.dprintf4 debug "Found ext with %a and %a" Ground.pp f2
- Ground.pp f;
- Egraph.register env n;
- Boolean.set_true env n)
- s
- | None -> ());
+ match GHT.find_opt db_gty env agty with
+ | Some s ->
+ Ground.S.iter
+ (fun f2 ->
+ let a = Ground.node f in
+ let b = Ground.node f2 in
+ let adist = mk_distinct_arrays env a b ind_gty val_gty in
+ let aeq = mk_eq env a b (Ground.Ty.array ind_gty val_gty) in
+ let n = mk_or env adist aeq in
+ Debug.dprintf4 debug "Found ext with %a and %a" Ground.pp f2
+ Ground.pp f;
+ Egraph.register env n;
+ Boolean.set_true env n)
+ s
+ | None -> ());
GHT.change
(function
| Some s -> Some (Ground.S.add f s)
diff --git a/colibri2/theories/array/WEGraph.ml b/colibri2/theories/array/WEGraph.ml
index e1a76711e284efdf1ecd91e7b192bc85ec2372a9..120ff94321549cddbd40b819e66031e781a8db60 100644
--- a/colibri2/theories/array/WEGraph.ml
+++ b/colibri2/theories/array/WEGraph.ml
@@ -38,6 +38,16 @@ module VHT = MkIHT (struct
let name = "wegraph_indices"
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
+
module Vertex = struct
let sort (a, b) = if DInt.compare a b <= 0 then (a, b) else (b, a)
@@ -157,17 +167,106 @@ module WEG = struct
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
+
+ let width_first_fold env curr ~f acc =
+ let rec aux env ?(seen = DInt.S.empty) ~curr f acc =
+ let tosee, nseen, nacc =
+ DInt.M.fold
+ (fun next next_ind (tosee, seen, acc) ->
+ if DInt.S.mem next seen then (tosee, seen, acc)
+ else
+ let b, nacc = f env ~curr ~next_ind ~next acc in
+ let nseen = DInt.S.add next seen in
+ if b then (DInt.S.add next tosee, nseen, nacc)
+ else (tosee, nseen, nacc))
+ (snd (find env curr))
+ (DInt.S.empty, DInt.S.add curr seen, acc)
+ in
+ DInt.S.fold
+ (fun curr (seen, acc) -> aux env ~seen ~curr f acc)
+ tosee (nseen, nacc)
+ in
+ snd (aux env ~curr f acc)
+
+ let breadth_first_fold env curr ~f acc =
+ let rec aux env ?(seen = DInt.S.empty) ~curr f acc =
+ DInt.M.fold
+ (fun next next_ind (seen, acc) ->
+ if DInt.S.mem next seen then (seen, acc)
+ else
+ let b, nacc = f env ~curr ~next_ind ~next acc in
+ let nseen = DInt.S.add next seen in
+ if b then aux env ~seen:nseen ~curr:next f nacc else (nseen, nacc))
+ (snd (find env curr))
+ (DInt.S.add curr seen, acc)
+ in
+ snd (aux env ~curr f acc)
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
+module KnownValues = struct
+ type t = { value : Node.t; propag : DInt.S.t; nopropag : DInt.S.t }
+ [@@deriving show]
-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
+ module HT = MkIHT (struct
+ type nonrec t = t DInt.M.t
+
+ let pp = DInt.M.pp pp
+ let name = "KnownValues.HT"
+ end)
+
+ let add env array_id ind_id value =
+ let rec aux env ?(seen = DInt.S.empty) array_id ind_id value =
+ if
+ match HT.find env array_id with
+ | exception Not_found -> true
+ | m -> (
+ match DInt.M.find ind_id m with
+ | exception Not_found -> true
+ | { value = v; _ } -> not (Egraph.is_equal env v value))
+ then (
+ let ind = VHT.find env ind_id in
+ let propag, nopropag, seen =
+ DInt.M.fold
+ (fun next next_ind (propag, nopropag, seen) ->
+ if DInt.S.mem next seen then (propag, nopropag, seen)
+ else if Equality.is_disequal env (VHT.find env next_ind) ind then
+ (DInt.S.add next propag, nopropag, DInt.S.add next seen)
+ else (propag, DInt.S.add next nopropag, DInt.S.add next seen))
+ (snd (WEG.find env array_id))
+ (DInt.S.empty, DInt.S.empty, DInt.S.add array_id seen)
+ in
+ HT.change env array_id ~f:(function
+ | None -> Some (DInt.M.singleton ind_id { value; propag; nopropag })
+ | Some m ->
+ Some
+ (DInt.M.change
+ (function
+ | None -> Some { value; propag; nopropag }
+ | Some { value = fvalue; propag = p1; nopropag = p2 } ->
+ let _, val_gty =
+ get_array_gty_args env (EHT.find env array_id)
+ in
+ let eq = mk_eq env value fvalue val_gty in
+ Egraph.register env eq;
+ Boolean.set_true env eq;
+ (* ? *)
+ let propag = DInt.S.union p1 propag in
+ let nopropag =
+ DInt.S.filter
+ (fun i -> not (DInt.S.mem i propag))
+ (DInt.S.union p2 nopropag)
+ in
+ Some { value; propag; nopropag })
+ ind_id m));
+ ();
+ DInt.S.fold
+ (fun a_id seen ->
+ aux env ~seen:(DInt.S.add a_id seen) a_id ind_id value)
+ propag seen)
+ else seen
+ in
+ ignore (aux env array_id ind_id value)
+end
let s_remove_opt s_opt v =
match s_opt with
@@ -321,9 +420,9 @@ let are_k_neibnours env aid bid iid =
match WEG.find_opt env aid with
| None -> false
| Some (_, m2) -> (
- match DInt.M.find_opt iid m2 with
+ match DInt.M.find_opt bid m2 with
| None -> false
- | Some bid' -> bid = bid')
+ | Some iid' -> iid = iid')
let add_edge env aid bid iid =
(* when adding a node dest as a neighbour to a node src, dest is also added
@@ -509,11 +608,10 @@ let update env a b ind _v =
let aid = Array_Id_dom.get_id env a in
let bid = Array_Id_dom.get_id env b in
let iid = Index_Id_dom.get_id env ind in
- Debug.dprintf9 debug "WEGraph.update: %a(%d) %a(%d) %a(%d)" Node.pp a aid
- Node.pp b bid Node.pp ind iid;
Debug.dprintf6 debug "WEGraph.update: %a %a %a" (pp_eid env) aid (pp_eid env)
bid (pp_vid env) iid;
add_edge env aid bid iid;
+ KnownValues.add env aid iid _v;
if Debug.test_flag WEG.wegraph_opt then
WEG.pp_dot_wegraph
~msg:
diff --git a/colibri2/theories/array/array.ml b/colibri2/theories/array/array.ml
index 486f7e4da2f325e88b1ded5fbbc33762b8838df4..c975e4fdf899386ec774bef75d53a16857d8fac4 100644
--- a/colibri2/theories/array/array.ml
+++ b/colibri2/theories/array/array.ml
@@ -74,6 +74,7 @@ let converter env (f : Ground.t) =
let gty = Ground.Ty.convert subst (List.nth arg_tys i) in
match gty with
| { app = { builtin = Expr.Array; _ }; _ } ->
+ Array_Id_dom.set_id env n;
Ground.add_ty env n gty;
Foreign_dom.set_dom env gty n IsForeign
| _ -> ())
@@ -91,9 +92,9 @@ let converter env (f : Ground.t) =
add_array_gty env a ind_gty val_gty;
Array_Id_dom.set_id env a;
(* update of the Foreign domain *)
- if Options.get env restrict_ext && ind_gty.app.builtin == Expr.Array then (
- Ground.add_ty env i ind_gty;
- Foreign_dom.set_dom env (Ground.Ty.array ind_gty val_gty) i IsForeign);
+ if Options.get env restrict_ext && ind_gty.app.builtin == Expr.Array then
+ (* id and ground type are set during registration *)
+ Foreign_dom.set_dom env (Ground.Ty.array ind_gty val_gty) i IsForeign;
if Options.get env extended_comb then (
(* when a new read is encountered, check if map⇑ can be applied *)
Array_dom.add_read env a i;
@@ -238,7 +239,6 @@ let init env =
Foreign_dom.register_hook_new_foreign_array env (apply_res_ext_2_2 env))
else (
(* (a = b) ≡ false |> (a[k] ≠b[k]) *)
- (* TODO: Are a and b always of the same type? *)
Equality.register_hook_new_disequality env (apply_res_ext_1_1 env);
(* a, b, {a,b} ⊆ foreign |> (a = b) ⋠(a[k] ≠b[k]) *)
Foreign_dom.register_hook_new_foreign_array env (apply_res_ext_2_1 env));
diff --git a/colibri2/theories/array/common.ml b/colibri2/theories/array/common.ml
index e08f6fe7dccf3e644cf2706097349c42bd0ca82e..b7575ec3d52e732ccff138a849934792043a6c4e 100644
--- a/colibri2/theories/array/common.ml
+++ b/colibri2/theories/array/common.ml
@@ -126,7 +126,6 @@ let array_gty_args : Ground.Ty.t -> Ground.Ty.t * Ground.Ty.t = function
| ty -> failwith (Fmt.str "'%a' is not an array ground type!" Ground.Ty.pp ty)
let get_node_ty env n =
- (* TODO: fix somehow *)
match Ground.Ty.S.elements (Ground.tys env n) with
| h :: _ -> h
| [] -> failwith (Fmt.str "The type of the node %a was not set" Node.pp n)
@@ -348,6 +347,7 @@ module type HTS = sig
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
end
module MkIHT (V : sig
@@ -366,14 +366,27 @@ end) : HTS with type t = V.t = struct
let remove (env : Egraph.wt) = HT.remove db env
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
+end
+
+module type IdDomSig = sig
+ val register_merge_hook :
+ Egraph.wt ->
+ (Egraph.wt -> Node.t * int -> Node.t * int -> bool -> unit) ->
+ unit
+
+ val register_new_id_hook :
+ Egraph.wt -> (Egraph.wt -> int -> Node.t -> unit) -> unit
+
+ val set_id : Egraph.wt -> Node.t -> unit
+ val get_id : Egraph.wt -> Node.t -> int
end
module MkIdDom (N : sig
val n1 : string
val n2 : string
val n3 : string
-end) =
-struct
+end) : IdDomSig = struct
let merge_hooks = Datastructure.Push.create Fmt.nop N.n1
let register_merge_hook env (f : Egraph.wt -> 'a -> 'a -> bool -> unit) =
@@ -424,28 +437,18 @@ struct
match Egraph.get_dom env D.key n with
| None ->
incr id_counter;
- Debug.dprintf1 debug "set_id:\n%s@."
- (Printexc.raw_backtrace_to_string @@ Printexc.get_callstack 1000);
Debug.dprintf4 debug "set_id(%s) of %a: none -> %d" N.n2 Node.pp n
!id_counter;
D.set_dom env n !id_counter;
Datastructure.Push.iter new_id_hooks env ~f:(fun new_id_hook ->
- Debug.dprintf4 debug "apply new_id_hooks(%s) on %d %a@." N.n2
- (Datastructure.Push.length new_id_hooks env)
- Node.pp n;
new_id_hook env !id_counter n)
- | Some id -> Debug.dprintf3 debug "set_id of %a: %d" Node.pp n id
+ | Some id -> Debug.dprintf4 debug "set_id(%s) of %a: %d" N.n2 Node.pp n id
in
let get_id env n =
- (* is this a good idea?
- TODO: Find out why it crashes occasionally with
- restricted extensionality *)
match Egraph.get_dom env D.key n with
| Some id -> id
| None ->
- Debug.dprintf3 debug "get_id(%s) of %a: No Id found!" N.n2 Node.pp n;
- set_id env n;
- !id_counter
+ failwith (Fmt.str "get_id(%s) of %a: No Id found!" N.n2 Node.pp n)
in
(set_id, get_id)
end
diff --git a/colibri2/theories/array/common.mli b/colibri2/theories/array/common.mli
index fe0f8e472647d496075284351805c57f6a9bcf7b..bd4609c9b44ae5008ab001affb877958ae2b79a1 100644
--- a/colibri2/theories/array/common.mli
+++ b/colibri2/theories/array/common.mli
@@ -144,6 +144,7 @@ module type HTS = sig
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
end
module MkIHT (V : sig
@@ -153,21 +154,21 @@ module MkIHT (V : sig
val name : string
end) : HTS with type t = V.t
-module MkIdDom (_ : sig
- val n1 : string
- val n2 : string
- val n3 : string
-end) : sig
+module type IdDomSig = sig
val register_merge_hook :
Egraph.wt ->
(Egraph.wt -> Node.t * int -> Node.t * int -> bool -> unit) ->
unit
- module D : Dom.DS with type t = int
-
val register_new_id_hook :
Egraph.wt -> (Egraph.wt -> int -> Node.t -> unit) -> unit
val set_id : Egraph.wt -> Node.t -> unit
val get_id : Egraph.wt -> Node.t -> int
end
+
+module MkIdDom (_ : sig
+ val n1 : string
+ val n2 : string
+ val n3 : string
+end) : IdDomSig