diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index a3f63a696..cd3253495 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -6646,6 +6646,10 @@ class Solver(Z3PPObject): except Z3Exception: raise Z3Exception("model is not available") + def import_model_converter(self, other): + """Import model converter from other into the current solver""" + Z3_solver_import_model_converter(self.ctx.ref(), other.solver, self.solver) + def unsat_core(self): """Return a subset (as an AST vector) of the assumptions provided to the last check(). @@ -8310,11 +8314,17 @@ def AtLeast(*args): _args, sz = _to_ast_array(args1) return BoolRef(Z3_mk_atleast(ctx.ref(), sz, _args, k), ctx) +def _reorder_pb_arg(arg): + a, b = arg + if not _is_int(b) and _is_int(a): + return b, a + return arg def _pb_args_coeffs(args, default_ctx = None): args = _get_args_ast_list(args) if len(args) == 0: return _get_ctx(default_ctx), 0, (Ast * 0)(), (ctypes.c_int * 0)() + args = [_reorder_pb_arg(arg) for arg in args] args, coeffs = zip(*args) if z3_debug(): _z3_assert(len(args) > 0, "Non empty list of arguments expected") diff --git a/src/api/z3_api.h b/src/api/z3_api.h index 642c959cc..8acf35d2c 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -6213,6 +6213,14 @@ extern "C" { /** \brief Ad-hoc method for importing model conversion from solver. + + This method is used for scenarios where \c src has been used to solve a set + of formulas and was interrupted. The \c dst solver may be a strengthening of \c src + obtained from cubing (assigning a subset of literals or adding constraints over the + assertions available in \c src). If \c dst ends up being satisfiable, the model for \c dst + may not correspond to a model of the original formula due to inprocessing in \c src. + This method is used to take the side-effect of inprocessing into account when returning + a model for \c dst. def_API('Z3_solver_import_model_converter', VOID, (_in(CONTEXT), _in(SOLVER), _in(SOLVER))) */ diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index ddb7df74b..3a951025b 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -23,16 +23,12 @@ Revision History: namespace sat { - model_converter::model_converter(): m_solver(nullptr) { + model_converter::model_converter(): m_solver(nullptr), m_exposed_lim(0) { } model_converter::~model_converter() { - reset(); } - void model_converter::reset() { - m_entries.finalize(); - } model_converter& model_converter::operator=(model_converter const& other) { copy(other); @@ -40,21 +36,19 @@ namespace sat { } bool model_converter::legal_to_flip(bool_var v) const { - // std::cout << "check " << v << " " << m_solver << "\n"; if (m_solver && m_solver->is_assumption(v)) { - std::cout << "flipping assumption v" << v << "\n"; + IF_VERBOSE(0, verbose_stream() << "flipping assumption v" << v << "\n";); UNREACHABLE(); throw solver_exception("flipping assumption"); } if (m_solver && m_solver->is_external(v) && m_solver->is_incremental()) { - std::cout << "flipping external v" << v << "\n"; + IF_VERBOSE(0, verbose_stream() << "flipping external v" << v << "\n";); UNREACHABLE(); throw solver_exception("flipping external"); } return !m_solver || !m_solver->is_assumption(v); } - void model_converter::process_stack(model & m, literal_vector const& c, elim_stackv const& stack) const { SASSERT(!stack.empty()); unsigned sz = stack.size(); @@ -73,46 +67,33 @@ namespace sat { } void model_converter::operator()(model & m) const { - vector::const_iterator begin = m_entries.begin(); - vector::const_iterator it = m_entries.end(); bool first = false; - //SASSERT(!m_solver || m_solver->check_clauses(m)); - while (it != begin) { - --it; - bool_var v0 = it->var(); - SASSERT(it->get_kind() != ELIM_VAR || v0 == null_bool_var || m[v0] == l_undef); - // if it->get_kind() == BCE, then it might be the case that m[v] != l_undef, + literal_vector clause; + for (unsigned i = m_entries.size(); i-- > m_exposed_lim; ) { + entry const& e = m_entries[i]; + bool_var v0 = e.var(); + SASSERT(e.get_kind() != ELIM_VAR || v0 == null_bool_var || m[v0] == l_undef); + // if e.get_kind() == BCE, then it might be the case that m[v] != l_undef, // and the following procedure flips its value. bool sat = false; bool var_sign = false; unsigned index = 0; - literal_vector clause; + clause.reset(); VERIFY(v0 == null_bool_var || legal_to_flip(v0)); - for (literal l : it->m_clauses) { + for (literal l : e.m_clauses) { if (l == null_literal) { // end of clause - if (!sat && it->get_kind() == ATE) { - IF_VERBOSE(0, display(verbose_stream() << "violated ate\n", *it) << "\n"); - IF_VERBOSE(0, for (unsigned v = 0; v < m.size(); ++v) verbose_stream() << v << " := " << m[v] << "\n";); - IF_VERBOSE(0, display(verbose_stream())); - UNREACHABLE(); - first = false; - } - if (!sat && it->get_kind() != ATE && v0 != null_bool_var) { + VERIFY (sat || e.get_kind() != ATE); + if (!sat && e.get_kind() != ATE && v0 != null_bool_var) { VERIFY(legal_to_flip(v0)); m[v0] = var_sign ? l_false : l_true; - //IF_VERBOSE(0, verbose_stream() << "assign " << v0 << " "<< m[v0] << "\n"); } - elim_stack* st = it->m_elim_stack[index]; + elim_stack* st = e.m_elim_stack[index]; if (st) { process_stack(m, clause, st->stack()); } sat = false; - if (first && m_solver && !m_solver->check_clauses(m)) { - IF_VERBOSE(0, display(verbose_stream() << "after processing stack\n", *it) << "\n"); - IF_VERBOSE(0, display(verbose_stream())); - first = false; - } + VERIFY(!first || !m_solver || m_solver->check_clauses(m)); ++index; clause.reset(); continue; @@ -123,7 +104,6 @@ namespace sat { continue; bool sign = l.sign(); bool_var v = l.var(); - if (v >= m.size()) std::cout << v << " model size: " << m.size() << "\n"; VERIFY(v < m.size()); if (v == v0) var_sign = sign; @@ -133,25 +113,21 @@ namespace sat { VERIFY(legal_to_flip(v)); // clause can be satisfied by assigning v. m[v] = sign ? l_false : l_true; - // if (first) std::cout << "set: " << l << "\n"; sat = true; - if (first && m_solver && !m_solver->check_clauses(m)) { - IF_VERBOSE(0, display(verbose_stream() << "after flipping undef\n", *it) << "\n"); - first = false; - } + VERIFY(!first || !m_solver || m_solver->check_clauses(m)); } } DEBUG_CODE({ // all clauses must be satisfied bool sat = false; bool undef = false; - for (literal const& l : it->m_clauses) { + for (literal const& l : e.m_clauses) { if (l == null_literal) { CTRACE("sat", !sat, if (m_solver) m_solver->display(tout); display(tout); for (unsigned v = 0; v < m.size(); ++v) tout << v << ": " << m[v] << "\n"; - for (literal const& l2 : it->m_clauses) { + for (literal const& l2 : e.m_clauses) { if (l2 == null_literal) tout << "\n"; else tout << l2 << " "; if (&l == &l2) break; } @@ -179,24 +155,21 @@ namespace sat { */ bool model_converter::check_model(model const & m) const { bool ok = true; - vector::const_iterator begin = m_entries.begin(); - vector::const_iterator it = m_entries.end(); - while (it != begin) { - --it; + for (entry const & e : m_entries) { bool sat = false; - literal_vector::const_iterator it2 = it->m_clauses.begin(); - literal_vector::const_iterator itbegin = it2; - literal_vector::const_iterator end2 = it->m_clauses.end(); - for (; it2 != end2; ++it2) { - literal l = *it2; + literal_vector::const_iterator it = e.m_clauses.begin(); + literal_vector::const_iterator itbegin = it; + literal_vector::const_iterator end = e.m_clauses.end(); + for (; it != end; ++it) { + literal l = *it; if (l == null_literal) { // end of clause if (!sat) { - TRACE("sat_model_bug", tout << "failed eliminated: " << mk_lits_pp(static_cast(it2 - itbegin), itbegin) << "\n";); + TRACE("sat_model_bug", tout << "failed eliminated: " << mk_lits_pp(static_cast(it - itbegin), itbegin) << "\n";); ok = false; } sat = false; - itbegin = it2; + itbegin = it; itbegin++; continue; } @@ -239,6 +212,16 @@ namespace sat { stackv().reset(); } + void model_converter::set_clause(entry & e, literal l1, literal l2) { + e.m_clause.push_back(l1); + e.m_clause.push_back(l2); + } + + void model_converter::set_clause(entry & e, clause const & c) { + e.m_clause.append(c.size(), c.begin()); + } + + void model_converter::insert(entry & e, clause const & c) { SASSERT(c.contains(e.var())); SASSERT(m_entries.begin() <= &e); @@ -349,27 +332,27 @@ namespace sat { out << l; } out << ")"; - for (literal l : entry.m_clauses) { - if (l != null_literal && l.var() != null_bool_var) { - if (false && m_solver && m_solver->was_eliminated(l.var())) out << "\neliminated: " << l; - } - } return out; } void model_converter::copy(model_converter const & src) { - reset(); + m_entries.reset(); m_entries.append(src.m_entries); + m_exposed_lim = src.m_exposed_lim; } void model_converter::flush(model_converter & src) { VERIFY(this != &src); m_entries.append(src.m_entries); + m_exposed_lim = src.m_exposed_lim; src.m_entries.reset(); + src.m_exposed_lim = 0; } void model_converter::collect_vars(bool_var_set & s) const { - for (entry const & e : m_entries) s.insert(e.m_var); + for (entry const & e : m_entries) { + s.insert(e.m_var); + } } unsigned model_converter::max_var(unsigned min) const { @@ -398,7 +381,8 @@ namespace sat { void model_converter::expand(literal_vector& update_stack) { sat::literal_vector clause; - for (entry const& e : m_entries) { + for (unsigned i = m_exposed_lim; i < m_entries.size(); ++i) { + entry const& e = m_entries[i]; unsigned index = 0; clause.reset(); for (literal l : e.m_clauses) { @@ -427,6 +411,56 @@ namespace sat { } } } + m_exposed_lim = m_entries.size(); + } + + void model_converter::init_search(solver& s) { +#if 0 + unsigned j = 0, k = 0; + literal_vector clause; + for (unsigned i = 0; i < m_entries.size(); ++i) { + entry & e = m_entries[i]; + if (!m_mark[e.var()]) { + m_entries[j++] = e; + if (i < m_exposed_lim) k++; + continue; + } + clause.reset(); + // For covered clauses we record the original clause. The role of m_clauses is to record ALA + // tautologies and are not part of the clause that is removed. + + if (!e.m_clause.empty()) { + clause.append(e.m_clause); + s.mk_clause(clause.size(), clause.c_ptr(), false); + continue; + } + for (literal lit : e.m_clauses) { + if (lit == null_literal) { + s.mk_clause(clause.size(), clause.c_ptr(), false); + clause.reset(); + } + else { + clause.push_back(lit); + } + } + } + m_entries.shrink(j); + m_exposed_lim = k; + for (bool& m : m_mark) { + m = false; + } +#endif + } + + void model_converter::add_clause(unsigned n, literal const* lits) { + if (m_entries.empty()) { + return; + } + // TBD: we just mark variables instead of literals because entries don't have directly literal information. + for (unsigned i = 0; i < n; ++i) { + m_mark.reserve(lits[i].var() + 1); + m_mark[lits[i].var()] = true; + } } }; diff --git a/src/sat/sat_model_converter.h b/src/sat/sat_model_converter.h index 2ca340e5d..585f8c312 100644 --- a/src/sat/sat_model_converter.h +++ b/src/sat/sat_model_converter.h @@ -72,20 +72,25 @@ namespace sat { bool_var m_var; kind m_kind; literal_vector m_clauses; // the different clauses are separated by null_literal + literal_vector m_clause; // original clause in case of CCE sref_vector m_elim_stack; entry(kind k, bool_var v): m_var(v), m_kind(k) {} public: entry(entry const & src): m_var(src.m_var), m_kind(src.m_kind), - m_clauses(src.m_clauses) { + m_clauses(src.m_clauses), + m_clause(src.m_clause) + { m_elim_stack.append(src.m_elim_stack); } bool_var var() const { return m_var; } kind get_kind() const { return m_kind; } }; private: - vector m_entries; + vector m_entries; // entries accumulated during SAT search + unsigned m_exposed_lim; // last entry that was exposed to model converter. + svector m_mark; // literals that are used in asserted clauses. solver const* m_solver; elim_stackv m_elim_stack; @@ -113,6 +118,8 @@ namespace sat { void insert(entry & e, literal l1, literal l2); void insert(entry & e, clause_wrapper const & c); void insert(entry & c, literal_vector const& covered_clause); + void set_clause(entry & e, literal l1, literal l2); + void set_clause(entry & e, clause const & c); void add_ate(literal_vector const& lits); void add_ate(literal l1, literal l2); @@ -121,7 +128,9 @@ namespace sat { bool empty() const { return m_entries.empty(); } unsigned size() const { return m_entries.size(); } - void reset(); + void init_search(solver& s); + void add_clause(unsigned n, literal const* lits); + bool check_invariant(unsigned num_vars) const; void display(std::ostream & out) const; bool check_model(model const & m) const; diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 95d60491c..d918f7459 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -1223,8 +1223,6 @@ namespace sat { } for (unsigned i = idx; i > 0; --i) { literal lit = m_covered_clause[i]; - //s.mark_visited(lit); - //continue; if (!s.is_marked(lit)) continue; clause_ante const& ante = m_covered_antecedent[i]; if (ante.cls()) { @@ -1591,6 +1589,7 @@ namespace sat { } } m_mc.insert(new_entry, m_covered_clause); + m_mc.set_clause(new_entry, c); } void block_covered_binary(watched const& w, literal l1, literal blocked, model_converter::kind k) { @@ -1600,6 +1599,7 @@ namespace sat { TRACE("blocked_clause", tout << "new blocked clause: " << l2 << " " << l1 << "\n";); s.set_learned(l1, l2); m_mc.insert(new_entry, m_covered_clause); + m_mc.set_clause(new_entry, l1, l2); m_queue.decreased(~l2); } diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 722b91b26..b88a3ec3c 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -357,6 +357,9 @@ namespace sat { m_drat.add(m_lemma); } ++m_stats.m_non_learned_generation; + if (!m_searching) { + m_mc.add_clause(num_lits, lits); + } } switch (num_lits) { @@ -1832,8 +1835,8 @@ namespace sat { m_min_core_valid = false; m_min_core.reset(); m_simplifier.init_search(); + m_mc.init_search(*this); TRACE("sat", display(tout);); - } bool solver::should_simplify() const { @@ -4485,13 +4488,14 @@ namespace sat { lbool solver::get_bounded_consequences(literal_vector const& asms, bool_var_vector const& vars, vector& conseq) { bool_var_set unfixed_vars; unsigned num_units = 0, num_iterations = 0; - for (unsigned i = 0; i < vars.size(); ++i) { - unfixed_vars.insert(vars[i]); + for (bool_var v : vars) { + unfixed_vars.insert(v); } TRACE("sat", tout << asms << "\n";); m_antecedents.reset(); pop_to_base_level(); if (inconsistent()) return l_false; + flet _searching(m_searching, true); init_search(); propagate(false); if (inconsistent()) return l_false; diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index f817cb190..9532b4bb4 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -348,7 +348,6 @@ namespace sat { bool limit_reached() { if (!m_rlimit.inc()) { - m_mc.reset(); m_model_is_current = false; TRACE("sat", tout << "canceled\n";); m_reason_unknown = "sat.canceled"; diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index a53ed94a8..884b533cd 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -934,7 +934,6 @@ void sat2goal::mc::flush_smc(sat::solver_core& s, atom2bool_var const& map) { void sat2goal::mc::flush_gmc() { sat::literal_vector updates; m_smc.expand(updates); - m_smc.reset(); if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal"); // now gmc owns the model converter sat::literal_vector clause; diff --git a/src/smt/smt_theory.cpp b/src/smt/smt_theory.cpp index 9fec0e1d3..642c0aca8 100644 --- a/src/smt/smt_theory.cpp +++ b/src/smt/smt_theory.cpp @@ -120,6 +120,9 @@ namespace smt { } literal theory::mk_eq(expr * a, expr * b, bool gate_ctx) { + if (a == b) { + return true_literal; + } context & ctx = get_context(); app * eq = ctx.mk_eq_atom(a, b); TRACE("mk_var_bug", tout << "mk_eq: " << eq->get_id() << " " << a->get_id() << " " << b->get_id() << "\n"; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 64ca608cd..c005a859c 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -268,6 +268,7 @@ theory_seq::theory_seq(ast_manager& m, theory_seq_params const & params): m_params(params), m_rep(m, m_dm), m_reset_cache(false), + m_lts_checked(false), m_eq_id(0), m_find(*this), m_overlap(m), @@ -336,12 +337,16 @@ final_check_status theory_seq::final_check_eh() { ++m_stats.m_solve_eqs; TRACEFIN("solve_eqs"); return FC_CONTINUE; - } + } if (check_contains()) { ++m_stats.m_propagate_contains; TRACEFIN("propagate_contains"); return FC_CONTINUE; } + if (check_lts()) { + TRACEFIN("check_lts"); + return FC_CONTINUE; + } if (solve_nqs(0)) { ++m_stats.m_solve_nqs; TRACEFIN("solve_nqs"); @@ -2147,6 +2152,57 @@ bool theory_seq::check_contains() { } return m_new_propagation || ctx.inconsistent(); } + +bool theory_seq::check_lts() { + context& ctx = get_context(); + if (m_lts.empty() || m_lts_checked) { + return false; + } + unsigned sz = m_lts.size(); + m_trail_stack.push(value_trail(m_lts_checked)); + m_lts_checked = true; + expr* a = nullptr, *b = nullptr, *c = nullptr, *d = nullptr; + bool is_strict1, is_strict2; + for (unsigned i = 0; i + 1 < sz; ++i) { + expr* p1 = m_lts[i]; + VERIFY(m_util.str.is_lt(p1, a, b) || m_util.str.is_le(p1, a, b)); + literal r1 = ctx.get_literal(p1); + if (ctx.get_assignment(r1) == l_false) { + std::swap(a, b); + r1.neg(); + is_strict1 = m_util.str.is_le(p1); + } + else { + is_strict1 = m_util.str.is_lt(p1); + } + for (unsigned j = i + 1; j < sz; ++j) { + expr* p2 = m_lts[j]; + VERIFY(m_util.str.is_lt(p2, c, d) || m_util.str.is_le(p2, c, d)); + literal r2 = ctx.get_literal(p2); + if (ctx.get_assignment(r2) == l_false) { + std::swap(c, d); + r2.neg(); + is_strict2 = m_util.str.is_le(p2); + } + else { + is_strict2 = m_util.str.is_lt(p2); + } + if (ctx.get_enode(b)->get_root() == ctx.get_enode(c)->get_root()) { + + literal eq = (b == c) ? true_literal : mk_eq(b, c, false); + bool is_strict = is_strict1 || is_strict2; + if (is_strict) { + add_axiom(~r1, ~r2, ~eq, mk_literal(m_util.str.mk_lex_lt(a, d))); + } + else { + add_axiom(~r1, ~r2, ~eq, mk_literal(m_util.str.mk_lex_le(a, d))); + } + } + } + } + return true; +} + /* - Eqs = 0 - Diseqs evaluate to false @@ -5491,7 +5547,7 @@ void theory_seq::assign_eh(bool_var v, bool is_true) { // no-op } else if (m_util.str.is_lt(e) || m_util.str.is_le(e)) { - // no-op + m_lts.push_back(e); } else { TRACE("seq", tout << mk_pp(e, m) << "\n";); @@ -5619,6 +5675,7 @@ void theory_seq::push_scope_eh() { m_eqs.push_scope(); m_nqs.push_scope(); m_ncs.push_scope(); + m_lts.push_scope(); m_internal_nth_lim.push_back(m_internal_nth_es.size()); } @@ -5632,6 +5689,7 @@ void theory_seq::pop_scope_eh(unsigned num_scopes) { m_eqs.pop_scope(num_scopes); m_nqs.pop_scope(num_scopes); m_ncs.pop_scope(num_scopes); + m_lts.pop_scope(num_scopes); m_rewrite.reset(); if (ctx.get_base_level() > ctx.get_scope_level() - num_scopes) { m_replay.reset(); @@ -5927,10 +5985,10 @@ void theory_seq::propagate_not_suffix(expr* e) { !(e1 < e2) => e1 = e2 or e2 = empty or e2 = xdz !(e1 < e2) => e1 = e2 or e2 = empty or d < c !(e1 < e2) => e1 = e2 or e1 = xcy + !(e1 = e2) or !(e1 < e2) optional: e1 < e2 or e1 = e2 or e2 < e1 - !(e1 = e2) or !(e1 < e2) !(e1 = e2) or !(e2 < e1) !(e1 < e2) or !(e2 < e1) */ @@ -5962,13 +6020,7 @@ void theory_seq::add_lt_axiom(expr* n) { add_axiom(lt, eq, e1xcy); add_axiom(lt, eq, emp2, ltdc); add_axiom(lt, eq, emp2, e2xdz); - if (e1->get_id() <= e2->get_id()) { - literal gt = mk_literal(m_util.str.mk_lex_lt(e2, e1)); - add_axiom(lt, eq, gt); - add_axiom(~eq, ~lt); - add_axiom(~eq, ~gt); - add_axiom(~lt, ~gt); - } + add_axiom(~eq, ~lt); } /** diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index bfd982279..fd4b59e38 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -328,6 +328,8 @@ namespace smt { scoped_vector m_eqs; // set of current equations. scoped_vector m_nqs; // set of current disequalities. scoped_vector m_ncs; // set of non-contains constraints. + scoped_vector m_lts; // set of asserted str.<, str.<= literals + bool m_lts_checked; unsigned m_eq_id; th_union_find m_find; @@ -460,6 +462,7 @@ namespace smt { bool check_extensionality(); bool check_contains(); + bool check_lts(); bool solve_eqs(unsigned start); bool solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, dependency* dep, unsigned idx); bool simplify_eq(expr_ref_vector& l, expr_ref_vector& r, dependency* dep);