[Array] Attempt at solving sat problems

colibri2/tests/solve/smt_array/sat/dune.inc

+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat 
+--dont-print-result %{dep:neq.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status sat --learning --dont-print-result %{dep:neq.smt2})) (package colibri2))

colibri2/tests/solve/smt_array/sat/eq.txt

+(set-logic ALL)
+(declare-fun a () (Array Int Int))
+(assert (= (store a 0 0) (store a 1 0)))
+(check-sat)
\ No newline at end of file

colibri2/tests/solve/smt_array/sat/neq.smt2

+(set-logic ALL)
+(declare-fun a () (Array Int Int))
+(declare-fun b () (Array Int Int))
+(assert (not (= a b)))
+(check-sat)

colibri2/theories/array/SharingIsCaring.ml

@@ -116,8 +116,8 @@ let init env =
   if Options.get env use_diff_graph then
     Id_dom.register_merge_hook env eq_arrays_norm
 
-(* TODO: should this converter not redo what was already done in GEADP.converter?
-   is it safe? *)
+(* TODO: should this converter not redo what was already done in
+   GEADP.converter? is it safe? *)
 let converter env (f : Ground.t) =
   if Options.get env use_diff_graph then
     let s = Ground.sem f in

colibri2/theories/array/array.ml

@@ -20,6 +20,10 @@
 (*************************************************************************)
 
 open Colibri2_core
+open Colibri2_popop_lib
+open Popop_stdlib
+open Common
+open Colibri2_theories_quantifiers
 
 (*
   Command line options:
@@ -40,7 +44,100 @@ let converter env f =
   GE_Array_DP.converter env f;
   SharingIsCaring.converter env f
 
+module ArrayModelVal = struct
+  type aval = {
+    ind_ty : Ground.Ty.t;
+    val_ty : Ground.Ty.t;
+    vals : Value.t Value.M.t;
+  }
+
+  include Value.Register (struct
+    module T = struct
+      type t = aval = {
+        ind_ty : Ground.Ty.t;
+        val_ty : Ground.Ty.t;
+        vals : Value.t Value.M.t;
+      }
+      [@@deriving eq, ord, hash]
+
+      let pp fmt { ind_ty; val_ty; _ } =
+        Format.fprintf fmt "Array(%a => %a)" Ground.Ty.pp ind_ty Ground.Ty.pp
+          val_ty
+    end
+
+    include T
+    include MkDatatype (T)
+
+    let name = "Array.model.val"
+  end)
+end
+
+let init_ty d =
+  let open Interp.SeqLim in
+  Interp.Register.ty d (fun d ty ->
+      match ty with
+      | { app = { builtin = Expr.Array; _ }; args = [ ind_ty; val_ty ]; _ } ->
+          Some
+            (let+ seq = of_seq d (Base.Sequence.singleton Value.M.empty)
+             and* indv = Interp.ty d ind_ty
+             and* valv = Interp.ty d val_ty in
+             let vals = Value.M.add indv valv seq in
+             ArrayModelVal.nodevalue
+               (ArrayModelVal.index { ind_ty; val_ty; vals }))
+      | _ -> None)
+
+let interp env n = Opt.get_exn Impossible (Egraph.get_value env n)
+
+let compute d g =
+  match Ground.sem g with
+  | { app = { builtin = Expr.Select; _ }; args; _ } -> (
+      let a, k = IArray.extract2_exn args in
+      let av =
+        ArrayModelVal.value (ArrayModelVal.coerce_nodevalue (interp d a))
+      in
+      let kv = interp d k in
+      match Value.M.find_opt kv av.vals with
+      | Some fv -> `Some fv
+      | None -> `Uninterpreted)
+  | { app = { builtin = Expr.Store; _ }; args; _ } ->
+      let a, k, v = IArray.extract3_exn args in
+      let av =
+        ArrayModelVal.value (ArrayModelVal.coerce_nodevalue (interp d a))
+      in
+      let kv = interp d k in
+      let vv = interp d v in
+      `Some
+        (ArrayModelVal.of_value { av with vals = Value.M.add kv vv av.vals })
+  | { app = { builtin = Builtin.Array_diff; _ }; args; _ } -> (
+      let a, b = IArray.extract2_exn args in
+      let av =
+        ArrayModelVal.value (ArrayModelVal.coerce_nodevalue (interp d a))
+      in
+      let bv =
+        ArrayModelVal.value (ArrayModelVal.coerce_nodevalue (interp d b))
+      in
+      match Value.M.choose (Value.M.set_inter av.vals bv.vals) with
+      | k, _ -> `Some k
+      | exception Not_found -> `Uninterpreted)
+  | _ -> `None
+
+let init_check env =
+  Interp.Register.check env (fun d t ->
+      match compute d t with
+      | `None -> NA
+      | `Some r ->
+          Interp.check_of_bool (Value.equal r (interp d (Ground.node t)))
+      | `Uninterpreted ->
+          Interp.check_of_bool (Uninterp.On_uninterpreted_domain.check d t));
+  Interp.Register.compute env (fun d t ->
+      match compute d t with
+      | `None -> NA
+      | `Some v -> Value v
+      | `Uninterpreted -> Uninterp.On_uninterpreted_domain.compute d t)
+
 let init env =
+  init_ty env;
+  init_check env;
   Ground.register_converter env converter;
   GE_Array_DP.init env