diff --git a/src/ast/rewriter/expr_safe_replace.cpp b/src/ast/rewriter/expr_safe_replace.cpp index 9b67f5b5b..362384d2c 100644 --- a/src/ast/rewriter/expr_safe_replace.cpp +++ b/src/ast/rewriter/expr_safe_replace.cpp @@ -37,6 +37,8 @@ void expr_safe_replace::insert(expr* src, expr* dst) { } void expr_safe_replace::operator()(expr_ref_vector& es) { + if (empty()) + return; expr_ref val(m); for (unsigned i = 0; i < es.size(); ++i) { (*this)(es.get(i), val); @@ -65,6 +67,10 @@ expr* expr_safe_replace::cache_find(expr* a) { void expr_safe_replace::operator()(expr* e, expr_ref& res) { + if (empty()) { + res = e; + return; + } m_todo.push_back(e); expr* a, *b; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 0af1a3548..a280ee94d 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -3523,6 +3523,12 @@ namespace sat { } void solver::shrink_vars(unsigned v) { + unsigned j = 0; + for (bool_var w : m_free_vars) + if (w < v) + m_free_vars[j++] = w; + m_free_vars.shrink(j); + for (bool_var i = v; i < m_justification.size(); ++i) { m_case_split_queue.del_var_eh(i); m_probing.reset_cache(literal(i, true)); diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index 875b940a3..cfe7cbe31 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -1126,27 +1126,24 @@ namespace arith { void solver::set_conflict_or_lemma(literal_vector const& core, bool is_conflict) { reset_evidence(); m_core.append(core); - TRACE("arith", - tout << "Core - " << is_conflict << "\n"; - for (literal c : m_core) tout << literal2expr(c) << "\n";); ++m_num_conflicts; ++m_stats.m_conflicts; for (auto const& ev : m_explanation) set_evidence(ev.ci(), m_core, m_eqs); + TRACE("arith", + tout << "Lemma - " << (is_conflict ? "conflict" : "propagation") << "\n"; + for (literal c : m_core) tout << literal2expr(c) << "\n"; + for (auto p : m_eqs) tout << ctx.bpp(p.first) << " == " << ctx.bpp(p.second) << "\n";); DEBUG_CODE( if (is_conflict) { for (literal c : m_core) VERIFY(s().value(c) == l_true); for (auto p : m_eqs) VERIFY(p.first->get_root() == p.second->get_root()); }); for (auto const& eq : m_eqs) - m_core.push_back(eq_internalize(eq.first, eq.second)); + m_core.push_back(ctx.mk_literal(m.mk_eq(eq.first->get_expr(), eq.second->get_expr()))); for (literal& c : m_core) c.neg(); - TRACE("arith", display(tout << "is-conflict: " << is_conflict << "\n"); - tout << "Clause\n"; - for (literal c : m_core) tout << literal2expr(c) << "\n"; - ); add_clause(m_core); } diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp index 234f57a3c..95a475788 100644 --- a/src/sat/smt/euf_model.cpp +++ b/src/sat/smt/euf_model.cpp @@ -38,8 +38,13 @@ namespace euf { mdl->register_usort(kv.m_key, kv.m_value->size(), kv.m_value->c_ptr()); } - void add(unsigned id, sort* srt) { - expr_ref value(factory.get_fresh_value(srt), m); + void add(enode* r, sort* srt) { + unsigned id = r->get_expr_id(); + expr_ref value(m); + if (m.is_value(r->get_expr())) + value = r->get_expr(); + else + value = factory.get_fresh_value(srt); values.set(id, value); expr_ref_vector* vals = nullptr; if (!sort2values.find(srt, vals)) { @@ -58,9 +63,9 @@ namespace euf { void solver::update_model(model_ref& mdl) { for (auto* mb : m_solvers) mb->init_model(); - deps_t deps; m_values.reset(); m_values2root.reset(); + deps_t deps; user_sort us(*this, m_values, mdl); collect_dependencies(us, deps); deps.topological_sort(); @@ -142,13 +147,9 @@ namespace euf { } continue; } - if (m.is_value(n->get_root()->get_expr())) { - m_values.set(id, n->get_root()->get_expr()); - continue; - } sort* srt = m.get_sort(e); if (m.is_uninterp(srt)) - us.add(id, srt); + us.add(n->get_root(), srt); else if (auto* mbS = sort2solver(srt)) mbS->add_value(n, *mdl, m_values); else if (auto* mbE = expr2solver(e)) diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp index 066c24ddd..1ba985fbf 100644 --- a/src/sat/smt/q_mbi.cpp +++ b/src/sat/smt/q_mbi.cpp @@ -35,8 +35,7 @@ namespace q { ctx(ctx), m_qs(s), m(s.get_manager()), - m_model_fixer(ctx, m_qs), - m_fresh_trail(m) { + m_model_fixer(ctx, m_qs) { auto* ap = alloc(mbp::arith_project_plugin, m); ap->set_check_purified(false); ap->set_apply_projection(true); @@ -50,34 +49,16 @@ namespace q { expr_ref_vector eqs(m); for (expr* e : universe) eqs.push_back(m.mk_eq(sk, e)); - expr_ref fml(m.mk_or(eqs), m); + expr_ref fml = mk_or(eqs); + std::cout << "restrict to universe " << fml << "\n"; m_solver->assert_expr(fml); } - void mbqi::register_value(expr* e) { - sort* s = m.get_sort(e); - obj_hashtable* values = nullptr; - if (!m_fresh.find(s, values)) { - values = alloc(obj_hashtable); - m_fresh.insert(s, values); - m_values.push_back(values); - } - if (!values->contains(e)) { - for (expr* b : *values) - m_qs.add_unit(~m_qs.eq_internalize(e, b)); - values->insert(e); - m_fresh_trail.push_back(e); - } - } - - // sort -> [ value -> expr ] - // for fixed value return expr - // new fixed value is distinct from other expr expr_ref mbqi::replace_model_value(expr* e) { - if (m.is_model_value(e)) { - register_value(e); - return expr_ref(e, m); - } + auto const& v2r = ctx.values2root(); + euf::enode* r = nullptr; + if (v2r.find(e, r)) + return choose_term(r); if (is_app(e) && to_app(e)->get_num_args() > 0) { expr_ref_vector args(m); for (expr* arg : *to_app(e)) @@ -101,11 +82,14 @@ namespace q { quantifier* q_flat = m_qs.flatten(q); init_solver(); ::solver::scoped_push _sp(*m_solver); + std::cout << "quantifier\n" << mk_pp(q, m, 4) << "\n"; + // std::cout << *m_model << "\n"; auto* qb = specialize(q_flat); if (!qb) return l_undef; if (m.is_false(qb->mbody)) return l_true; + std::cout << "body\n" << qb->mbody << "\n"; m_solver->assert_expr(qb->mbody); lbool r = m_solver->check_sat(0, nullptr); if (r == l_undef) @@ -122,12 +106,21 @@ namespace q { if (!qb->var_args.empty()) { ::solver::scoped_push _sp(*m_solver); add_domain_eqs(*mdl0, *qb); + std::cout << "check\n"; for (; i < m_max_cex && l_true == m_solver->check_sat(0, nullptr); ++i) { m_solver->get_model(mdl1); proj = solver_project(*mdl1, *qb); if (!proj) break; TRACE("q", tout << "project: " << proj << "\n";); + std::cout << "project\n" << proj << "\n"; + std::cout << *m_model << "\n"; + + static unsigned s_count = 0; + ++s_count; + if (s_count == 3) + exit(0); + ++m_stats.m_num_instantiations; m_qs.add_clause(~qlit, ~ctx.mk_literal(proj)); m_solver->assert_expr(m.mk_not(proj)); } @@ -137,7 +130,9 @@ namespace q { proj = solver_project(*mdl0, *qb); if (!proj) return l_undef; + std::cout << "project-base\n" << proj << "\n"; TRACE("q", tout << "project-base: " << proj << "\n";); + ++m_stats.m_num_instantiations; m_qs.add_clause(~qlit, ~ctx.mk_literal(proj)); } // TODO: add as top-level clause for relevancy @@ -178,59 +173,48 @@ namespace q { return result; } - /** - * A most rudimentary projection operator that only tries to find proxy terms from the set of existing terms. - * Refinements: - * - grammar based from MBQI paper - * - quantifier elimination based on projection operators defined in qe. - * - * - eliminate as-array terms, use lambda - */ - expr_ref mbqi::basic_project(model& mdl, quantifier* q, app_ref_vector& vars) { - unsigned sz = q->get_num_decls(); - expr_ref_vector vals(m); - vals.resize(sz, nullptr); - for (unsigned i = 0; i < sz; ++i) { - app* v = vars.get(i); - vals[i] = assign_value(mdl, v); - if (!vals.get(i)) - return expr_ref(m); - } - var_subst subst(m); - return subst(q->get_expr(), vals); - } - expr_ref mbqi::solver_project(model& mdl, q_body& qb) { + model::scoped_model_completion _sc(mdl, true); for (app* v : qb.vars) m_model->register_decl(v->get_decl(), mdl(v)); expr_ref_vector fmls(qb.vbody); app_ref_vector vars(qb.vars); - fmls.append(qb.domain_eqs); + bool fmls_extracted = false; TRACE("q", - tout << "Project\n"; - tout << *m_model << "\n"; - tout << fmls << "\n"; - tout << "model of projection\n" << mdl << "\n"; - tout << "var args: " << qb.var_args.size() << "\n"; - for (expr* f : fmls) - if (m_model->is_false(f)) - tout << mk_pp(f, m) << " := false\n"; - ); - // - // TBD: need to compute projection based on eliminate_nested_vars, - // but apply it based on original formulas, or add constraints that - // nested variable occurrences are equal to their subsitutions. - // The result may not be a proper projection. - // - eliminate_nested_vars(fmls, qb); - mbp::project_plugin proj(m); - proj.extract_literals(*m_model, vars, fmls); + tout << "Project\n"; + tout << *m_model << "\n"; + tout << fmls << "\n"; + tout << "model of projection\n" << mdl << "\n"; + tout << "var args: " << qb.var_args.size() << "\n"; + for (expr* f : fmls) + if (m_model->is_false(f)) + tout << mk_pp(f, m) << " := false\n"; + tout << "vars: " << vars << "\n";); + + expr_safe_replace rep(m); for (unsigned i = 0; i < vars.size(); ++i) { app* v = vars.get(i); auto* p = get_plugin(v); + if (p && !fmls_extracted) { + fmls.append(qb.domain_eqs); + eliminate_nested_vars(fmls, qb); + mbp::project_plugin proj(m); + proj.extract_literals(*m_model, vars, fmls); + fmls_extracted = true; + } if (p) (*p)(*m_model, vars, fmls); } + for (app* v : vars) { + expr_ref term(m); + expr_ref val = (*m_model)(v); + val = m_model->unfold_as_array(val); + term = replace_model_value(val); + rep.insert(v, term); + if (val != term) + rep.insert(val, term); + } + rep(fmls); return mk_and(fmls); } @@ -253,6 +237,7 @@ namespace q { if (!m_model->eval_expr(bounds, mbounds, true)) return; mbounds = subst(mbounds, qb.vars); + std::cout << "domain eqs " << mbounds << "\n"; m_solver->assert_expr(mbounds); qb.domain_eqs.push_back(vbounds); } @@ -325,23 +310,6 @@ namespace q { } } - expr_ref mbqi::assign_value(model& mdl, app* v) { - func_decl* f = v->get_decl(); - expr_ref val(mdl.get_some_const_interp(f), m); - if (!val) - return expr_ref(m); - val = mdl.unfold_as_array(val); - if (!val) - return expr_ref(m); - euf::enode* r = nullptr; - auto const& v2r = ctx.values2root(); - if (v2r.find(val, r)) - val = choose_term(r); - else - val = replace_model_value(val); - return val; - } - lbool mbqi::operator()() { lbool result = l_true; m_model = nullptr; @@ -401,6 +369,7 @@ 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); } } diff --git a/src/sat/smt/q_mbi.h b/src/sat/smt/q_mbi.h index 49fccbb3c..7e6c80e40 100644 --- a/src/sat/smt/q_mbi.h +++ b/src/sat/smt/q_mbi.h @@ -30,6 +30,15 @@ namespace q { class solver; class mbqi { + struct stats { + unsigned m_num_instantiations; + + stats() { reset(); } + + void reset() { + memset(this, 0, sizeof(*this)); + } + }; struct q_body { app_ref_vector vars; expr_ref mbody; // body specialized with respect to model @@ -42,25 +51,22 @@ namespace q { euf::solver& ctx; solver& m_qs; ast_manager& m; + stats m_stats; model_fixer m_model_fixer; model_ref m_model; ref<::solver> m_solver; - obj_map*> m_fresh; scoped_ptr_vector> m_values; - expr_ref_vector m_fresh_trail; scoped_ptr_vector m_plugins; obj_map m_q2body; unsigned m_max_cex{ 1 }; void restrict_to_universe(expr * sk, ptr_vector const & universe); - void register_value(expr* e); + // void register_value(expr* e); expr_ref replace_model_value(expr* e); expr_ref choose_term(euf::enode* r); lbool check_forall(quantifier* q); q_body* specialize(quantifier* q); - expr_ref basic_project(model& mdl, quantifier* q, app_ref_vector& vars); expr_ref solver_project(model& mdl, q_body& qb); - expr_ref assign_value(model& mdl, app* v); void add_domain_eqs(model& mdl, q_body& qb); void add_domain_bounds(model& mdl, q_body& qb); void eliminate_nested_vars(expr_ref_vector& fmls, q_body& qb); diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp index 588277ab4..243734ca6 100644 --- a/src/sat/smt/q_solver.cpp +++ b/src/sat/smt/q_solver.cpp @@ -35,9 +35,9 @@ namespace q { if (!is_forall(e) && !is_exists(e)) return; if (l.sign() == is_forall(e)) - add_clause(~l, skolemize(to_quantifier(e))); + add_clause(~l, skolemize(to_quantifier(e))); else { - add_clause(~l, specialize(to_quantifier(e))); + // add_clause(~l, specialize(to_quantifier(e))); ctx.push_vec(m_universal, l); } m_stats.m_num_quantifier_asserts++; diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 12e3c09ea..59218f38d 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -63,9 +63,9 @@ namespace smt { \brief Instantiation sets are the S_{k,j} sets in the Complete quantifier instantiation paper. */ class instantiation_set { - ast_manager& m; + ast_manager& m; obj_map m_elems; // and the associated generation - obj_map m_inv; + obj_map m_inv; expr_mark m_visited; public: instantiation_set(ast_manager& m) :m(m) {} @@ -252,11 +252,9 @@ namespace smt { if (r1->m_eqc_size > r2->m_eqc_size) std::swap(r1, r2); r1->m_find = r2; - r2->m_eqc_size += r1->m_eqc_size; - if (r1->m_mono_proj) - r2->m_mono_proj = true; - if (r1->m_signed_proj) - r2->m_signed_proj = true; + r2->m_eqc_size += r1->m_eqc_size; + r2->m_mono_proj |= r1->m_mono_proj; + r2->m_signed_proj |= r1->m_signed_proj; dappend(r2->m_avoid_set, r1->m_avoid_set); dappend(r2->m_exceptions, r1->m_exceptions); } @@ -393,17 +391,17 @@ namespace smt { // This auxiliary constant is used as a "witness" that is asserted as different from a // finite number of terms. // It is only safe to use this constant for infinite sorts. - obj_map m_sort2k; + obj_map m_sort2k; expr_ref_vector m_ks; // range of m_sort2k // Support for evaluating expressions in the current model. - proto_model* m_model{ nullptr }; - obj_map m_eval_cache[2]; + proto_model* m_model{ nullptr }; + obj_map m_eval_cache[2]; expr_ref_vector m_eval_cache_range; ptr_vector m_root_nodes; - expr_ref_vector* m_new_constraints{ nullptr }; + expr_ref_vector* m_new_constraints{ nullptr }; random_gen m_rand;