From ce57d86b46be13d92e90180d1aedef30168d6d09 Mon Sep 17 00:00:00 2001
From: hra687261 <hichem.ait-el-hara@ocamlpro.com>
Date: Sun, 5 Feb 2023 13:47:52 +0100
Subject: [PATCH] [Array] Use Ground.apply instead of convert
---
colibri2/theories/array/GE_Array_DP.ml | 45 ++++++++-----------------
colibri2/theories/array/array.ml | 46 +++++++++-----------------
colibri2/theories/array/common.ml | 43 +++++++++++++++---------
colibri2/theories/array/common.mli | 20 ++++++++++-
4 files changed, 75 insertions(+), 79 deletions(-)
diff --git a/colibri2/theories/array/GE_Array_DP.ml b/colibri2/theories/array/GE_Array_DP.ml
index ab753e26f..d0d02e9f3 100644
--- a/colibri2/theories/array/GE_Array_DP.ml
+++ b/colibri2/theories/array/GE_Array_DP.ml
@@ -50,21 +50,6 @@ let check_gty_num_size =
GTHT.set gty_ns_db env gty (gty_size gty);
false
-let distinct_term_node ~subst env ta tb =
- let diff_term = Builtin.apply_array_diff ta tb in
- let diff_eq = Expr.Term.eq diff_term (Builtin.apply_array_diff tb ta) in
- let diff_eq_node = convert ~subst env diff_eq in
- Egraph.register env diff_eq_node;
- Boolean.set_true env diff_eq_node;
- convert ~subst env
- @@ Expr.Term._or
- [
- Expr.Term.eq ta tb;
- Expr.Term.neq
- (mk_select_term ta diff_term)
- (mk_select_term tb diff_term);
- ]
-
(* ⇓: a ≡ b[i <- v], a[j] |> (i = j) \/ a[j] = b[j] *)
let adown_pattern, adown_run =
let a = mk_store_term STV.tb STV.ti STV.tv in
@@ -331,30 +316,28 @@ let new_array =
(* Extensionality rule ext: a, b ⇒ (a = b) ⋠(a[k] ≠b[k]) *)
if not (Options.get env restrict_ext) then (
Datastructure.Push.iter db env ~f:(fun f2 ->
- let subst =
- mk_subst
- [ (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 STV.ta STV.tb in
+ 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);
Datastructure.Push.push db env f);
(* ðð›¿: a |> a[ð] = 𛿠*)
if Options.get env extended_comb then (
Debug.dprintf0 debug "Application of the epsilon_delta rule";
- let subst =
- mk_subst
- [ (STV.va, Ground.node f) ]
- [ (STV.ind_ty_var, ind_gty); (STV.val_ty_var, val_gty) ]
+ let a = Ground.node f in
+ let def_ind =
+ ground_apply env Builtin.array_default_index [ ind_gty; val_gty ] [ a ]
in
- let epsilon_delta_eq =
- Expr.Term.eq
- (mk_select_term STV.ta (Builtin.apply_array_def_index STV.ta))
- (Builtin.apply_array_def_value STV.ta)
+ let def_val =
+ ground_apply env Builtin.array_default_value [ ind_gty; val_gty ] [ a ]
in
- let n = convert ~subst env epsilon_delta_eq in
+ let select_n = mk_select env a def_ind ind_gty val_gty in
+ let n = mk_eq env select_n def_val (Ground.Ty.array ind_gty val_gty) in
Egraph.register env n;
Boolean.set_true env n)
diff --git a/colibri2/theories/array/array.ml b/colibri2/theories/array/array.ml
index 424fc810f..b12c5d297 100644
--- a/colibri2/theories/array/array.ml
+++ b/colibri2/theories/array/array.ml
@@ -101,13 +101,10 @@ let converter env (f : Ground.t) =
(* when a new read is encountered, check if map⇑ can be applied *)
Array_dom.add_read env a i;
(* ð≠: v = a[i], i is not ð |> i ≠ð or blast *)
- let subst =
- mk_subst
- [ (STV.va, a); (STV.vi, i) ]
- [ (STV.ind_ty_var, ind_gty); (STV.val_ty_var, val_gty) ]
+ let eps_node =
+ ground_apply env Builtin.array_default_index [ ind_gty; val_gty ]
+ [ a ]
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 (
let ind_gty, _ = array_gty_args ind_gty in
@@ -117,7 +114,7 @@ let converter env (f : Ground.t) =
else
(* application of ð≠*)
let i_eps_neq_node =
- convert ~subst env (Expr.Term.neq eps_term STV.ti)
+ mk_neq env eps_node i (Ground.Ty.array ind_gty val_gty)
in
Egraph.register env i_eps_neq_node;
Boolean.set_true env i_eps_neq_node))
@@ -141,26 +138,14 @@ let converter env (f : Ground.t) =
if Options.get env restrict_aup then
Linearity_dom.upd_dom env fn (Linear b);
(* application of the `idx` rule *)
- let subst =
- mk_subst
- [ (STV.va, b); (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 STV.ta STV.tk STV.tv in
- let rn =
- convert ~subst env
- (Expr.Term.eq (mk_select_term store_term STV.tk) STV.tv)
- in
+ let agty = Ground.Ty.array val_gty ind_gty in
+ let store_n = mk_store env b k v ind_gty val_gty in
+ let rn = mk_eq env (mk_select env store_n k ind_gty val_gty) v agty in
Egraph.register env rn;
Boolean.set_true env rn;
(* application of the `Uð›¿` rule *)
if Options.get env default_values then (
- let eq_term =
- Expr.Term.eq
- (Builtin.apply_array_def_value store_term)
- (Builtin.apply_array_def_value STV.ta)
- in
- let eq_node = convert ~subst env eq_term in
+ let eq_node = mk_eq env store_n b agty in
Egraph.register env eq_node;
Boolean.set_true env eq_node);
if Options.get env use_diff_graph then (
@@ -198,7 +183,7 @@ let converter env (f : Ground.t) =
| {
app = { builtin = Builtin.Array_const; _ };
args;
- tyargs = [ val_gty ];
+ tyargs = [ ind_gty; val_gty ];
_;
} ->
Array_value.propagate_value env f;
@@ -206,15 +191,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 [ (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 STV.tv))
- STV.tv)
+ let const_n = mk_array_const env v val_gty in
+ let defv_n =
+ ground_apply env Builtin.array_default_value
+ [ Ground.Ty.array ind_gty val_gty ]
+ [ const_n ]
in
+ let eq_node = mk_eq env defv_n v val_gty in
Egraph.register env eq_node;
Boolean.set_true env eq_node)
| {
diff --git a/colibri2/theories/array/common.ml b/colibri2/theories/array/common.ml
index 137645ffc..d7f95f7aa 100644
--- a/colibri2/theories/array/common.ml
+++ b/colibri2/theories/array/common.ml
@@ -289,29 +289,33 @@ let mk_subst term_l ty_l =
Ground.Subst.
{ term = Expr.Term.Var.M.of_list term_l; ty = Expr.Ty.Var.M.of_list ty_l }
-let mk_or env a b =
- sem_to_node
- (Ground.apply env Expr.Term.Const.or_ [] (IArray.of_list [ a; b ]))
+let ground_apply env cstr tyl nl =
+ sem_to_node (Ground.apply env cstr tyl (IArray.of_list nl))
-let mk_eq env a b gty =
- sem_to_node
- (Ground.apply env Expr.Term.Const.eq [ gty ] (IArray.of_list [ a; b ]))
+let mk_or env a b = ground_apply env Expr.Term.Const.or_ [] [ a; b ]
+let mk_eq env a b gty = ground_apply env Expr.Term.Const.eq [ gty ] [ a; b ]
+let mk_neq env a b gty = ground_apply env Expr.Term.Const.neq [ gty ] [ a; b ]
let mk_distinct env l gty =
- sem_to_node
- (Ground.apply env
- (Expr.Term.Const.distinct (List.length l))
- [ gty ] (IArray.of_list l))
+ ground_apply env (Expr.Term.Const.distinct (List.length l)) [ gty ] l
let mk_select env a k ind_gty val_gty =
- sem_to_node
- (Ground.apply env Expr.Term.Const.Array.select [ ind_gty; val_gty ]
- (IArray.of_list [ a; k ]))
+ ground_apply env Expr.Term.Const.Array.select [ ind_gty; val_gty ] [ a; k ]
+
+let mk_store env a k v ind_gty val_gty =
+ ground_apply env Expr.Term.Const.Array.store [ ind_gty; val_gty ] [ a; k; v ]
let mk_array_diff env a b ind_gty val_gty =
- sem_to_node
- (Ground.apply env Builtin.array_diff [ ind_gty; val_gty ]
- (IArray.of_list [ a; b ]))
+ let diff_ab =
+ ground_apply env Builtin.array_diff [ ind_gty; val_gty ] [ a; b ]
+ in
+ let diff_ba =
+ ground_apply env Builtin.array_diff [ ind_gty; val_gty ] [ b; a ]
+ in
+ let eq = mk_eq env diff_ab diff_ba (Ground.Ty.array ind_gty val_gty) in
+ Egraph.register env eq;
+ Boolean.set_true env eq;
+ diff_ab
let mk_distinct_arrays env a b ind_gty val_gty =
let diffn = mk_array_diff env a b ind_gty val_gty in
@@ -322,6 +326,13 @@ let mk_distinct_arrays env a b ind_gty val_gty =
]
(Ground.Ty.array ind_gty val_gty)
+let mk_array_const env v val_gty =
+ let wc_ty =
+ Ground.Ty.convert Ground.Subst.empty.ty
+ (Expr.Ty.of_var (Expr.Ty.Var.wildcard ()))
+ in
+ ground_apply env Builtin.array_const [ wc_ty; val_gty ] [ v ]
+
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 ]
diff --git a/colibri2/theories/array/common.mli b/colibri2/theories/array/common.mli
index 01c50eb83..1517008ce 100644
--- a/colibri2/theories/array/common.mli
+++ b/colibri2/theories/array/common.mli
@@ -105,13 +105,31 @@ val mk_subst :
(Dolmen_std.Expr.ty_var * Ground.Ty.t) list ->
Ground.Subst.t
+val ground_apply :
+ Egraph.wt ->
+ Dolmen_std.Expr.term_cst ->
+ Ground.Ty.t list ->
+ Node.t list ->
+ Node.t
+
val mk_or : 'a Egraph.t -> Node.t -> Node.t -> Node.t
val mk_eq : 'a Egraph.t -> Node.t -> Node.t -> Ground.Ty.t -> Node.t
+val mk_neq : 'a Egraph.t -> Node.t -> Node.t -> Ground.Ty.t -> Node.t
+
+val mk_store :
+ 'a Egraph.t ->
+ Node.t ->
+ Node.t ->
+ Node.t ->
+ Ground.Ty.t ->
+ Ground.Ty.t ->
+ Node.t
val mk_select :
'a Egraph.t -> Node.t -> Node.t -> Ground.Ty.t -> Ground.Ty.t -> Node.t
val mk_distinct_arrays :
- 'a Egraph.t -> Node.t -> Node.t -> Ground.Ty.t -> Ground.Ty.t -> Node.t
+ Egraph.wt -> Node.t -> Node.t -> Ground.Ty.t -> Ground.Ty.t -> Node.t
+val mk_array_const : 'a Egraph.t -> Node.t -> Ground.Ty.t -> Node.t
val distinct_arrays_term : Expr.term -> Expr.term -> Expr.term
--
GitLab