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

src/ast/ast.cpp

@@ -2883,9 +2883,9 @@ proof* ast_manager::mk_hyper_resolve(unsigned num_premises, proof* const* premis
     ptr_vector<expr> fmls;
     SASSERT(positions.size() + 1 == substs.size());
     for (unsigned i = 0; i < num_premises; ++i) {
-        TRACE("dl", tout << mk_pp(premises[i], *this) << "\n";);
+        TRACE("hyper_res", tout << mk_pp(premises[i], *this) << "\n";);
         fmls.push_back(get_fact(premises[i]));
-    }
+    }    
     SASSERT(is_bool(concl));
     vector<parameter> params;
     for (unsigned i = 0; i < substs.size(); ++i) {
@@ -2898,6 +2898,10 @@ proof* ast_manager::mk_hyper_resolve(unsigned num_premises, proof* const* premis
             params.push_back(parameter(positions[i].second));
         }
     }
+    TRACE("hyper_res", 
+          for (unsigned i = 0; i < params.size(); ++i) {
+              params[i].display(tout); tout << "\n";
+          });
     ptr_vector<sort> sorts;
     ptr_vector<expr> args;
     for (unsigned i = 0; i < num_premises; ++i) {

src/muz_qe/dl_util.cpp

@@ -638,7 +638,16 @@ namespace datalog {
 
         TRACE("dl", 
               tout << premises[0]->get_id() << " " << mk_pp(premises[0].get(), m) << "\n";
-              tout << premises[1]->get_id() << " " << mk_pp(premises[1].get(), m) << "\n";); 
+              for (unsigned i = 0; i < s1.size(); ++i) {
+                  tout << mk_pp(s1[i], m) << " ";
+              }
+              tout << "\n";
+              tout << premises[1]->get_id() << " " << mk_pp(premises[1].get(), m) << "\n";
+              for (unsigned i = 0; i < s2.size(); ++i) {
+                  tout << mk_pp(s2[i], m) << " ";
+              }
+              tout << "\n";
+              ); 
 
         pr = m.mk_hyper_resolve(2, premises.c_ptr(), fml3, positions, substs);
         pc->insert(pr);

src/muz_qe/pdr_context.cpp

@@ -42,6 +42,7 @@ Notes:
 #include "dl_mk_rule_inliner.h"
 #include "ast_smt2_pp.h"
 #include "qe_lite.h"
+#include "ast_ll_pp.h"
 
 namespace pdr {
 
@@ -398,6 +399,9 @@ namespace pdr {
         lbool is_sat = m_solver.check_conjunction_as_assumptions(n.state());
         if (is_sat == l_true && core) {            
             core->reset();
+            TRACE("pdr", tout << "updating model\n"; 
+                  model_smt2_pp(tout, m, *model, 0);
+                  tout << mk_pp(n.state(), m) << "\n";);
             n.set_model(model);
         }
         return is_sat;
@@ -758,7 +762,7 @@ namespace pdr {
         }
         r0 = const_cast<datalog::rule*>(&pt().find_rule(*m_model.get()));
         app_ref_vector& inst = pt().get_inst(r0);
-        TRACE("pdr", tout << mk_pp(state(), m) << "\n";);
+        TRACE("pdr", tout << mk_pp(state(), m) << " instance: " << inst.size() << "\n";);
         for (unsigned i = 0; i < inst.size(); ++i) {
             expr* v;
             if (model.find(inst[i].get(), v)) {
@@ -1421,6 +1425,7 @@ namespace pdr {
         proof_ref proof(m);
         SASSERT(m_last_result == l_true);
         proof = m_search.get_proof_trace(*this);
+        TRACE("pdr", tout << "PDR trace: " << mk_pp(proof, m) << "\n";);
         apply(m, m_pc.get(), proof);
         return proof;
     }
@@ -1844,7 +1849,7 @@ namespace pdr {
             break;
         }
         case l_true: {
-            strm << mk_ismt2_pp(mk_sat_answer(), m);
+            strm << mk_pp(mk_sat_answer(), m);
             break;
         }
         case l_undef: {

src/muz_qe/pdr_util.cpp

@@ -126,9 +126,6 @@ void model_evaluator::setup_model(model_ref& model) {
         m_refs.push_back(e);
         assign_value(e, val);
     }
-
-    m_level1 = m1.get_level();
-    m_level2 = m2.get_level();
 }
 
 void model_evaluator::reset() {
@@ -170,11 +167,11 @@ expr_ref_vector model_evaluator::minimize_literals(ptr_vector<expr> const& formu
         tout << "formulas:\n";
         for (unsigned i = 0; i < formulas.size(); ++i) tout << mk_pp(formulas[i], m) << "\n"; 
     );
-    
+
-    setup_model(mdl);
     expr_ref_vector result(m);
     ptr_vector<expr> tocollect;
-
+    
+    setup_model(mdl);
     collect(formulas, tocollect);
     for (unsigned i = 0; i < tocollect.size(); ++i) {
         expr* e = tocollect[i];
@@ -301,8 +298,6 @@ void model_evaluator::collect(ptr_vector<expr> const& formulas, ptr_vector<expr>
     ptr_vector<expr> todo;
     todo.append(formulas);
     m_visited.reset();
-    m1.set_level(m_level1);
-    m2.set_level(m_level2);
     
     VERIFY(check_model(formulas));
     
@@ -923,13 +918,32 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
         arith_util a;
         bool m_is_dl;
 
-        // NB. ite terms are non-arihmetical but their then/else branches can be.
+        bool is_numeric(expr* e) const {
-        // this gets ignored (also in static_features)
+            if (a.is_numeral(e)) {
+                return true;
+            }
+            expr* cond, *th, *el;
+            if (m.is_ite(e, cond, th, el)) {
+                return is_numeric(th) && is_numeric(el);
+            }
+            return false;
+        }
         
         bool is_arith_expr(expr *e) const {
             return is_app(e) && a.get_family_id() == to_app(e)->get_family_id();
         }
 
+        bool is_var_or_numeric(expr* e) const {
+            if (a.is_numeral(e)) {
+                return true;
+            }
+            expr* cond, *th, *el;
+            if (m.is_ite(e, cond, th, el)) {
+                return is_var_or_numeric(th) && is_var_or_numeric(el);
+            }
+            return !is_arith_expr(e);
+        }
+
         bool is_minus_one(expr const * e) const { 
             rational r; return a.is_numeral(e, r) && r.is_minus_one(); 
         }
@@ -939,14 +953,14 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
             SASSERT(to_app(e)->get_num_args() == 2);
             expr * lhs = to_app(e)->get_arg(0);
             expr * rhs = to_app(e)->get_arg(1);
-            if (!is_arith_expr(lhs) && !is_arith_expr(rhs)) 
+            if (is_var_or_numeric(lhs) && is_var_or_numeric(rhs)) 
                 return true;    
-            if (!a.is_numeral(rhs)) 
+            if (!is_numeric(rhs)) 
                 std::swap(lhs, rhs);
-            if (!a.is_numeral(rhs)) 
+            if (!is_numeric(rhs)) 
                 return false;    
             // lhs can be 'x' or '(+ x (* -1 y))'
-            if (!is_arith_expr(lhs))
+            if (is_var_or_numeric(lhs))
                 return true;
             expr* arg1, *arg2;
             if (!a.is_add(lhs, arg1, arg2)) 
@@ -960,7 +974,7 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
             expr* m1, *m2;
             if (!a.is_mul(arg2, m1, m2))
                 return false;
-            return is_minus_one(m1) && !is_arith_expr(m2);
+            return is_minus_one(m1) && is_var_or_numeric(m2);
         }
 
         bool test_eq(expr* e) const {
@@ -976,21 +990,21 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
         }
 
         bool test_term(expr* e) const {
-            if (!is_arith_expr(e)) {
-                return true;
-            }
             if (m.is_bool(e)) {
                 return true;
             }
             if (a.is_numeral(e)) {
                 return true;
             }
+            if (is_var_or_numeric(e)) {
+                return true;
+            }
             expr* lhs, *rhs;
             if (a.is_add(e, lhs, rhs)) {
                 if (!a.is_numeral(lhs)) {
                     std::swap(lhs, rhs);
                 }
-                return a.is_numeral(lhs) && !is_arith_expr(rhs);
+                return a.is_numeral(lhs) && is_var_or_numeric(rhs);
             }
             if (a.is_mul(e, lhs, rhs)) {
                 return is_minus_one(lhs) || is_minus_one(rhs);
@@ -998,6 +1012,17 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
             return false;
         }
 
+        bool is_non_arith_or_basic(expr* e) {
+            if (!is_app(e)) {
+                return false;
+            }
+            family_id fid = to_app(e)->get_family_id();
+            return 
+                fid != m.get_basic_family_id() &&
+                fid != null_family_id &&
+                fid != a.get_family_id();
+        }
+
     public:
         test_diff_logic(ast_manager& m): m(m), a(m), m_is_dl(true) {}
         
@@ -1011,8 +1036,11 @@ bool model_evaluator::check_model(ptr_vector<expr> const& formulas) {
             else if (m.is_eq(e)) {
                 m_is_dl = test_eq(e);
             }
+            else if (is_non_arith_or_basic(e)) {
+                m_is_dl = false;
+            }
             else if (is_app(e)) {
-                app* a = to_app(e);
+                app* a = to_app(e);                
                 for (unsigned i = 0; m_is_dl && i < a->get_num_args(); ++i) {
                     m_is_dl = test_term(a->get_arg(i));
                 }

src/muz_qe/pdr_util.h

@@ -65,10 +65,8 @@ namespace pdr {
         //01 -- X
         //10 -- false
         //11 -- true
-        ast_fast_mark1 m1;
+        expr_mark      m1;
-        ast_fast_mark2 m2;
+        expr_mark      m2;
-        unsigned       m_level1;
-        unsigned       m_level2;
         expr_mark      m_visited;
         
 
@@ -84,7 +82,7 @@ namespace pdr {
         void inherit_value(expr* e, expr* v);
         
         inline bool is_unknown(expr* x)  { return !m1.is_marked(x) && !m2.is_marked(x); }
-        inline void set_unknown(expr* x)  { m1.reset_mark(x); m2.reset_mark(x); }
+        inline void set_unknown(expr* x)  { m1.mark(x, false); m2.mark(x, false); }
         inline bool is_x(expr* x)  { return !m1.is_marked(x) && m2.is_marked(x); }
         inline bool is_false(expr* x)  { return m1.is_marked(x) && !m2.is_marked(x); }
         inline bool is_true(expr* x)  { return m1.is_marked(x) && m2.is_marked(x); }

src/muz_qe/qe_datatype_plugin.cpp

@@ -107,6 +107,7 @@ namespace qe {
         ast_manager&     m;
         app_ref_vector   m_recognizers;
         expr_ref_vector  m_eqs;
+        expr_ref_vector  m_neqs;
         app_ref_vector   m_eq_atoms;
         app_ref_vector   m_neq_atoms;
         app_ref_vector   m_unsat_atoms;
@@ -117,7 +118,8 @@ namespace qe {
         datatype_atoms(ast_manager& m) :
             m(m), 
             m_recognizers(m),
-            m_eqs(m), 
+            m_eqs(m),
+            m_neqs(m),
             m_eq_atoms(m), m_neq_atoms(m), m_unsat_atoms(m), m_eq_conds(m),
             m_util(m) {}
         
@@ -291,6 +293,7 @@ namespace qe {
                 }
                 app* a = to_app(a0);
                 if (a == x) {
+                    m_neqs.push_back(b);
                     return true;
                 }
                 if (!m_util.is_constructor(a)) {

src/smt/theory_diff_logic_def.h

@@ -972,6 +972,7 @@ model_value_proc * theory_diff_logic<Ext>::mk_value(enode * n, model_generator &
     SASSERT(v != null_theory_var);
     numeral val = m_graph.get_assignment(v);
     rational num = val.get_rational().to_rational() + m_delta * val.get_infinitesimal().to_rational();
+    TRACE("arith", tout << mk_pp(n->get_owner(), get_manager()) << " |-> " << num << "\n";);
     return alloc(expr_wrapper_proc, m_factory->mk_value(num, m_util.is_int(n->get_owner())));
 }