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

README.md

@@ -105,6 +105,19 @@ Z3 has a build system using CMake. Read the [README-CMake.md](README-CMake.md)
 file for details. It is recommended for most build tasks, 
 except for building OCaml bindings.
 
+## Building Z3 using vcpkg
+
+vcpkg is a full platform package manager, you can easily install libzmq with vcpkg.
+ 
+Execute:
+
+```bash
+git clone https://github.com/microsoft/vcpkg.git
+./bootstrap-vcpkg.bat # For powershell
+./bootstrap-vcpkg.sh # For bash
+./vcpkg install z3
+```
+
 ## Dependencies
 Z3 itself has few dependencies. It uses C++ runtime libraries, including pthreads for multi-threading.
 It is optionally possible to use GMP for multi-precision integers, but Z3 contains its own self-contained 

src/ast/rewriter/arith_rewriter.cpp

@@ -706,6 +706,31 @@ br_status arith_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result
     return st;
 }
 
+br_status arith_rewriter::mk_and_core(unsigned n, expr* const* args, expr_ref& result) {
+    if (n <= 1)
+        return BR_FAILED;
+    expr* x, * y, * z, * u;
+    rational a, b;
+    if (m_util.is_le(args[0], x, y) && m_util.is_numeral(x, a)) {
+        expr* arg0 = args[0];
+        ptr_buffer<expr> rest;
+        for (unsigned i = 1; i < n; ++i) {
+            if (m_util.is_le(args[i], z, u) && u == y && m_util.is_numeral(z, b)) {
+                if (b > a)
+                    arg0 = args[i];
+            }
+            else
+                rest.push_back(args[i]);
+        }
+        if (rest.size() < n - 1) {
+            rest.push_back(arg0);
+            result = m().mk_and(rest);
+            return BR_REWRITE1;
+        }
+    }
+    return BR_FAILED;
+}
+
 bool arith_rewriter::mk_eq_mod(expr* arg1, expr* arg2, expr_ref& result) {
     expr* x = nullptr, *y = nullptr, *z = nullptr, *u = nullptr;
     rational p, k, l;

src/ast/rewriter/arith_rewriter.h

@@ -149,6 +149,8 @@ public:
 
     br_status mk_abs_core(expr * arg, expr_ref & result);
 
+    br_status mk_and_core(unsigned n, expr* const* args, expr_ref& result);
+
     br_status mk_div_core(expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_idiv_core(expr * arg1, expr * arg2, expr_ref & result);
     br_status mk_idivides(unsigned k, expr * arg, expr_ref & result);

src/ast/rewriter/bool_rewriter.cpp

@@ -175,7 +175,7 @@ br_status bool_rewriter::mk_flat_and_core(unsigned num_args, expr * const * args
         }
         if (mk_nflat_and_core(flat_args.size(), flat_args.data(), result) == BR_FAILED)
             result = m().mk_and(flat_args);
-        return BR_DONE;
+        return BR_REWRITE1;
     }
     return mk_nflat_and_core(num_args, args, result);
 }
@@ -874,7 +874,7 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re
                 expr_ref tmp(m());
                 mk_not(c, tmp);
                 mk_and(tmp, e, result);
-                return BR_DONE;
+                return BR_REWRITE1;
             }
         }
         if (m().is_true(e) && m_elim_ite) {            
@@ -885,11 +885,11 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re
         }
         if (m().is_false(e) && m_elim_ite) {
             mk_and(c, t, result);
-            return BR_DONE;
+            return BR_REWRITE1;
         }
         if (c == e && m_elim_ite) {
             mk_and(c, t, result);
-            return BR_DONE;
+            return BR_REWRITE1;
         }
         if (c == t && m_elim_ite) {
             mk_or(c, e, result);
@@ -912,13 +912,13 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re
         expr_ref a(m());
         mk_and(c, t2, a);
         result = m().mk_not(m().mk_eq(t1, a));
-        return BR_REWRITE2;
+        return BR_REWRITE3;
     }
     if (m().is_not(t, t1) && m().is_eq(t1, t2, t1) && e == t1) {
         expr_ref a(m());
         mk_and(c, t2, a);
         result = m().mk_eq(t1, a);
-        return BR_REWRITE2;
+        return BR_REWRITE3;
     }
 #endif
 
