From c9900720f8180cf202f52f23f20d024c11ea6a24 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 22 Oct 2020 11:31:41 -0700 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 2 +- src/qe/mbp/mbp_plugin.cpp | 3 ++- src/qe/mbp/mbp_plugin.h | 2 +- src/sat/smt/arith_axioms.cpp | 19 ++++++++++++++++++- src/sat/smt/q_mbi.cpp | 1 + src/sat/smt/q_model_fixer.cpp | 25 +++++++++++++++---------- src/sat/smt/q_model_fixer.h | 2 +- 7 files changed, 39 insertions(+), 15 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index e41b7310c..baed826e6 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1674,7 +1674,7 @@ void cmd_context::add_declared_functions(model& mdl) { expr* val = mdl.get_some_value(f->get_range()); if (f->get_arity() == 0) { mdl.register_decl(f, val); - } + } else { func_interp* fi = alloc(func_interp, m(), f->get_arity()); fi->set_else(val); diff --git a/src/qe/mbp/mbp_plugin.cpp b/src/qe/mbp/mbp_plugin.cpp index be43f1f0c..3a73e8b50 100644 --- a/src/qe/mbp/mbp_plugin.cpp +++ b/src/qe/mbp/mbp_plugin.cpp @@ -341,6 +341,7 @@ namespace mbp { m_non_ground.mark(v); for (unsigned i = 0; m.inc() && i < lits.size(); ++i) lits[i] = purify(inv, eval, lits.get(i), lits); + std::cout << m_pure_eqs << "\n"; lits.append(m_pure_eqs); TRACE("mbp", tout << lits << "\n";); } @@ -371,7 +372,7 @@ namespace mbp { m_pure_eqs.push_back(m.mk_eq(t, s)); unsigned i = 0; for (expr* arg : *t) - push_back(lits, inv.invert_arg(t, i++, eval(arg))); + inv.invert_arg(t, i++, eval(arg), lits); m_to_visit.pop_back(); } else diff --git a/src/qe/mbp/mbp_plugin.h b/src/qe/mbp/mbp_plugin.h index f339aa07a..2d84fb576 100644 --- a/src/qe/mbp/mbp_plugin.h +++ b/src/qe/mbp/mbp_plugin.h @@ -43,7 +43,7 @@ namespace mbp { class euf_inverter { public: virtual expr* invert_app(app* t, expr* value) = 0; - virtual expr* invert_arg(app* t, unsigned i, expr* value) = 0; + virtual void invert_arg(app* t, unsigned i, expr* value, expr_ref_vector& lits) = 0; }; class project_plugin { diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp index e8e609db9..2b74b328d 100644 --- a/src/sat/smt/arith_axioms.cpp +++ b/src/sat/smt/arith_axioms.cpp @@ -301,10 +301,17 @@ namespace arith { return; expr* e1 = var2expr(v1); expr* e2 = var2expr(v2); + if (e1 == e2) + return; literal le, ge; - literal eq = eq_internalize(e1, e2); if (a.is_numeral(e1)) std::swap(e1, e2); + if (a.is_numeral(e1)) { + add_unit(~mk_literal(m.mk_eq(e1, e2))); + std::cout << "two numerals\n"; + return; + } + literal eq = eq_internalize(e1, e2); if (a.is_numeral(e2)) { le = mk_literal(a.mk_le(e1, e2)); ge = mk_literal(a.mk_ge(e1, e2)); @@ -313,9 +320,19 @@ namespace arith { expr_ref diff(a.mk_sub(e1, e2), m); expr_ref zero(a.mk_numeral(rational(0), a.is_int(e1)), m); rewrite(diff); + if (a.is_numeral(diff)) { + std::cout << "diff " << diff << " " << mk_pp(e1, m) << " " << mk_pp(e2, m) << "\n"; + if (zero == diff) + add_unit(eq); + else + add_unit(~eq); + return; + } le = mk_literal(a.mk_le(diff, zero)); ge = mk_literal(a.mk_ge(diff, zero)); } + std::cout << mk_pp(e1, m) << " " << mk_pp(e2, m) << " "; + std::cout << le << " " << ge << "\n"; add_clause(~eq, le); add_clause(~eq, ge); add_clause(~le, ~ge, eq); diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp index f9c5d9e93..485f7f642 100644 --- a/src/sat/smt/q_mbi.cpp +++ b/src/sat/smt/q_mbi.cpp @@ -190,6 +190,7 @@ namespace q { app_ref_vector vars(qb.vars); mbp::project_plugin proj(m); proj.purify(m_model_fixer, *m_model, vars, fmls); + std::cout << "fmls\n" << fmls << "\n"; for (unsigned i = 0; i < vars.size(); ++i) { app* v = vars.get(i); auto* p = get_plugin(v); diff --git a/src/sat/smt/q_model_fixer.cpp b/src/sat/smt/q_model_fixer.cpp index 4b02e324b..dd01761ec 100644 --- a/src/sat/smt/q_model_fixer.cpp +++ b/src/sat/smt/q_model_fixer.cpp @@ -221,18 +221,18 @@ namespace q { return value; } - expr* model_fixer::invert_arg(app* t, unsigned i, expr* value) { + void model_fixer::invert_arg(app* t, unsigned i, expr* value, expr_ref_vector& lits) { TRACE("q", tout << "invert-arg " << mk_pp(t, m) << " " << i << " " << mk_pp(value, m) << "\n";); auto const* md = get_projection_data(t->get_decl(), i); if (!md) - return m.mk_true(); + return; auto* proj = get_projection(t->get_decl()->get_domain(i)); if (!proj) - return m.mk_true(); + return; unsigned sz = md->values.size(); if (sz <= 1) - return m.mk_true(); + return; // // md->values are sorted @@ -251,13 +251,18 @@ namespace q { expr* arg = t->get_arg(i); - if (is_lt(md->values[1])) - return proj->mk_lt(arg, term(1)); + if (is_lt(md->values[1])) { + lits.push_back(proj->mk_lt(arg, term(1))); + return; + } for (unsigned j = 2; j < sz; ++j) - if (is_lt(md->values[j])) - return m.mk_and(proj->mk_le(term(j-1), arg), proj->mk_lt(arg, term(j))); - - return proj->mk_le(term(sz-1), arg); + if (is_lt(md->values[j])) { + lits.push_back(proj->mk_le(term(j - 1), arg)); + lits.push_back(proj->mk_lt(arg, term(j))); + return; + } + + lits.push_back(proj->mk_le(term(sz-1), arg)); } } diff --git a/src/sat/smt/q_model_fixer.h b/src/sat/smt/q_model_fixer.h index aae50a6f0..aabf4ed24 100644 --- a/src/sat/smt/q_model_fixer.h +++ b/src/sat/smt/q_model_fixer.h @@ -108,7 +108,7 @@ namespace q { quantifier_macro_info* operator()(quantifier* q) override; expr* invert_app(app* t, expr* value) override; - expr* invert_arg(app* t, unsigned i, expr* value) override; + void invert_arg(app* t, unsigned i, expr* value, expr_ref_vector& lits) override; }; }