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

src/api/python/z3.py

@@ -6449,7 +6449,7 @@ class Tactic:
 
 def _to_goal(a):
     if isinstance(a, BoolRef):
-        goal = Goal()
+        goal = Goal(ctx = a.ctx)
         goal.add(a)
         return goal
     else:

src/muz/base/dl_context.cpp

@@ -576,7 +576,7 @@ namespace datalog {
 
     void context::check_uninterpreted_free(rule_ref& r) {
         func_decl* f = 0;
-        if (r->has_uninterpreted_non_predicates(f)) {
+        if (r->has_uninterpreted_non_predicates(m, f)) {
             std::stringstream stm;
             stm << "Uninterpreted '" 
                 << f->get_name() 

src/muz/base/dl_rule.cpp

@@ -43,6 +43,7 @@ Revision History:
 #include"expr_safe_replace.h"
 #include"filter_model_converter.h"
 #include"scoped_proof.h"
+#include"datatype_decl_plugin.h"
 
 namespace datalog {
 
@@ -881,9 +882,12 @@ namespace datalog {
     }
 
     struct uninterpreted_function_finder_proc {
+        ast_manager& m;
+        datatype_util m_dt;
         bool m_found;
         func_decl* m_func;
-        uninterpreted_function_finder_proc() : m_found(false), m_func(0) {}
+        uninterpreted_function_finder_proc(ast_manager& m): 
+            m(m), m_dt(m), m_found(false), m_func(0) {}
         void operator()(var * n) { }
         void operator()(quantifier * n) { }
         void operator()(app * n) {
@@ -891,6 +895,14 @@ namespace datalog {
                 m_found = true;
                 m_func = n->get_decl();
             }
+            else if (m_dt.is_accessor(n)) {
+                sort* s = m.get_sort(n->get_arg(0));
+                SASSERT(m_dt.is_datatype(s));
+                if (m_dt.get_datatype_constructors(s)->size() > 1) {
+                    m_found = true;
+                    m_func = n->get_decl();
+                }
+            }
         }
 
         bool found(func_decl*& f) const { f = m_func; return m_found; }
@@ -900,9 +912,9 @@ namespace datalog {
     // non-predicates may appear only in the interpreted tail, it is therefore 
     // sufficient only to check the tail.
     //
-    bool rule::has_uninterpreted_non_predicates(func_decl*& f) const {
+    bool rule::has_uninterpreted_non_predicates(ast_manager& m, func_decl*& f) const {
         unsigned sz = get_tail_size();
-        uninterpreted_function_finder_proc proc;
+        uninterpreted_function_finder_proc proc(m);
         expr_mark visited;
         for (unsigned i = get_uninterpreted_tail_size(); i < sz && !proc.found(f); ++i) {
             for_each_expr(proc, visited, get_tail(i));
@@ -910,6 +922,7 @@ namespace datalog {
         return proc.found(f);
     }
 
+
     struct quantifier_finder_proc {
         bool m_exist;
         bool m_univ;

src/muz/base/dl_rule.h

@@ -293,7 +293,7 @@ namespace datalog {
         */
         bool is_in_tail(const func_decl * p, bool only_positive=false) const;
 
-        bool has_uninterpreted_non_predicates(func_decl*& f) const;
+        bool has_uninterpreted_non_predicates(ast_manager& m, func_decl*& f) const;
         void has_quantifiers(bool& existential, bool& universal) const;
         bool has_quantifiers() const;
         bool has_negation() const;

src/muz/pdr/pdr_util.cpp

@@ -112,8 +112,8 @@ namespace pdr {
             set_value(e, val);
         }
         else {
-            IF_VERBOSE(3, verbose_stream() << "Not evaluated " << mk_pp(e, m) << "\n";);
+            IF_VERBOSE(3, verbose_stream() << "Not evaluated " << mk_pp(e, m) << " := " << mk_pp(val, m) << "\n";);
-            TRACE("pdr", tout << "Variable is not tracked: " << mk_pp(e, m) << "\n";);
+            TRACE("pdr", tout << "Variable is not tracked: " << mk_pp(e, m) << " := " << mk_pp(val, m) << "\n";);
             set_x(e);
         }
     }
@@ -672,7 +672,19 @@ namespace pdr {
             eval_array_eq(e, arg1, arg2);
         }
         else if (is_x(arg1) || is_x(arg2)) {
-            set_x(e);
+            expr_ref eq(m), vl(m);
+            eq = m.mk_eq(arg1, arg2);
+            m_model->eval(eq, vl);
+            if (m.is_true(vl)) {
+                set_bool(e, true);                
+            }
+            else if (m.is_false(vl)) {
+                set_bool(e, false);
+            }
+            else {
+                TRACE("pdr", tout << "cannot evaluate: " << mk_pp(vl, m) <<  "\n";);
+                set_x(e);
+            }
         }
         else if (m.is_bool(arg1)) {
             bool val = is_true(arg1) == is_true(arg2);

src/smt/diff_logic.h

@@ -820,6 +820,7 @@ public:
         }
     }
 
+private:
     // Update the assignment of variable v, that is,
     // m_assignment[v] += inc
     // This method also stores the old value of v in the assignment stack.
@@ -829,6 +830,12 @@ public:
         m_assignment[v] += inc;
     }
 
+public:
+
+    void inc_assignment(dl_var v, numeral const& inc) {
+        m_assignment[v] += inc;
+    }    
+
 
     struct every_var_proc {
         bool operator()(dl_var v) const {

src/smt/theory_bv.cpp

@@ -581,10 +581,13 @@ namespace smt {
     void theory_bv::assert_int2bv_axiom(app* n) {
         //
         // create the axiom:
-        // bv2int(n) = e mod 2^bit_width 
+        //   bv2int(n) = e mod 2^bit_width 
-        //
         // where n = int2bv(e)
         //
+        // Create the axioms:
+        //   bit2bool(i,n) == ((e div 2^i) mod 2 != 0)
+        // for i = 0,.., sz-1
+        //
         SASSERT(get_context().e_internalized(n));
         SASSERT(m_util.is_int2bv(n));
         ast_manager & m = get_manager();
@@ -592,10 +595,12 @@ namespace smt {
 
         parameter param(m_autil.mk_int());
         expr* n_expr = n;
-        expr* lhs = m.mk_app(get_id(), OP_BV2INT, 1, &param, 1, &n_expr);
+        expr* e = n->get_arg(0);
+        expr_ref lhs(m), rhs(m);
+        lhs = m.mk_app(get_id(), OP_BV2INT, 1, &param, 1, &n_expr);
         unsigned sz = m_util.get_bv_size(n);
         numeral mod = power(numeral(2), sz);
-        expr* rhs = m_autil.mk_mod(n->get_arg(0), m_autil.mk_numeral(mod, true));
+        rhs = m_autil.mk_mod(e, m_autil.mk_numeral(mod, true));
 
         literal l(mk_eq(lhs, rhs, false));
         ctx.mark_as_relevant(l);
@@ -605,6 +610,24 @@ namespace smt {
               tout << mk_pp(lhs, m) << " == \n";
               tout << mk_pp(rhs, m) << "\n";
               );
+
+        expr_ref_vector n_bits(m);
+        enode * n_enode = mk_enode(n);
+        get_bits(n_enode, n_bits);
+
+        for (unsigned i = 0; i < sz; ++i) {
+            numeral div = power(numeral(2), i);
+            mod = numeral(2);
+            rhs = m_autil.mk_idiv(e, m_autil.mk_numeral(div,true));
+            rhs = m_autil.mk_mod(rhs, m_autil.mk_numeral(mod, true));
+            rhs = m.mk_eq(rhs, m_autil.mk_numeral(rational(1), true));
+            lhs = n_bits.get(i);
+            TRACE("bv", tout << mk_pp(lhs, m) << " == " << mk_pp(rhs, m) << "\n";);
+            l = literal(mk_eq(lhs, rhs, false));
+            ctx.mark_as_relevant(l);
+            ctx.mk_th_axiom(get_id(), 1, &l);
+            
+        }
     }
 
 

src/smt/theory_utvpi_def.h

@@ -752,7 +752,8 @@ namespace smt {
 
             for (unsigned j = 0; j < zero_v.size(); ++j) {
                 int v = zero_v[j];
-                m_graph.acc_assignment(v, numeral(-1));
+                
+                m_graph.inc_assignment(v, numeral(-1));
                 th_var k = from_var(v);
                 if (!is_parity_ok(k)) {
                     todo.push_back(k);