@@ -931,14 +931,14 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re
             expr_ref new_c(m());
             mk_and(c, not_c2, new_c);
             result = m().mk_ite(new_c, to_app(t)->get_arg(2), e);
-            return BR_REWRITE1;
+            return BR_REWRITE2;
         }
         // (ite c1 (ite c2 t1 t2) t2) ==> (ite (and c1 c2) t1 t2)
         if (e == to_app(t)->get_arg(2)) {
             expr_ref new_c(m());
             mk_and(c, to_app(t)->get_arg(0), new_c);
             result = m().mk_ite(new_c, to_app(t)->get_arg(1), e);
-            return BR_REWRITE1;
+            return BR_REWRITE2;
         }
 
 
@@ -955,7 +955,7 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re
                 expr_ref new_c(m());
                 mk_or(and1, and2, new_c);
                 result = m().mk_ite(new_c, to_app(t)->get_arg(1), to_app(t)->get_arg(2));
-                return BR_REWRITE1;
+                return BR_REWRITE3;
             }
 
             // (ite c1 (ite c2 t1 t2) (ite c3 t2 t1)) ==> (ite (or (and c1 c2) (and (not c1) (not c3))) t1 t2)
@@ -972,7 +972,7 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re
                 expr_ref new_c(m());
                 mk_or(and1, and2, new_c);
                 result = m().mk_ite(new_c, to_app(t)->get_arg(1), to_app(t)->get_arg(2));
-                return BR_REWRITE1;
+                return BR_REWRITE3;
             }
         }
     }

src/ast/rewriter/th_rewriter.cpp

@@ -215,6 +215,11 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
                 if (st != BR_FAILED)
                     return st;
             }
+            if (false && k == OP_AND) {
+                st = m_a_rw.mk_and_core(num, args, result);
+                if (st != BR_FAILED)
+                    return st;
+            }
             if (k == OP_EQ && m_seq_rw.u().has_seq() && is_app(args[0]) &&
                 to_app(args[0])->get_family_id() == m_seq_rw.get_fid()) {
                 st = m_seq_rw.mk_eq_core(args[0], args[1], result);

src/model/model_evaluator.cpp

@@ -262,6 +262,11 @@ struct evaluator_cfg : public default_rewriter_cfg {
                 if (st != BR_FAILED)
                     return st;
             }
+            if (k == OP_AND) {
+                st = m_a_rw.mk_and_core(num, args, result);
+                if (st != BR_FAILED)
+                    return st;
+            }
             return m_b_rw.mk_app_core(f, num, args, result);
         }
         if (fid == m_a_rw.get_fid())

src/sat/sat_lookahead.h

@@ -353,7 +353,7 @@ namespace sat {
             candidate(bool_var v, double r): m_var(v), m_rating(r) {}
         };
         svector<candidate> m_candidates;
-        uint_set           m_select_lookahead_vars;
+        tracked_uint_set   m_select_lookahead_vars;
 
         double get_rating(bool_var v) const { return m_rating[v]; }
         double get_rating(literal l) const { return get_rating(l.var()); }

src/sat/sat_solver.cpp

@@ -428,9 +428,8 @@ namespace sat {
             }
 
             ++m_stats.m_non_learned_generation;
-            if (!m_searching) {
+            if (!m_searching) 
-                m_mc.add_clause(num_lits, lits);
+                m_mc.add_clause(num_lits, lits);            
-            }
         }       
 
 
