[Array] fixed some bugs, added tests

and the selectstore and distinct2neq rules

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

@@ -2,8 +2,38 @@
 --dont-print-result %{dep:eq.smt2})) (package colibri2))
 (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:eq.smt2})) (package colibri2))
 (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat 
+--dont-print-result %{dep:eq2.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:eq2.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat 
+--dont-print-result %{dep:eq3.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:eq3.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat 
+--dont-print-result %{dep:eq3_distinct.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:eq3_distinct.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat 
+--dont-print-result %{dep:eq4.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:eq4.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat 
+--dont-print-result %{dep:impls1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:impls1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat 
+--dont-print-result %{dep:impls2.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:impls2.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat 
+--dont-print-result %{dep:impls3.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:impls3.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat 
+--dont-print-result %{dep:impls4.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:impls4.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat 
+--dont-print-result %{dep:impls5.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:impls5.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat 
 --dont-print-result %{dep:select.smt2})) (package colibri2))
 (rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:select.smt2})) (package colibri2))
 (rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat 
---dont-print-result %{dep:store.smt2})) (package colibri2))
-(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:store.smt2})) (package colibri2))
+--dont-print-result %{dep:selectstore1.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:selectstore1.smt2})) (package colibri2))
+(rule (alias runtest) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat 
+--dont-print-result %{dep:selectstore2.smt2})) (package colibri2))
+(rule (alias runtest-learning) (action (run %{bin:colibri2} --size=50M --time=60s --max-steps 3500 --check-status unsat --learning --dont-print-result %{dep:selectstore2.smt2})) (package colibri2))

colibri2/tests/solve/smt_array/unsat/eq2.smt2

+(set-logic ALL)
+
+(declare-fun a () (Array Int Int))
+
+(assert (let ((a1 (store a 0 1)) (a2 (store a 0 2))) (= a1 a2)))
+
+(check-sat)

colibri2/tests/solve/smt_array/unsat/eq3.smt2

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

colibri2/tests/solve/smt_array/unsat/eq3_distinct.smt2

+(set-logic ALL)
+
+(declare-fun a () (Array Int Int))
+(declare-fun i () Int)
+
+(assert (distinct a (store a i (select a i))))
+
+(check-sat)

colibri2/tests/solve/smt_array/unsat/eq4.smt2

+(set-logic ALL)
+
+(declare-fun a () (Array Int Int))
+(declare-fun b () (Array Int Int))
+(declare-fun i () Int)
+(declare-fun j () Int)
+
+(assert (distinct (select a i) (select (store b j (select a i)) j)))
+
+(check-sat)

colibri2/tests/solve/smt_array/unsat/impls1.smt2

+(set-logic ALL)
+
+(declare-fun a () (Array Int Int))
+
+(declare-fun k () Int)
+(declare-fun i () Int)
+(declare-fun j () Int)
+(declare-fun v () Int)
+(declare-fun w () Int)
+
+(assert (not (=>
+  (distinct i j)
+  (< k i)
+  (distinct k j)
+  (= (select (store (store a i v) j w) k) 100)
+  (= (select (store (store a j w) i v) k) 200)
+  false
+)))
+
+(check-sat)

colibri2/tests/solve/smt_array/unsat/impls2.smt2

+(set-logic ALL)
+
+(declare-fun a () (Array Int Int))
+(declare-fun i () Int)
+(declare-fun j () Int)
+(declare-fun v () Int)
+(declare-fun w () Int)
+
+(assert (not (=>
+  (distinct i j)
+  (distinct v w)
+  (= (store (store a i v) j w) (store (store a j w) i v))
+)))
+
+(check-sat)

colibri2/tests/solve/smt_array/unsat/impls3.smt2

+(set-logic ALL)
+
+(declare-fun a () (Array Int Int))
+(declare-fun b () (Array Int Int))
+(declare-fun i () Int)
+(declare-fun v () Int)
+
+(assert (not (=>
+  (= b (store a i v))
+  (= v (select b i))
+)))
+
+(check-sat)

colibri2/tests/solve/smt_array/unsat/impls4.smt2

+(set-logic ALL)
+
+(declare-fun a () (Array Int Int))
+(declare-fun i () Int)
+(declare-fun j () Int)
+(declare-fun v () Int)
+
+(assert (not (=>
+  (= i j)
+  (= a (store a i (select a j)))
+)))
+
+(check-sat)

colibri2/tests/solve/smt_array/unsat/impls5.smt2

+(set-logic ALL)
+
+(declare-fun a () (Array Int Int))
+(declare-fun i () Int)
+(declare-fun v () Int)
+
+(assert (not (=>
+  (= a (store a i v))
+  (= (select a i) v)
+)))
+
+(check-sat)

colibri2/tests/solve/smt_array/unsat/selectstore2.smt2

+(set-logic ALL)
+
+(declare-fun a () (Array Int Int))
+
+(assert (= (- (select (store a 0 2) 0) 2) 1))
+
+(check-sat)

colibri2/theories/array/array.ml

@@ -22,6 +22,10 @@
 open Colibri2_core
 open Colibri2_popop_lib
 
+(*
+
+*)
+
 let converter env (f : Ground.t) =
   let _r = Ground.node f in
   match Ground.sem f with
@@ -62,6 +66,50 @@ module Select_store = struct
 
   open Colibri2_theories_quantifiers
 
