From 8221a09659ea878f29d4aa413122f9e4a73b88d9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 28 Jul 2016 16:49:19 -0700 Subject: [PATCH] fast path for antecedent extraction in smt_context Signed-off-by: Nikolaj Bjorner --- contrib/cmake/src/smt/CMakeLists.txt | 1 + src/smt/smt_consequences.cpp | 189 +++++++++++++++++++++++++++ src/smt/smt_context.cpp | 7 + src/smt/smt_context.h | 8 ++ src/smt/smt_kernel.cpp | 8 ++ src/smt/smt_kernel.h | 5 + src/smt/smt_solver.cpp | 4 + src/solver/solver.cpp | 4 + src/solver/solver.h | 5 + src/solver/solver_na2as.cpp | 5 + src/solver/solver_na2as.h | 1 + 11 files changed, 237 insertions(+) create mode 100644 src/smt/smt_consequences.cpp diff --git a/contrib/cmake/src/smt/CMakeLists.txt b/contrib/cmake/src/smt/CMakeLists.txt index e9306b2d6..035ac07c9 100644 --- a/contrib/cmake/src/smt/CMakeLists.txt +++ b/contrib/cmake/src/smt/CMakeLists.txt @@ -18,6 +18,7 @@ z3_add_component(smt smt_checker.cpp smt_clause.cpp smt_conflict_resolution.cpp + smt_consequences.cpp smt_context.cpp smt_context_inv.cpp smt_context_pp.cpp diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp new file mode 100644 index 000000000..083fd6e0c --- /dev/null +++ b/src/smt/smt_consequences.cpp @@ -0,0 +1,189 @@ +/*++ +Copyright (c) 2006 Microsoft Corporation + +Module Name: + + smt_consequences.cpp + +Abstract: + + Tuned consequence finding for smt_context. + +Author: + + nbjorner 2016-07-28. + +Revision History: + +--*/ +#include "smt_context.h" +#include "ast_util.h" + +namespace smt { + + expr_ref context::antecedent2fml(uint_set const& vars) { + expr_ref_vector premises(m_manager); + uint_set::iterator it = vars.begin(), end = vars.end(); + for (; it != end; ++it) { + premises.push_back(bool_var2expr(*it)); + } + return mk_and(premises); + } + + void context::extract_fixed_consequences(unsigned start, obj_map& vars, obj_hashtable const& assumptions, expr_ref_vector& conseq) { + ast_manager& m = m_manager; + pop_to_search_lvl(); + literal_vector const& lits = assigned_literals(); + unsigned sz = lits.size(); + expr* e1, *e2; + expr_ref fml(m); + for (unsigned i = start; i < sz; ++i) { + literal lit = lits[i]; + if (lit == true_literal) continue; + expr* e = bool_var2expr(lit.var()); + uint_set s; + if (assumptions.contains(e)) { + s.insert(get_literal(e).var()); + } + else { + b_justification js = get_justification(lit.var()); + switch (js.get_kind()) { + case b_justification::CLAUSE: { + clause * cls = js.get_clause(); + unsigned num_lits = cls->get_num_literals(); + for (unsigned j = 0; j < num_lits; ++j) { + literal lit2 = cls->get_literal(j); + if (lit2.var() != lit.var()) { + s |= m_antecedents.find(lit2.var()); + } + } + break; + } + case b_justification::BIN_CLAUSE: { + s |= m_antecedents.find(js.get_literal().var()); + break; + } + case b_justification::AXIOM: { + break; + } + case b_justification::JUSTIFICATION: + justification* j = js.get_justification(); + // warning_msg("TODO: extract antecedents from theory justification"); + // std::cout << "TODO: justification\n"; + break; + } + } + m_antecedents.insert(lit.var(), s); + bool found = false; + if (vars.contains(e)) { + found = true; + fml = lit.sign()?m.mk_not(e):e; + vars.erase(e); + } + else if (!lit.sign() && m.is_eq(e, e1, e2)) { + if (vars.contains(e2)) { + std::swap(e1, e2); + } + if (vars.contains(e1) && m.is_value(e2)) { + found = true; + fml = e; + vars.erase(e1); + } + } + if (found) { + fml = m.mk_implies(antecedent2fml(s), fml); + conseq.push_back(fml); + } + } + } + + lbool context::get_consequences(expr_ref_vector const& assumptions, + expr_ref_vector const& vars, expr_ref_vector& conseq) { + + lbool is_sat = check(assumptions.size(), assumptions.c_ptr()); + if (is_sat != l_true) { + return is_sat; + } + obj_map var2val; + obj_hashtable _assumptions; + for (unsigned i = 0; i < assumptions.size(); ++i) { + _assumptions.insert(assumptions[i]); + } + model_ref mdl; + get_model(mdl); + expr_ref_vector trail(m_manager); + model_evaluator eval(*mdl.get()); + expr_ref val(m_manager); + for (unsigned i = 0; i < vars.size(); ++i) { + eval(vars[i], val); + if (m_manager.is_value(val)) { + trail.push_back(val); + var2val.insert(vars[i], val); + } + } + extract_fixed_consequences(0, var2val, _assumptions, conseq); + unsigned num_units = assigned_literals().size(); + app_ref eq(m_manager); + TRACE("context", + tout << "pop: " << num_levels << "\n"; + tout << "vars: " << vars.size() << "\n"; + tout << "lits: " << num_units << "\n";); + m_case_split_queue->init_search_eh(); + while (!var2val.empty()) { + obj_map::iterator it = var2val.begin(); + expr* e = it->m_key; + expr* val = it->m_value; + push_scope(); + unsigned current_level = m_scope_lvl; + + literal lit; + if (m_manager.is_bool(e)) { + lit = literal(get_bool_var(e), m_manager.is_true(val)); + } + else { + eq = mk_eq_atom(e, val); + internalize_formula(eq, false); + lit = literal(get_bool_var(eq), true); + } + assign(lit, b_justification::mk_axiom(), true); + flet l(m_searching, true); + while (true) { + is_sat = bounded_search(); + TRACE("context", tout << "search result: " << is_sat << "\n";); + if (is_sat != l_true && m_last_search_failure != OK) { + return is_sat; + } + if (is_sat == l_undef) { + TRACE("context", tout << "restart\n";); + inc_limits(); + continue; + } + break; + } + if (get_assignment(lit) == l_true) { + var2val.erase(e); + } + else if (get_assign_level(lit) > get_search_level()) { + TRACE("context", tout << "Retry fixing: " << mk_pp(e, m_manager) << "\n";); + pop_to_search_lvl(); + continue; + } + else { + TRACE("context", tout << "Fixed: " << mk_pp(e, m_manager) << "\n";); + } + extract_fixed_consequences(num_units, var2val, _assumptions, conseq); + num_units = assigned_literals().size(); + if (var2val.contains(e)) { + TRACE("context", tout << "TBD: Fixed value to " << mk_pp(e, m_manager) << " was not retrieved\n";); + var2val.erase(e); + SASSERT(get_assignment(lit) == l_false); + } + + // repeat until we either have a model with negated literal or + // the literal is implied at base. + TRACE("context", tout << "Unfixed variables: " << var2val.size() << "\n";); + } + return l_true; + } + +} diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 5b60b6893..3aeb623f9 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -2460,6 +2460,13 @@ namespace smt { SASSERT(m_scope_lvl == m_base_lvl); } + void context::pop_to_search_lvl() { + unsigned num_levels = m_scope_lvl - get_search_level(); + if (num_levels > 0) { + pop_scope(num_levels); + } + } + /** \brief Simplify the given clause using the assignment. Return true if the clause was already satisfied, and false otherwise. diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 3c260abbe..b5e143d9d 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1322,6 +1322,7 @@ namespace smt { virtual void setup_context(bool use_static_features); void setup_components(void); void pop_to_base_lvl(); + void pop_to_search_lvl(); #ifdef Z3DEBUG bool already_internalized_theory(theory * th) const; bool already_internalized_theory_core(theory * th, expr_ref_vector const & s) const; @@ -1343,6 +1344,11 @@ namespace smt { literal lit, context& src_ctx, context& dst_ctx, vector b2v, ast_translation& tr); + u_map m_antecedents; + void extract_fixed_consequences(unsigned idx, obj_map& vars, obj_hashtable const& assumptions, expr_ref_vector& conseq); + + expr_ref antecedent2fml(uint_set const& ante); + public: context(ast_manager & m, smt_params & fp, params_ref const & p = params_ref()); @@ -1382,6 +1388,8 @@ namespace smt { void pop(unsigned num_scopes); lbool check(unsigned num_assumptions = 0, expr * const * assumptions = 0, bool reset_cancel = true); + + lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq); lbool setup_and_check(bool reset_cancel = true); diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp index 418dfdb04..8f18b7311 100644 --- a/src/smt/smt_kernel.cpp +++ b/src/smt/smt_kernel.cpp @@ -98,6 +98,10 @@ namespace smt { lbool check(unsigned num_assumptions, expr * const * assumptions) { return m_kernel.check(num_assumptions, assumptions); } + + lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq) { + return m_kernel.get_consequences(assumptions, vars, conseq); + } void get_model(model_ref & m) const { m_kernel.get_model(m); @@ -264,6 +268,10 @@ namespace smt { return r; } + lbool kernel::get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq) { + return m_imp->get_consequences(assumptions, vars, conseq); + } + void kernel::get_model(model_ref & m) const { m_imp->get_model(m); } diff --git a/src/smt/smt_kernel.h b/src/smt/smt_kernel.h index bf559a775..4cf170681 100644 --- a/src/smt/smt_kernel.h +++ b/src/smt/smt_kernel.h @@ -126,6 +126,11 @@ namespace smt { lbool check(app_ref_vector const& asms) { return check(asms.size(), (expr* const*)asms.c_ptr()); } + /** + \brief extract consequences among variables. + */ + lbool get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq); + /** \brief Return the model associated with the last check command. */ diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index 6ae7f107c..ec874ed8f 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -67,6 +67,10 @@ namespace smt { m_context.collect_statistics(st); } + virtual lbool get_consequences_core(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq) { + return m_context.get_consequences(assumptions, vars, conseq); + } + virtual void assert_expr(expr * t) { m_context.assert_expr(t); } diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index c587a1722..7b11317d1 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -48,6 +48,10 @@ struct scoped_assumption_push { }; lbool solver::get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) { + return get_consequences_core(asms, vars, consequences); +} + +lbool solver::get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) { ast_manager& m = asms.get_manager(); lbool is_sat = check_sat(asms); if (is_sat != l_true) { diff --git a/src/solver/solver.h b/src/solver/solver.h index d55db9821..7f36e2ad7 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -171,6 +171,11 @@ public: ~scoped_push() { if (!m_nopop) s.pop(1); } void disable_pop() { m_nopop = true; } }; + +protected: + + virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences); + }; #endif diff --git a/src/solver/solver_na2as.cpp b/src/solver/solver_na2as.cpp index 2ca6e187c..99917fff8 100644 --- a/src/solver/solver_na2as.cpp +++ b/src/solver/solver_na2as.cpp @@ -65,6 +65,11 @@ lbool solver_na2as::check_sat(unsigned num_assumptions, expr * const * assumptio return check_sat_core(m_assumptions.size(), m_assumptions.c_ptr()); } +lbool solver_na2as::get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) { + append_assumptions app(m_assumptions, asms.size(), asms.c_ptr()); + return get_consequences_core(m_assumptions, vars, consequences); +} + void solver_na2as::push() { m_scopes.push_back(m_assumptions.size()); push_core(); diff --git a/src/solver/solver_na2as.h b/src/solver/solver_na2as.h index 9aeb56fb1..45253e950 100644 --- a/src/solver/solver_na2as.h +++ b/src/solver/solver_na2as.h @@ -45,6 +45,7 @@ public: virtual unsigned get_num_assumptions() const { return m_assumptions.size(); } virtual expr * get_assumption(unsigned idx) const { return m_assumptions[idx]; } + virtual lbool get_consequences(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences); protected: virtual lbool check_sat_core(unsigned num_assumptions, expr * const * assumptions) = 0; virtual void push_core() = 0;