@@ -941,10 +940,12 @@ namespace sat {
         m_inconsistent = true;
         m_conflict = c;
         m_not_l    = not_l;
+        TRACE("sat", display(display_justification(tout << "conflict " << not_l << " ", c) << "\n"));
     }
 
     void solver::assign_core(literal l, justification j) {
         SASSERT(value(l) == l_undef);
+        SASSERT(!m_trail.contains(l) && !m_trail.contains(~l));
         TRACE("sat_assign_core", tout << l << " " << j << "\n";);
         if (j.level() == 0) {
             if (m_config.m_drat) 
@@ -1803,24 +1804,21 @@ namespace sat {
 
 
     void solver::init_assumptions(unsigned num_lits, literal const* lits) {
-        if (num_lits == 0 && m_user_scope_literals.empty()) {
+        if (num_lits == 0 && m_user_scope_literals.empty()) 
-            return;
+            return;        
-        }
 
         SASSERT(at_base_lvl());
         reset_assumptions();
         push();
 
         propagate(false);
-        if (inconsistent()) {
+        if (inconsistent()) 
-            return;
+            return;        
-        }
 
         TRACE("sat",
               tout << literal_vector(num_lits, lits) << "\n";
-              if (!m_user_scope_literals.empty()) {
+              if (!m_user_scope_literals.empty()) 
-                  tout << "user literals: " << m_user_scope_literals << "\n";
+                  tout << "user literals: " << m_user_scope_literals << "\n";              
-              }
               m_mc.display(tout);
               );
 
@@ -1897,13 +1895,11 @@ namespace sat {
                   tout << "consistent: " << !inconsistent() << "\n";
                   for (literal a : m_assumptions) {
                       index_set s;
-                      if (m_antecedents.find(a.var(), s)) {
+                      if (m_antecedents.find(a.var(), s)) 
-                          tout << a << ": "; display_index_set(tout, s) << "\n";
+                          tout << a << ": "; display_index_set(tout, s) << "\n";                      
-                      }
-                  }
-                  for (literal lit : m_user_scope_literals) {
-                      tout << "user " << lit << "\n"; 
                   }
+                  for (literal lit : m_user_scope_literals) 
+                      tout << "user " << lit << "\n";                   
                   );
         }
     }
@@ -2419,7 +2415,9 @@ namespace sat {
         m_conflict_lvl = get_max_lvl(m_not_l, m_conflict, unique_max);        
         justification js = m_conflict;
 
-        if (m_conflict_lvl <= 1 && (!m_assumptions.empty() || !m_user_scope_literals.empty())) {
+        if (m_conflict_lvl <= 1 && (!m_assumptions.empty() || 
+                                    !m_ext_assumption_set.empty() || 
+                                    !m_user_scope_literals.empty())) {
             TRACE("sat", tout << "unsat core\n";);
             resolve_conflict_for_unsat_core();
             return l_false;
@@ -3654,11 +3652,14 @@ namespace sat {
             }
         }
         m_trail.shrink(old_sz);        
+        DEBUG_CODE(for (literal l : m_trail) SASSERT(lvl(l.var()) <= new_lvl););
         m_qhead = m_trail.size();
         if (!m_replay_assign.empty()) IF_VERBOSE(20, verbose_stream() << "replay assign: " << m_replay_assign.size() << "\n");
         CTRACE("sat", !m_replay_assign.empty(), tout << "replay-assign: " << m_replay_assign << "\n";);
         for (unsigned i = m_replay_assign.size(); i-- > 0; ) {
             literal lit = m_replay_assign[i];
+            SASSERT(value(lit) == l_true);
+            SASSERT(!m_trail.contains(lit) && !m_trail.contains(~lit));
             m_trail.push_back(lit);            
         }
         
@@ -3709,11 +3710,11 @@ namespace sat {
     //
 
     void solver::user_push() {
-
         pop_to_base_level();
         m_free_var_freeze.push_back(m_free_vars);
         m_free_vars.reset(); // resetting free_vars forces new variables to be assigned above new_v
         bool_var new_v = mk_var(true, false);
+        SASSERT(new_v + 1 == m_justification.size()); // there are no active variables that have higher values
         literal lit = literal(new_v, false);
         m_user_scope_literals.push_back(lit);
         m_cut_simplifier = nullptr; // for simplicity, wipe it out
@@ -3724,13 +3725,13 @@ namespace sat {
 
     void solver::user_pop(unsigned num_scopes) {
         unsigned old_sz = m_user_scope_literals.size() - num_scopes;
-        bool_var max_var = m_user_scope_literals[old_sz].var();
+        bool_var max_var = m_user_scope_literals[old_sz].var();        
         m_user_scope_literals.shrink(old_sz);
 
         pop_to_base_level();
         if (m_ext)
             m_ext->user_pop(num_scopes);
-
+    
         gc_vars(max_var);
         TRACE("sat", display(tout););
 
@@ -3743,7 +3744,7 @@ namespace sat {
         m_free_vars.append(m_free_var_freeze[old_sz]); 
         m_free_var_freeze.shrink(old_sz);
         scoped_suspend_rlimit _sp(m_rlimit);
-        propagate(false);
+        propagate(false);     
     }
 
     void solver::pop_to_base_level() {
@@ -4832,20 +4833,22 @@ namespace sat {
         return true;
     }
 
+    void solver::init_ts(unsigned n, svector<unsigned>& v, unsigned& ts) {
+        if (v.empty()) 
+            ts = 0;
+        
+        ts++;
+        if (ts == 0) {
+            ts = 1;
+            v.reset();
+        }
+        while (v.size() < n) 
+            v.push_back(0);        
+    }
+
     void solver::init_visited() {
-        if (m_visited.empty()) {
+        init_ts(2 * num_vars(), m_visited, m_visited_ts);
-            m_visited_ts = 0;
-        }
-        m_visited_ts++;
-        if (m_visited_ts == 0) {
-            m_visited_ts = 1;
-            m_visited.reset();
-        }
-        while (m_visited.size() < 2*num_vars()) {
-            m_visited.push_back(0);
-        }
     }
 
 
-
 };

src/sat/sat_solver.h

@@ -343,6 +343,7 @@ namespace sat {
         void push_reinit_stack(clause & c);
         void push_reinit_stack(literal l1, literal l2);
 
+        void init_ts(unsigned n, svector<unsigned>& v, unsigned& ts);
         void init_visited();
         void mark_visited(literal l) { m_visited[l.index()] = m_visited_ts; }
         void mark_visited(bool_var v) { mark_visited(literal(v, false)); }

src/sat/sat_solver/inc_sat_solver.cpp

@@ -596,10 +596,10 @@ public:
 
     void convert_internalized() {
         m_solver.pop_to_base_level();
-        if (!is_internalized() && m_fmls_head > 0) {
+        if (!is_internalized() && m_fmls_head > 0) 
-            internalize_formulas();
+            internalize_formulas();        
-        }
+        if (!is_internalized() || m_internalized_converted) 
-        if (!is_internalized() || m_internalized_converted) return;
+            return;
         sat2goal s2g;
         m_cached_mc = nullptr;
         goal g(m, false, true, false);

src/sat/smt/arith_solver.cpp

@@ -385,20 +385,16 @@ namespace arith {
         TRACE("arith", tout << b << "\n";);
         lp::constraint_index ci = b.get_constraint(is_true);
         lp().activate(ci);
-        if (is_infeasible()) {
+        if (is_infeasible()) 
             return;
-        }
         lp::lconstraint_kind k = bound2constraint_kind(b.is_int(), b.get_bound_kind(), is_true);
-        if (k == lp::LT || k == lp::LE) {
+        if (k == lp::LT || k == lp::LE) 
             ++m_stats.m_assert_lower;
-        }
+        else 
-        else {
             ++m_stats.m_assert_upper;
-        }
         inf_rational value = b.get_value(is_true);
-        if (propagate_eqs() && value.is_rational()) {
+        if (propagate_eqs() && value.is_rational()) 
             propagate_eqs(b.tv(), ci, k, b, value.get_rational());
-        }
 #if 0
         if (propagation_mode() != BP_NONE)
             lp().mark_rows_for_bound_prop(b.tv().id());
@@ -1118,16 +1114,23 @@ namespace arith {
     }
 
     bool solver::check_delayed_eqs() {
-        for (auto p : m_delayed_eqs) {
+        bool found_diseq = false;
+        if (m_delayed_eqs_qhead == m_delayed_eqs.size())
+            return true;
+        force_push();
+        ctx.push(value_trail<unsigned>(m_delayed_eqs_qhead));
+        for (; m_delayed_eqs_qhead < m_delayed_eqs.size(); ++ m_delayed_eqs_qhead) {
+            auto p = m_delayed_eqs[m_delayed_eqs_qhead];
             auto const& e = p.first;
             if (p.second)
                 new_eq_eh(e);
             else if (is_eq(e.v1(), e.v2())) {
                 mk_diseq_axiom(e);
-                return false;
+                found_diseq = true;
+                break;
             }
-        }
+        }        
-        return true;
+        return !found_diseq;
     }
 
     lbool solver::check_lia() {

src/sat/smt/arith_solver.h

@@ -218,6 +218,7 @@ namespace arith {
         svector<euf::enode_pair>                      m_equalities;      // asserted rows corresponding to equalities.
         svector<theory_var>                           m_definitions;     // asserted rows corresponding to definitions
         svector<std::pair<euf::th_eq, bool>>          m_delayed_eqs;
+        unsigned                                      m_delayed_eqs_qhead = 0;
 
         literal_vector  m_asserted;
         expr* m_not_handled{ nullptr };

src/sat/smt/array_axioms.cpp

@@ -700,6 +700,23 @@ namespace array {
             n->unmark1();
     }
 
+    /**
+    * \brief check that lambda expressions are beta redexes.
+    * The array solver is not a decision procedure for lambdas that do not occur in beta 
+    * redexes.
+    */
+    bool solver::check_lambdas() {
+        unsigned num_vars = get_num_vars();
+        for (unsigned i = 0; i < num_vars; i++) {
+            auto* n = var2enode(i);
+            if (a.is_as_array(n->get_expr()) || is_lambda(n->get_expr()))
+                for (euf::enode* p : euf::enode_parents(n))
+                    if (!ctx.is_beta_redex(p, n))
+                        return false;
+        }
+        return true;
+    }
+
     bool solver::is_shared_arg(euf::enode* r) {
         SASSERT(r->is_root());
         for (euf::enode* n : euf::enode_parents(r)) {

src/sat/smt/array_internalize.cpp

@@ -252,6 +252,8 @@ namespace array {
             return p->get_arg(0)->get_root() == n->get_root();
         if (a.is_map(p->get_expr()))
             return true;
+        if (a.is_store(p->get_expr()))
+            return true;
         return false;
     }
 

src/sat/smt/array_solver.cpp

@@ -108,7 +108,9 @@ namespace array {
         if (m_delay_qhead < m_axiom_trail.size()) 
             return sat::check_result::CR_CONTINUE;
 
-        
+        if (!check_lambdas())
+            return sat::check_result::CR_GIVEUP;
+
         // validate_check();
         return sat::check_result::CR_DONE;
     }

src/sat/smt/array_solver.h

@@ -218,6 +218,7 @@ namespace array {
         bool should_prop_upward(var_data const& d) const;
         bool can_beta_reduce(euf::enode* n) const { return can_beta_reduce(n->get_expr()); }
         bool can_beta_reduce(expr* e) const;
+        bool check_lambdas();
 
         var_data& get_var_data(euf::enode* n) { return get_var_data(n->get_th_var(get_id())); }
         var_data& get_var_data(theory_var v) { return *m_var_data[v]; }

src/sat/smt/euf_internalize.cpp

@@ -264,7 +264,11 @@ namespace euf {
         sat::status st = sat::status::th(m_is_redundant, m.get_basic_family_id());
         if (sz <= 1) 
             return;
-        if (sz <= distinct_max_args) {
+        sort* srt = e->get_arg(0)->get_sort();
+        auto sort_sz = srt->get_num_elements();
+        if (sort_sz.is_finite() && sort_sz.size() < sz)
+            s().add_clause(0, nullptr, st);
+        else if (sz <= distinct_max_args) {
             for (unsigned i = 0; i < sz; ++i) {
                 for (unsigned j = i + 1; j < sz; ++j) {
                     expr_ref eq = mk_eq(args[i]->get_expr(), args[j]->get_expr());
@@ -274,8 +278,7 @@ namespace euf {
             }
         }
         else {
-            // dist-f(x_1) = v_1 & ... & dist-f(x_n) = v_n
+            // dist-f(x_1) = v_1 & ... & dist-f(x_n) = v_n            
-            sort* srt = e->get_arg(0)->get_sort();
             SASSERT(!m.is_bool(srt));
             sort_ref u(m.mk_fresh_sort("distinct-elems"), m);
             func_decl_ref f(m.mk_fresh_func_decl("dist-f", "", 1, &srt, u), m);

src/sat/smt/euf_solver.cpp

@@ -488,7 +488,8 @@ namespace euf {
         };
         if (merge_shared_bools())
             cont = true;
-        for (auto* e : m_solvers) {
+        for (unsigned i = 0; i < m_solvers.size(); ++i) {
+            auto* e = m_solvers[i];
             if (!m.inc())
                 return sat::check_result::CR_GIVEUP;
             if (e == m_qsolver)
@@ -616,15 +617,17 @@ namespace euf {
             else 
                 lit = si.internalize(e, false);
             VERIFY(lit.var() == v);     
-            if (!m_egraph.find(e) && (!m.is_iff(e) && !m.is_or(e) && !m.is_and(e) && !m.is_not(e))) {
+            if (!m_egraph.find(e) && !m.is_iff(e) && !m.is_or(e) && !m.is_and(e) && !m.is_not(e) && !m.is_implies(e) && !m.is_xor(e)) {
                 ptr_buffer<euf::enode> args;
                 if (is_app(e))
                     for (expr* arg : *to_app(e))
                         args.push_back(e_internalize(arg));
+                internalize(e, true);
                 if (!m_egraph.find(e))
                     mk_enode(e, args.size(), args.data());
             }
-            attach_lit(lit, e);            
+            else 
+                attach_lit(lit, e);            
         }
         
         if (relevancy_enabled())
@@ -863,7 +866,13 @@ namespace euf {
         out << "bool-vars\n";
         for (unsigned v : m_var_trail) {
             expr* e = m_bool_var2expr[v];
-            out << v << (is_relevant(v)?"":"n") << ": " << e->get_id() << " " << m_solver->value(v) << " " << mk_bounded_pp(e, m, 1) << "\n";        
+            out << v << (is_relevant(v)?"":"n") << ": " << e->get_id() << " " << m_solver->value(v) << " " << mk_bounded_pp(e, m, 1);
+            euf::enode* n = m_egraph.find(e);
+            if (n) {
+                for (auto const& th : enode_th_vars(n))
+                    out << " " << m_id2solver[th.get_id()]->name();
+            }
+            out << "\n";        
         }
         for (auto* e : m_solvers)
             e->display(out);

src/sat/smt/q_mbi.cpp

@@ -635,8 +635,8 @@ namespace q {
     void mbqi::collect_statistics(statistics& st) const {
         if (m_solver)
             m_solver->collect_statistics(st);
-        st.update("q-num-instantiations", m_stats.m_num_instantiations);
+        st.update("q mbi instantiations", m_stats.m_num_instantiations);
-        st.update("q-num-checks", m_stats.m_num_checks);
+        st.update("q mbi num checks", m_stats.m_num_checks);
     }
 
 }

src/util/sat_literal.h

@@ -110,12 +110,10 @@ namespace sat {
 
     inline void negate(literal_vector& ls) { for (unsigned i = 0; i < ls.size(); ++i) ls[i].neg(); }
 
-    typedef tracked_uint_set uint_set;
+    typedef tracked_uint_set bool_var_set;
-
-    typedef uint_set bool_var_set;
 
     class literal_set {
-        uint_set m_set;
+        tracked_uint_set m_set;
     public:
         literal_set(literal_vector const& v) {
             for (unsigned i = 0; i < v.size(); ++i) insert(v[i]);
@@ -141,9 +139,9 @@ namespace sat {
         void reset() { m_set.reset(); }
         void finalize() { m_set.finalize(); }
         class iterator {
-            uint_set::iterator m_it;
+            tracked_uint_set::iterator m_it;
         public:
-            iterator(uint_set::iterator it):m_it(it) {}
+            iterator(tracked_uint_set::iterator it):m_it(it) {}
             literal operator*() const { return to_literal(*m_it); }
             iterator& operator++() { ++m_it; return *this; }
             iterator operator++(int) { iterator tmp = *this; ++m_it; return tmp; }