mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

defer blocking propagation until all properties of literal have been axiomatized. Deals with seq part of #2071

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-01-07 09:00:11 -08:00
parent fb397cbe25
commit cec34c745a
1 changed files with 10 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

17
src/smt/theory_seq.cpp
View file

@ -262,6 +262,7 @@ final_check_status theory_seq::final_check_eh() {
m_new_propagation = false; m_new_propagation = false;
TRACE("seq", display(tout << "level: " << get_context().get_scope_level() << "\n");); TRACE("seq", display(tout << "level: " << get_context().get_scope_level() << "\n"););
TRACE("seq_verbose", get_context().display(tout);); TRACE("seq_verbose", get_context().display(tout););
if (simplify_and_solve_eqs()) { if (simplify_and_solve_eqs()) {
++m_stats.m_solve_eqs; ++m_stats.m_solve_eqs;
TRACEFIN("solve_eqs"); TRACEFIN("solve_eqs");
@ -5559,14 +5560,9 @@ void theory_seq::propagate_accept(literal lit, expr* acc) {
propagate_lit(nullptr, 1, &lit, false_literal); propagate_lit(nullptr, 1, &lit, false_literal);
return; return;
} }
if (_idx.get_unsigned() > m_max_unfolding_depth &&
m_max_unfolding_lit != null_literal && ctx.get_scope_level() > 0) {
propagate_lit(nullptr, 1, &lit, ~m_max_unfolding_lit);
return;
}
expr_ref len = mk_len(e); expr_ref len = mk_len(e);
literal_vector lits; literal_vector lits;
lits.push_back(~lit); lits.push_back(~lit);
if (aut->is_final_state(src)) { if (aut->is_final_state(src)) {
@ -5576,9 +5572,11 @@ void theory_seq::propagate_accept(literal lit, expr* acc) {
else { else {
propagate_lit(nullptr, 1, &lit, ~mk_literal(m_autil.mk_le(len, idx))); propagate_lit(nullptr, 1, &lit, ~mk_literal(m_autil.mk_le(len, idx)));
} }
eautomaton::moves mvs; eautomaton::moves mvs;
aut->get_moves_from(src, mvs); aut->get_moves_from(src, mvs);
TRACE("seq", tout << mvs.size() << "\n";); TRACE("seq", tout << mk_pp(acc, m) << " #moves " << mvs.size() << "\n";);
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);
@ -5587,6 +5585,11 @@ void theory_seq::propagate_accept(literal lit, expr* acc) {
lits.push_back(step); lits.push_back(step);
} }
ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
if (_idx.get_unsigned() > m_max_unfolding_depth &&
m_max_unfolding_lit != null_literal && ctx.get_scope_level() > 0) {
propagate_lit(nullptr, 1, &lit, ~m_max_unfolding_lit);
}
} }
void theory_seq::add_theory_assumptions(expr_ref_vector & assumptions) { void theory_seq::add_theory_assumptions(expr_ref_vector & assumptions) {