Fix quantifiers selector over store rewrite (#2510)

Due an ordering on if's the rewrite sel( store( a, i, j ), k ) ---> ite( k=i, j, sel( a, k ) ) was very rarely kicking in.

After the change, we are +61-7 on SMT LIB:
https://www.starexec.org/starexec/secure/details/job.jsp?id=30581

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 1f94dd3df042326cf1d6ccaa460b1b4c054a740a..e2a26f6e60e4672310ac2d3bd0e3c34ce0d6a85c 100644 (file)
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -667,7 +667,28 @@ Node QuantifiersRewriter::computeProcessTerms2( Node body, bool hasPol, bool pol
           }
         }
       }
-    }else if( elimExtArith ){
+    }
+    else if (ret.getKind() == SELECT && ret[0].getKind() == STORE)
+    {
+      Node st = ret[0];
+      Node index = ret[1];
+      std::vector<Node> iconds;
+      std::vector<Node> elements;
+      while (st.getKind() == STORE)
+      {
+        iconds.push_back(index.eqNode(st[1]));
+        elements.push_back(st[2]);
+        st = st[0];
+      }
+      ret = nm->mkNode(SELECT, st, index);
+      // conditions
+      for (int i = (iconds.size() - 1); i >= 0; i--)
+      {
+        ret = nm->mkNode(ITE, iconds[i], elements[i], ret);
+      }
+    }
+    else if( elimExtArith )
+    {
       if( ret.getKind()==INTS_DIVISION_TOTAL || ret.getKind()==INTS_MODULUS_TOTAL ){
         Node num = ret[0];
         Node den = ret[1];
@@ -711,25 +732,6 @@ Node QuantifiersRewriter::computeProcessTerms2( Node body, bool hasPol, bool pol
         }
       }
     }
-    else if (ret.getKind() == SELECT && ret[0].getKind() == STORE)
-    {
-      Node st = ret[0];
-      Node index = ret[1];
-      std::vector<Node> iconds;
-      std::vector<Node> elements;
-      while (st.getKind() == STORE)
-      {
-        iconds.push_back(index.eqNode(st[1]));
-        elements.push_back(st[2]);
-        st = st[0];
-      }
-      ret = nm->mkNode(SELECT, st, index);
-      // conditions
-      for (int i = (iconds.size() - 1); i >= 0; i--)
-      {
-        ret = nm->mkNode(ITE, iconds[i], elements[i], ret);
-      }
-    }
     icache[prev] = ret;
     return ret;
   }

diff --git a/test/regress/regress0/quantifiers/qarray-sel-over-store.smt2 b/test/regress/regress0/quantifiers/qarray-sel-over-store.smt2
new file mode 100644 (file)
index 0000000..f7e5a3a
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qarray-sel-over-store.smt2
@@ -0,0 +1,32 @@
+; EXPECT: unsat
+(set-logic AUFBV)
+(set-info :status unsat)
+(set-info :category "crafted")
+(declare-sort Element 0)
+
+(declare-fun a1 () (Array (_ BitVec 8) Element))
+(declare-fun a2 () (Array (_ BitVec 8) Element))
+(declare-fun a3 () (Array (_ BitVec 8) Element))
+(declare-fun a4 () (Array (_ BitVec 8) Element))
+
+(declare-fun i2 () (_ BitVec 8))
+(declare-fun i3 () (_ BitVec 8))
+
+(declare-fun e1 () Element)
+(declare-fun e2 () Element)
+
+(assert (not (= e1 e2)))
+(assert (= a3 (store a1 (_ bv3 8) e1)))
+(assert (= a4 (store a2 (_ bv3 8) e1)))
+(assert (= (select a3 (_ bv2 8)) e1))
+(assert (= (select a4 (_ bv2 8)) e2))
+
+; (assert (eqrange a3 a4 (_ bv0 8) (_ bv2 8)))
+
+(assert (forall ((x (_ BitVec 8)))
+    (=> (and (bvule (_ bv0 8) x) (bvule x (_ bv2 8))) (= (select a3 x) (select a4 x)))
+    ))
+
+
+(check-sat)
+(exit)