Merge branch 'master' of https://github.com/z3prover/z3

src/api/c++/z3++.h

@@ -599,6 +599,7 @@ namespace z3 {
         iterator begin() const noexcept { return iterator(this, 0); }
         iterator end() const { return iterator(this, size()); }
         friend std::ostream & operator<<(std::ostream & out, ast_vector_tpl const & v) { out << Z3_ast_vector_to_string(v.ctx(), v); return out; }
+        std::string to_string() const { return std::string(Z3_ast_vector_to_string(ctx(), m_vector)); }
     };
 
 

src/ast/rewriter/array_rewriter.cpp

@@ -31,7 +31,7 @@ void array_rewriter::updt_params(params_ref const & _p) {
     m_expand_store_eq = p.expand_store_eq();
     m_expand_nested_stores = p.expand_nested_stores();
     m_blast_select_store = p.blast_select_store();
-    m_expand_select_ite = false;
+    m_expand_select_ite = p.expand_select_ite();
 }
 
 void array_rewriter::get_param_descrs(param_descrs & r) {
@@ -226,8 +226,7 @@ br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args,
         result = subst(q->get_expr(), _args.size(), _args.data());
         inv_var_shifter invsh(m());
         invsh(result, _args.size(), result);
-        return BR_REWRITE_FULL;
+        return BR_REWRITE_FULL;        
-        
     }
 
     if (m_util.is_map(args[0])) {
@@ -698,7 +697,7 @@ br_status array_rewriter::mk_eq_core(expr * lhs, expr * rhs, expr_ref & result)
     if (m_util.is_const(lhs, v) && m_util.is_store(rhs)) {
         unsigned n = to_app(rhs)->get_num_args();
         result = m().mk_and(m().mk_eq(lhs, to_app(rhs)->get_arg(0)),
- 			  m().mk_eq(v, to_app(rhs)->get_arg(n - 1)));
+                            m().mk_eq(v, to_app(rhs)->get_arg(n - 1)));
         return BR_REWRITE2;
     }
     if (m_util.is_const(lhs, v) && m_util.is_const(rhs, w)) {

src/params/array_rewriter_params.pyg

@@ -4,5 +4,6 @@ def_module_params(module_name='rewriter',
                   params=(("expand_select_store", BOOL, False, "conservatively replace a (select (store ...) ...) term by an if-then-else term"),
                           ("blast_select_store", BOOL, False, "eagerly replace all (select (store ..) ..) term by an if-then-else term"),
                           ("expand_nested_stores", BOOL, False, "replace nested stores by a lambda expression"),
+                          ("expand_select_ite", BOOL, False, "expand select over ite expressions"),
                           ("expand_store_eq", BOOL, False, "reduce (store ...) = (store ...) with a common base into selects"),
                           ("sort_store", BOOL, False, "sort nested stores when the indices are known to be different")))

src/sat/smt/arith_internalize.cpp

@@ -42,6 +42,7 @@ namespace arith {
     void solver::init_internalize() {
         force_push();
         // initialize 0, 1 variables:
+        
         if (!m_internalize_initialized) {
             get_one(true);
             get_one(false);
@@ -484,10 +485,10 @@ namespace arith {
             return st.vars()[0];
         }
         else if (is_one(st) && a.is_numeral(term)) {
-            return get_one(a.is_int(term));
+            return lp().local_to_external(get_one(a.is_int(term)));
         }
         else if (is_zero(st) && a.is_numeral(term)) {
-            return get_zero(a.is_int(term));
+            return lp().local_to_external(get_zero(a.is_int(term)));
         }
         else {
             init_left_side(st);

src/sat/smt/array_axioms.cpp

@@ -451,6 +451,7 @@ namespace array {
         expr_ref alpha(a.mk_select(args), m);
         expr_ref beta(alpha);
         rewrite(beta);
+        TRACE("array", tout << alpha << " == " << beta << "\n";);
         return ctx.propagate(e_internalize(alpha), e_internalize(beta), array_axiom());
     }
 

src/sat/smt/euf_internalize.cpp

@@ -342,7 +342,9 @@ namespace euf {
                 break;
             }
         }
-
+        if (m.is_bool(n->get_expr()) && th_id != m.get_basic_family_id())
+            return true;
+        
         for (enode* parent : euf::enode_parents(n)) {
             app* p = to_app(parent->get_expr());
             family_id fid = p->get_family_id();

src/sat/smt/euf_solver.cpp

@@ -300,7 +300,7 @@ namespace euf {
         size_t* c = to_ptr(l);
         SASSERT(is_literal(c));
         SASSERT(l == get_literal(c));
-	    if (n->value_conflict()) {
+        if (n->value_conflict()) {
             euf::enode* nb = sign ? mk_false() : mk_true();
             euf::enode* r = n->get_root();
             euf::enode* rb = sign ? mk_true() : mk_false();
@@ -458,6 +458,8 @@ namespace euf {
             give_up = true;
         
         unsigned num_nodes = m_egraph.num_nodes();
+        if (merge_shared_bools())
+            cont = true;
         for (auto* e : m_solvers) {
             if (!m.inc())
                 return sat::check_result::CR_GIVEUP;
@@ -485,6 +487,24 @@ namespace euf {
         return sat::check_result::CR_DONE;
     }
 
+    bool solver::merge_shared_bools() {
+        bool merged = false;
+        for (unsigned i = m_egraph.nodes().size(); i-- > 0; ) {
+            euf::enode* n = m_egraph.nodes()[i];
+            if (!is_shared(n) || !m.is_bool(n->get_expr()))
+                continue;
+            if (n->value() == l_true && !m.is_true(n->get_root()->get_expr())) {
+                m_egraph.merge(n, mk_true(), to_ptr(sat::literal(n->bool_var())));
+                merged = true;                    
+            }
+            if (n->value() == l_false && !m.is_false(n->get_root()->get_expr())) {
+                m_egraph.merge(n, mk_false(), to_ptr(~sat::literal(n->bool_var())));
+                merged = true;
+            }
+        }
+        return merged;
+    }
+
     void solver::push() {
         si.push();
         scope s;

src/sat/smt/euf_solver.h

@@ -165,6 +165,7 @@ namespace euf {
         bool is_self_propagated(th_eq const& e);
         void get_antecedents(literal l, constraint& j, literal_vector& r, bool probing);
         void new_diseq(enode* a, enode* b, literal lit);
+        bool merge_shared_bools();
 
         // proofs
         void log_antecedents(std::ostream& out, literal l, literal_vector const& r);
@@ -286,6 +287,7 @@ namespace euf {
 
         void propagate(literal lit, th_explain* p) { propagate(lit, p->to_index()); }
         bool propagate(enode* a, enode* b, th_explain* p) { return propagate(a, b, p->to_index()); }
+        size_t* to_justification(sat::literal l) { return to_ptr(l); }
         void set_conflict(th_explain* p) { set_conflict(p->to_index()); }
 
         bool set_root(literal l, literal r) override;

src/sat/smt/q_eval.cpp

@@ -181,23 +181,25 @@ namespace q {
         while (!todo.empty()) {
             expr* t = todo.back();
             SASSERT(!is_ground(t) || ctx.get_egraph().find(t));
-            if (is_ground(t) || (has_quantifiers(t) && !has_free_vars(t))) {
-                m_mark.mark(t);
-                m_eval.setx(t->get_id(), ctx.get_egraph().find(t), nullptr);                
-                if (!m_eval[t->get_id()])
-                    return nullptr;
-                todo.pop_back();
-                continue;
-            }
             if (m_mark.is_marked(t)) {
                 todo.pop_back();
                 continue;
             }
-            if (is_var(t)) {
+            if (is_ground(t) || (has_quantifiers(t) && !has_free_vars(t))) {
+                m_eval.setx(t->get_id(), ctx.get_egraph().find(t), nullptr);                
+                if (!m_eval[t->get_id()])
+                    return nullptr;
                 m_mark.mark(t);
+                todo.pop_back();
+                continue;
+            }
+            if (is_var(t)) {
                 if (to_var(t)->get_idx() >= n)
                     return nullptr;
                 m_eval.setx(t->get_id(), binding[n - 1 - to_var(t)->get_idx()], nullptr);
+                if (!m_eval[t->get_id()])
+                    return nullptr;
+                m_mark.mark(t);
                 todo.pop_back();
                 continue;
             }

src/sat/smt/q_mam.cpp

@@ -3745,7 +3745,7 @@ namespace q {
             // However, the simplifier may turn a non-ground pattern into a ground one.
             // So, we should check it again here.
             for (expr* arg : *mp)
-                if (is_ground(arg))
+                if (is_ground(arg) || has_quantifiers(arg))
                     return; // ignore multi-pattern containing ground pattern.
             update_filters(qa, mp);
             m_new_patterns.push_back(qp_pair(qa, mp));

src/sat/tactic/goal2sat.cpp

@@ -251,7 +251,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
             return;
         }
         n -= m_num_scopes;
-        m_num_scopes = 0;
+        m_num_scopes = 0;        
         m_map.pop(n);
         unsigned k = m_cache_lim[m_cache_lim.size() - n];
         for (unsigned i = m_cache_trail.size(); i-- > k; ) {
@@ -284,7 +284,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
         m_cache_trail.push_back(t);
     }
     
-    void convert_atom(expr * t, bool root, bool sign) {
+    void convert_atom(expr * t, bool root, bool sign) {       
         SASSERT(m.is_bool(t));
         sat::literal  l;
         sat::bool_var v = m_map.to_bool_var(t);
@@ -954,9 +954,11 @@ struct goal2sat::imp : public sat::sat_internalizer {
     }
 
     void user_push() {
+        push();
     }
 
     void user_pop(unsigned n) {
+        pop(n);
     }
 
 };
@@ -1010,15 +1012,7 @@ void goal2sat::operator()(goal const & g, params_ref const & p, sat::solver_core
         for (unsigned i = 0; i < m_scopes; ++i)
             m_imp->user_push();
     }
-    (*m_imp)(g);
+    (*m_imp)(g);    
-    
-    if (!t.get_extension() && m_imp->interpreted_funs().empty()) {
-        dealloc(m_imp);
-        m_imp = nullptr;
-    }
-    else 
-        m_scopes = 0;
-
 }
 
 void goal2sat::get_interpreted_funs(func_decl_ref_vector& funs) {

src/smt/smt_context_inv.cpp

@@ -371,7 +371,7 @@ namespace smt {
             case l_true:
                 if (!m_proto_model->eval(n, res, false)) 
                     return true;
-                CTRACE("model", !m.is_true(res), tout << n << " evaluates to " << res << "\n";); 
+                CTRACE("model", !m.is_true(res), tout << n << " evaluates to " << res << "\n" << *m_proto_model << "\n";); 
                 if (m.is_false(res)) {
                     return false;
                 }
@@ -379,7 +379,7 @@ namespace smt {
             case l_false:
                 if (!m_proto_model->eval(n, res, false)) 
                     return true;
-                CTRACE("model", !m.is_false(res), tout << n << " evaluates to " << res << "\n";); 
+                CTRACE("model", !m.is_false(res), tout << n << " evaluates to " << res << "\n" << *m_proto_model << "\n";); 
                 if (m.is_true(res)) {
                     return false;
                 }

src/smt/theory_lra.cpp

@@ -807,10 +807,10 @@ class theory_lra::imp {
             return st.vars()[0];
         }
         else if (is_one(st) && a.is_numeral(term)) {
-            return get_one(a.is_int(term));
+            return lp().local_to_external(get_one(a.is_int(term)));
         }
         else if (is_zero(st) && a.is_numeral(term)) {
-            return get_zero(a.is_int(term));
+            return lp().local_to_external(get_zero(a.is_int(term)));
         }
         else {
             init_left_side(st);

src/solver/assertions/asserted_formulas.cpp

@@ -532,14 +532,14 @@ void asserted_formulas::propagate_values() {
     flush_cache();
 
     unsigned num_prop = 0;
-    unsigned delta_prop = m_formulas.size();
+    unsigned sz = m_formulas.size();
-    while (!inconsistent() && m_formulas.size()/20 < delta_prop) {
+    unsigned delta_prop = sz;
+    while (!inconsistent() && sz/20 < delta_prop) {
         m_expr2depth.reset();
         m_scoped_substitution.push();
         unsigned prop = num_prop;
         TRACE("propagate_values", display(tout << "before:\n"););
         unsigned i  = m_qhead;
-        unsigned sz = m_formulas.size();
         for (; i < sz; i++) {
             prop += propagate_values(i);
         }
@@ -558,6 +558,9 @@ void asserted_formulas::propagate_values() {
         TRACE("propagate_values", tout << "after:\n"; display(tout););
         delta_prop = prop - num_prop;
         num_prop = prop;
+        if (sz <= m_formulas.size())
+            break;
+        sz = m_formulas.size();
     }
     TRACE("asserted_formulas", tout << num_prop << "\n";);
     if (num_prop > 0)

src/tactic/portfolio/solver_subsumption_tactic.h

@@ -19,7 +19,7 @@ class tactic;
 tactic * mk_solver_subsumption_tactic(ast_manager & m, params_ref const & p = params_ref());
 
 /*
-  ADD_TACTIC("solver_subsumption", "remove assertions that are subsumed.", "mk_solver_subsumption_tactic(m, p)")
+  ADD_TACTIC("solver-subsumption", "remove assertions that are subsumed.", "mk_solver_subsumption_tactic(m, p)")
 */