mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

fix #3625

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-31 12:30:13 -07:00
parent 0ff97d5a31
commit 2b5247a37b
4 changed files with 35 additions and 37 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/smt/smt_context.cpp
View file

@ -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);

3
src/smt/theory_arith_core.h
View file

@ -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);

56
src/smt/theory_arith_int.h
View file

@ -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<expr*(void)> 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<unsigned> var2index; // map theory variables to positions in 'rows'.
u_map<theory_var> 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<expr*(void)> 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<expr*(void)> 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<expr*(void)> 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);

10
src/smt/theory_arith_nl.h
View file

@ -804,13 +804,11 @@ bool theory_arith<Ext>::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<expr*(void)> 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());