diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index d57cee2a4..e7c9e72ea 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1166,7 +1166,13 @@ namespace opt { out << mk_pp(term, m); app* q = m.mk_fresh_const(out.str().c_str(), m.get_sort(term)); if (!fm) fm = alloc(generic_model_converter, m, "opt"); - m_hard_constraints.push_back(m.mk_eq(q, term)); + if (m_arith.is_int_real(term)) { + m_hard_constraints.push_back(m_arith.mk_ge(q, term)); + m_hard_constraints.push_back(m_arith.mk_le(q, term)); + } + else { + m_hard_constraints.push_back(m.mk_eq(q, term)); + } fm->hide(q); return q; } diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index 5959c4d19..3d0c872df 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -186,6 +186,7 @@ namespace opt { void add_hard_constraint(expr* f, expr* t); void get_hard_constraints(expr_ref_vector& hard); + expr_ref_vector get_hard_constraints() { expr_ref_vector hard(m); get_hard_constraints(hard); return hard; } expr_ref get_objective(unsigned i); void push() override; diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp index 77f910260..b6494ef5f 100644 --- a/src/qe/qe_mbi.cpp +++ b/src/qe/qe_mbi.cpp @@ -38,6 +38,7 @@ Notes: #include "qe/qe_mbi.h" #include "qe/qe_term_graph.h" #include "qe/qe_arith.h" +#include "opt/opt_context.h" namespace qe { @@ -139,6 +140,10 @@ namespace qe { if (m_arith.is_int_real(a)) { m_avars.push_back(a); + if (!m_seen.contains(a)) { + m_proxies.push_back(a); + m_seen.insert(a); + } } for (expr* arg : *a) { if (is_app(arg) && !m_seen.contains(arg) && m_arith.is_int_real(arg)) { @@ -259,27 +264,31 @@ namespace qe { TRACE("qe", tout << m_solver->get_assertions() << "\n";); - // 1. arithmetical variables - atomic and in purified positions + // . arithmetical variables - atomic and in purified positions app_ref_vector proxies(m); app_ref_vector avars = get_arith_vars(mdl, lits, proxies); TRACE("qe", tout << "vars: " << avars << "\nproxies: " << proxies << "\nlits: " << lits << "\n";); - // 2. project private non-arithmetical variables from lits + // . project private non-arithmetical variables from lits project_euf(mdl, lits, avars); - // 3. Order arithmetical variables and purified positions + // . Minimzie span between smallest and largest proxy variable. + minimize_span(mdl, avars, proxies); + + // . Order arithmetical variables and purified positions order_avars(mdl, lits, avars, proxies); TRACE("qe", tout << "ordered: " << lits << "\n";); - // 4. Perform arithmetical projection + // . Perform arithmetical projection arith_project_plugin ap(m); ap.set_check_purified(false); auto defs = ap.project(*mdl.get(), avars, lits); TRACE("qe", tout << "aproject: " << lits << "\n";); - // 5. Substitute solution into lits + // . Substitute solution into lits substitute(defs, lits); TRACE("qe", tout << "substitute: " << lits << "\n";); + IF_VERBOSE(1, verbose_stream() << lits << "\n"); } /** @@ -307,12 +316,7 @@ namespace qe { TRACE("qe", tout << "project: " << lits << "\n";); } - /** - * \brief Order arithmetical variables: - * 1. add literals that order the proxies according to the model. - * 2. sort arithmetical terms, such that deepest terms are first. - */ - void euf_arith_mbi_plugin::order_avars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars, app_ref_vector const& proxies) { + vector> euf_arith_mbi_plugin::sort_proxies(model_ref& mdl, app_ref_vector const& proxies) { arith_util a(m); model_evaluator mev(*mdl.get()); vector> vals; @@ -328,15 +332,61 @@ namespace qe { return x.first < y.first; } }; - // add linear order between proxies + // add offset ordering between proxies compare_first cmp; std::sort(vals.begin(), vals.end(), cmp); + return vals; + } + + void euf_arith_mbi_plugin::minimize_span(model_ref& mdl, app_ref_vector& avars, app_ref_vector const& proxies) { + arith_util a(m); + opt::context opt(m); + expr_ref_vector fmls(m); + m_solver->get_assertions(fmls); + for (expr* l : fmls) opt.add_hard_constraint(l); + vector> vals = sort_proxies(mdl, proxies); + app_ref t(m); for (unsigned i = 1; i < vals.size(); ++i) { - if (vals[i-1].first == vals[i].first) { - lits.push_back(m.mk_eq(vals[i-1].second, vals[i].second)); + rational offset = vals[i].first - vals[i-1].first; + expr* t1 = vals[i-1].second; + expr* t2 = vals[i].second; + if (offset.is_zero()) { + t = m.mk_eq(t1, t2); } else { - lits.push_back(a.mk_lt(vals[i-1].second, vals[i].second)); + SASSERT(offset.is_pos()); + t = a.mk_lt(t1, t2); + } + opt.add_hard_constraint(t); + } + t = a.mk_sub(vals[0].second, vals.back().second); + opt.add_objective(t, true); + expr_ref_vector asms(m); + VERIFY(l_true == opt.optimize(asms)); + opt.get_model(mdl); + model_evaluator mev(*mdl.get()); + std::cout << mev(t) << "\n"; + } + + /** + * \brief Order arithmetical variables: + * 1. add literals that order the proxies according to the model. + * 2. sort arithmetical terms, such that deepest terms are first. + */ + void euf_arith_mbi_plugin::order_avars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars, app_ref_vector const& proxies) { + arith_util a(m); + model_evaluator mev(*mdl.get()); + vector> vals = sort_proxies(mdl, proxies); + for (unsigned i = 1; i < vals.size(); ++i) { + rational offset = vals[i].first - vals[i-1].first; + expr* t1 = vals[i-1].second; + expr* t2 = vals[i].second; + if (offset.is_zero()) { + lits.push_back(m.mk_eq(t1, t2)); + } + else { + expr_ref t(a.mk_add(t1, a.mk_numeral(offset, true)), m); + lits.push_back(a.mk_le(t, t2)); } } @@ -355,9 +405,11 @@ namespace qe { } void euf_arith_mbi_plugin::block(expr_ref_vector const& lits) { - collect_atoms(lits); - m_fmls.push_back(mk_not(mk_and(lits))); - m_solver->assert_expr(m_fmls.back()); + // want to rely only on atoms from original literals: collect_atoms(lits); + expr_ref conj(mk_not(mk_and(lits)), m); + //m_fmls.push_back(conj); + TRACE("qe", tout << "block " << lits << "\n";); + m_solver->assert_expr(conj); } diff --git a/src/qe/qe_mbi.h b/src/qe/qe_mbi.h index 12e6a8080..0458bd8e0 100644 --- a/src/qe/qe_mbi.h +++ b/src/qe/qe_mbi.h @@ -107,6 +107,8 @@ namespace qe { bool get_literals(model_ref& mdl, expr_ref_vector& lits); void collect_atoms(expr_ref_vector const& fmls); void project_euf(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars); + vector> sort_proxies(model_ref& mdl, app_ref_vector const& proxies); + void minimize_span(model_ref& mdl, app_ref_vector& avars, app_ref_vector const& proxies); void order_avars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars, app_ref_vector const& proxies); void substitute(vector const& defs, expr_ref_vector& lits); void filter_private_arith(app_ref_vector& avars); diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index a6b27784f..731034921 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -753,6 +753,7 @@ namespace smt { } void setup::setup_lra_arith() { + // m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params)); m_context.register_plugin(alloc(smt::theory_lra, m_manager, m_params)); } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 01330269c..fd8481649 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -3149,20 +3149,22 @@ public: theory_lra::inf_eps value(theory_var v) { lp::impq ival = get_ivalue(v); - return inf_eps(0, inf_rational(ival.x, ival.y)); + return inf_eps(rational(0), inf_rational(ival.x, ival.y)); } theory_lra::inf_eps maximize(theory_var v, expr_ref& blocker, bool& has_shared) { lp::impq term_max; lp::lp_status st; + lp::var_index vi = 0; if (!can_get_bound(v)) { + TRACE("arith", tout << "cannot get bound for v" << v << "\n";); st = lp::lp_status::UNBOUNDED; } else { - lp::var_index vi = m_theory_var2var_index[v]; + vi = m_theory_var2var_index[v]; st = m_solver->maximize_term(vi, term_max); } - TRACE("arith", display(tout << st << " v" << v << "\n");); + TRACE("arith", display(tout << st << " v" << v << " vi: " << vi << "\n");); switch (st) { case lp::lp_status::OPTIMAL: { init_variable_values();