From 13a4798fcd096610d0faad9d89ec1dc24c96ea71 Mon Sep 17 00:00:00 2001
From: hra687261 <hichem.ait-el-hara@ocamlpro.com>
Date: Tue, 3 Jan 2023 15:26:19 +0100
Subject: [PATCH] [Array] DiffGraph and foreign_dom inetroperation In addition,
added interface files and headers
---
Makefile | 4 +-
.../solve/smt_array/{sat => errors}/eq.txt | 0
.../tests/solve/smt_array/errors/ite_1.txt | 15 +
.../tests/solve/smt_array/errors/ite_2.txt | 13 +
.../tests/solve/smt_array/errors/notes.txt | 4 +
colibri2/theories/LRA/LRA_build.mli | 20 ++
colibri2/theories/array/DiffGraph.ml | 68 ++++
colibri2/theories/array/DiffGraph.mli | 49 +++
colibri2/theories/array/GE_Array_DP.ml | 339 ++++++++++++------
colibri2/theories/array/GE_Array_DP.mli | 23 ++
colibri2/theories/array/SharingIsCaring.ml | 83 ++---
colibri2/theories/array/SharingIsCaring.mli | 23 ++
colibri2/theories/array/common.ml | 141 +++++---
colibri2/theories/array/common.mli | 104 ++++++
colibri2/theories/nseq/nseq.ml | 2 +-
colibri2/theories/nseq/nseq.mli | 1 +
16 files changed, 658 insertions(+), 231 deletions(-)
rename colibri2/tests/solve/smt_array/{sat => errors}/eq.txt (100%)
create mode 100644 colibri2/tests/solve/smt_array/errors/ite_1.txt
create mode 100644 colibri2/tests/solve/smt_array/errors/ite_2.txt
create mode 100644 colibri2/tests/solve/smt_array/errors/notes.txt
create mode 100644 colibri2/theories/array/DiffGraph.mli
create mode 100644 colibri2/theories/array/GE_Array_DP.mli
create mode 100644 colibri2/theories/array/SharingIsCaring.mli
create mode 100644 colibri2/theories/array/common.mli
diff --git a/Makefile b/Makefile
index 8b9998196..c5639cb0e 100644
--- a/Makefile
+++ b/Makefile
@@ -106,7 +106,9 @@ WITAN_FILES = colibri2/stdlib/std.ml colibri2/stdlib/std.mli \
colibri2/stdlib/keys_sig.ml colibri2/stdlib/comp_keys.ml \
colibri2/stdlib/comp_keys.mli colibri2/bin/options.ml
-OCAMLPRO_FILES = $(filter-out colibri2/theories/array/dune, $(wildcard colibri2/theories/array/*))
+OCAMLPRO_FILES = \
+ $(filter-out colibri2/theories/array/dune colibri2/theories/nseq/dune, \
+ $(wildcard colibri2/theories/array/* colibri2/theories/nseq/*))
COLIBRI2_FILES = Makefile $(filter-out $(WHY3_FILES) $(OCAML_FILES) \
diff --git a/colibri2/tests/solve/smt_array/sat/eq.txt b/colibri2/tests/solve/smt_array/errors/eq.txt
similarity index 100%
rename from colibri2/tests/solve/smt_array/sat/eq.txt
rename to colibri2/tests/solve/smt_array/errors/eq.txt
diff --git a/colibri2/tests/solve/smt_array/errors/ite_1.txt b/colibri2/tests/solve/smt_array/errors/ite_1.txt
new file mode 100644
index 000000000..651ff0c59
--- /dev/null
+++ b/colibri2/tests/solve/smt_array/errors/ite_1.txt
@@ -0,0 +1,15 @@
+(set-logic QF_AX)
+(declare-sort I 0)
+(declare-sort E 0)
+(declare-fun i () I)
+(declare-fun a () (Array I E))
+(declare-fun j () I)
+(declare-fun v1 () E)
+(declare-fun v2 () E)
+(assert (not
+ (ite
+ (= (store a j v1) (store (store a i v2) j v1))
+ (= i j)
+ true
+ )))
+(check-sat)
\ No newline at end of file
diff --git a/colibri2/tests/solve/smt_array/errors/ite_2.txt b/colibri2/tests/solve/smt_array/errors/ite_2.txt
new file mode 100644
index 000000000..b88968a72
--- /dev/null
+++ b/colibri2/tests/solve/smt_array/errors/ite_2.txt
@@ -0,0 +1,13 @@
+(set-logic ALL)
+(declare-fun i () Int)
+(declare-fun a () (Array Int Int))
+(declare-fun j () Int)
+(declare-fun v1 () Int)
+(declare-fun v2 () Int)
+(assert (not
+ (ite
+ (= (store a j v1) (store (store a i v2) j v1))
+ (= i j)
+ true
+ )))
+(check-sat)
\ No newline at end of file
diff --git a/colibri2/tests/solve/smt_array/errors/notes.txt b/colibri2/tests/solve/smt_array/errors/notes.txt
new file mode 100644
index 000000000..16453a420
--- /dev/null
+++ b/colibri2/tests/solve/smt_array/errors/notes.txt
@@ -0,0 +1,4 @@
+
+- eq.txt: timeout
+- ite_1.txt: unsound (--array-res-ext)
+- ite_2.txt: timeout (--array-res-ext)
diff --git a/colibri2/theories/LRA/LRA_build.mli b/colibri2/theories/LRA/LRA_build.mli
index f182f5b1e..c6f5c216d 100644
--- a/colibri2/theories/LRA/LRA_build.mli
+++ b/colibri2/theories/LRA/LRA_build.mli
@@ -1,3 +1,23 @@
+(*************************************************************************)
+(* This file is part of Colibri2. *)
+(* *)
+(* Copyright (C) 2014-2021 *)
+(* CEA (Commissariat à l'énergie atomique et aux énergies *)
+(* alternatives) *)
+(* *)
+(* 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). *)
+(*************************************************************************)
+
module LastEffort : sig
val add' : _ Egraph.t -> A.t -> Node.t -> A.t -> Node.t -> Node.t
val add : _ Egraph.t -> Node.t -> Node.t -> Node.t
diff --git a/colibri2/theories/array/DiffGraph.ml b/colibri2/theories/array/DiffGraph.ml
index 1d16ea432..12247a6ba 100644
--- a/colibri2/theories/array/DiffGraph.ml
+++ b/colibri2/theories/array/DiffGraph.ml
@@ -1,6 +1,28 @@
+(*************************************************************************)
+(* 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 Colibri2_core
open Colibri2_popop_lib
open Popop_stdlib
+open Common
module NP = struct
module T = struct
@@ -28,4 +50,50 @@ module DG = struct
let remove (env : Egraph.wt) = HT.remove diff_graph env
end
+let mk_np id node = { id; node }
let get_neighbours env a = DG.find env a
+
+let rm_edge env { id; node } rnp k =
+ Debug.dprintf6 debug "DiffGraph: Removing the edge %a linking %a to %a"
+ Node.pp k Node.pp node Node.pp rnp.node;
+ DG.change env id ~f:(function
+ | None ->
+ failwith
+ (Fmt.str
+ "%a is supposed to be a neighbour of %a, it's neighbour map \
+ mustn't be empty"
+ Node.pp node Node.pp rnp.node)
+ | Some m -> (
+ match NP.M.find_opt rnp m with
+ | None ->
+ failwith
+ (Fmt.str "There is no edge from %a to the node %a." Node.pp node
+ Node.pp rnp.node)
+ | Some k' ->
+ assert (Egraph.is_equal env k k');
+ Some (NP.M.remove rnp m)))
+
+let add_neighbour env src dest k ind_ty =
+ Debug.dprintf6 debug "DiffGraph: adding %a as a neighbour to %a through %a"
+ Node.pp dest.node Node.pp src.node Node.pp k;
+ DG.change env src.id ~f:(function
+ | None -> Some (NP.M.singleton dest k)
+ | Some m -> (
+ match NP.M.find_opt dest m with
+ | Some k' ->
+ if Egraph.is_equal env k k' then Some m
+ else
+ (* if a and b are already neighbours and k and k' are not equal
+ then set (k = k') to true *)
+ let eqn = sem_to_node (mk_eq env k k' ind_ty) in
+ Egraph.register env eqn;
+ Boolean.set_true env eqn;
+ Some m
+ | None -> Some (NP.M.add dest k m)))
+
+let add_edge env a b k =
+ Debug.dprintf6 debug "DiffGraph: adding the edge %a between %a and %a" Node.pp
+ k Node.pp a.node Node.pp b.node;
+ let ind_ty, _ = array_gty_args (get_node_ty env a.node) in
+ add_neighbour env a b k ind_ty;
+ add_neighbour env b a k ind_ty
diff --git a/colibri2/theories/array/DiffGraph.mli b/colibri2/theories/array/DiffGraph.mli
new file mode 100644
index 000000000..928ead7c7
--- /dev/null
+++ b/colibri2/theories/array/DiffGraph.mli
@@ -0,0 +1,49 @@
+(*************************************************************************)
+(* 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). *)
+(*************************************************************************)
+
+include sig
+ module T : sig
+ type t = { id : int; node : Node.t }
+ end
+
+ module M : Colibri2_popop_lib.Map_intf.PMap with type key = T.t
+end
+
+type t = T.t = { id : int; node : Node.t }
+
+module DG : sig
+ module HT : sig
+ type 'a t = 'a Datastructure.Hashtbl(Colibri2_popop_lib.Popop_stdlib.DInt).t
+ end
+
+ val diff_graph : Node.t M.t HT.t
+ val find : Egraph.wt -> int -> Node.t M.t option
+
+ val change :
+ f:(Node.t M.t option -> Node.t M.t option) -> 'a Egraph.t -> int -> unit
+
+ val remove : Egraph.wt -> int -> unit
+end
+
+val mk_np : int -> Node.t -> t
+val get_neighbours : Egraph.wt -> int -> Node.t M.t option
+val rm_edge : 'a Egraph.t -> t -> t -> Node.t -> unit
+val add_edge : Egraph.wt -> t -> t -> Node.t -> unit
diff --git a/colibri2/theories/array/GE_Array_DP.ml b/colibri2/theories/array/GE_Array_DP.ml
index a11ff600b..214258a84 100644
--- a/colibri2/theories/array/GE_Array_DP.ml
+++ b/colibri2/theories/array/GE_Array_DP.ml
@@ -1,8 +1,31 @@
+(*************************************************************************)
+(* 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 Colibri2_core
open Colibri2_popop_lib
open Popop_stdlib
open Common
open Colibri2_theories_quantifiers
+module GHT = Datastructure.Hashtbl (Ground)
+module GTHT = Datastructure.Hashtbl (Ground.Ty)
let restrict_ext =
Options.register ~pp:Fmt.bool "Array.res-ext"
@@ -11,12 +34,12 @@ let restrict_ext =
& info [ "array-res-ext" ] ~doc:"Restrict the extensionality rule")
let restrict_aup =
- Options.register ~pp:Fmt.bool "Array.res-ext"
+ Options.register ~pp:Fmt.bool "Array.res-aup"
Cmdliner.Arg.(
value & flag & info [ "array-res-aup" ] ~doc:"Restrict the ⇑ rule")
let extended_comb =
- Options.register ~pp:Fmt.bool "Array.res-ext"
+ Options.register ~pp:Fmt.bool "Array.res-comb"
Cmdliner.Arg.(
value & flag & info [ "array-ext-comb" ] ~doc:"Extended combinators")
@@ -74,8 +97,8 @@ let distinct_term_node ~subst env ta tb =
(* ⇓: a ≡ b[i <- v], a[j] |> (i = j) \/ a[j] = b[j] *)
let adown_pattern, adown_run =
- let a = mk_store_term Terms.tb Terms.ti Terms.tv in
- let term = mk_select_term a Terms.tj in
+ let a = mk_store_term STV.tb STV.ti STV.tv in
+ let term = mk_select_term a 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;
@@ -84,10 +107,9 @@ let adown_pattern, adown_run =
convert ~subst env
(Expr.Term._or
[
- Expr.Term.eq Terms.ti Terms.tj;
- Expr.Term.eq
- (mk_select_term a Terms.tj)
- (mk_select_term Terms.tb Terms.tj);
+ 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;
@@ -98,13 +120,13 @@ let adown_pattern, adown_run =
(* ⇑: a ≡ b[i <- v], b[j] |> (i = j) \/ a[j] = b[j] *)
let aup_pattern, aup_run =
- let term = mk_store_term Terms.tb Terms.ti Terms.tv in
+ let term = mk_store_term STV.tb STV.ti STV.tv in
let aup_pattern = Pattern.of_term_exn ~subst:Ground.Subst.empty term in
let aup_run env subst =
let n = convert ~subst env term in
Egraph.register env n;
Debug.dprintf2 debug "Found aup1 with %a" Ground.Subst.pp subst;
- let term_bis = mk_select_term Terms.tb Terms.tj in
+ let term_bis = mk_select_term STV.tb STV.tj in
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
@@ -113,10 +135,10 @@ let aup_pattern, aup_run =
convert ~subst env
(Expr.Term._or
[
- Expr.Term.eq Terms.ti Terms.tj;
+ Expr.Term.eq STV.ti STV.tj;
Expr.Term.eq
- (mk_select_term term Terms.tj)
- (mk_select_term Terms.tb Terms.tj);
+ (mk_select_term term STV.tj)
+ (mk_select_term STV.tb STV.tj);
])
in
Egraph.register env v;
@@ -128,28 +150,28 @@ 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 =
- let term = mk_store_term Terms.tb Terms.ti Terms.tv in
+ 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 =
Debug.dprintf2 debug "Found raup1 with %a" Ground.Subst.pp subst;
let n = convert ~subst env term in
Egraph.register env n;
- let term_bis = mk_select_term Terms.tb Terms.tj in
+ let term_bis = mk_select_term STV.tb STV.tj in
let raup_pattern_bis = Pattern.of_term_exn ~subst term_bis in
let raup_run_bis env subst_bis =
Debug.dprintf2 debug "Found raup2 with %a" Ground.Subst.pp subst;
let subst = Ground.Subst.distinct_union subst_bis subst in
- let bn = convert ~subst env Terms.tb in
+ 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 Terms.ti Terms.tj;
+ Expr.Term.eq STV.ti STV.tj;
Expr.Term.eq
- (mk_select_term term Terms.tj)
- (mk_select_term Terms.tb Terms.tj);
+ (mk_select_term term STV.tj)
+ (mk_select_term STV.tb STV.tj);
])
in
Egraph.register env v;
@@ -162,80 +184,135 @@ let raup_pattern, raup_run =
(* K⇓: a = K(v), a[j] |> a[j] = v *)
let const_read_pattern, const_read_run =
- let term = mk_select_term (Builtin.apply_array_const Terms.tv) Terms.tj in
+ let term = mk_select_term (Builtin.apply_array_const STV.tv) STV.tj in
let const_read_pattern = Pattern.of_term_exn ~subst:Ground.Subst.empty term in
let const_read_run env subst =
Debug.dprintf2 debug "Found const_read with %a" Ground.Subst.pp subst;
- let v = convert ~subst env (Expr.Term.eq term Terms.tv) in
+ let v = convert ~subst env (Expr.Term.eq term STV.tv) in
Egraph.register env v;
Boolean.set_true env v
in
(const_read_pattern, const_read_run)
-let apply_res_ext_1 env s =
- let rec aux terms_acc tsubsts_acc vtnodes =
- match vtnodes with
- | (nvar, nterm, nnode) :: t ->
+let apply_res_ext_1_1_aux _env ind_gty val_gty l tyvt =
+ 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 nterm oterm :: acc)
+ (fun acc (oterm, _) -> distinct_arrays nterm oterm :: acc)
[] t
in
- aux (nterms @ terms_acc) ((nvar, nnode) :: tsubsts_acc) t
- | [] -> (terms_acc, tsubsts_acc)
+ List.rev_append nterms (aux t)
+ | [] -> []
in
- let l = Node.S.elements s in
- match l with
- | h :: t -> (
- (* TODO: fix *)
- match get_array_gty env h with
- | { app = { builtin = Expr.Array; _ }; args = [ ind_gty; val_gty ] } ->
- Debug.dprintf2 debug "Found unequal arrays (%a)" Node.S.pp s;
- let tyvt = Expr.Ty.array ind_ty val_ty in
- (* TODO: all the arrays are supposed to have the same type, right? *)
- let a0v = Expr.Term.Var.mk "a0" tyvt in
- let a0vt = Expr.Term.of_var a0v in
- let terms, var_term_node, _ =
- List.fold_left
- (fun (nterms, nsubsts, cnt) node ->
- let anv = Expr.Term.Var.mk (Format.sprintf "a%d" cnt) tyvt in
- let anvt = Expr.Term.of_var anv in
- ( distinct_arrays a0vt anvt :: nterms,
- (anv, anvt, node) :: nsubsts,
- cnt + 1 ))
- ([], [], 1) t
- in
- let terms, tsubsts = aux terms [ (a0v, h) ] var_term_node in
- let subst =
- mk_subst tsubsts [ (ind_ty_var, ind_gty); (val_ty_var, val_gty) ]
- in
- let n = convert ~subst env (Expr.Term._and terms) in
- Debug.dprintf2 debug "Application of the res-ext-1 rule on (%a)"
- Node.S.pp s;
- Egraph.register env n;
- Boolean.set_true env n
- | (exception Not_found) | _ -> ())
- | [] -> ()
+ 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
+ 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)
+
+let apply_res_ext_1_2_aux env ind_gty val_gty l tyvt =
+ 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 * DiffGraph.t) list) =
+ match tnl with
+ | (nterm, idn) :: t -> (
+ match DiffGraph.get_neighbours env idn.id with
+ | Some m ->
+ let nterms =
+ List.fold_left
+ (fun acc (oterm, _) ->
+ if DiffGraph.M.mem idn m then
+ distinct_arrays nterm oterm :: acc
+ else acc)
+ [] t
+ in
+ List.rev_append nterms (aux t)
+ | None -> 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, DiffGraph.mk_np (Id_dom.get_id env node) node) :: tns ))
+ (0, [], []) l
+ 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)
+
+(* (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)
+ | exception Not_An_Array -> ()
+ in
+ let apply_res_ext_1_1 = apply_res_ext_1 apply_res_ext_1_1_aux in
+ let apply_res_ext_1_2 = apply_res_ext_1 apply_res_ext_1_2_aux in
+ (apply_res_ext_1_1, apply_res_ext_1_2)
+
+(** given a new foreign array and a set of all the other foreign arrays,
+ applies res-ext-2 on the new foreign array and all the other foregin arrays
+ which are its neighbours in the DiffGraph *)
+let get_foreign_neighbours env a arr_set =
+ match DiffGraph.get_neighbours env (Id_dom.get_id env a) with
+ | Some m ->
+ Node.S.filter
+ (fun node -> DiffGraph.M.mem { id = Id_dom.get_id env node; node } m)
+ arr_set
+ | None -> Node.M.empty
-let apply_res_ext_2 env =
+(* 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
let apply_ext env a b =
let gtya, gtyb = array_gty_args (get_array_gty env a) in
let n =
convert
~subst:
(mk_subst
- [ (Terms.va, a); (Terms.vb, b) ]
- [ (ind_ty_var, gtya); (val_ty_var, gtyb) ])
+ [ (STV.va, a); (STV.vb, b) ]
+ [ (STV.ind_ty_var, gtya); (STV.val_ty_var, gtyb) ])
env
(Expr.Term._or
[
- Expr.Term.eq Terms.ta Terms.tb;
+ Expr.Term.eq STV.ta STV.tb;
Expr.Term.distinct
[
- Expr.Term.Array.select Terms.ta
- (Builtin.apply_array_diff Terms.ta Terms.tb);
- Expr.Term.Array.select Terms.tb
- (Builtin.apply_array_diff Terms.ta Terms.tb);
+ Expr.Term.Array.select STV.ta
+ (Builtin.apply_array_diff STV.ta STV.tb);
+ Expr.Term.Array.select STV.tb
+ (Builtin.apply_array_diff STV.ta STV.tb);
];
])
in
@@ -244,35 +321,56 @@ let apply_res_ext_2 env =
Egraph.register env n;
Boolean.set_true env n
in
- let foreign_array_db = GTHT.create Node.S.pp "foreign_array_db" in
- fun (aty : Ground.Ty.t) a ->
- Debug.dprintf2 debug "Application of the res-ext-2 rule on %a" Node.pp a;
+ let apply_res_ext_2 f env aty a =
match aty with
- | { app = { builtin = Expr.Array; _ }; _ } ->
+ | Ground.Ty.{ app = { builtin = Expr.Array; _ }; _ } ->
GTHT.change
(fun opt ->
match opt with
- | Some arr_set ->
+ | Some fa_set ->
Debug.dprintf2 debug
"Found new foreign array (%a) on which to apply \
new_foreign_array the hook"
Node.pp a;
- Node.S.iter (apply_ext env a) arr_set;
- Some (Node.S.add a arr_set)
+ f env a fa_set;
+ Some (Node.S.add a fa_set)
| None -> Some (Node.S.singleton a))
foreign_array_db env aty
| _ -> ()
+ in
+ 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)
+ 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))
+ env aty a
+ in
+ (apply_res_ext_2_1, apply_res_ext_2_2)
+(** applied the res-ext rule only on neighbours in the diff-graphs *)
let init env =
(* extáµ£ (restricted extensionality):
- - (a = b) ≡ false |> (a = b) ⋠(a[k] ≠b[k])
+ - (a = b) ≡ false |> (a[k] ≠b[k])
- a, b, {a,b} ⊆ foreign |> (a = b) ⋠(a[k] ≠b[k]) *)
- if Options.get env restrict_ext then (
- (* (a = b) ≡ false |> (a = b) ⋠(a[k] ≠b[k]) *)
- (* Are a and b always of the same type? *)
- Equality.register_hook_new_disequality env (apply_res_ext_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 env));
+ if Options.get env restrict_ext then
+ if Options.get env use_diff_graph then (
+ (* (a = b) ≡ false |> (a[k] ≠b[k]) (when a and b are neighbours) *)
+ Equality.register_hook_new_disequality env (apply_res_ext_1_2 env);
+ (* a, b, {a,b} ⊆ foreign |> (a = b) ⋠(a[k] ≠b[k])
+ (when a and b are neighbours) *)
+ 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));
let l = [ (adown_pattern, adown_run) ] in
let l =
if Options.get env restrict_aup then (raup_pattern, raup_run) :: l
@@ -293,11 +391,11 @@ let new_array =
Datastructure.Push.iter db env ~f:(fun f2 ->
let subst =
mk_subst
- [ (Terms.va, Ground.node f2); (Terms.vb, Ground.node f) ]
- [ (ind_ty_var, ind_gty); (val_ty_var, val_gty) ]
+ [ (STV.va, Ground.node f2); (STV.vb, Ground.node f) ]
+ [ (STV.ind_ty_var, ind_gty); (STV.val_ty_var, val_gty) ]
in
Debug.dprintf2 debug "Found ext with %a" Ground.Subst.pp subst;
- let n = distinct_term_node ~subst env Terms.ta Terms.tb in
+ let n = distinct_term_node ~subst env STV.ta STV.tb in
Egraph.register env n;
Boolean.set_true env n);
Datastructure.Push.push db env f);
@@ -306,13 +404,13 @@ let new_array =
Debug.dprintf0 debug "Application of the epsilon_delta rule";
let subst =
mk_subst
- [ (Terms.va, Ground.node f) ]
- [ (ind_ty_var, ind_gty); (val_ty_var, val_gty) ]
+ [ (STV.va, Ground.node f) ]
+ [ (STV.ind_ty_var, ind_gty); (STV.val_ty_var, val_gty) ]
in
let epsilon_delta_eq =
Expr.Term.eq
- (mk_select_term Terms.ta (Builtin.apply_array_def_index Terms.ta))
- (Builtin.apply_array_def_value Terms.ta)
+ (mk_select_term STV.ta (Builtin.apply_array_def_index STV.ta))
+ (Builtin.apply_array_def_value STV.ta)
in
let n = convert ~subst env epsilon_delta_eq in
Egraph.register env n;
@@ -322,16 +420,16 @@ let new_array =
let map_adowm map_term f_term bitl =
let map_read_pattern =
Pattern.of_term_exn ~subst:Ground.Subst.empty
- (mk_select_term map_term Terms.tj)
+ (mk_select_term map_term STV.tj)
in
let map_read_run env subst =
Debug.dprintf2 debug "Found array_map(f,b1, ..., bn)[j] with %a"
Ground.Subst.pp subst;
let term =
Expr.Term.eq
- (mk_select_term map_term Terms.tj)
+ (mk_select_term map_term STV.tj)
(Expr.Term.apply f_term []
- (List.map (fun bi -> mk_select_term bi Terms.tj) bitl))
+ (List.map (fun bi -> mk_select_term bi STV.tj) bitl))
in
let n = convert ~subst env term in
Egraph.register env n;
@@ -346,23 +444,26 @@ let apply_map_aup env index_n gt
let arg_nodes = List.tl argl in
let a_node = Ground.node gt in
let fvar =
- Expr.Term.Var.mk "f" (Expr.Ty.arrow (replicate f_arity alpha_ty) val_ty)
+ Expr.Term.Var.mk "f"
+ (Expr.Ty.arrow (replicate f_arity STV.alpha_ty) STV.val_ty)
in
let fterm = Expr.Term.of_var fvar in
let ty_subst =
[
- (ind_ty_var, bi_ind_ty); (alpha_ty_var, bi_val_ty); (val_ty_var, a_val_ty);
+ (STV.ind_ty_var, bi_ind_ty);
+ (STV.alpha_ty_var, bi_val_ty);
+ (STV.val_ty_var, a_val_ty);
]
in
- let t_subst = [ (Terms.vj, index_n); (fvar, f_node); (Terms.va, a_node) ] in
+ let t_subst = [ (STV.vj, index_n); (fvar, f_node); (STV.va, a_node) ] in
let _, bij_list, t_subst =
List.fold_left
(fun (n, t_acc, s_acc) node ->
- let biv = Expr.Term.Var.mk (Format.sprintf "b%n" n) array_ty_alpha in
+ let biv =
+ Expr.Term.Var.mk (Format.sprintf "b%n" n) STV.array_ty_alpha
+ in
let bit = Expr.Term.of_var biv in
- ( n - 1,
- Expr.Term.Array.select bit Terms.tj :: t_acc,
- (biv, node) :: s_acc ))
+ (n - 1, Expr.Term.Array.select bit STV.tj :: t_acc, (biv, node) :: s_acc))
(f_arity, [], t_subst) (List.rev arg_nodes)
in
let n =
@@ -370,7 +471,7 @@ let apply_map_aup env index_n gt
~subst:(mk_subst t_subst ty_subst)
env
(Expr.Term.eq
- (Expr.Term.Array.select Terms.ta Terms.tj)
+ (Expr.Term.Array.select STV.ta STV.tj)
(Expr.Term.apply fterm [] bij_list))
in
Egraph.register env n;
@@ -433,7 +534,7 @@ let map_def map_term f_term bitl =
let d_bil = List.map (fun bi -> Builtin.apply_array_def_value bi) bitl in
let term =
Expr.Term.eq
- (Builtin.apply_array_def_value Terms.ta)
+ (Builtin.apply_array_def_value STV.ta)
(Expr.Term.apply f_term [] d_bil)
in
let n = convert ~subst env term in
@@ -456,8 +557,8 @@ let new_map =
in
let new_map_db =
NM.create Fmt.nop "new_map_db" (fun env f_arity ->
- let b_ty = Expr.Ty.array ind_ty alpha_ty in
- let f_ty = Expr.Ty.arrow (replicate f_arity alpha_ty) val_ty in
+ let b_ty = Expr.Ty.array STV.ind_ty STV.alpha_ty in
+ let f_ty = Expr.Ty.arrow (replicate f_arity STV.alpha_ty) STV.val_ty in
let bitl = mk_tlist [] f_arity b_ty in
let f_var = Expr.Term.Var.mk "f" f_ty in
let f_term = Expr.Term.of_var f_var in
@@ -489,7 +590,9 @@ let get_gty_inhabitants (gty : Ground.Ty.t) =
let apply_blast_rule =
let mk_delta_fv ind_gty n =
Expr.Term.of_var
- (Expr.Term.Var.mk (Fmt.str "delta_%a_%d" Ground.Ty.pp ind_gty n) val_ty)
+ (Expr.Term.Var.mk
+ (Fmt.str "delta_%a_%d" Ground.Ty.pp ind_gty n)
+ STV.val_ty)
in
let mk_conjonction_node env array_node val_gty sigmas =
let vals, _ =
@@ -497,14 +600,14 @@ let apply_blast_rule =
(fun (acc, n) sigma ->
let term =
Expr.Term.eq
- (Expr.Term.Array.select Terms.ta sigma)
+ (Expr.Term.Array.select STV.ta sigma)
(mk_delta_fv val_gty n)
in
(term :: acc, n + 1))
([], 1) sigmas
in
convert
- ~subst:(mk_subst [ (Terms.va, array_node) ] [ (val_ty_var, val_gty) ])
+ ~subst:(mk_subst [ (STV.va, array_node) ] [ (STV.val_ty_var, val_gty) ])
env (Expr.Term._and vals)
in
fun env array_node (ind_gty : Ground.Ty.t) (val_gty : Ground.Ty.t) ->
@@ -575,10 +678,10 @@ let converter env (f : Ground.t) =
(* ð≠: v = a[i], i is not ð |> i ≠ð or blast *)
let subst =
mk_subst
- [ (Terms.va, a); (Terms.vi, i) ]
- [ (ind_ty_var, ind_gty); (val_ty_var, val_gty) ]
+ [ (STV.va, a); (STV.vi, i) ]
+ [ (STV.ind_ty_var, ind_gty); (STV.val_ty_var, val_gty) ]
in
- let eps_term = Builtin.apply_array_def_index Terms.ta in
+ let eps_term = Builtin.apply_array_def_index STV.ta in
let eps_node = convert ~subst env eps_term in
Egraph.register env eps_node;
if not (Egraph.is_equal env i eps_node) then (
@@ -589,7 +692,7 @@ let converter env (f : Ground.t) =
else
(* application of ð≠*)
let i_eps_neq_node =
- convert ~subst env (Expr.Term.neq eps_term Terms.ti)
+ convert ~subst env (Expr.Term.neq eps_term STV.ti)
in
Egraph.register env i_eps_neq_node;
Boolean.set_true env i_eps_neq_node))
@@ -611,13 +714,13 @@ let converter env (f : Ground.t) =
(* application of the `idx` rule *)
let subst =
mk_subst
- [ (Terms.va, a); (Terms.vk, k); (Terms.vv, v) ]
- [ (ind_ty_var, ind_gty); (val_ty_var, val_gty) ]
+ [ (STV.va, a); (STV.vk, k); (STV.vv, v) ]
+ [ (STV.ind_ty_var, ind_gty); (STV.val_ty_var, val_gty) ]
in
- let store_term = mk_store_term Terms.ta Terms.tk Terms.tv in
+ let store_term = mk_store_term STV.ta STV.tk STV.tv in
let rn =
convert ~subst env
- (Expr.Term.eq (mk_select_term store_term Terms.tk) Terms.tv)
+ (Expr.Term.eq (mk_select_term store_term STV.tk) STV.tv)
in
Egraph.register env rn;
Boolean.set_true env rn;
@@ -626,7 +729,7 @@ let converter env (f : Ground.t) =
let eq_term =
Expr.Term.eq
(Builtin.apply_array_def_value store_term)
- (Builtin.apply_array_def_value Terms.ta)
+ (Builtin.apply_array_def_value STV.ta)
in
let eq_node = convert ~subst env eq_term in
Egraph.register env eq_node;
@@ -655,14 +758,14 @@ let converter env (f : Ground.t) =
Egraph.register env v;
(* application of the `Kð›¿` rule *)
if Options.get env default_values then (
- let subst = mk_subst [ (Terms.vv, v) ] [ (val_ty_var, val_gty) ] in
+ let subst = mk_subst [ (STV.vv, v) ] [ (STV.val_ty_var, val_gty) ] in
(* TODO: make a separate array node and set it's type? *)
let eq_node =
convert ~subst env
(Expr.Term.eq
(Builtin.apply_array_def_value
- (Builtin.apply_array_const Terms.tv))
- Terms.tv)
+ (Builtin.apply_array_const STV.tv))
+ STV.tv)
in
Egraph.register env eq_node;
Boolean.set_true env eq_node)
diff --git a/colibri2/theories/array/GE_Array_DP.mli b/colibri2/theories/array/GE_Array_DP.mli
new file mode 100644
index 000000000..325a7d158
--- /dev/null
+++ b/colibri2/theories/array/GE_Array_DP.mli
@@ -0,0 +1,23 @@
+(*************************************************************************)
+(* 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 init : Egraph.wt -> unit
+val converter : Egraph.wt -> Ground.t -> unit
diff --git a/colibri2/theories/array/SharingIsCaring.ml b/colibri2/theories/array/SharingIsCaring.ml
index 5445f58d9..0fe087506 100644
--- a/colibri2/theories/array/SharingIsCaring.ml
+++ b/colibri2/theories/array/SharingIsCaring.ml
@@ -1,61 +1,30 @@
+(*************************************************************************)
+(* 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 Colibri2_core
open Colibri2_popop_lib
open Common
open DiffGraph
-let use_diff_graph =
- Options.register ~pp:Fmt.bool "Array.diff-graph"
- Cmdliner.Arg.(
- value & flag
- & info [ "array-diff-graph" ] ~doc:"Use the array's diff graph")
-
-let rm_edge env { id; node } rnp k =
- Debug.dprintf6 debug "DiffGraph: Removing the edge %a linking %a to %a"
- Node.pp k Node.pp node Node.pp rnp.node;
- DG.change env id ~f:(function
- | None ->
- failwith
- (Fmt.str
- "%a is supposed to be a neighbour of %a, it's neighbour map \
- mustn't be empty"
- Node.pp node Node.pp rnp.node)
- | Some m -> (
- match NP.M.find_opt rnp m with
- | None ->
- failwith
- (Fmt.str "There is no edge from %a to the node %a." Node.pp node
- Node.pp rnp.node)
- | Some k' ->
- assert (Egraph.is_equal env k k');
- Some (NP.M.remove rnp m)))
-
-let add_neighbour env src dest k ind_ty =
- Debug.dprintf6 debug "DiffGraph: adding %a as a neighbour to %a through %a"
- Node.pp dest.node Node.pp src.node Node.pp k;
- DG.change env src.id ~f:(function
- | None -> Some (NP.M.singleton dest k)
- | Some m -> (
- match NP.M.find_opt dest m with
- | Some k' ->
- if Egraph.is_equal env k k' then Some m
- else
- (* if a and b are already neighbours and k and k' are not equal
- then set (k = k') to true *)
- let eqn = sem_to_node (mk_eq env k k' ind_ty) in
- Egraph.register env eqn;
- Boolean.set_true env eqn;
- Some m
- | None -> Some (NP.M.add dest k m)))
-
-(** if (a = b[k <- _]) then the edge a--k--b is added to the graph. *)
-let add_edge env a b k =
- Debug.dprintf6 debug "DiffGraph: adding the edge %a between %a and %a" Node.pp
- k Node.pp a.node Node.pp b.node;
- let ind_ty, _ = array_gty_args (get_node_ty env a.node) in
- add_neighbour env a b k ind_ty;
- add_neighbour env b a k ind_ty
-
-let neighbours_union env knp rnp { id; node } kk_opt kr_opt acc =
+let merge_node_neighbours env knp rnp { id; node } kk_opt kr_opt acc =
match (kk_opt, kr_opt) with
| Some k1, Some k2 ->
(* if a node X is a neighbour of both A and B through the edges
@@ -67,12 +36,12 @@ let neighbours_union env knp rnp { id; node } kk_opt kr_opt acc =
Egraph.register env eqn;
Boolean.set_true env eqn);
rm_edge env { id; node } rnp k2;
- NP.M.add knp k1 acc
- | Some k, None -> NP.M.add knp k acc
+ M.add knp k1 acc
+ | Some k, None -> M.add knp k acc
| None, Some k ->
rm_edge env { id; node } rnp k;
add_edge env { id; node } knp k;
- NP.M.add knp k acc
+ M.add knp k acc
| None, None ->
failwith
(Fmt.str
@@ -97,7 +66,7 @@ let eq_arrays_norm env (a : t) (b : t) =
in
(* iterate over all the neighbours *)
let abns =
- NP.M.fold2_union (neighbours_union env knp rnp) knm rnm NP.M.empty
+ M.fold2_union (merge_node_neighbours env knp rnp) knm rnm M.empty
in
DG.remove env rnp.id;
DG.change env knp.id ~f:(function
diff --git a/colibri2/theories/array/SharingIsCaring.mli b/colibri2/theories/array/SharingIsCaring.mli
new file mode 100644
index 000000000..325a7d158
--- /dev/null
+++ b/colibri2/theories/array/SharingIsCaring.mli
@@ -0,0 +1,23 @@
+(*************************************************************************)
+(* 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 init : Egraph.wt -> unit
+val converter : Egraph.wt -> Ground.t -> unit
diff --git a/colibri2/theories/array/common.ml b/colibri2/theories/array/common.ml
index 29af59c27..2728f76cc 100644
--- a/colibri2/theories/array/common.ml
+++ b/colibri2/theories/array/common.ml
@@ -1,11 +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). *)
+(*************************************************************************)
+
open Colibri2_core
open Colibri2_popop_lib
open Popop_stdlib
-module NHT = Datastructure.Hashtbl (Node)
-module IHT = Datastructure.Hashtbl (DInt)
-module GHT = Datastructure.Hashtbl (Ground)
-module GTHT = Datastructure.Hashtbl (Ground.Ty)
+let use_diff_graph =
+ Options.register ~pp:Fmt.bool "Array.diff-graph"
+ Cmdliner.Arg.(
+ value & flag
+ & info [ "array-diff-graph" ] ~doc:"Use the array's diff graph")
let debug =
Debug.register_info_flag ~desc:"Debugging messages of the array theory"
@@ -15,22 +37,41 @@ let convert ~subst =
Colibri2_theories_quantifiers.Subst.convert ~subst_old:Ground.Subst.empty
~subst_new:subst
-let ind_ty_var = Expr.Ty.Var.mk "ind_ty"
-let val_ty_var = Expr.Ty.Var.mk "val_ty"
-let alpha_ty_var = Expr.Ty.Var.mk "alpha"
-let a_ty_var = Expr.Ty.Var.mk "a"
-let b_ty_var = Expr.Ty.Var.mk "b"
-let c_ty_var = Expr.Ty.Var.mk "c"
-let ind_ty = Expr.Ty.of_var ind_ty_var
-let val_ty = Expr.Ty.of_var val_ty_var
-let a_ty = Expr.Ty.of_var a_ty_var
-let b_ty = Expr.Ty.of_var b_ty_var
-let c_ty = Expr.Ty.of_var c_ty_var
-let alpha_ty = Expr.Ty.of_var alpha_ty_var
-let array_ty = Expr.Ty.array ind_ty val_ty
-let array_ty_ab = Expr.Ty.array a_ty b_ty
-let array_ty_ac = Expr.Ty.array a_ty c_ty
-let array_ty_alpha = Expr.Ty.array ind_ty alpha_ty
+module STV = struct
+ let ind_ty_var = Expr.Ty.Var.mk "ind_ty"
+ let val_ty_var = Expr.Ty.Var.mk "val_ty"
+ let alpha_ty_var = Expr.Ty.Var.mk "alpha"
+ let a_ty_var = Expr.Ty.Var.mk "a"
+ let b_ty_var = Expr.Ty.Var.mk "b"
+ let c_ty_var = Expr.Ty.Var.mk "c"
+ let ind_ty = Expr.Ty.of_var ind_ty_var
+ let val_ty = Expr.Ty.of_var val_ty_var
+ let a_ty = Expr.Ty.of_var a_ty_var
+ let b_ty = Expr.Ty.of_var b_ty_var
+ let c_ty = Expr.Ty.of_var c_ty_var
+ let alpha_ty = Expr.Ty.of_var alpha_ty_var
+ let array_ty = Expr.Ty.array ind_ty val_ty
+ let array_ty_ab = Expr.Ty.array a_ty b_ty
+ let array_ty_ac = Expr.Ty.array a_ty c_ty
+ let array_ty_alpha = Expr.Ty.array ind_ty alpha_ty
+ let term_of_var = Expr.Term.of_var
+ let mk_index_var name = Expr.Term.Var.mk name ind_ty
+ let mk_value_var name = Expr.Term.Var.mk name val_ty
+ let mk_array_var name = Expr.Term.Var.mk name array_ty
+ let vi = mk_index_var "i"
+ let vj = mk_index_var "j"
+ let vk = mk_index_var "k"
+ let vv = mk_value_var "v"
+ let ti = term_of_var vi
+ let tj = term_of_var vj
+ let tk = term_of_var vk
+ let tv = term_of_var vv
+ let va = mk_array_var "a"
+ let vb = mk_array_var "b"
+ let ta = term_of_var va
+ let tb = term_of_var vb
+end
+
let replicate n v = List.init n (fun _ -> v)
let mk_store_term = Expr.Term.Array.store
let mk_select_term = Expr.Term.Array.select
@@ -46,19 +87,22 @@ let array_gty_args : Ground.Ty.t -> Ground.Ty.t * Ground.Ty.t = function
(ind_gty, val_gty)
| ty -> failwith (Fmt.str "'%a' is not an array ground type!" Ground.Ty.pp ty)
-let node_tyl env n = Ground.Ty.S.elements (Ground.tys env n)
-
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)
+exception Not_An_Array
+
let get_array_gty env n =
- List.find
- (function
- | Ground.Ty.{ app = { builtin = Expr.Array; _ }; _ } -> true | _ -> false)
- (Ground.Ty.S.elements (Ground.tys env n))
+ try
+ List.find
+ (function
+ | Ground.Ty.{ app = { builtin = Expr.Array; _ }; _ } -> true
+ | _ -> false)
+ (Ground.Ty.S.elements (Ground.tys env n))
+ with Not_found -> raise Not_An_Array
let get_array_gty_args env n = array_gty_args (get_array_gty env n)
@@ -81,14 +125,15 @@ module Builtin = struct
let array_diff : Dolmen_std.Expr.term_cst =
Expr.Id.mk ~name:"colibri2_array_diff" ~builtin:Array_diff
(Dolmen_std.Path.global "colibri2_array_diff")
- (Expr.Ty.pi [ a_ty_var; b_ty_var ]
- (Expr.Ty.arrow [ array_ty_ab; array_ty_ab ] a_ty))
+ (Expr.Ty.pi
+ [ STV.a_ty_var; STV.b_ty_var ]
+ (Expr.Ty.arrow [ STV.array_ty_ab; STV.array_ty_ab ] STV.a_ty))
let array_const : Dolmen_std.Expr.term_cst =
Expr.Id.mk ~name:"colibri2_array_const" ~builtin:Array_const
(Dolmen_std.Path.global "colibri2_array_const")
- (Expr.Ty.pi [ b_ty_var ]
- (Expr.Ty.arrow [ b_ty ] (Expr.Ty.array ind_ty b_ty)))
+ (Expr.Ty.pi [ STV.b_ty_var ]
+ (Expr.Ty.arrow [ STV.b_ty ] (Expr.Ty.array STV.ind_ty STV.b_ty)))
let array_map : int -> Dolmen_std.Expr.term_cst =
let cache = DInt.H.create 13 in
@@ -98,8 +143,9 @@ module Builtin = struct
| exception Not_found ->
let ty =
Expr.Ty.arrow
- (Expr.Ty.arrow (replicate i b_ty) c_ty :: replicate i array_ty_ab)
- array_ty_ac
+ (Expr.Ty.arrow (replicate i STV.b_ty) STV.c_ty
+ :: replicate i STV.array_ty_ab)
+ STV.array_ty_ac
in
DInt.H.add cache i ty;
ty
@@ -107,17 +153,23 @@ module Builtin = struct
fun i ->
Expr.Id.mk ~name:"colibri2_array_map" ~builtin:Array_map
(Dolmen_std.Path.global "colibri2_array_map")
- (Expr.Ty.pi [ a_ty_var; b_ty_var; c_ty_var ] (get_ty i))
+ (Expr.Ty.pi
+ [ STV.a_ty_var; STV.b_ty_var; STV.c_ty_var ]
+ (get_ty i))
let array_default_index : Dolmen_std.Expr.term_cst =
Expr.Id.mk ~name:"colibri2_array_default_index" ~builtin:Array_default_index
(Dolmen_std.Path.global "colibri2_array_default_index")
- (Expr.Ty.pi [ a_ty_var; b_ty_var ] (Expr.Ty.arrow [ array_ty_ab ] a_ty))
+ (Expr.Ty.pi
+ [ STV.a_ty_var; STV.b_ty_var ]
+ (Expr.Ty.arrow [ STV.array_ty_ab ] STV.a_ty))
let array_default_value : Dolmen_std.Expr.term_cst =
Expr.Id.mk ~name:"colibri2_array_default_value" ~builtin:Array_default_value
(Dolmen_std.Path.global "colibri2_array_default_value")
- (Expr.Ty.pi [ a_ty_var; b_ty_var ] (Expr.Ty.arrow [ array_ty_ab ] b_ty))
+ (Expr.Ty.pi
+ [ STV.a_ty_var; STV.b_ty_var ]
+ (Expr.Ty.arrow [ STV.array_ty_ab ] STV.b_ty))
let apply_array_diff a b =
let ind_ty, val_ty = array_ty_args a.Expr.term_ty in
@@ -205,22 +257,3 @@ let distinct_arrays a b =
Expr.Term.distinct [ mk_select_term a diff; mk_select_term b diff ]
let sem_to_node s = Ground.node (Ground.index s)
-
-module Terms = struct
- let term_of_var = Expr.Term.of_var
- let mk_index_var name = Expr.Term.Var.mk name ind_ty
- let mk_value_var name = Expr.Term.Var.mk name val_ty
- let mk_array_var name = Expr.Term.Var.mk name array_ty
- let vi = mk_index_var "i"
- let vj = mk_index_var "j"
- let vk = mk_index_var "k"
- let vv = mk_value_var "v"
- let ti = term_of_var vi
- let tj = term_of_var vj
- let tk = term_of_var vk
- let tv = term_of_var vv
- let va = mk_array_var "a"
- let vb = mk_array_var "b"
- let ta = term_of_var va
- let tb = term_of_var vb
-end
diff --git a/colibri2/theories/array/common.mli b/colibri2/theories/array/common.mli
new file mode 100644
index 000000000..b1aaf85e7
--- /dev/null
+++ b/colibri2/theories/array/common.mli
@@ -0,0 +1,104 @@
+(*************************************************************************)
+(* 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 use_diff_graph : bool Options.t
+val debug : Debug.flag
+val convert : subst:Ground.Subst.t -> 'a Egraph.t -> Expr.term -> Node.t
+
+module STV : sig
+ val ind_ty_var : Dolmen_std.Expr.ty_var
+ val val_ty_var : Dolmen_std.Expr.ty_var
+ val alpha_ty_var : Dolmen_std.Expr.ty_var
+ val a_ty_var : Dolmen_std.Expr.ty_var
+ val b_ty_var : Dolmen_std.Expr.ty_var
+ val c_ty_var : Dolmen_std.Expr.ty_var
+ val ind_ty : Expr.ty
+ val val_ty : Expr.ty
+ val a_ty : Expr.ty
+ val b_ty : Expr.ty
+ val c_ty : Expr.ty
+ val alpha_ty : Expr.ty
+ val array_ty : Expr.ty
+ val array_ty_ab : Expr.ty
+ val array_ty_ac : Expr.ty
+ val array_ty_alpha : Expr.ty
+ val term_of_var : Dolmen_std.Expr.term_var -> Expr.term
+ val mk_index_var : string -> Dolmen_std.Expr.term_var
+ val mk_value_var : string -> Dolmen_std.Expr.term_var
+ val mk_array_var : string -> Dolmen_std.Expr.term_var
+ val vi : Dolmen_std.Expr.term_var
+ val vj : Dolmen_std.Expr.term_var
+ val vk : Dolmen_std.Expr.term_var
+ val vv : Dolmen_std.Expr.term_var
+ val ti : Expr.term
+ val tj : Expr.term
+ val tk : Expr.term
+ val tv : Expr.term
+ val va : Dolmen_std.Expr.term_var
+ val vb : Dolmen_std.Expr.term_var
+ val ta : Expr.term
+ val tb : Expr.term
+end
+
+val replicate : int -> 'a -> 'a list
+val mk_store_term : Expr.term -> Expr.term -> Expr.term -> Expr.term
+val mk_select_term : Expr.term -> Expr.term -> Expr.term
+
+val apply_cst :
+ Dolmen_std.Expr.term_cst -> Expr.ty list -> Expr.term list -> Expr.term
+
+val array_gty_args : Ground.Ty.t -> Ground.Ty.t * Ground.Ty.t
+val get_node_ty : 'a Egraph.t -> Node.t -> Ground.Ty.t
+
+exception Not_An_Array
+
+val get_array_gty : 'a Egraph.t -> Node.t -> Ground.Ty.t
+val get_array_gty_args : 'a Egraph.t -> Node.t -> Ground.Ty.t * Ground.Ty.t
+val add_array_gty : Egraph.wt -> Node.t -> Ground.Ty.t -> Ground.Ty.t -> unit
+
+module Builtin : sig
+ type 'a Builtin.t +=
+ | Array_diff
+ | Array_const
+ | Array_map
+ | Array_default_index
+ | Array_default_value
+
+ val array_diff : Dolmen_std.Expr.term_cst
+ val array_const : Dolmen_std.Expr.term_cst
+ val array_map : int -> Dolmen_std.Expr.term_cst
+ val array_default_index : Dolmen_std.Expr.term_cst
+ val array_default_value : Dolmen_std.Expr.term_cst
+ val apply_array_diff : Expr.term -> Expr.term -> Expr.term
+ val apply_array_const : Expr.term -> Expr.term
+ val apply_array_def_index : Expr.term -> Expr.term
+ val apply_array_def_value : Expr.term -> Expr.term
+ val apply_array_map : int -> Expr.term -> Expr.term list -> Expr.term
+end
+
+val mk_subst :
+ (Dolmen_std.Expr.term_var * Node.t) list ->
+ (Dolmen_std.Expr.ty_var * Ground.Ty.t) list ->
+ Ground.Subst.t
+
+val mk_eq : 'a Egraph.t -> Node.t -> Node.t -> Ground.Ty.t -> Ground.s
+val distinct_arrays : Expr.term -> Expr.term -> Expr.term
+val sem_to_node : Ground.s -> Node.t
diff --git a/colibri2/theories/nseq/nseq.ml b/colibri2/theories/nseq/nseq.ml
index 5c5c2f3d1..71dda86de 100644
--- a/colibri2/theories/nseq/nseq.ml
+++ b/colibri2/theories/nseq/nseq.ml
@@ -152,7 +152,7 @@ module Builtin = struct
in
Expr.add_builtins (fun env s ->
match s with
- | Dolmen_loop.Typer.T.Id { ns = Sort; name = Simple "seq" } ->
+ | Dolmen_loop.Typer.T.Id { ns = Sort; name = Simple "NSeq" } ->
ty_app1 env s nseq_ty_const
| Dolmen_loop.Typer.T.Id { ns = Term; name = Simple "nseq_first" } ->
app1 env s nseq_first
diff --git a/colibri2/theories/nseq/nseq.mli b/colibri2/theories/nseq/nseq.mli
index 4bf15b085..b04ecb6fc 100644
--- a/colibri2/theories/nseq/nseq.mli
+++ b/colibri2/theories/nseq/nseq.mli
@@ -18,3 +18,4 @@
(* See the GNU Lesser General Public License version 2.1 *)
(* for more details (enclosed in the file licenses/LGPLv2.1). *)
(*************************************************************************)
+
--
GitLab