From 535b8893aea4d13669944e527041f2bd2d910779 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Tue, 12 Jun 2018 17:23:46 -0700 Subject: [PATCH] Complete euf project with eq and diseq on pure representatives --- src/qe/qe_mbi.cpp | 43 ++++++++++++++++++++-------------------- src/qe/qe_term_graph.cpp | 39 ++++++++++++++++++++++++++++++++++++ src/qe/qe_term_graph.h | 10 +++++----- 3 files changed, 65 insertions(+), 27 deletions(-) diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp index 09ab76559..ae989ba02 100644 --- a/src/qe/qe_mbi.cpp +++ b/src/qe/qe_mbi.cpp @@ -33,18 +33,18 @@ Notes: Sketch of approach by example: A: s <= 2a <= t & f(a) = q - + B: t <= 2b <= s + 1 & f(b) != q 1. Extract arithmetic consequences of A over shared vocabulary. - A -> s <= t & (even(t) | s < t) - + A -> s <= t & (even(t) | s < t) + 2a. Send to B, have B solve shared variables with EUF_B. epsilon b . B & A_pure - epsilon b . t <= 2b <= s + 1 & s <= t & (even(t) | s < t) - = t <= s + 1 & (even(t) | t <= s) & s <= t & (even(t) | s < t) - = even(t) & t = s + epsilon b . t <= 2b <= s + 1 & s <= t & (even(t) | s < t) + = t <= s + 1 & (even(t) | t <= s) & s <= t & (even(t) | s < t) + = even(t) & t = s b := t div 2 B & A_pure -> B[b/t div 2] = f(t div 2) != q & t <= s + 1 @@ -53,13 +53,13 @@ Notes: A & B_pure -> false Invoke the ping-pong principle to extract interpolant. - + 2b. Solve for shared variables with EUF. - epsilon a . A + epsilon a . A = a := (s + 1) div 2 & s < t & f((s + 1) div 2) = q - 3b. Send to B. Produces core + 3b. Send to B. Produces core s < t & f((s + 1) div 2) = q 4b Solve again in arithmetic for shared variables with EUF. @@ -71,7 +71,7 @@ Notes: Send to B, produces core (s != t | f(t div 2) != q) 5b. There is no longer a solution for A. A is unsat. - + --*/ #include "ast/ast_util.h" @@ -138,7 +138,7 @@ namespace qe { void prop_mbi_plugin::block(expr_ref_vector const& lits) { m_solver->assert_expr(mk_not(mk_and(lits))); - } + } // ------------------------------- // euf_mbi, TBD @@ -158,8 +158,8 @@ namespace qe { void operator()(expr*) {} }; - euf_mbi_plugin::euf_mbi_plugin(solver* s, solver* sNot): - m(s->get_manager()), + euf_mbi_plugin::euf_mbi_plugin(solver* s, solver* sNot): + m(s->get_manager()), m_atoms(m), m_solver(s), m_dual_solver(sNot) { @@ -205,11 +205,11 @@ namespace qe { // use the dual solver to find a 'small' implicant m_dual_solver->get_unsat_core(core); TRACE("qe", tout << "core: " << core << "\n";); - // project the implicant onto vars + // project the implicant onto vars tg.set_vars(vars, false); tg.add_lits(core); - lits.reset(); - lits.append(tg.project()); + lits.reset(); + lits.append(tg.project(*mdl)); TRACE("qe", tout << "project: " << lits << "\n";); return mbi_sat; case l_undef: @@ -232,8 +232,8 @@ namespace qe { void euf_mbi_plugin::block(expr_ref_vector const& lits) { m_solver->assert_expr(mk_not(mk_and(lits))); - } - + } + /** -------------------------------------------------------------- * ping-pong interpolation of Gurfinkel & Vizel @@ -255,7 +255,7 @@ namespace qe { auto* t2 = turn ? &b : &a; mbi_result next_res = (*t1)(vars, lits, mdl); switch (next_res) { - case mbi_sat: + case mbi_sat: if (last_res == mbi_sat) { itp = nullptr; return l_true; @@ -264,7 +264,7 @@ namespace qe { break; // continue case mbi_unsat: { if (lits.empty()) { - // TBD, either a => itp and itp => !b + // TBD, either a => itp and itp => !b // or b => itp and itp => !a itp = mk_and(itps[!turn]); return l_false; @@ -282,7 +282,7 @@ namespace qe { case mbi_augment: break; case mbi_undef: - return l_undef; + return l_undef; } turn = !turn; last_res = next_res; @@ -319,4 +319,3 @@ namespace qe { } } }; - diff --git a/src/qe/qe_term_graph.cpp b/src/qe/qe_term_graph.cpp index 82b6e9d2e..467a0cc48 100644 --- a/src/qe/qe_term_graph.cpp +++ b/src/qe/qe_term_graph.cpp @@ -24,6 +24,7 @@ Notes: #include "ast/for_each_expr.h" #include "ast/occurs.h" #include "qe/qe_term_graph.h" +#include "model/model_evaluator.h" namespace qe { @@ -546,6 +547,7 @@ namespace qe { u_map m_term2app; u_map m_root2rep; + model_ref m_model; expr_ref_vector m_pinned; // tracks expr in the maps expr* mk_pure(term const& t) { @@ -565,6 +567,7 @@ namespace qe { return pure; } + bool is_better_rep(expr *t1, expr *t2) { if (!t2) return t1 != nullptr; return m.is_unique_value(t1) && !m.is_unique_value(t2); @@ -740,20 +743,49 @@ namespace qe { return is_uninterp_const(rhs) && !occurs(rhs, lhs); } + /// Add equalities and disequalities for all pure representatives + /// based on their equivalence in the model + void model_complete(expr_ref_vector &res) { + if (!m_model) return; + obj_map val2rep; + model_evaluator mev(*m_model); + for (auto &kv : m_root2rep) { + expr *rep = kv.m_value; + expr_ref val(m); + expr *u = nullptr; + if (!mev.eval(rep, val)) continue; + if (val2rep.find(val, u)) { + res.push_back(m.mk_eq(u, rep)); + } + else { + val2rep.insert(val, rep); + } + } + ptr_buffer reps; + for (auto &kv : val2rep) { + reps.push_back(kv.m_value); + } + res.push_back(m.mk_distinct(reps.size(), reps.c_ptr())); + } + public: projector(term_graph &tg) : m_tg(tg), m(m_tg.m), m_pinned(m) {} + void set_model(model &mdl) { m_model = &mdl; } + void reset() { m_tg.reset_marks(); m_term2app.reset(); m_root2rep.reset(); m_pinned.reset(); + m_model.reset(); } expr_ref_vector project() { expr_ref_vector res(m); purify(); mk_lits(res); mk_pure_equalities(res); + model_complete(res); reset(); return res; } @@ -780,6 +812,13 @@ namespace qe { return p.project(); } + expr_ref_vector term_graph::project(model &mdl) { + m_is_var.reset_solved(); + projector p(*this); + p.set_model(mdl); + return p.project(); + } + expr_ref_vector term_graph::solve() { // reset solved vars so that they are not considered pure by projector m_is_var.reset_solved(); diff --git a/src/qe/qe_term_graph.h b/src/qe/qe_term_graph.h index ac13e1e44..97e14dc62 100644 --- a/src/qe/qe_term_graph.h +++ b/src/qe/qe_term_graph.h @@ -23,6 +23,7 @@ Notes: #include "util/plugin_manager.h" #include "qe/qe_solve_plugin.h" #include "qe/qe_vartest.h" +#include "model/model.h" namespace qe { @@ -85,8 +86,6 @@ namespace qe { void display(std::ostream &out); bool is_pure_def(expr* atom, expr *& v); - void solve_for_vars(); - public: term_graph(ast_manager &m); @@ -111,9 +110,10 @@ namespace qe { * onto the vocabulary of decls (if exclude is false) or outside the * vocabulary of decls (if exclude is true). */ - expr_ref_vector project(); - expr_ref_vector solve(); - + expr_ref_vector project(); + expr_ref_vector solve(); + expr_ref_vector project(model &mdl); + }; }