mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-26 18:45:33 +00:00
Code Activity

fix #2802

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-12-13 13:02:49 -08:00
parent a069b65669
commit c560ee54e8
3 changed files with 16 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_clause_proof.cpp
View file

@ -99,7 +99,7 @@ namespace smt {
}
void clause_proof::update(status st, expr_ref_vector& v, proof* p) {
TRACE("clause_proof", tout << st << " " << v << "\n";);
TRACE("clause_proof", tout << m_trail.size() << " " << st << " " << v << "\n";);
IF_VERBOSE(3, verbose_stream() << st << " " << v << "\n");
m_trail.push_back(info(st, v, p));
}

22
src/smt/smt_solver.cpp
View file

@ -88,24 +88,24 @@ namespace smt {
smt_solver * result = alloc(smt_solver, m, p, m_logic);
smt::kernel::copy(m_context, result->m_context);
if (mc0())
result->set_model_converter(mc0()->translate(translator));
for (auto & kv : m_name2assertion) {
expr* val = translator(kv.m_value);
expr* t = translator(kv.m_key);
result->m_name2assertion.insert(t, val);
result->solver_na2as::assert_expr(val, t);
m.inc_ref(val);
expr* key = translator(kv.m_key);
result->assert_expr(val, key);
}
return result;
}
~smt_solver() override {
dec_ref_values(get_manager(), m_name2assertion);
dealloc(m_cuber);
for (auto& kv : m_name2assertion) {
get_manager().dec_ref(kv.m_key);
get_manager().dec_ref(kv.m_value);
}
}
void updt_params(params_ref const & p) override {
@ -159,6 +159,7 @@ namespace smt {
}
solver_na2as::assert_expr_core2(t, a);
get_manager().inc_ref(t);
get_manager().inc_ref(a);
m_name2assertion.insert(a, t);
}
@ -173,13 +174,12 @@ namespace smt {
SASSERT(n <= lvl);
unsigned new_lvl = lvl - n;
unsigned old_sz = m_scopes[new_lvl];
for (unsigned i = cur_sz; i > old_sz; ) {
--i;
expr * key = m_assumptions[i].get();
SASSERT(m_name2assertion.contains(key));
for (unsigned i = cur_sz; i-- > old_sz; ) {
expr * key = m_assumptions.get(i);
expr * value = m_name2assertion.find(key);
m.dec_ref(value);
m_name2assertion.erase(key);
m.dec_ref(value);
m.dec_ref(key);
}
}
m_context.pop(n);

15
src/smt/theory_seq.cpp
View file

@ -5632,17 +5632,10 @@ void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, liter
TRACE("seq", ctx.display_literals_verbose(tout << "assert:", lits) << "\n";);
m_new_propagation = true;
++m_stats.m_add_axiom;
{
std::function<expr*(void)> fn = [&]() { return m.mk_or(exprs.size(), exprs.c_ptr()); };
scoped_trace_stream _sts(*this, fn);
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
}
#if 0
if (!ctx.at_base_level() && l2 == null_literal) {
m_trail_stack.push(push_replay(alloc(replay_unit_literal, m, ctx.bool_var2expr(l1.var()), l1.sign())));
}
#endif
std::function<expr*(void)> fn = [&]() { return m.mk_or(exprs.size(), exprs.c_ptr()); };
scoped_trace_stream _sts(*this, fn);
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
}