mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-26 07:43:41 +00:00
Code Activity

fix #1968

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-11-27 10:36:03 -08:00
parent 253f457425
commit 2b34e4f738
1 changed files with 7 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/smt/theory_seq.cpp
View file

@ -2133,6 +2133,7 @@ void theory_seq::propagate_lit(dependency* dep, unsigned n, literal const* _lits
if (!linearize(dep, eqs, lits)) if (!linearize(dep, eqs, lits))
return; return;
TRACE("seq", TRACE("seq",
tout << "scope: " << ctx.get_scope_level() << "\n";
ctx.display_detailed_literal(tout << "assert:", lit); ctx.display_detailed_literal(tout << "assert:", lit);
ctx.display_literals_verbose(tout << " <- ", lits); ctx.display_literals_verbose(tout << " <- ", lits);
if (!lits.empty()) tout << "\n"; display_deps(tout, dep);); if (!lits.empty()) tout << "\n"; display_deps(tout, dep););
@ -5509,16 +5510,18 @@ void theory_seq::propagate_step(literal lit, expr* step) {
void theory_seq::propagate_accept(literal lit, expr* acc) { void theory_seq::propagate_accept(literal lit, expr* acc) {
expr *e = nullptr, *idx = nullptr, *re = nullptr; expr *e = nullptr, *idx = nullptr, *re = nullptr;
unsigned src = 0; unsigned src = 0;
context& ctx = get_context();
rational _idx; rational _idx;
eautomaton* aut = nullptr; eautomaton* aut = nullptr;
VERIFY(is_accept(acc, e, idx, re, src, aut)); VERIFY(is_accept(acc, e, idx, re, src, aut));
VERIFY(m_autil.is_numeral(idx, _idx));
VERIFY(aut); VERIFY(aut);
if (aut->is_sink_state(src)) { if (aut->is_sink_state(src)) {
propagate_lit(nullptr, 1, &lit, false_literal); propagate_lit(nullptr, 1, &lit, false_literal);
return; return;
} }
VERIFY(m_autil.is_numeral(idx, _idx)); if (_idx.get_unsigned() > m_max_unfolding_depth &&
if (_idx.get_unsigned() > m_max_unfolding_depth && m_max_unfolding_lit != null_literal) { m_max_unfolding_lit != null_literal && ctx.get_scope_level() > 0) {
propagate_lit(nullptr, 1, &lit, ~m_max_unfolding_lit); propagate_lit(nullptr, 1, &lit, ~m_max_unfolding_lit);
return; return;
} }
@ -5540,11 +5543,11 @@ void theory_seq::propagate_accept(literal lit, expr* acc) {
for (auto const& mv : mvs) { for (auto const& mv : mvs) {
expr_ref nth = mk_nth(e, idx); expr_ref nth = mk_nth(e, idx);
expr_ref t = mv.t()->accept(nth); expr_ref t = mv.t()->accept(nth);
get_context().get_rewriter()(t); ctx.get_rewriter()(t);
literal step = mk_literal(mk_step(e, idx, re, src, mv.dst(), t)); literal step = mk_literal(mk_step(e, idx, re, src, mv.dst(), t));
lits.push_back(step); lits.push_back(step);
} }
get_context().mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
} }
void theory_seq::add_theory_assumptions(expr_ref_vector & assumptions) { void theory_seq::add_theory_assumptions(expr_ref_vector & assumptions) {