diff --git a/src/ast/rewriter/maximize_ac_sharing.cpp b/src/ast/rewriter/maximize_ac_sharing.cpp index b560132db..d7e8df7a2 100644 --- a/src/ast/rewriter/maximize_ac_sharing.cpp +++ b/src/ast/rewriter/maximize_ac_sharing.cpp @@ -151,11 +151,7 @@ void maximize_ac_sharing::restore_entries(unsigned old_lim) { } void maximize_ac_sharing::reset() { - restore_entries(0); - m_entries.reset(); m_cache.reset(); - m_region.reset(); - m_scopes.reset(); } void maximize_bv_sharing::init_core() { diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index c52ad851c..11cc846b8 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -170,7 +170,7 @@ void asserted_formulas::get_assertions(ptr_vector & result) const { void asserted_formulas::push_scope() { SASSERT(inconsistent() || m_qhead == m_formulas.size() || m.canceled()); - TRACE("asserted_formulas_scopes", tout << "push:\n"; display(tout);); + TRACE("asserted_formulas_scopes", tout << "before push: " << m_scopes.size() << "\n";); m_scoped_substitution.push(); m_scopes.push_back(scope()); scope & s = m_scopes.back(); @@ -181,10 +181,11 @@ void asserted_formulas::push_scope() { m_bv_sharing.push_scope(); m_macro_manager.push_scope(); commit(); + TRACE("asserted_formulas_scopes", tout << "after push: " << m_scopes.size() << "\n";); } void asserted_formulas::pop_scope(unsigned num_scopes) { - TRACE("asserted_formulas_scopes", tout << "before pop " << num_scopes << "\n"; display(tout);); + TRACE("asserted_formulas_scopes", tout << "before pop " << num_scopes << " of " << m_scopes.size() << "\n";); m_bv_sharing.pop_scope(num_scopes); m_macro_manager.pop_scope(num_scopes); unsigned new_lvl = m_scopes.size() - num_scopes; @@ -196,7 +197,7 @@ void asserted_formulas::pop_scope(unsigned num_scopes) { m_qhead = s.m_formulas_lim; m_scopes.shrink(new_lvl); flush_cache(); - TRACE("asserted_formulas_scopes", tout << "after pop " << num_scopes << "\n"; display(tout);); + TRACE("asserted_formulas_scopes", tout << "after pop " << num_scopes << "\n";); } void asserted_formulas::reset() { diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 901f4b5ac..ac7b1f44b 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -487,6 +487,7 @@ namespace smt { */ void context::add_eq(enode * n1, enode * n2, eq_justification js) { unsigned old_trail_size = m_trail_stack.size(); + scoped_suspend_rlimit _suspend_cancel(m_manager.limit()); try { TRACE("add_eq", tout << "assigning: #" << n1->get_owner_id() << " = #" << n2->get_owner_id() << "\n";); @@ -541,10 +542,14 @@ namespace smt { mark_as_relevant(r1); } + TRACE("add_eq", tout << "to trail\n";); + push_trail(add_eq_trail(r1, n1, r2->get_num_parents())); + TRACE("add_eq", tout << "qmanager add_eq\n";); m_qmanager->add_eq_eh(r1, r2); + TRACE("add_eq", tout << "merge theory_vars\n";); merge_theory_vars(n2, n1, js); // 'Proof' tree @@ -577,6 +582,7 @@ namespace smt { #endif + TRACE("add_eq", tout << "remove_parents_from_cg_table\n";); remove_parents_from_cg_table(r1); enode * curr = r1; @@ -588,8 +594,10 @@ namespace smt { SASSERT(r1->get_root() == r2); + TRACE("add_eq", tout << "reinsert_parents_into_cg_table\n";); reinsert_parents_into_cg_table(r1, r2, n1, n2, js); + TRACE("add_eq", tout << "propagate_bool_enode_assignment\n";); if (n2->is_bool()) propagate_bool_enode_assignment(r1, r2, n1, n2); @@ -604,6 +612,7 @@ namespace smt { catch (...) { // Restore trail size since procedure was interrupted in the middle. // If the add_eq_trail remains on the trail stack, then Z3 may crash when the destructor is invoked. + TRACE("add_eq", tout << "add_eq interrupted. This is unsafe " << m_manager.limit().get_cancel_flag() << "\n";); m_trail_stack.shrink(old_trail_size); throw; } @@ -972,7 +981,7 @@ namespace smt { enode * parent = *it; if (parent->is_cgc_enabled()) { TRACE("add_eq_parents", tout << "removing: #" << parent->get_owner_id() << "\n";); - CTRACE("add_eq", !parent->is_cgr(), + CTRACE("add_eq", !parent->is_cgr() || !m_cg_table.contains_ptr(parent), tout << "old num_parents: " << r2_num_parents << ", num_parents: " << r2->m_parents.size() << ", parent: #" << parent->get_owner_id() << ", parents: \n"; for (unsigned i = 0; i < r2->m_parents.size(); i++) { diff --git a/src/util/rlimit.cpp b/src/util/rlimit.cpp index f3f45c654..e625cab95 100644 --- a/src/util/rlimit.cpp +++ b/src/util/rlimit.cpp @@ -21,6 +21,7 @@ Revision History: reslimit::reslimit(): m_cancel(0), + m_suspend(false), m_count(0), m_limit(0) { } @@ -31,12 +32,12 @@ uint64 reslimit::count() const { bool reslimit::inc() { ++m_count; - return m_cancel == 0 && (m_limit == 0 || m_count <= m_limit); + return (m_cancel == 0 && (m_limit == 0 || m_count <= m_limit)) || m_suspend; } bool reslimit::inc(unsigned offset) { m_count += offset; - return m_cancel == 0 && (m_limit == 0 || m_count <= m_limit); + return (m_cancel == 0 && (m_limit == 0 || m_count <= m_limit)) || m_suspend; } void reslimit::push(unsigned delta_limit) { diff --git a/src/util/rlimit.h b/src/util/rlimit.h index 3b278d132..0c81f9449 100644 --- a/src/util/rlimit.h +++ b/src/util/rlimit.h @@ -23,12 +23,14 @@ Revision History: class reslimit { volatile unsigned m_cancel; + bool m_suspend; uint64 m_count; uint64 m_limit; svector m_limits; ptr_vector m_children; void set_cancel(unsigned f); + friend class scoped_suspend_rlimit; public: reslimit(); @@ -42,7 +44,7 @@ public: uint64 count() const; - bool get_cancel_flag() const { return m_cancel > 0; } + bool get_cancel_flag() const { return m_cancel > 0 && !m_suspend; } char const* get_cancel_msg() const; void cancel(); void reset_cancel(); @@ -61,6 +63,17 @@ public: }; +class scoped_suspend_rlimit { + reslimit & m_limit; +public: + scoped_suspend_rlimit(reslimit& r): m_limit(r) { + r.m_suspend = true; + } + ~scoped_suspend_rlimit() { + m_limit.m_suspend = false; + } +}; + struct scoped_limits { reslimit& m_limit; unsigned m_sz;