From d5081a48b0778441383b2e5b546957540a53b61b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 12 Jun 2018 07:27:50 -0700 Subject: [PATCH] merge while skyping Signed-off-by: Nikolaj Bjorner --- src/opt/maxres.cpp | 30 +++++++++++---------- src/qe/qe_mbi.cpp | 58 ++++++++++++++++++++++++++++++++++++++++- src/smt/smt_context.cpp | 1 - src/smt/smt_context.h | 1 - 4 files changed, 73 insertions(+), 17 deletions(-) diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index e86b20820..a8a4dfa71 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -383,8 +383,8 @@ public: } TRACE("opt", tout << "num cores: " << cores.size() << "\n"; - for (unsigned i = 0; i < cores.size(); ++i) { - display_vec(tout, cores[i]); + for (auto const& c : cores) { + display_vec(tout, c); } tout << "num satisfying: " << asms.size() << "\n";); @@ -476,8 +476,8 @@ public: } void process_unsat(vector const& cores) { - for (unsigned i = 0; i < cores.size(); ++i) { - process_unsat(cores[i]); + for (auto const & c : cores) { + process_unsat(c); } } @@ -602,8 +602,7 @@ public: } void display(std::ostream& out) { - for (unsigned i = 0; i < m_asms.size(); ++i) { - expr* a = m_asms[i].get(); + for (expr * a : m_asms) { out << mk_pp(a, m) << " : " << get_weight(a) << "\n"; } } @@ -710,8 +709,8 @@ public: void update_assignment(model* mdl) { unsigned correction_set_size = 0; - for (unsigned i = 0; i < m_asms.size(); ++i) { - if (is_false(mdl, m_asms[i].get())) { + for (expr* a : m_asms) { + if (is_false(mdl, a)) { ++correction_set_size; } } @@ -722,10 +721,12 @@ public: rational upper(0); expr_ref tmp(m); - for (unsigned i = 0; i < m_soft.size(); ++i) { - if (!is_true(mdl, m_soft[i])) { + unsigned i = 0; + for (expr* s : m_soft) { + if (!is_true(mdl, s)) { upper += m_weights[i]; } + ++i; } if (upper > m_upper) { @@ -741,8 +742,9 @@ public: TRACE("opt", model_smt2_pp(tout << "updated model\n", m, *m_model, 0);); - for (unsigned i = 0; i < m_soft.size(); ++i) { - m_assignment[i] = is_true(m_soft[i]); + i = 0; + for (expr* s : m_soft) { + m_assignment[i++] = is_true(s); } // DEBUG_CODE(verify_assignment();); @@ -759,8 +761,8 @@ public: pb_util u(m); expr_ref_vector nsoft(m); expr_ref fml(m); - for (unsigned i = 0; i < m_soft.size(); ++i) { - nsoft.push_back(mk_not(m, m_soft[i])); + for (expr* s : m_soft) { + nsoft.push_back(mk_not(m, s)); } fml = u.mk_lt(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper); TRACE("opt", tout << "block upper bound " << fml << "\n";);; diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp index d9b62fb96..509800c62 100644 --- a/src/qe/qe_mbi.cpp +++ b/src/qe/qe_mbi.cpp @@ -16,6 +16,62 @@ Author: Revision History: +Notes: + + Reduction into: + T_EUF + T_LIRA + + Other theories: DT, ARR reduced to EUF + BV is EUF/Boolean. + + Purify EUF1 & LIRA1 & EUF2 & LIRA2 + + Then EUF1 & EUF2 |- false + LIRA1 & LIRA2 |- false + + 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) + + 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 + b := t div 2 + + B & A_pure -> B[b/t div 2] = f(t div 2) != q & t <= s + 1 + + 3a. Send purified result to A + A & B_pure -> false + + Invoke the ping-pong principle to extract interpolant. + + 2b. Solve for shared variables with EUF. + + epsilon a . A + = a := (s + 1) div 2 & s < t & f((s + 1) div 2) = q + + 3b. Send to B. Produces core + s < t & f((s + 1) div 2) = q + + 4b Solve again in arithmetic for shared variables with EUF. + + epsion a . A & (s >= t | f((s + 1) div 2) != q) + + a := t div 2 | s = t & f(t div 2) = q & even(t) + + 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" @@ -129,7 +185,6 @@ namespace qe { // optionally minimize core using superposition. return mbi_unsat; case l_true: { - expr_ref_vector fmls(m); m_solver->get_model(mdl); model_evaluator mev(*mdl.get()); lits.reset(); @@ -263,3 +318,4 @@ namespace qe { } } }; + diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 0bc21d627..54fd1cb2b 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3438,7 +3438,6 @@ namespace smt { th->init_search_eh(); } m_qmanager->init_search_eh(); - m_assumption_core.reset(); m_incomplete_theories.reset(); m_num_conflicts = 0; m_num_conflicts_since_restart = 0; diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 7e09c3be2..e85348a07 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -894,7 +894,6 @@ namespace smt { failure m_last_search_failure; ptr_vector m_incomplete_theories; //!< theories that failed to produce a model bool m_searching; - ptr_vector m_assumption_core; unsigned m_num_conflicts; unsigned m_num_conflicts_since_restart; unsigned m_num_conflicts_since_lemma_gc;