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

src/api/api_solver.cpp

@@ -114,7 +114,7 @@ extern "C" {
     }
 
     solver2smt2_pp::solver2smt2_pp(ast_manager& m, const std::string& file):
-        m_pp_util(m), m_out(file), m_tracked(m) {
+        m_pp_util(m), m_out(file, std::ofstream::trunc | std::ofstream::out), m_tracked(m) {
         if (!m_out) {
             throw default_exception("could not open " + file + " for output");
         }

src/ast/ast.cpp

@@ -27,6 +27,7 @@ Revision History:
 #include "ast/ast_util.h"
 #include "ast/ast_smt2_pp.h"
 #include "ast/array_decl_plugin.h"
+#include "ast/arith_decl_plugin.h"
 #include "ast/ast_translation.h"
 #include "util/z3_version.h"
 
@@ -2131,12 +2132,17 @@ bool ast_manager::coercion_needed(func_decl * decl, unsigned num_args, expr * co
 expr* ast_manager::coerce_to(expr* e, sort* s) {
     sort* se = e->get_sort();
     if (s != se && s->get_family_id() == arith_family_id && se->get_family_id() == arith_family_id) {
-        if (s->get_decl_kind() == REAL_SORT) {
+        if (s->get_decl_kind() == REAL_SORT) 
             return mk_app(arith_family_id, OP_TO_REAL, e);
-        }
+        else 
-        else {
             return mk_app(arith_family_id, OP_TO_INT, e);                
-        }
+    }
+    if (s != se && s->get_family_id() == arith_family_id && is_bool(e)) {
+        arith_util au(*this);
+        if (s->get_decl_kind() == REAL_SORT) 
+            return mk_ite(e, au.mk_real(1), au.mk_real(0));
+        else 
+            return mk_ite(e, au.mk_int(1), au.mk_int(0));
     }
     else {
         return e;

src/ast/rewriter/seq_rewriter.cpp

@@ -5531,44 +5531,37 @@ lbool seq_rewriter::eq_length(expr* x, expr* y) {
     maximal length (the sequence is bounded).
 */
 
-bool seq_rewriter::min_length(expr* e, unsigned& len) {
+bool seq_rewriter::min_length(unsigned sz, expr* const* ss, unsigned& len) {
+    ptr_buffer<expr> es;
+    for (unsigned i = 0; i < sz; ++i)
+        es.push_back(ss[i]);
     zstring s;
     len = 0;
-    if (str().is_unit(e)) {
+    bool bounded = true;
-        len = 1;
+    while (!es.empty()) {
-        return true;
+        expr* e = es.back();
+        es.pop_back();
+        if (str().is_unit(e)) 
+            len += 1;
+        else if (str().is_empty(e)) 
+            continue;
+        else if (str().is_string(e, s)) 
+            len += s.length();
+        else if (str().is_concat(e)) 
+            for (expr* arg : *to_app(e))
+                es.push_back(arg);
+        else
+            bounded = false;
     }
-    else if (str().is_empty(e)) {
+    return bounded;
-        len = 0;
+}
-        return true;
+
-    }
+bool seq_rewriter::min_length(expr* e, unsigned& len) {
-    else if (str().is_string(e, s)) {
+    return min_length(1, &e, len);
-        len = s.length();
-        return true;
-    }
-    else if (str().is_concat(e)) {
-        unsigned min_l = 0;
-        bool bounded = true;
-        for (expr* arg : *to_app(e)) {
-            if (!min_length(arg, min_l))
-                bounded = false;
-            len += min_l;
-        }
-        return bounded;
-    }
-    return false;
 }
 
 bool seq_rewriter::min_length(expr_ref_vector const& es, unsigned& len) {
-    unsigned min_l = 0;
+    return min_length(es.size(), es.data(), len);
-    bool bounded = true;
-    len = 0;
-    for (expr* arg : es) {
-        if (!min_length(arg, min_l))
-            bounded = false;
-        len += min_l;
-    }
-    return bounded;
 }
 
 bool seq_rewriter::max_length(expr* e, rational& len) {

src/ast/rewriter/seq_rewriter.h

@@ -322,6 +322,7 @@ class seq_rewriter {
     bool reduce_eq_empty(expr* l, expr* r, expr_ref& result);    
     bool min_length(expr_ref_vector const& es, unsigned& len);
     bool min_length(expr* e, unsigned& len);
+    bool min_length(unsigned sz, expr* const* es, unsigned& len);
     bool max_length(expr* e, rational& len);
     lbool eq_length(expr* x, expr* y);
     expr* concat_non_empty(expr_ref_vector& es);

src/opt/opt_context.cpp

@@ -301,7 +301,7 @@ namespace opt {
 
         IF_VERBOSE(1, verbose_stream() << "(optimize:check-sat)\n");
         
-        lbool is_sat = s.check_sat(asms.size(),asms.data());
+        lbool is_sat = s.check_sat(asms.size(), asms.data());
 
         TRACE("opt", s.display(tout << "initial search result: " << is_sat << "\n");); 
         if (is_sat != l_false) {

src/sat/sat_scc.cpp

@@ -67,15 +67,8 @@ namespace sat {
         }
     };
 
-    unsigned scc::operator()() {
+    bool scc::extract_roots(literal_vector& roots, bool_var_vector& to_elim) {
-        if (m_solver.m_inconsistent)
+        literal_vector lits;
-            return 0;
-        if (!m_scc)
-            return 0;
-        CASSERT("scc_bug", m_solver.check_invariant());
-        report rpt(*this);
-        TRACE("scc", m_solver.display(tout););
-        TRACE("scc_details", m_solver.display_watches(tout););
         unsigned_vector index;
         unsigned_vector lowlink;
         unsigned_vector s;
@@ -84,11 +77,9 @@ namespace sat {
         index.resize(num_lits, UINT_MAX);
         lowlink.resize(num_lits, UINT_MAX);
         in_s.resize(num_lits, false);
-        literal_vector roots, lits;
         roots.resize(m_solver.num_vars(), null_literal);
         unsigned next_index = 0;
         svector<frame>   frames;
-        bool_var_vector  to_elim;
         
         for (unsigned l_idx = 0; l_idx < num_lits; l_idx++) {
             if (index[l_idx] != UINT_MAX)
@@ -182,7 +173,7 @@ namespace sat {
                             j--;
                             if (to_literal(l2_idx) == ~l) {
                                 m_solver.set_conflict();
-                                return 0;
+                                return false;
                             }
                             if (m_solver.is_external(to_literal(l2_idx).var())) {
                                 r = to_literal(l2_idx);
@@ -226,6 +217,23 @@ namespace sat {
                 roots[i] = literal(i, false);
             }
         }
+        return true;
+    }
+
+
+    unsigned scc::operator()() {
+        if (m_solver.m_inconsistent)
+            return 0;
+        if (!m_scc)
+            return 0;
+        CASSERT("scc_bug", m_solver.check_invariant());
+        report rpt(*this);
+        TRACE("scc", m_solver.display(tout););
+        TRACE("scc_details", m_solver.display_watches(tout););
+        literal_vector roots;
+        bool_var_vector to_elim;
+        if (!extract_roots(roots, to_elim))
+            return 0;
         TRACE("scc", for (unsigned i = 0; i < roots.size(); i++) { tout << i << " -> " << roots[i] << "\n"; }
               tout << "to_elim: "; for (unsigned v : to_elim) tout << v << " "; tout << "\n";);
         m_num_elim += to_elim.size();
@@ -234,9 +242,8 @@ namespace sat {
         TRACE("scc_detail", m_solver.display(tout););
         CASSERT("scc_bug", m_solver.check_invariant());
 
-        if (m_scc_tr) {
+        if (m_scc_tr) 
             reduce_tr();
-        }
         TRACE("scc_detail", m_solver.display(tout););
         return to_elim.size();
     }

src/sat/sat_scc.h

@@ -41,9 +41,13 @@ namespace sat {
         void reduce_tr();
         unsigned reduce_tr(bool learned);
 
+
     public:
 
         scc(solver & s, params_ref const & p);
+
+        bool extract_roots(literal_vector& roots, bool_var_vector& lits);
+
         unsigned operator()();
 
         void updt_params(params_ref const & p);

src/sat/sat_solver.cpp

@@ -4174,7 +4174,7 @@ namespace sat {
     lbool solver::find_mutexes(literal_vector const& lits, vector<literal_vector> & mutexes) {
         max_cliques<neg_literal> mc;
         m_user_bin_clauses.reset();
-        m_binary_clause_graph.reset();
+        // m_binary_clause_graph.reset();
         collect_bin_clauses(m_user_bin_clauses, true, false);
         hashtable<literal_pair, pair_hash<literal_hash, literal_hash>, default_eq<literal_pair> > seen_bc;
         for (auto const& b : m_user_bin_clauses) {
@@ -4189,7 +4189,7 @@ namespace sat {
         vector<unsigned_vector> _mutexes;
         literal_vector _lits(lits);
         if (m_ext) {
-            // m_ext->find_mutexes(_lits, mutexes);
+            m_ext->find_mutexes(_lits, mutexes);
         }
         unsigned_vector ps;
         for (literal lit : _lits) {

src/sat/sat_solver.h

@@ -755,7 +755,7 @@ namespace sat {
 
         u_map<index_set>       m_antecedents;
         literal_vector         m_todo_antecedents;
-        vector<literal_vector> m_binary_clause_graph;
+        // vector<literal_vector> m_binary_clause_graph;
 
         bool extract_assumptions(literal lit, index_set& s);
         

src/sat/smt/atom2bool_var.cpp

@@ -19,6 +19,7 @@ Notes:
 
 #include "util/ref_util.h"
 #include "ast/ast_smt2_pp.h"
+#include "ast/ast_util.h"
 #include "tactic/goal.h"
 #include "sat/smt/atom2bool_var.h"
 
@@ -27,7 +28,7 @@ void atom2bool_var::mk_inv(expr_ref_vector & lit2expr) const {
         sat::literal l(static_cast<sat::bool_var>(kv.m_value), false);
         lit2expr.set(l.index(), kv.m_key);
         l.neg();
-        lit2expr.set(l.index(), m().mk_not(kv.m_key));
+        lit2expr.set(l.index(), mk_not(m(), kv.m_key));
     }
 }
 

src/sat/smt/pb_solver.cpp

@@ -21,6 +21,7 @@ Author:
 #include "sat/smt/pb_solver.h"
 #include "sat/smt/euf_solver.h"
 #include "sat/sat_simplifier_params.hpp"
+#include "sat/sat_scc.h"
 
 namespace pb {
 
@@ -1422,7 +1423,7 @@ namespace pb {
             c->watch_literal(*this, ~lit);
         }     
         if (!c->well_formed()) 
-            std::cout << *c << "\n";
+            IF_VERBOSE(0, verbose_stream() << *c << "\n");
         VERIFY(c->well_formed());
         if (m_solver && m_solver->get_config().m_drat) {
             std::function<void(std::ostream& out)> fn = [&](std::ostream& out) {
@@ -3133,32 +3134,35 @@ namespace pb {
     void solver::find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes) {
         sat::literal_set slits(lits);
         bool change = false;
-        for (constraint* cp : m_constraints) {
-            if (!cp->is_card()) continue;
-            card const& c = cp->to_card();
-            if (c.size() == c.k() + 1) {
-                literal_vector mux;
-                for (literal lit : c) {
-                    if (slits.contains(~lit)) {
-                        mux.push_back(~lit);
-                    }
-                }
-                if (mux.size() <= 1) {
-                    continue;
-                }
         
-                for (literal m : mux) {
+        for (constraint* cp : m_constraints) {
-                    slits.remove(m);
+            if (!cp->is_card()) 
-                }
+                continue;
-                change = true;
+            if (cp->lit() != sat::null_literal)
-                mutexes.push_back(mux);
+                continue;
-            }
+            card const& c = cp->to_card();
+            if (c.size() != c.k() + 1) 
+                continue;
+
+            literal_vector mux;
+            for (literal lit : c) 
+                if (slits.contains(~lit)) 
+                    mux.push_back(~lit);
+
+            if (mux.size() <= 1) 
+                continue;
+            
+            for (literal m : mux) 
+                slits.remove(m);
+
+            change = true;
+            mutexes.push_back(mux);            
         }        
-        if (!change) return;
+        if (!change) 
+            return;
         lits.reset();
-        for (literal l : slits) {
+        for (literal l : slits) 
             lits.push_back(l);
-        }
     }
 
     void solver::display(std::ostream& out, ineq const& ineq, bool values) const {

src/sat/tactic/goal2sat.cpp

@@ -805,6 +805,7 @@ struct goal2sat::imp : public sat::sat_internalizer {
     }
 
     sat::literal internalize(expr* n, bool redundant) override {
+        bool is_not = m.is_not(n, n);
         flet<bool> _top(m_top_level, false);
         unsigned sz = m_result_stack.size();
         (void)sz;
@@ -820,6 +821,9 @@ struct goal2sat::imp : public sat::sat_internalizer {
             m_map.insert(n, result.var());    
             m_solver.set_external(result.var());
         }
+
+        if (is_not)
+            result.neg();
         return result;
     }
 

src/sat/tactic/sat2goal.cpp

@@ -218,7 +218,7 @@ struct sat2goal::imp {
             }
             sat::literal lit(l.var(), false);
             m_lit2expr.set(lit.index(), aux);
-            m_lit2expr.set((~lit).index(), m.mk_not(aux));
+            m_lit2expr.set((~lit).index(), mk_not(m, aux));
         }        
         return m_lit2expr.get(l.index());
     }

src/smt/smt_context.cpp

@@ -3731,7 +3731,7 @@ namespace smt {
         if (status == l_false) {
             return false;
         }
-        if (status == l_true && !m_qmanager->has_quantifiers()) {
+        if (status == l_true && !m_qmanager->has_quantifiers() && !m_has_lambda) {
             return false;
         }
         if (status == l_true && m_qmanager->has_quantifiers()) {
@@ -3754,6 +3754,11 @@ namespace smt {
                 break;
             }
         }
+        if (status == l_true && m_has_lambda) {
+            m_last_search_failure = LAMBDAS;
+            status = l_undef;
+            return false;
+        }
         inc_limits();
         if (status == l_true || !m_fparams.m_restart_adaptive || m_agility < m_fparams.m_restart_agility_threshold) {
             SASSERT(!inconsistent());
@@ -3765,13 +3770,13 @@ namespace smt {
                 pop_scope(m_scope_lvl - curr_lvl);
                 SASSERT(at_search_level());
             }
-            for (theory* th : m_theory_set) {
+            for (theory* th : m_theory_set) 
-                if (!inconsistent()) th->restart_eh();
+                if (!inconsistent()) 
-            }
+                    th->restart_eh();
+
             TRACE("mbqi_bug_detail", tout << "before instantiating quantifiers...\n";);
-            if (!inconsistent()) {
+            if (!inconsistent()) 
                 m_qmanager->restart_eh();
-            }
             if (inconsistent()) {
                 VERIFY(!resolve_conflict());
                 status = l_false;
@@ -3993,6 +3998,10 @@ namespace smt {
         TRACE("final_check_step", tout << "RESULT final_check: " << result << "\n";);
         if (result == FC_GIVEUP && f != OK)
             m_last_search_failure = f;
+        if (result == FC_DONE && m_has_lambda) {
+            m_last_search_failure = LAMBDAS;
+            result = FC_GIVEUP;
+        }
         return result;
     }
 

src/smt/smt_context.h

@@ -773,6 +773,7 @@ namespace smt {
 
         void internalize_quantifier(quantifier * q, bool gate_ctx);
 
+        bool m_has_lambda = false;
         void internalize_lambda(quantifier * q);
 
         void internalize_formula_core(app * n, bool gate_ctx);

src/smt/smt_context_pp.cpp

@@ -56,6 +56,8 @@ namespace smt {
             return out;
         case QUANTIFIERS:
             return out << "QUANTIFIERS";
+        case LAMBDAS:
+            return out << "LAMBDAS";
         }
         UNREACHABLE();
         return out << "?";
@@ -79,6 +81,7 @@ namespace smt {
         }
         case RESOURCE_LIMIT: r = "(resource limits reached)"; break;
         case QUANTIFIERS: r = "(incomplete quantifiers)"; break;
+        case LAMBDAS: r = "(incomplete lambdas)"; break;
         case UNKNOWN: r = m_unknown; break;
         }
         return r;

src/smt/smt_failure.h

@@ -31,6 +31,7 @@ namespace smt {
         NUM_CONFLICTS, //!< Maximum number of conflicts was reached
         THEORY,        //!< Theory is incomplete
         RESOURCE_LIMIT,
+        LAMBDAS,       //!< Logical context contains lambdas.
         QUANTIFIERS    //!< Logical context contains universal quantifiers.
     };
 

src/smt/smt_internalizer.cpp

@@ -605,6 +605,8 @@ namespace smt {
         bool_var bv = get_bool_var(fa);
         assign(literal(bv, false), nullptr);
         mark_as_relevant(bv);
+        push_trail(value_trail<bool>(m_has_lambda));
+        m_has_lambda = true;
     }
 
     /**

src/smt/theory_array_full.cpp

@@ -793,7 +793,6 @@ namespace smt {
             app_ref sel1(m), sel2(m);
             sel1 = mk_select(args1);
             sel2 = mk_select(args2);
-            std::cout << "small domain " << sel1 << " " << sel2 << "\n";
             is_new = try_assign_eq(sel1, sel2);
 #endif
         }

src/tactic/arith/lia2card_tactic.cpp

@@ -216,11 +216,10 @@ public:
             }
             // IF_VERBOSE(0, verbose_stream() << mk_pp(g->form(i), m) << "\n--->\n" << new_curr << "\n";);
             g->update(i, new_curr, new_pr, g->dep(i));
-
         }
-        for (expr* a : axioms) {
+        for (expr* a : axioms) 
             g->assert_expr(a);
-        }
+
         if (m_mc) g->add(m_mc.get());
         g->inc_depth();
         result.push_back(g.get());