diff --git a/colibri2/theories/array/array.ml b/colibri2/theories/array/array.ml
index 3b8b623792daba8df9756fe08b90969fb16cc0a5..652f0682a91d5ff1efea513e9603784e768aecd7 100644
--- a/colibri2/theories/array/array.ml
+++ b/colibri2/theories/array/array.ml
@@ -22,6 +22,8 @@
open Colibri2_core
open Colibri2_popop_lib
+let restrict_ext = ref false
+let restrict_aup = ref false
let db = Datastructure.Push.create Ground.pp "Array.db"
let debug = Debug.register_info_flag ~desc:"For array theory" "Array"
let stats = Debug.register_stats_int "Array.rule"
@@ -33,6 +35,22 @@ let convert ~subst =
let int_ty = Expr.Ty.int
let array_ty = Expr.Ty.array int_ty int_ty
+(* Helper functions *)
+let is_array env n =
+ Ground.Ty.S.exists
+ (function { app = { builtin = Expr.Array; _ }; _ } -> true | _ -> false)
+ (Ground.tys env n)
+
+let is_foreign env n =
+ match Egraph.get_dom env Foreign_dom.key n with
+ | Some IsForeign -> true
+ | _ -> false
+
+let is_nonlinear env n =
+ match Egraph.get_dom env Linearity_dom.key n with
+ | Some NonLinear -> true
+ | _ -> false
+
(* Builtins *)
module Builtin = struct
type _ Expr.t += Arr_diff
@@ -139,12 +157,78 @@ module Theory = struct
in
(aup_pattern, aup_run)
+ (* extáµ£ (restricted extensionality):
+ - (a = b) ≡ false |> (a = b) ⋠(a[k] ≠b[k])
+ - a, b, {a,b} ⊆ foreign |> (a = b) ⋠(a[k] ≠b[k]) *)
+ let rext_pattern, rext_run =
+ let rext_pattern = Pattern.of_term_exn ~subst:Ground.Subst.empty ta in
+ let rext_run env subst =
+ Debug.dprintf2 debug "Found rext1 with %a" Ground.Subst.pp subst;
+ let an = convert ~subst env ta in
+ Egraph.register env an;
+ let rext_pattern_bis = Pattern.of_term_exn ~subst tb in
+ let rext_run_bis env subst_bis =
+ Debug.dprintf2 debug "Found rext2 with %a" Ground.Subst.pp subst;
+ let subst = Ground.Subst.distinct_union subst_bis subst in
+ let bn = convert ~subst env tb in
+ Egraph.register env bn;
+ let eq = convert ~subst env (Expr.Term.eq ta tb) in
+ let is_registered = Egraph.is_registered env eq in
+ Egraph.register env eq;
+ (* it can't be false if it is not registered? *)
+ let is_false = Boolean.is_false env eq in
+ if
+ (is_registered && is_false) || (is_foreign env an && is_foreign env bn)
+ then (
+ let v = convert ~subst env distinct_term in
+ Egraph.register env v;
+ Boolean.set_true env v)
+ in
+ InvertedPath.add_callback env rext_pattern_bis rext_run_bis
+ in
+ (rext_pattern, rext_run)
+
+ (* ⇑ᵣ: a ≡ b[i <- v], b[j], b ∈ non-linear |> (i = j) \/ a[j] = b[j] *)
+ let raup_pattern, raup_run =
+ let term = Expr.Term.store tb ti 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 = Expr.Term.select tb 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 tb in
+ if is_nonlinear env bn then (
+ let v =
+ convert ~subst env
+ (Expr.Term._or
+ [
+ Expr.Term.eq ti tj;
+ Expr.Term.eq (Expr.Term.select term tj)
+ (Expr.Term.select tb tj);
+ ])
+ in
+ Egraph.register env v;
+ Boolean.set_true env v)
+ in
+ InvertedPath.add_callback env raup_pattern_bis raup_run_bis
+ in
+ (raup_pattern, raup_run)
+
let init env =
- List.iter
- (fun (p, r) -> InvertedPath.add_callback env p r)
- [ (adown_pattern, adown_run); (aup_pattern, aup_run) ]
+ let l = [ (adown_pattern, adown_run) ] in
+ let l = if !restrict_ext then (rext_pattern, rext_run) :: l else l in
+ let l =
+ if !restrict_aup then (raup_pattern, raup_run) :: l
+ else (aup_pattern, aup_run) :: l
+ in
+ List.iter (fun (p, r) -> InvertedPath.add_callback env p r) l
- (* ext: a, b ⇒ (a = b) ⋠(a[k] ≠b[k]) *)
+ (* ext: a, b ⇒ (a = b) ⋠(a[k] ≠b[k]) *)
let new_array env f =
Datastructure.Push.iter db env ~f:(fun f2 ->
let subst =
@@ -166,18 +250,32 @@ end
let converter env (f : Ground.t) =
let s = Ground.sem f in
(match s.ty with
- | { app = { builtin = Expr.Array; _ }; _ } -> Theory.new_array env f
+ | { app = { builtin = Expr.Array; _ }; _ } when not !restrict_ext ->
+ (* Application of the extentionality rule *)
+ Theory.new_array env f
| _ -> ());
match s with
+ | { app = { builtin = Expr.Base; _ }; args; _ }
+ when IArray.is_empty args && !restrict_aup ->
+ (* Update of the restrict_aup domain *)
+ Linearity_dom.upd_dom env (Ground.node f) Empty
+ | { app = { builtin = Expr.Base; _ }; args; _ } when !restrict_ext ->
+ IArray.iter
+ ~f:(fun n -> if is_array env n then Foreign_dom.set_dom env n IsForeign)
+ args
| { app = { builtin = Expr.Select; _ }; args; _ } ->
let a, k = IArray.extract2_exn args in
Egraph.register env a;
- Egraph.register env k
+ Egraph.register env k;
+ if !restrict_ext && is_array env k then
+ Foreign_dom.set_dom env k IsForeign
| { app = { builtin = Expr.Store; _ }; args; _ } ->
let a, k, v = IArray.extract3_exn args in
Egraph.register env a;
Egraph.register env k;
Egraph.register env v;
+ (* Update of the restrict_aup/Linearity domain *)
+ if !restrict_aup then Linearity_dom.upd_dom env (Ground.node f) (Linear a);
(* application of the `idx` rule *)
let subst =
Ground.Subst.
diff --git a/colibri2/theories/array/foreign_dom.ml b/colibri2/theories/array/foreign_dom.ml
new file mode 100644
index 0000000000000000000000000000000000000000..4864f8fabd2db2f6e42bb44fd794c1f67cff7e8a
--- /dev/null
+++ b/colibri2/theories/array/foreign_dom.ml
@@ -0,0 +1,38 @@
+open Colibri2_core
+open Colibri2_popop_lib
+open Popop_stdlib
+
+module FVal = struct
+ module T = struct
+ type t = IsForeign [@@deriving eq, ord, hash]
+
+ let pp fmt = function IsForeign -> Fmt.pf fmt "IsForeign"
+ end
+
+ include T
+ include MkDatatype (T)
+
+ let name = "Array.foreign.value"
+end
+
+module D = struct
+ module Value = Value.Register (FVal)
+
+ type t = FVal.t = IsForeign [@@deriving eq]
+
+ let is_singleton (_ : Egraph.wt) _v = None (* ? *)
+
+ let key =
+ Dom.Kind.create
+ (module struct
+ type nonrec t = t
+
+ let name = "Array.foreign"
+ end)
+
+ let inter (_ : Egraph.wt) IsForeign IsForeign = Some IsForeign
+ let pp = FVal.pp
+end
+
+include D
+include Dom.Lattice (D)
diff --git a/colibri2/theories/array/foreign_dom.mli b/colibri2/theories/array/foreign_dom.mli
new file mode 100644
index 0000000000000000000000000000000000000000..3c92f9cf512f5040e6fd4d9f2d6d46befb21f9f6
--- /dev/null
+++ b/colibri2/theories/array/foreign_dom.mli
@@ -0,0 +1,9 @@
+type t = IsForeign
+
+val equal : t -> t -> bool
+val is_singleton : Egraph.wt -> t -> Colibri2_core.Value.t option
+val key : t Dom.Kind.t
+val inter : Egraph.wt -> t -> t -> t option
+val pp : t Fmt.t
+val set_dom : Egraph.wt -> Node.t -> t -> unit
+val upd_dom : Egraph.wt -> Node.t -> t -> unit
diff --git a/colibri2/theories/array/linearity_dom.ml b/colibri2/theories/array/linearity_dom.ml
new file mode 100644
index 0000000000000000000000000000000000000000..e39dfb745c0b1d3905d06c7a7df95f3c65c24f11
--- /dev/null
+++ b/colibri2/theories/array/linearity_dom.ml
@@ -0,0 +1,61 @@
+open Colibri2_core
+open Colibri2_popop_lib
+open Popop_stdlib
+
+module LVal = struct
+ module T = struct
+ type t = NonLinear | Linear of Node.t | Empty [@@deriving eq, ord, hash]
+
+ let pp fmt = function
+ | NonLinear -> Fmt.pf fmt "NonLinear"
+ | Linear n -> Fmt.pf fmt "Linear(%a)" Node.pp n
+ | Empty -> Fmt.pf fmt "Empty"
+ end
+
+ include T
+ include MkDatatype (T)
+
+ let name = "Array.linearity.value"
+end
+
+module D = struct
+ module Value = Value.Register (LVal)
+
+ type t = LVal.t = NonLinear | Linear of Node.t | Empty [@@deriving eq]
+
+ let is_singleton _ _ = None
+
+ let key =
+ Dom.Kind.create
+ (module struct
+ type nonrec t = t
+
+ let name = "Array.linearity"
+ end)
+
+ let inter d d1 d2 =
+ match (d1, d2) with
+ | NonLinear, NonLinear | NonLinear, Empty | Empty, NonLinear ->
+ Some NonLinear
+ | Linear n, Empty | Empty, Linear n -> Some (Linear n)
+ | Linear n1, Linear n2 ->
+ if Egraph.is_equal d n1 n2 then
+ (* does this ever happen? *)
+ Some (Linear n1)
+ else (
+ Egraph.set_dom d key n1 NonLinear;
+ Egraph.set_dom d key n2 NonLinear;
+ Some NonLinear)
+ | NonLinear, Linear n | Linear n, NonLinear ->
+ Egraph.set_dom d key n NonLinear;
+ Some NonLinear
+ | Empty, Empty -> Some Empty
+
+ let pp fmt = function
+ | NonLinear -> Fmt.pf fmt "NonLinear"
+ | Linear n -> Fmt.pf fmt "Linear(%a)" Node.pp n
+ | Empty -> Fmt.pf fmt "Empty"
+end
+
+include D
+include Dom.Lattice (D)
diff --git a/colibri2/theories/array/linearity_dom.mli b/colibri2/theories/array/linearity_dom.mli
new file mode 100644
index 0000000000000000000000000000000000000000..73de77b9963f68421bf05d1ce57e31adee291ffe
--- /dev/null
+++ b/colibri2/theories/array/linearity_dom.mli
@@ -0,0 +1,9 @@
+type t = NonLinear | Linear of Node.t | Empty
+
+val equal : t -> t -> bool
+val is_singleton : Egraph.wt -> t -> Colibri2_core.Value.t option
+val key : t Dom.Kind.t
+val inter : Egraph.wt -> t -> t -> t option
+val pp : t Fmt.t
+val set_dom : Egraph.wt -> Node.t -> t -> unit
+val upd_dom : Egraph.wt -> Node.t -> t -> unit