From c5dd441947c28dd2a3a6a74e17f21a40efeb6682 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 7 Sep 2016 11:50:26 -0700 Subject: [PATCH] fixes to consequence generation and cancellation Signed-off-by: Nikolaj Bjorner --- src/api/api_context.cpp | 37 ++++++++++++------------- src/api/api_context.h | 2 +- src/api/z3_replayer.cpp | 2 +- src/smt/asserted_formulas.cpp | 8 ++++-- src/smt/asserted_formulas.h | 1 + src/smt/smt_consequences.cpp | 52 +++++++++++++++-------------------- src/smt/smt_context.cpp | 8 ++++-- src/smt/smt_context.h | 2 ++ src/util/rlimit.cpp | 2 +- 9 files changed, 58 insertions(+), 56 deletions(-) diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp index b6c3384e7..bcd3c60f2 100644 --- a/src/api/api_context.cpp +++ b/src/api/api_context.cpp @@ -70,22 +70,6 @@ namespace api { // // ------------------------ - context::set_interruptable::set_interruptable(context & ctx, event_handler & i): - m_ctx(ctx) { - #pragma omp critical (set_interruptable) - { - SASSERT(m_ctx.m_interruptable == 0); - m_ctx.m_interruptable = &i; - } - } - - context::set_interruptable::~set_interruptable() { - #pragma omp critical (set_interruptable) - { - m_ctx.m_interruptable = 0; - } - } - context::context(context_params * p, bool user_ref_count): m_params(p != 0 ? *p : context_params()), m_user_ref_count(user_ref_count), @@ -105,11 +89,10 @@ namespace api { m_print_mode = Z3_PRINT_SMTLIB_FULL; m_searching = false; - m_interruptable = 0; - m_smtlib_parser = 0; m_smtlib_parser_has_decls = false; - + + m_interruptable = 0; m_error_handler = &default_error_handler; m_basic_fid = m().get_basic_family_id(); @@ -139,6 +122,22 @@ namespace api { } } + context::set_interruptable::set_interruptable(context & ctx, event_handler & i): + m_ctx(ctx) { + #pragma omp critical (set_interruptable) + { + SASSERT(m_ctx.m_interruptable == 0); + m_ctx.m_interruptable = &i; + } + } + + context::set_interruptable::~set_interruptable() { + #pragma omp critical (set_interruptable) + { + m_ctx.m_interruptable = 0; + } + } + void context::interrupt() { #pragma omp critical (set_interruptable) { diff --git a/src/api/api_context.h b/src/api/api_context.h index d2c0b3ad4..4685fd04e 100644 --- a/src/api/api_context.h +++ b/src/api/api_context.h @@ -94,7 +94,7 @@ namespace api { event_handler * m_interruptable; // Reference to an object that can be interrupted by Z3_interrupt - public: + public: // Scoped obj for setting m_interruptable class set_interruptable { context & m_ctx; diff --git a/src/api/z3_replayer.cpp b/src/api/z3_replayer.cpp index 826e767f2..651cb730f 100644 --- a/src/api/z3_replayer.cpp +++ b/src/api/z3_replayer.cpp @@ -515,7 +515,7 @@ struct z3_replayer::imp { if (idx >= m_cmds.size()) throw z3_replayer_exception("invalid command"); try { - TRACE("z3_replayer_cmd", tout << m_cmds_names[idx] << "\n";); + TRACE("z3_replayer_cmd", tout << idx << ":" << m_cmds_names[idx] << "\n";); m_cmds[idx](m_owner); } catch (z3_error & ex) { diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 3ba6693d9..3c67cadcf 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -543,8 +543,12 @@ void asserted_formulas::infer_patterns() { } void asserted_formulas::commit() { - m_macro_manager.mark_forbidden(m_asserted_formulas.size() - m_asserted_qhead, m_asserted_formulas.c_ptr() + m_asserted_qhead); - m_asserted_qhead = m_asserted_formulas.size(); + commit(m_asserted_formulas.size()); +} + +void asserted_formulas::commit(unsigned new_qhead) { + m_macro_manager.mark_forbidden(new_qhead - m_asserted_qhead, m_asserted_formulas.c_ptr() + m_asserted_qhead); + m_asserted_qhead = new_qhead; } void asserted_formulas::eliminate_term_ite() { diff --git a/src/smt/asserted_formulas.h b/src/smt/asserted_formulas.h index 75fb86703..9e9ecf33a 100644 --- a/src/smt/asserted_formulas.h +++ b/src/smt/asserted_formulas.h @@ -113,6 +113,7 @@ public: unsigned get_formulas_last_level() const; unsigned get_qhead() const { return m_asserted_qhead; } void commit(); + void commit(unsigned new_qhead); expr * get_formula(unsigned idx) const { return m_asserted_formulas.get(idx); } proof * get_formula_proof(unsigned idx) const { return m_manager.proofs_enabled() ? m_asserted_formula_prs.get(idx) : 0; } expr * const * get_formulas() const { return m_asserted_formulas.c_ptr(); } diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp index df4f0f180..b1c277792 100644 --- a/src/smt/smt_consequences.cpp +++ b/src/smt/smt_consequences.cpp @@ -174,6 +174,9 @@ namespace smt { else if (e_internalized(k) && m.are_distinct(v, get_enode(k)->get_root()->get_owner())) { to_delete.push_back(k); } + else if (get_assignment(mk_diseq(k, v)) == l_true) { + to_delete.push_back(k); + } } for (unsigned i = 0; i < to_delete.size(); ++i) { var2val.remove(to_delete[i]); @@ -215,9 +218,7 @@ namespace smt { for (unsigned i = 0; i < literals.size(); ++i) { literals[i].neg(); } - eq = mk_eq_atom(k, v); - internalize_formula(eq, false); - literal lit(get_bool_var(eq), false); + literal lit = mk_diseq(k, v); literals.push_back(lit); mk_clause(literals.size(), literals.c_ptr(), 0); TRACE("context", display_literals_verbose(tout, literals.size(), literals.c_ptr());); @@ -229,6 +230,18 @@ namespace smt { return to_delete.size(); } + literal context::mk_diseq(expr* e, expr* val) { + ast_manager& m = m_manager; + if (m.is_bool(e)) { + return literal(get_bool_var(e), m.is_true(val)); + } + else { + expr_ref eq(mk_eq_atom(e, val), m); + internalize_formula(eq, false); + return literal(get_bool_var(eq), true); + } + } + lbool context::get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq, @@ -288,18 +301,7 @@ namespace smt { // the opposite value of the current reference model. // If the variable is a non-Boolean, it means adding a disequality. // - literal lit; - if (m.is_bool(e)) { - lit = literal(get_bool_var(e), m.is_true(val)); - } - else { - eq = mk_eq_atom(e, val); - internalize_formula(eq, false); - lit = literal(get_bool_var(eq), true); - TRACE("context", tout << mk_pp(e, m) << " " << mk_pp(val, m) << "\n"; - display_literal_verbose(tout, lit); tout << "\n"; - tout << "Equal: " << are_equal(e, val) << "\n";); - } + literal lit = mk_diseq(e, val); mark_as_relevant(lit); push_scope(); assign(lit, b_justification::mk_axiom(), true); @@ -434,6 +436,7 @@ namespace smt { pop_to_base_lvl(); lbool is_sat = check(assumptions.size(), assumptions.c_ptr()); if (is_sat != l_true) { + TRACE("context", tout << is_sat << "\n";); return is_sat; } obj_map var2val; @@ -475,20 +478,12 @@ namespace smt { obj_map::iterator it = var2val.begin(), end = var2val.end(); unsigned num_vars = 0; for (; it != end && num_vars < chunk_size; ++it) { + if (get_cancel_flag()) { + return l_undef; + } expr* e = it->m_key; expr* val = it->m_value; - literal lit; - if (m.is_bool(e)) { - lit = literal(get_bool_var(e), m.is_true(val)); - } - else { - eq = mk_eq_atom(e, val); - internalize_formula(eq, false); - lit = literal(get_bool_var(eq), true); - TRACE("context", tout << mk_pp(e, m) << " " << mk_pp(val, m) << "\n"; - display_literal_verbose(tout, lit); tout << "\n"; - tout << "Equal: " << are_equal(e, val) << "\n";); - } + literal lit = mk_diseq(e, val); mark_as_relevant(lit); if (get_assignment(lit) != l_undef) { continue; @@ -504,9 +499,6 @@ namespace smt { m_not_l = null_literal; SASSERT(m_search_lvl == get_search_level()); } - if (get_cancel_flag()) { - return l_undef; - } } } SASSERT(!inconsistent()); diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 0b3147d6b..5f258fc61 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -1833,7 +1833,7 @@ namespace smt { m_stats.m_num_decisions++; push_scope(); - TRACE("context", tout << "splitting, lvl: " << m_scope_lvl << "\n";); + TRACE("decide", tout << "splitting, lvl: " << m_scope_lvl << "\n";); TRACE("decide_detail", tout << mk_pp(bool_var2expr(var), m_manager) << "\n";); @@ -2949,7 +2949,11 @@ namespace smt { if (!m_asserted_formulas.inconsistent()) { unsigned sz = m_asserted_formulas.get_num_formulas(); unsigned qhead = m_asserted_formulas.get_qhead(); - while (qhead < sz && !m_manager.canceled()) { + while (qhead < sz) { + if (get_cancel_flag()) { + m_asserted_formulas.commit(qhead); + return; + } expr * f = m_asserted_formulas.get_formula(qhead); proof * pr = m_asserted_formulas.get_formula_proof(qhead); internalize_assertion(f, pr, 0); diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index dfb1389c2..01471c603 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1356,6 +1356,8 @@ namespace smt { expr_ref antecedent2fml(uint_set const& ante); + literal mk_diseq(expr* v, expr* val); + void validate_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector const& conseq, expr_ref_vector const& unfixed); diff --git a/src/util/rlimit.cpp b/src/util/rlimit.cpp index b3f055955..37b1f7904 100644 --- a/src/util/rlimit.cpp +++ b/src/util/rlimit.cpp @@ -36,7 +36,7 @@ bool reslimit::inc() { bool reslimit::inc(unsigned offset) { m_count += offset; - return !m_cancel && (m_limit == 0 || m_count <= m_limit); + return m_cancel == 0 && (m_limit == 0 || m_count <= m_limit); } void reslimit::push(unsigned delta_limit) {