mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

fix #2726

Browse source
This commit is contained in:
Nikolaj Bjorner 2019-12-01 20:14:35 -08:00
parent 86c35bc7c1
commit 17d67c1b50
2 changed files with 23 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

24
src/smt/theory_seq.cpp
View file

@ -288,6 +288,7 @@ theory_seq::theory_seq(ast_manager& m, theory_seq_params const & params):
m_autil(m), m_autil(m),
m_arith_value(m), m_arith_value(m),
m_trail_stack(*this), m_trail_stack(*this),
m_internalize_depth(0),
m_ls(m), m_rs(m), m_ls(m), m_rs(m),
m_lhs(m), m_rhs(m), m_lhs(m), m_rhs(m),
m_res(m), m_res(m),
@ -3681,6 +3682,13 @@ bool theory_seq::internalize_term(app* term) {
mk_var(e); mk_var(e);
return true; return true;
} }
flet<unsigned> _depth(m_internalize_depth, m_internalize_depth+1);
if (m_internalize_depth > 50 && m_ensure_todo.empty()) {
ensure_enodes(term);
return true;
}
for (auto arg : *term) { for (auto arg : *term) {
mk_var(ensure_enode(arg)); mk_var(ensure_enode(arg));
} }
@ -5115,6 +5123,14 @@ enode* theory_seq::ensure_enode(expr* e) {
return n; return n;
} }
struct theory_seq::compare_depth {
bool operator()(expr* a, expr* b) const {
unsigned d1 = get_depth(a);
unsigned d2 = get_depth(b);
return d1 < d2 || (d1 == d2 && a->get_id() < b->get_id());
}
};
void theory_seq::ensure_enodes(expr* e) { void theory_seq::ensure_enodes(expr* e) {
if (!m_ensure_todo.empty()) return; if (!m_ensure_todo.empty()) return;
context& ctx = get_context(); context& ctx = get_context();
@ -5132,9 +5148,11 @@ void theory_seq::ensure_enodes(expr* e) {
} }
} }
} }
// TBD: std::stable_sort(m_ensure_todo.begin(), m_ensure_todo.end(), compare_depth); compare_depth cd;
for (unsigned i = m_ensure_todo.size(); i-- > 0; ) { std::stable_sort(m_ensure_todo.begin(), m_ensure_todo.end(), cd);
ensure_enode(m_ensure_todo[i]);
for (expr* e : m_ensure_todo) {
ensure_enode(e);
} }
m_ensure_todo.reset(); m_ensure_todo.reset();
} }

2
src/smt/theory_seq.h
View file

@ -51,6 +51,7 @@ namespace smt {
class seq_value_proc; class seq_value_proc;
struct validate_model_proc; struct validate_model_proc;
struct compare_depth;
// cache to track evaluations under equalities // cache to track evaluations under equalities
class eval_cache { class eval_cache {
@ -383,6 +384,7 @@ namespace smt {
symbol m_tail, m_seq_first, m_seq_last, m_indexof_left, m_indexof_right, m_aut_step; symbol m_tail, m_seq_first, m_seq_last, m_indexof_left, m_indexof_right, m_aut_step;
symbol m_pre, m_post, m_eq, m_seq_align; symbol m_pre, m_post, m_eq, m_seq_align;
ptr_vector<expr> m_todo; ptr_vector<expr> m_todo;
unsigned m_internalize_depth;
expr_ref_vector m_ls, m_rs, m_lhs, m_rhs; expr_ref_vector m_ls, m_rs, m_lhs, m_rhs;
// maintain automata with regular expressions. // maintain automata with regular expressions.