From 1d199b707b084b3a677485a2ea3e9fdfd8794fa4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 29 Sep 2020 23:51:09 -0700 Subject: [PATCH] connect mbi Signed-off-by: Nikolaj Bjorner --- src/sat/smt/euf_solver.cpp | 19 ++++++- src/sat/smt/euf_solver.h | 4 +- src/sat/smt/q_mbi.cpp | 49 ++++++++++++++----- src/sat/smt/q_mbi.h | 3 ++ src/sat/smt/q_solver.cpp | 17 +++++-- src/sat/smt/q_solver.h | 4 +- src/solver/solver.h | 2 + src/tactic/portfolio/smt_strategic_solver.cpp | 3 ++ 8 files changed, 82 insertions(+), 19 deletions(-) diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index de60726db..bb5d9d4a1 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -23,6 +23,7 @@ Author: #include "sat/smt/bv_solver.h" #include "sat/smt/euf_solver.h" #include "sat/smt/array_solver.h" +#include "sat/smt/q_solver.h" namespace euf { @@ -67,10 +68,24 @@ namespace euf { th_solver* solver::expr2solver(expr* e) { if (is_app(e)) - return func_decl2solver(to_app(e)->get_decl()); + return func_decl2solver(to_app(e)->get_decl()); + if (is_forall(e) || is_exists(e)) + return quantifier2solver(); return nullptr; } + th_solver* solver::quantifier2solver() { + family_id fid = m.mk_family_id(q::solver::name()); + auto* ext = m_id2solver.get(fid, nullptr); + if (ext) + return ext; + ext = alloc(q::solver, *this); + ext->set_solver(m_solver); + ext->push_scopes(s().num_scopes()); + add_solver(fid, ext); + return ext; + } + th_solver* solver::get_solver(family_id fid, func_decl* f) { if (fid == null_family_id) return nullptr; @@ -122,6 +137,8 @@ namespace euf { void solver::init_search() { TRACE("before_search", s().display(tout);); + for (auto* s : m_solvers) + s->init_search(); } bool solver::is_external(bool_var v) { diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index 844f0acb6..44b3dae9c 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -111,7 +111,7 @@ namespace euf { bool visit(expr* e) override; bool visited(expr* e) override; bool post_visit(expr* e, bool sign, bool root) override; - sat::literal attach_lit(sat::literal lit, expr* e); + void add_distinct_axiom(app* e, euf::enode* const* args); void add_not_distinct_axiom(app* e, euf::enode* const* args); void axiomatize_basic(enode* n); @@ -129,6 +129,7 @@ namespace euf { th_solver* get_solver(family_id fid, func_decl* f); th_solver* sort2solver(sort* s) { return get_solver(s->get_family_id(), nullptr); } th_solver* func_decl2solver(func_decl* f) { return get_solver(f->get_family_id(), f); } + th_solver* quantifier2solver(); th_solver* expr2solver(expr* e); th_solver* bool_var2solver(sat::bool_var v); th_solver* fid2solver(family_id fid) const { return m_id2solver.get(fid, nullptr); } @@ -287,6 +288,7 @@ namespace euf { expr_ref mk_eq(euf::enode* n1, euf::enode* n2) { return mk_eq(n1->get_expr(), n2->get_expr()); } euf::enode* mk_enode(expr* e, unsigned n, enode* const* args) { return m_egraph.mk(e, n, args); } expr* bool_var2expr(sat::bool_var v) { return m_var2expr.get(v, nullptr); } + sat::literal attach_lit(sat::literal lit, expr* e); void unhandled_function(func_decl* f); th_rewriter& get_rewriter() { return m_rewriter; } bool is_shared(euf::enode* n) const; diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp index dd9cb53c0..ad3ba5723 100644 --- a/src/sat/smt/q_mbi.cpp +++ b/src/sat/smt/q_mbi.cpp @@ -64,8 +64,7 @@ namespace q { expr_ref mbqi::replace_model_value(expr* e) { if (m.is_model_value(e)) { register_value(e); - expr_ref r(e, m); - return r; + return expr_ref(e, m); } if (is_app(e) && to_app(e)->get_num_args() > 0) { expr_ref_vector args(m); @@ -98,16 +97,35 @@ namespace q { return r; if (r == l_false) return l_true; - model_ref mdl; - m_solver->get_model(mdl); - expr_ref proj = project(*mdl, q, vars); - if (!proj) - return l_undef; - if (is_forall(q)) - qs.add_clause(~ctx.expr2literal(q), ctx.b_internalize(proj)); - else - qs.add_clause(ctx.expr2literal(q), ~ctx.b_internalize(proj)); - return l_true; + model_ref mdl0, mdl1; + m_solver->get_model(mdl0); + expr_ref proj(m); + auto add_projection = [&](model& mdl) { + proj = project(*mdl1, q, vars); + if (!proj) + return; + if (is_forall(q)) + qs.add_clause(~ctx.expr2literal(q), ctx.b_internalize(proj)); + else + qs.add_clause(ctx.expr2literal(q), ~ctx.b_internalize(proj)); + }; + bool added = false; +#if 0 + restrict_vars_to_instantiation_sets(mdl0, q, vars); + for (unsigned i = 0; i < m_max_cex && l_true == m_solver->check_sat(0, nullptr); ++i) { + m_solver->get_model(mdl1); + add_projection(*mdl1); + if (!proj) + break; + added = true; + m_solver->assert_expr(m.mk_not(proj)); + } +#endif + if (!added) { + add_projection(*mdl0); + added = proj; + } + return added ? l_false : l_undef; } expr_ref mbqi::specialize(quantifier* q, expr_ref_vector& vars) { @@ -181,6 +199,7 @@ namespace q { break; } } + m_max_cex += ctx.get_config().m_mbqi_max_cexs; return result; } @@ -193,7 +212,11 @@ namespace q { void mbqi::init_solver() { if (!m_solver) - m_solver = ctx.mk_solver(); + m_solver = mk_smt2_solver(m, ctx.s().params()); + } + + void mbqi::init_search() { + m_max_cex = ctx.get_config().m_mbqi_max_cexs; } } diff --git a/src/sat/smt/q_mbi.h b/src/sat/smt/q_mbi.h index 17dad0bfc..1fe507dc7 100644 --- a/src/sat/smt/q_mbi.h +++ b/src/sat/smt/q_mbi.h @@ -36,6 +36,7 @@ namespace q { obj_map*> m_fresh; scoped_ptr_vector> m_values; expr_ref_vector m_fresh_trail; + unsigned m_max_cex{ 10 }; void restrict_to_universe(expr * sk, ptr_vector const & universe); void register_value(expr* e); @@ -53,6 +54,8 @@ namespace q { mbqi(euf::solver& ctx, solver& s); lbool operator()(); + + void init_search(); }; } diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp index 1f25d52f8..343e5b2ae 100644 --- a/src/sat/smt/q_solver.cpp +++ b/src/sat/smt/q_solver.cpp @@ -25,7 +25,7 @@ Author: namespace q { solver::solver(euf::solver& ctx): - th_euf_solver(ctx, ctx.get_manager().get_family_id("quant")), + th_euf_solver(ctx, ctx.get_manager().get_family_id(name())), m_mbqi(ctx, *this) {} @@ -38,7 +38,7 @@ namespace q { } else { // universal force - add_clause(~l, uskolemize(to_quantifier(e))); +// add_clause(~l, uskolemize(to_quantifier(e))); ctx.push_vec(m_universal, l); } } @@ -106,5 +106,16 @@ namespace q { NOT_IMPLEMENTED_YET(); return sat::null_literal; } - + + void solver::init_search() { + m_mbqi.init_search(); + } + + sat::literal solver::internalize(expr* e, bool sign, bool root, bool learned) { + SASSERT(is_forall(e) || is_exists(e)); + sat::bool_var v = ctx.get_si().add_bool_var(e); + sat::literal lit = ctx.attach_lit(sat::literal(v, sign), e); + mk_var(ctx.get_egraph().find(e)); + return lit; + } } diff --git a/src/sat/smt/q_solver.h b/src/sat/smt/q_solver.h index 5fe9f8946..e4662d6aa 100644 --- a/src/sat/smt/q_solver.h +++ b/src/sat/smt/q_solver.h @@ -51,6 +51,7 @@ namespace q { solver(euf::solver& ctx); ~solver() override {} + static char const* name() { return "quant"; } bool is_external(sat::bool_var v) override { return false; } void get_antecedents(sat::literal l, sat::ext_justification_idx idx, sat::literal_vector& r, bool probing) override {} void asserted(sat::literal l) override; @@ -62,9 +63,10 @@ namespace q { void collect_statistics(statistics& st) const override; euf::th_solver* clone(sat::solver* s, euf::solver& ctx) override; bool unit_propagate() override; - sat::literal internalize(expr* e, bool sign, bool root, bool learned) override { UNREACHABLE(); return sat::null_literal; } + sat::literal internalize(expr* e, bool sign, bool root, bool learned) override; void internalize(expr* e, bool redundant) override { UNREACHABLE(); } euf::theory_var mk_var(euf::enode* n) override; + void init_search() override; ast_manager& get_manager() { return m; } }; diff --git a/src/solver/solver.h b/src/solver/solver.h index 9d7ecd690..0ab8be126 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -34,6 +34,8 @@ public: solver_factory * mk_smt_strategic_solver_factory(symbol const & logic = symbol::null); +solver* mk_smt2_solver(ast_manager& m, params_ref const& p); + /** \brief Abstract interface for making solvers available in the Z3 API and front-ends such as SMT 2.0 and (legacy) SMT 1.0. diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index 1704e9802..f85dbca15 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -168,3 +168,6 @@ solver_factory * mk_smt_strategic_solver_factory(symbol const & logic) { return alloc(smt_strategic_solver_factory, logic); } +solver* mk_smt2_solver(ast_manager& m, params_ref const& p) { + return mk_inc_sat_solver(m, p); +}