Merge branch 'unstable' of https://git01.codeplex.com/z3 into unstable

src/api/api_context.cpp

@@ -139,7 +139,7 @@ namespace api {
             if (m_interruptable)
                 (*m_interruptable)();
             m().set_cancel(true);
-            if (m_rcf_manager.get() == 0)
+            if (m_rcf_manager.get() != 0)
                 m_rcf_manager->set_cancel(true);
         }
     }

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();

src/smt/theory_dl.cpp

@@ -91,7 +91,7 @@ namespace smt {
                 rational val;
                 if (ctx.e_internalized(rep_of) && th_bv && 
                     th_bv->get_fixed_value(rep_of.get(), val)) {
-                        result = m_th.u().mk_numeral(val.get_int64(), s);
+                    result = m_th.u().mk_numeral(val.get_int64(), s);
                 }
                 else {
                     result = m_th.u().mk_numeral(0, s);

src/test/polynorm.cpp

@@ -2,6 +2,7 @@
 #include "smt2parser.h"
 #include "arith_decl_plugin.h"
 #include "reg_decl_plugins.h"
+#include "arith_rewriter.h"
 #include "ast_pp.h"
 
 
@@ -27,6 +28,114 @@ static char const* example1 = "(= (+ (- (* x x) (* 2 y)) y) 0)";
 static char const* example2 = "(= (+ 4 3 (- (* x x) (* 2 y)) y) 0)";
 
 
+class poly_nf {
+    expr_ref        m_coefficient;
+    expr_ref_vector m_coefficients;
+    expr_ref_vector m_factors;
+public:
+    poly_nf(ast_manager& m):
+        m_coefficient(m),
+        m_coefficients(m),
+        m_factors(m) {}
+    
+    expr_ref& coefficient() { return m_coefficient; }
+    expr_ref_vector& coefficients() { return m_coefficients; }
+    expr_ref_vector& factors() { return m_factors; }
+
+    void reset() {
+        m_coefficient.reset();
+        m_coefficients.reset();
+        m_factors.reset();
+    }
+
+};
+
+class polynorm {
+    ast_manager&   m;
+    arith_util     m_arith;
+    arith_rewriter m_arith_rw;
+    th_rewriter    m_rw;
+public:
+    polynorm(ast_manager& m): m(m), m_arith(m), m_arith_rw(m), m_rw(m) {}
+
+private:
+    expr_ref_vector mk_fresh_constants(unsigned num, sort* s) {
+        expr_ref_vector result(m);
+        for (unsigned i = 0; i < num; ++i) {
+            result.push_back(m.mk_fresh_const("fresh", s));
+        }
+        return result;
+    }
+
+    expr_ref_vector mk_fresh_reals(unsigned num) {
+        return mk_fresh_constants(num, m_arith.mk_real());
+    }
+
+    expr_ref mk_mul(unsigned num_args, expr* const* args) {
+        expr_ref result(m);
+        m_arith_rw.mk_mul(num_args, args, result);
+        return result;
+    }
+
+    void nf(expr_ref& term, obj_hashtable<expr>& constants, poly_nf& poly) {
+
+        expr_ref_vector& factors = poly.factors();
+        expr_ref_vector& coefficients = poly.coefficients();
+        expr_ref& coefficient = poly.coefficient();
+
+        m_rw(term);
+
+        if (m_arith.is_add(term)) {
+            factors.append(to_app(term)->get_num_args(), to_app(term)->get_args());
+        }
+        else {
+            factors.push_back(term);
+        }
+        for (unsigned i = 0; i < factors.size(); ++i) {
+            expr* f = factors[i].get();
+            unsigned num_args = 1;
+            expr* const* args = &f;
+            if (m_arith.is_mul(f)) {
+                num_args = to_app(f)->get_num_args();
+                args = to_app(f)->get_args();
+            }
+            for (unsigned j = 0; j < num_args; ++j) {
+                if (m_arith.is_numeral(args[j]) || constants.contains(args[j])) {
+                    //consts.push_back(args[j]);
+                }
+                else {
+                    // vars.push_back(args[j]);
+                }
+                // deal with the relevant corner cases.
+            }
+#if 0
+            rational r;
+            if (m_arith.is_mul(f) && m_arith.is_numeral(to_app(f)->get_arg(0), r)) {
+                coefficients.push_back(r);            
+                factors[i] = mk_mul(to_app(f)->get_num_args()-1, to_app(f)->get_args()+1);
+            }
+            else if (m_arith.is_numeral(f, r)) {
+                factors[i] = factors.back();
+                factors.pop_back();
+                SASSERT(coefficient.is_zero());
+                SASSERT(!r.is_zero());
+                coefficient = r;
+                --i; // repeat examining 'i'
+            }
+            else {
+                coefficients.push_back(rational(1));
+            }
+#endif
+        }
+
+        TRACE("polynorm",
+              tout << mk_pp(coefficient, m) << "\n";
+              for (unsigned i = 0; i < factors.size(); ++i) {
+                  tout << mk_pp(factors[i].get(), m) << " * " << mk_pp(coefficients[i].get(), m) << "\n";
+              });
+    }
+};
+
 // ast
 ///  sort : ast
 ///  func_decl : ast