+  (* a[i <- v][j] |> ITE(i = j, v, a[j]) *)
+  (* Shouldn't be necessary, because that information can be obtained from idx
+     passes: eq4 impls2, selectstore1, selectstore2 *)
+  let selectstore_pattern, selectstore_run =
+    let selectstore_term = Expr.Term.select (Expr.Term.store ta ti tv) tj in
+    let selectstore_pattern =
+      Pattern.of_term_exn ~subst:Ground.Subst.empty selectstore_term
+    in
+    let selectstore_run env subst =
+      Debug.dprintf2 debug "Found select_store with %a" Ground.Subst.pp subst;
+      let n = Ground.convert ~subst env selectstore_term in
+      let v =
+        Ground.convert ~subst env
+          (Expr.Term.ite (Expr.Term.eq ti tj) tv (Expr.Term.select ta tj))
+      in
+      Egraph.register env n;
+      Egraph.register env v;
+      Egraph.merge env n v
+    in
+    (selectstore_pattern, selectstore_run)
+
+  (* distinct [a; b] |> not (a = b) *)
+  (* to make eq3_distinct pass,
+     Colibri2 doesn't seem to realize that by itself *)
+  (* TODO: do it for n args *)
+  let distinct2neq_pattern, distinct2neq_run =
+    let selectstore_term = Expr.Term.distinct [ ta; tb ] in
+    (* how to match n args? *)
+    let distinct2neq_pattern =
+      Pattern.of_term_exn ~subst:Ground.Subst.empty selectstore_term
+    in
+    let distinct2neq_run env subst =
+      Debug.dprintf2 debug "Found distinct with %a" Ground.Subst.pp subst;
+      let n = Ground.convert ~subst env selectstore_term in
+      let v =
+        Ground.convert ~subst env (Expr.Term.neg (Expr.Term.eqs [ ta; tb ]))
+      in
+      Egraph.register env n;
+      Egraph.register env v;
+      Egraph.merge env n v
+    in
+    (distinct2neq_pattern, distinct2neq_run)
+
+  (* a = b[i <- v] |> a[i] = v *)
   let idx_pattern, idx_run =
     let term = Expr.Term.eq ta (Expr.Term.store tb ti tv) in
     let idx_pattern = Pattern.of_term_exn ~subst:Ground.Subst.empty term in
@@ -77,6 +125,7 @@ module Select_store = struct
     in
     (idx_pattern, idx_run)
 
+  (* w = b[i <- v][j] |> (i = j) \/ a[j] = b[j] *)
   let adown_pattern, adown_run =
     let a = Expr.Term.store tb ti tv in
     let term = Expr.Term.eq tw (Expr.Term.select a tj) in
@@ -86,13 +135,11 @@ module Select_store = struct
       let n = Ground.convert ~subst env term in
       let v =
         Ground.convert ~subst env
-        @@ Expr.Term._or
+          (Expr.Term._or
              [
-               Expr.Term._and [ Expr.Term.eq ti tj; Expr.Term.eq tv tw ];
-               (* It was modified because otherwise colibri2 responds
-                  incorrectly on eq.smt2 *)
+               Expr.Term._and [ Expr.Term.eq ti tj ];
                Expr.Term.eq (Expr.Term.select a tj) (Expr.Term.select tb tj);
-             ]
+             ])
       in
       Egraph.register env n;
       Egraph.register env v;
@@ -100,17 +147,21 @@ module Select_store = struct
     in
     (adown_pattern, adown_run)
 
+  (* a = b[i <- v], w = b[j]  |> (i = j) \/ a[j] = b[j] *)
   let aup_pattern, aup_run =
     let term = Expr.Term.eq ta (Expr.Term.store tb ti tv) in
     let aup_pattern = Pattern.of_term_exn ~subst:Ground.Subst.empty term in
     let aup_run env subst =
+      let n = Ground.convert ~subst env term in
+      Egraph.register env n;
       Debug.dprintf2 debug "Found aup1 with %a" Ground.Subst.pp subst;
-      let aup_pattern_bis =
-        Pattern.of_term_exn ~subst (Expr.Term.eq tw (Expr.Term.select tb tj))
-      in
-      let aup_run_bis env subst =
+      let term_bis = Expr.Term.eq tw (Expr.Term.select tb tj) in
+      let aup_pattern_bis = Pattern.of_term_exn ~subst term_bis in
+      let aup_run_bis env subst2 =
+        let subst = Ground.Subst.distinct_union subst2 subst in
+        (* ? *)
         Debug.dprintf2 debug "Found aup2 with %a" Ground.Subst.pp subst;
-        let n = Ground.convert ~subst env term in
+        let n = Ground.convert ~subst env term_bis in
         let v =
           Ground.convert ~subst env
             (Expr.Term._or
@@ -134,7 +185,6 @@ module Select_store = struct
       let b_pattern = Pattern.of_term_exn ~subst tb in
       let b_run env subst =
         Debug.dprintf2 debug "Found ext2 with %a" Ground.Subst.pp subst;
-        let n = Ground.convert ~subst env tb in
         let v =
           Ground.convert ~subst env
             (Expr.Term._or
@@ -148,19 +198,23 @@ module Select_store = struct
                        (Expr.Term.select tb kab_t));
                ])
         in
-        Egraph.register env n;
-        Egraph.register env v;
-        Egraph.merge env n v
+        Egraph.register env v (* ? *)
       in
       InvertedPath.add_callback env b_pattern b_run
     in
     (a_pattern, a_run)
 
   let init env =
-    InvertedPath.add_callback env idx_pattern idx_run;
-    InvertedPath.add_callback env adown_pattern adown_run;
-    InvertedPath.add_callback env aup_pattern aup_run;
-    InvertedPath.add_callback env ext_pattern ext_run
+    List.iter
+      (fun (p, r) -> InvertedPath.add_callback env p r)
+      [
+        (selectstore_pattern, selectstore_run);
+        (distinct2neq_pattern, distinct2neq_run);
+        (idx_pattern, idx_run);
+        (adown_pattern, adown_run);
+        (aup_pattern, aup_run);
+        (ext_pattern, ext_run);
+      ]
 end
 
 let init env : unit =