remove duplicated definition of is_store and is_select

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/api/python/z3.py

@@ -3856,32 +3856,6 @@ def is_array(a):
     """
     return isinstance(a, ArrayRef)
 
-def is_select(a):
-    """Return `True` if `a` is a Z3 array select.
-    
-    >>> a = Array('a', IntSort(), IntSort())
-    >>> is_select(a)
-    False
-    >>> i = Int('i')
-    >>> is_select(a[i])
-    True
-    """
-    return is_app_of(a, Z3_OP_SELECT)
-
-def is_store(a):
-    """Return `True` if `a` is a Z3 array store.
-    
-    >>> a = Array('a', IntSort(), IntSort())
-    >>> is_store(a)
-    False
-    >>> i = Int('i')
-    >>> is_store(a[i])
-    False
-    >>> is_store(Store(a, i, i + 1))
-    True
-    """
-    return is_app_of(a, Z3_OP_STORE)
-
 def is_const_array(a):
     """Return `True` if `a` is a Z3 constant array.
 
@@ -4072,7 +4046,8 @@ def is_select(a):
     >>> a = Array('a', IntSort(), IntSort())
     >>> is_select(a)
     False
-    >>> is_select(a[0])
+    >>> i = Int('i')
+    >>> is_select(a[i])
     True
     """
     return is_app_of(a, Z3_OP_SELECT)

src/ast/simplifier/bv_simplifier_plugin.cpp

@@ -179,7 +179,7 @@ bool bv_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * const
     }
     SASSERT(result.get());
 
-    TRACE("bv_simplifier",
+    TRACE("bv_simplifier", 
           tout << mk_pp(f, m_manager) << "\n";
           for (unsigned i = 0; i < num_args; ++i) {
               tout << mk_pp(args[i], m_manager) << " ";

src/muz_qe/qe_lite.cpp

@@ -799,9 +799,15 @@ namespace ar {
         }
 
         /**
-           Ex A. A[x] = t & Phi where x \not\in A, t. 
+           Ex A. A[x] = t & Phi where x \not\in A, t. A \not\in t, x
            =>
            Ex A. Phi[store(A,x,t)]
+
+           Perhaps also:
+           Ex A. store(A,y,z)[x] = t & Phi where x \not\in A, t, y, z, A \not\in y z, t 
+           =>
+           Ex A, v . (x = y => z = t) & Phi[store(store(A,x,t),y,v)]
+
          */
 
         bool solve_select(expr_ref_vector& conjs, unsigned i, expr* e1, expr* e2) {
@@ -827,6 +833,7 @@ namespace ar {
                 expr_safe_replace rep(m);
                 rep.insert(A, B);
                 expr_ref tmp(m);
+                std::cout << mk_pp(e1, m) << " = " << mk_pp(e2, m) << "\n";
                 for (unsigned j = 0; j < conjs.size(); ++j) {
                     if (i == j) {
                         conjs[j] = m.mk_true();