From 2b5247a37b9385a7e7259e0279fa49984132b291 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 31 Mar 2020 12:30:13 -0700 Subject: [PATCH] fix #3625 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 3 +- src/smt/theory_arith_core.h | 3 +- src/smt/theory_arith_int.h | 56 ++++++++++++++++++------------------- src/smt/theory_arith_nl.h | 10 +++---- 4 files changed, 35 insertions(+), 37 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index f25079db5..d9219fcb6 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -2929,8 +2929,9 @@ namespace smt { TRACE("flush", tout << "m_scope_lvl: " << m_scope_lvl << "\n";); m_relevancy_propagator = nullptr; m_model_generator->reset(); - for (theory* t : m_theory_set) + for (theory* t : m_theory_set) { t->flush_eh(); + } del_clauses(m_aux_clauses, 0); del_clauses(m_lemmas, 0); del_justifications(m_justifications, 0); diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 3f0f37d1f..eab01c5f5 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -500,8 +500,7 @@ namespace smt { // literal lits[2] = {l_ante, l_conseq}; if (m.has_trace_stream()) { - app_ref body(m); - body = m.mk_or(ante, conseq); + app_ref body(m.mk_or(ante, conseq), m); log_axiom_instantiation(body); } mk_clause(l_ante, l_conseq, 0, nullptr); diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h index 5ef809267..fe3b3d4c8 100644 --- a/src/smt/theory_arith_int.h +++ b/src/smt/theory_arith_int.h @@ -216,16 +216,14 @@ namespace smt { expr_ref bound(m); expr* e = get_enode(v)->get_owner(); bound = m_util.mk_ge(e, m_util.mk_numeral(_k, m_util.is_int(e))); - if (m.has_trace_stream()) { - app_ref body(m); - body = m.mk_or(to_app(bound), m.mk_not(to_app(bound))); - log_axiom_instantiation(body); - } - TRACE("arith_int", tout << mk_bounded_pp(bound, m) << "\n";); context & ctx = get_context(); - ctx.internalize(bound, true); - ctx.mark_as_relevant(bound.get()); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; + { + std::function fn = [&]() { return m.mk_or(bound, m.mk_not(bound)); }; + scoped_trace_stream _sts(*this, fn); + TRACE("arith_int", tout << mk_bounded_pp(bound, m) << "\n";); + ctx.internalize(bound, true); + ctx.mark_as_relevant(bound.get()); + } } @@ -247,6 +245,7 @@ namespace smt { u_map var2index; // map theory variables to positions in 'rows'. u_map index2var; // map back positions in 'rows' to theory variables. context& ctx = get_context(); + ast_manager& m = get_manager(); if (ctx.get_cancel_flag()) return false; @@ -378,19 +377,16 @@ namespace smt { } mk_polynomial_ge(pol.size(), pol.c_ptr(), unsat_row[0]+rational(1), p2); - if (get_manager().has_trace_stream()) { - app_ref body(get_manager()); - body = get_manager().mk_or(p1, p2); - log_axiom_instantiation(body); + { + std::function fn = [&]() { return m.mk_or(p1, p2); }; + scoped_trace_stream _sts(*this, fn); + ctx.internalize(p1, false); + ctx.internalize(p2, false); + literal l1(ctx.get_literal(p1)), l2(ctx.get_literal(p2)); + ctx.mark_as_relevant(p1.get()); + ctx.mark_as_relevant(p2.get()); + ctx.mk_th_axiom(get_id(), l1, l2); } - ctx.internalize(p1, false); - ctx.internalize(p2, false); - literal l1(ctx.get_literal(p1)), l2(ctx.get_literal(p2)); - ctx.mark_as_relevant(p1.get()); - ctx.mark_as_relevant(p2.get()); - - ctx.mk_th_axiom(get_id(), l1, l2); - if (get_manager().has_trace_stream()) get_manager().trace_stream() << "[end-of-instance]\n"; TRACE("arith_int", tout << "cut: (or " << mk_pp(p1, get_manager()) << " " << mk_pp(p2, get_manager()) << ")\n"; @@ -417,11 +413,13 @@ namespace smt { theory_var v = it->m_var; expr* e = get_enode(v)->get_owner(); bool _is_int = m_util.is_int(e); - expr * bound = m_util.mk_ge(e, m_util.mk_numeral(rational::zero(), _is_int)); + expr_ref bound(m_util.mk_ge(e, m_util.mk_numeral(rational::zero(), _is_int)), get_manager()); context & ctx = get_context(); - if (get_manager().has_trace_stream()) log_axiom_instantiation(bound); - ctx.internalize(bound, true); - if (get_manager().has_trace_stream()) get_manager().trace_stream() << "[end-of-instance]\n"; + { + std::function fn = [&]() { return bound; }; + scoped_trace_stream _sts(*this, fn); + ctx.internalize(bound, true); + } ctx.mark_as_relevant(bound); result = true; } @@ -669,9 +667,11 @@ namespace smt { TRACE("gomory_cut", tout << "new cut:\n" << bound << "\n"; ante.display(tout);); literal l = null_literal; context & ctx = get_context(); - if (get_manager().has_trace_stream()) log_axiom_instantiation(bound); - ctx.internalize(bound, true); - if (get_manager().has_trace_stream()) get_manager().trace_stream() << "[end-of-instance]\n"; + { + std::function fn = [&]() { return bound; }; + scoped_trace_stream _sts(*this, fn); + ctx.internalize(bound, true); + } l = ctx.get_literal(bound); ctx.mark_as_relevant(l); dump_lemmas(l, ante); diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index c7550bf4b..c167ccb2f 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -804,13 +804,11 @@ bool theory_arith::branch_nl_int_var(theory_var v) { TRACE("non_linear", tout << "new bound:\n" << mk_pp(bound, get_manager()) << "\n";); context & ctx = get_context(); ast_manager & m = get_manager(); - if (m.has_trace_stream()) { - app_ref body(m); - body = m.mk_or(bound, m.mk_not(bound)); - log_axiom_instantiation(body); + { + std::function fn = [&]() { return m.mk_or(bound, m.mk_not(bound)); }; + scoped_trace_stream _sts(*this, fn); + ctx.internalize(bound, true); } - ctx.internalize(bound, true); - if (m.has_trace_stream()) m.trace_stream() << "[end-of-instance]\n"; ctx.mark_as_relevant(bound.get()); literal l = ctx.get_literal(bound); SASSERT(!l.sign());