From 246df792dfa7c8bd6dfdf181e5ee5f0df12d1d59 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 3 Jul 2018 15:51:50 -0700 Subject: [PATCH] sign of life for CSQ using pogo Signed-off-by: Nikolaj Bjorner --- src/qe/qe_arith.cpp | 18 --------- src/qe/qe_mbi.cpp | 81 +++++++++++++++++++++++++++++----------- src/qe/qe_mbi.h | 2 +- src/qe/qe_term_graph.cpp | 23 ++++++++++++ src/qe/qe_term_graph.h | 8 ++++ 5 files changed, 92 insertions(+), 40 deletions(-) diff --git a/src/qe/qe_arith.cpp b/src/qe/qe_arith.cpp index 8729edb36..cd81167e3 100644 --- a/src/qe/qe_arith.cpp +++ b/src/qe/qe_arith.cpp @@ -453,31 +453,13 @@ namespace qe { else if (!d.m_div.is_one() && !is_int) { t = a.mk_div(t, a.mk_numeral(d.m_div, is_int)); } - update_model(model, to_app(x), eval(t)); - SASSERT(eval(t) == eval(x)); result.push_back(def(expr_ref(x, m), t)); } } return result; } - void update_model(model& mdl, app* x, expr_ref const& val) { - if (is_uninterp_const(x)) { - mdl.register_decl(x->get_decl(), val); - } - else { - func_interp* fi = mdl.get_func_interp(x->get_decl()); - if (!fi) return; - model_evaluator eval(mdl); - expr_ref_vector args(m); - for (expr* arg : *x) { - args.push_back(eval(arg)); - } - fi->insert_entry(args.c_ptr(), val); - } - } - expr_ref mk_add(expr_ref_vector const& ts) { switch (ts.size()) { case 0: diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp index 0b0a9fe10..7dfa35003 100644 --- a/src/qe/qe_mbi.cpp +++ b/src/qe/qe_mbi.cpp @@ -219,16 +219,23 @@ namespace qe { struct euf_arith_mbi_plugin::is_arith_var_proc { ast_manager& m; - app_ref_vector& m_vars; + app_ref_vector& m_pvars; + app_ref_vector& m_svars; arith_util arith; - obj_hashtable m_exclude; - 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 : shared) m_exclude.insert(f); + obj_hashtable m_shared; + is_arith_var_proc(func_decl_ref_vector const& shared, app_ref_vector& pvars, app_ref_vector& svars): + m(pvars.m()), m_pvars(pvars), m_svars(svars), arith(m) { + for (func_decl* f : shared) m_shared.insert(f); } void operator()(app* a) { - 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); + if (!arith.is_int_real(a) || a->get_family_id() == arith.get_family_id()) { + // no-op + } + else if (m_shared.contains(a->get_decl())) { + m_svars.push_back(a); + } + else { + m_pvars.push_back(a); } } void operator()(expr*) {} @@ -283,12 +290,28 @@ namespace qe { } } - app_ref_vector euf_arith_mbi_plugin::get_arith_vars(expr_ref_vector const& lits) { + app_ref_vector euf_arith_mbi_plugin::get_arith_vars(model_ref& mdl, expr_ref_vector& lits) { arith_util a(m); - app_ref_vector avars(m); - is_arith_var_proc _proc(avars, m_shared); + app_ref_vector pvars(m), svars(m); // private and shared arithmetic variables. + is_arith_var_proc _proc(m_shared, pvars, svars); for_each_expr(_proc, lits); - return avars; + rational v1, v2; + for (expr* p : pvars) { + VERIFY(a.is_numeral((*mdl)(p), v1)); + for (expr* s : svars) { + VERIFY(a.is_numeral((*mdl)(s), v2)); + if (v1 < v2) { + lits.push_back(a.mk_lt(p, s)); + } + else if (v2 < v1) { + lits.push_back(a.mk_lt(s, p)); + } + else { + lits.push_back(m.mk_eq(s, p)); + } + } + } + return pvars; } mbi_result euf_arith_mbi_plugin::operator()(expr_ref_vector& lits, model_ref& mdl) { @@ -306,29 +329,45 @@ namespace qe { if (!get_literals(mdl, lits)) { return mbi_undef; } - app_ref_vector avars = get_arith_vars(lits); + TRACE("qe", tout << lits << "\n";); + // 1. Extract projected variables, add inequalities between + // projected variables and non-projected terms according to model. + // 2. Extract disequalities implied by congruence closure. + // 3. project arithmetic variables from pure literals. + // 4. Add projected definitions as equalities to EUF. + // 5. project remaining literals with respect to EUF. + + app_ref_vector avars = get_arith_vars(mdl, lits); TRACE("qe", tout << "vars: " << avars << " lits: " << lits << "\n";); - // 1. project arithmetic variables using mdl that satisfies core. - // ground any remaining arithmetic variables using model. + // 2. + term_graph tg1(m); + func_decl_ref_vector no_shared(m); + tg1.set_vars(no_shared, false); + tg1.add_lits(lits); + expr_ref_vector diseq = tg1.get_ackerman_disequalities(); + lits.append(diseq); + TRACE("qe", tout << "diseq: " << diseq << "\n";); + arith_project_plugin ap(m); ap.set_check_purified(false); + // 3. auto defs = ap.project(*mdl.get(), avars, lits); - // 2. Add the projected definitions to the remaining (euf) literals + + // 4. 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. - term_graph tg(m); - tg.set_vars(m_shared, false); - tg.add_lits(lits); + // 5. + term_graph tg2(m); + tg2.set_vars(m_shared, false); + tg2.add_lits(lits); lits.reset(); - //lits.append(tg.project(*mdl)); - lits.append(tg.project()); + lits.append(tg2.project()); TRACE("qe", tout << "project: " << lits << "\n";); return mbi_sat; } diff --git a/src/qe/qe_mbi.h b/src/qe/qe_mbi.h index 928bb7845..fdc4c3c6a 100644 --- a/src/qe/qe_mbi.h +++ b/src/qe/qe_mbi.h @@ -112,7 +112,7 @@ namespace qe { struct is_atom_proc; struct is_arith_var_proc; - app_ref_vector get_arith_vars(expr_ref_vector const& lits); + app_ref_vector get_arith_vars(model_ref& mdl, expr_ref_vector& lits); bool get_literals(model_ref& mdl, expr_ref_vector& lits); void collect_atoms(expr_ref_vector const& fmls); public: diff --git a/src/qe/qe_term_graph.cpp b/src/qe/qe_term_graph.cpp index e9ec3d4b7..2e81454a0 100644 --- a/src/qe/qe_term_graph.cpp +++ b/src/qe/qe_term_graph.cpp @@ -975,6 +975,22 @@ namespace qe { reset(); return res; } + + expr_ref_vector get_ackerman_disequalities() { + expr_ref_vector res(m); + purify(); + lits2pure(res); + unsigned sz = res.size(); + mk_distinct(res); + reset(); + unsigned j = 0; + for (unsigned i = sz; i < res.size(); ++i) { + res[j++] = res.get(i); + } + res.shrink(j); + return res; + } + expr_ref_vector solve() { expr_ref_vector res(m); purify(); @@ -1011,4 +1027,11 @@ namespace qe { return p.solve(); } + expr_ref_vector term_graph::get_ackerman_disequalities() { + m_is_var.reset_solved(); + term_graph::projector p(*this); + return p.get_ackerman_disequalities(); + } + + } diff --git a/src/qe/qe_term_graph.h b/src/qe/qe_term_graph.h index 0c66f4193..8c02163ab 100644 --- a/src/qe/qe_term_graph.h +++ b/src/qe/qe_term_graph.h @@ -114,6 +114,14 @@ namespace qe { expr_ref_vector solve(); expr_ref_vector project(model &mdl); + /** + * Return disequalities to ensure that disequalities between + * excluded functions are preserved. + * For example if f(a) = b, f(c) = d, and b and d are not + * congruent, then produce the disequality a != c. + */ + expr_ref_vector get_ackerman_disequalities(); + }; }