[Array] added restricted ext, aup rules

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.

colibri2/theories/array/foreign_dom.ml

+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)

colibri2/theories/array/foreign_dom.mli

+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

colibri2/theories/array/linearity_dom.ml

+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)

colibri2/theories/array/linearity_dom.mli

+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