From 9ba76a13326641dff18e52343617e852a278edb8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 13 Jun 2018 14:43:38 -0700 Subject: [PATCH] fixing eufi Signed-off-by: Nikolaj Bjorner --- src/cmd_context/extra_cmds/dbg_cmds.cpp | 12 ++++-- src/qe/qe_arith.cpp | 16 ++------ src/qe/qe_mbi.cpp | 50 +++++++++++++------------ src/qe/qe_mbi.h | 31 ++++++++++----- src/qe/qe_term_graph.cpp | 6 ++- 5 files changed, 64 insertions(+), 51 deletions(-) diff --git a/src/cmd_context/extra_cmds/dbg_cmds.cpp b/src/cmd_context/extra_cmds/dbg_cmds.cpp index d45cb9df9..64eeac42e 100644 --- a/src/cmd_context/extra_cmds/dbg_cmds.cpp +++ b/src/cmd_context/extra_cmds/dbg_cmds.cpp @@ -435,7 +435,9 @@ public: sB->assert_expr(b); qe::prop_mbi_plugin pA(sA.get()); qe::prop_mbi_plugin pB(sB.get()); - lbool res = mbi.pingpong(pA, pB, vars, itp); + pA.set_shared(vars); + pB.set_shared(vars); + lbool res = mbi.pingpong(pA, pB, itp); ctx.regular_stream() << res << " " << itp << "\n"; } }; @@ -485,9 +487,11 @@ public: sNotA->assert_expr(m.mk_not(a)); sB->assert_expr(b); sNotB->assert_expr(m.mk_not(b)); - qe::euf_mbi_plugin pA(sA.get(), sNotA.get()); - qe::euf_mbi_plugin pB(sB.get(), sNotB.get()); - lbool res = mbi.pogo(pA, pB, vars, itp); + qe::euf_arith_mbi_plugin pA(sA.get(), sNotA.get()); + qe::euf_arith_mbi_plugin pB(sB.get(), sNotB.get()); + pA.set_shared(vars); + pB.set_shared(vars); + lbool res = mbi.pogo(pA, pB, itp); ctx.regular_stream() << res << " " << itp << "\n"; } }; diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp index 1709711d7..cd11d4635 100644 --- a/src/qe/qe_arith.cpp +++ b/src/qe/qe_arith.cpp @@ -257,7 +257,7 @@ namespace qe { }; bool is_arith(expr* e) { - return a.is_int(e) || a.is_real(e); + return a.is_int_real(e); } rational n_sign(rational const& b) { @@ -276,7 +276,7 @@ namespace qe { bool operator()(model& model, app* v, app_ref_vector& vars, expr_ref_vector& lits) { app_ref_vector vs(m); vs.push_back(v); - (*this)(model, vs, lits); + project(model, vs, lits, false); return vs.empty(); } @@ -284,14 +284,6 @@ namespace qe { typedef opt::model_based_opt::row row; typedef vector vars; - vector project(model& model, app_ref_vector& vars, expr_ref_vector& lits) { - return project(model, vars, lits, true); - } - - void operator()(model& model, app_ref_vector& vars, expr_ref_vector& fmls) { - project(model, vars, fmls, false); - } - expr_ref var2expr(ptr_vector const& index2expr, var const& v) { expr_ref t(index2expr[v.m_id], m); if (!v.m_coeff.is_one()) { @@ -581,11 +573,11 @@ namespace qe { } void arith_project_plugin::operator()(model& model, app_ref_vector& vars, expr_ref_vector& lits) { - (*m_imp)(model, vars, lits); + m_imp->project(model, vars, lits, false); } vector arith_project_plugin::project(model& model, app_ref_vector& vars, expr_ref_vector& lits) { - return m_imp->project(model, vars, lits); + return m_imp->project(model, vars, lits, true); } void arith_project_plugin::set_check_purified(bool check_purified) { diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp index 20eaf9675..e3bd5e17f 100644 --- a/src/qe/qe_mbi.cpp +++ b/src/qe/qe_mbi.cpp @@ -87,9 +87,9 @@ Notes: namespace qe { - lbool mbi_plugin::check(func_decl_ref_vector const& vars, expr_ref_vector& lits, model_ref& mdl) { + lbool mbi_plugin::check(expr_ref_vector& lits, model_ref& mdl) { while (true) { - switch ((*this)(vars, lits, mdl)) { + switch ((*this)(lits, mdl)) { case mbi_sat: return l_true; case mbi_unsat: @@ -106,12 +106,11 @@ namespace qe { // ------------------------------- // prop_mbi - prop_mbi_plugin::prop_mbi_plugin(solver* s): m_solver(s) {} + prop_mbi_plugin::prop_mbi_plugin(solver* s): mbi_plugin(s->get_manager()), m_solver(s) {} // sketch of propositional - mbi_result prop_mbi_plugin::operator()(func_decl_ref_vector const& vars, expr_ref_vector& lits, model_ref& mdl) { - ast_manager& m = lits.m(); + mbi_result prop_mbi_plugin::operator()(expr_ref_vector& lits, model_ref& mdl) { lbool r = m_solver->check_sat(lits); switch (r) { case l_false: @@ -123,7 +122,7 @@ namespace qe { lits.reset(); for (unsigned i = 0, sz = mdl->get_num_constants(); i < sz; ++i) { func_decl* c = mdl->get_constant(i); - if (vars.contains(c)) { + if (m_shared.contains(c)) { if (m.is_true(mdl->get_const_interp(c))) { lits.push_back(m.mk_const(c)); } @@ -161,7 +160,7 @@ namespace qe { }; euf_mbi_plugin::euf_mbi_plugin(solver* s, solver* sNot): - m(s->get_manager()), + mbi_plugin(s->get_manager()), m_atoms(m), m_solver(s), m_dual_solver(sNot) { @@ -178,7 +177,7 @@ namespace qe { } } - mbi_result euf_mbi_plugin::operator()(func_decl_ref_vector const& vars, expr_ref_vector& lits, model_ref& mdl) { + mbi_result euf_mbi_plugin::operator()(expr_ref_vector& lits, model_ref& mdl) { lbool r = m_solver->check_sat(lits); switch (r) { case l_false: @@ -208,7 +207,7 @@ namespace qe { m_dual_solver->get_unsat_core(core); TRACE("qe", tout << "core: " << core << "\n";); // project the implicant onto vars - tg.set_vars(vars, false); + tg.set_vars(m_shared, false); tg.add_lits(core); lits.reset(); lits.append(tg.project(*mdl)); @@ -260,12 +259,13 @@ namespace qe { app_ref_vector& m_vars; arith_util arith; obj_hashtable m_exclude; - is_arith_var_proc(app_ref_vector& vars, func_decl_ref_vector const& excl): + is_arith_var_proc(app_ref_vector& vars, func_decl_ref_vector const& shared): m(vars.m()), m_vars(vars), arith(m) { - for (func_decl* f : excl) m_exclude.insert(f); + for (func_decl* f : shared) m_exclude.insert(f); } void operator()(app* a) { - if (arith.is_int_real(a) && a->get_family_id() != a->get_family_id() && !m_exclude.contains(a->get_decl())) { + TRACE("qe", tout << expr_ref(a, m) << " " << arith.is_int_real(a) << " " << a->get_family_id() << "\n";); + if (arith.is_int_real(a) && a->get_family_id() != arith.get_family_id() && !m_exclude.contains(a->get_decl())) { m_vars.push_back(a); } } @@ -274,7 +274,7 @@ namespace qe { }; euf_arith_mbi_plugin::euf_arith_mbi_plugin(solver* s, solver* sNot): - m(s->get_manager()), + mbi_plugin(s->get_manager()), m_atoms(m), m_solver(s), m_dual_solver(sNot) { @@ -291,13 +291,9 @@ namespace qe { } } - mbi_result euf_arith_mbi_plugin::operator()(func_decl_ref_vector const& vars, expr_ref_vector& lits, model_ref& mdl) { + mbi_result euf_arith_mbi_plugin::operator()(expr_ref_vector& lits, model_ref& mdl) { lbool r = m_solver->check_sat(lits); - // populate set of arithmetic variables to be projected. - app_ref_vector avars(m); - is_arith_var_proc _proc(avars, vars); - for (expr* l : lits) quick_for_each_expr(_proc, l); switch (r) { case l_false: lits.reset(); @@ -328,6 +324,11 @@ namespace qe { lits.reset(); lits.append(core); arith_util a(m); + // populate set of arithmetic variables to be projected. + app_ref_vector avars(m); + is_arith_var_proc _proc(avars, m_shared); + for (expr* l : lits) quick_for_each_expr(_proc, l); + TRACE("qe", tout << "vars: " << avars << " lits: " << lits << "\n";); // 1. project arithmetic variables using mdl that satisfies core. // ground any remaining arithmetic variables using model. @@ -339,9 +340,10 @@ namespace qe { for (auto const& def : defs) { lits.push_back(m.mk_eq(def.var, def.term)); } + TRACE("qe", tout << "# arith defs" << defs.size() << " avars: " << avars << " " << lits << "\n";); // 3. Project the remaining literals with respect to EUF. - tg.set_vars(vars, false); + tg.set_vars(m_shared, false); tg.add_lits(lits); lits.reset(); lits.append(tg.project(*mdl)); @@ -375,7 +377,7 @@ namespace qe { * ping-pong interpolation of Gurfinkel & Vizel * compute a binary interpolant. */ - lbool interpolator::pingpong(mbi_plugin& a, mbi_plugin& b, func_decl_ref_vector const& vars, expr_ref& itp) { + lbool interpolator::pingpong(mbi_plugin& a, mbi_plugin& b, expr_ref& itp) { model_ref mdl; expr_ref_vector lits(m); bool turn = true; @@ -389,7 +391,7 @@ namespace qe { while (true) { auto* t1 = turn ? &a : &b; auto* t2 = turn ? &b : &a; - mbi_result next_res = (*t1)(vars, lits, mdl); + mbi_result next_res = (*t1)(lits, mdl); switch (next_res) { case mbi_sat: if (last_res == mbi_sat) { @@ -429,14 +431,14 @@ namespace qe { * One-sided pogo creates clausal interpolants. * It creates a set of consequences of b that are inconsistent with a. */ - lbool interpolator::pogo(mbi_plugin& a, mbi_plugin& b, func_decl_ref_vector const& vars, expr_ref& itp) { + lbool interpolator::pogo(mbi_plugin& a, mbi_plugin& b, expr_ref& itp) { expr_ref_vector lits(m), itps(m); while (true) { model_ref mdl; lits.reset(); - switch (a.check(vars, lits, mdl)) { + switch (a.check(lits, mdl)) { case l_true: - switch (b.check(vars, lits, mdl)) { + switch (b.check(lits, mdl)) { case l_true: return l_true; case l_false: diff --git a/src/qe/qe_mbi.h b/src/qe/qe_mbi.h index 6d0d8dcf6..e0e2021d8 100644 --- a/src/qe/qe_mbi.h +++ b/src/qe/qe_mbi.h @@ -29,8 +29,21 @@ namespace qe { }; class mbi_plugin { + protected: + ast_manager& m; + func_decl_ref_vector m_shared; public: + mbi_plugin(ast_manager& m): m(m), m_shared(m) {} virtual ~mbi_plugin() {} + + /** + * Set the shared symbols. + */ + virtual void set_shared(func_decl_ref_vector const& vars) { + m_shared.reset(); + m_shared.append(vars); + } + /** * \brief Utility that works modulo a background state. * - vars @@ -50,7 +63,7 @@ namespace qe { * - mbi_undef: * inconclusive, */ - virtual mbi_result operator()(func_decl_ref_vector const& vars, expr_ref_vector& lits, model_ref& mdl) = 0; + virtual mbi_result operator()(expr_ref_vector& lits, model_ref& mdl) = 0; /** * \brief Block conjunction of lits from future mbi_augment or mbi_sat. @@ -60,7 +73,7 @@ namespace qe { /** * \brief perform a full check, consume internal auguments if necessary. */ - lbool check(func_decl_ref_vector const& vars, expr_ref_vector& lits, model_ref& mdl); + lbool check(expr_ref_vector& lits, model_ref& mdl); }; @@ -69,12 +82,11 @@ namespace qe { public: prop_mbi_plugin(solver* s); ~prop_mbi_plugin() override {} - mbi_result operator()(func_decl_ref_vector const& vars, expr_ref_vector& lits, model_ref& mdl) override; + mbi_result operator()(expr_ref_vector& lits, model_ref& mdl) override; void block(expr_ref_vector const& lits) override; }; class euf_mbi_plugin : public mbi_plugin { - ast_manager& m; expr_ref_vector m_atoms; solver_ref m_solver; solver_ref m_dual_solver; @@ -82,12 +94,11 @@ namespace qe { public: euf_mbi_plugin(solver* s, solver* sNot); ~euf_mbi_plugin() override {} - mbi_result operator()(func_decl_ref_vector const& vars, expr_ref_vector& lits, model_ref& mdl) override; + mbi_result operator()(expr_ref_vector& lits, model_ref& mdl) override; void block(expr_ref_vector const& lits) override; }; - class euf_arith_mbi_plugin : mbi_plugin { - ast_manager& m; + class euf_arith_mbi_plugin : public mbi_plugin { expr_ref_vector m_atoms; solver_ref m_solver; solver_ref m_dual_solver; @@ -96,7 +107,7 @@ namespace qe { public: euf_arith_mbi_plugin(solver* s, solver* sNot); ~euf_arith_mbi_plugin() override {} - mbi_result operator()(func_decl_ref_vector const& vars, expr_ref_vector& lits, model_ref& mdl) override; + mbi_result operator()(expr_ref_vector& lits, model_ref& mdl) override; void block(expr_ref_vector const& lits) override; }; @@ -107,8 +118,8 @@ namespace qe { ast_manager& m; public: interpolator(ast_manager& m):m(m) {} - lbool pingpong(mbi_plugin& a, mbi_plugin& b, func_decl_ref_vector const& vars, expr_ref& itp); - lbool pogo(mbi_plugin& a, mbi_plugin& b, func_decl_ref_vector const& vars, expr_ref& itp); + lbool pingpong(mbi_plugin& a, mbi_plugin& b, expr_ref& itp); + lbool pogo(mbi_plugin& a, mbi_plugin& b, expr_ref& itp); }; }; diff --git a/src/qe/qe_term_graph.cpp b/src/qe/qe_term_graph.cpp index 467a0cc48..ac68516c3 100644 --- a/src/qe/qe_term_graph.cpp +++ b/src/qe/qe_term_graph.cpp @@ -761,11 +761,15 @@ namespace qe { val2rep.insert(val, rep); } } + // TBD: this ignores types, need one use of 'distinct' per sort. + // TBD: probably ignore distinct on values + // TBD: ignore distinct on Booleans ptr_buffer reps; for (auto &kv : val2rep) { reps.push_back(kv.m_value); + std::cout << mk_pp(kv.m_value, m) << "\n"; } - res.push_back(m.mk_distinct(reps.size(), reps.c_ptr())); + // res.push_back(m.mk_distinct(reps.size(), reps.c_ptr())); } public: