mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

move deep internalization out of theory_seq

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-19 11:19:32 -07:00
parent b92b6c0fc6
commit 19e0285b83
2 changed files with 0 additions and 43 deletions
Download patch file Download diff file Expand all files Collapse all files

40
src/smt/theory_seq.cpp
View file

@ -302,7 +302,6 @@ theory_seq::theory_seq(ast_manager& m, theory_seq_params const & params):
m_ax(*this, m_rewrite), m_ax(*this, m_rewrite),
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_has_seq(m_util.has_seq()), m_has_seq(m_util.has_seq()),
@ -2081,12 +2080,6 @@ 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));
@ -3257,39 +3250,6 @@ expr_ref theory_seq::mk_len(expr* s) {
return result; return result;
} }
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) {
if (!m_ensure_todo.empty()) return;
context& ctx = get_context();
if (ctx.e_internalized(e)) return;
m_ensure_todo.push_back(e);
expr_mark visited;
for (unsigned i = 0; i < m_ensure_todo.size(); ++i) {
e = m_ensure_todo[i];
if (is_app(e) && to_app(e)->get_family_id() == m_util.get_family_id()) {
for (expr* arg : *to_app(e)) {
if (!ctx.e_internalized(arg) && !visited.is_marked(arg)) {
m_ensure_todo.push_back(arg);
visited.mark(arg);
}
}
}
}
compare_depth cd;
std::stable_sort(m_ensure_todo.begin(), m_ensure_todo.end(), cd);
for (expr* e : m_ensure_todo) {
ensure_enode(e);
}
m_ensure_todo.reset();
}
template <class T> template <class T>
static T* get_th_arith(context& ctx, theory_id afid, expr* e) { static T* get_th_arith(context& ctx, theory_id afid, expr* e) {

3
src/smt/theory_seq.h
View file

@ -407,7 +407,6 @@ namespace smt {
th_trail_stack m_trail_stack; th_trail_stack m_trail_stack;
stats m_stats; stats m_stats;
ptr_vector<expr> m_todo, m_concat; ptr_vector<expr> m_todo, m_concat;
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;
bool m_has_seq; bool m_has_seq;
@ -630,8 +629,6 @@ namespace smt {
expr_ref mk_sub(expr* a, expr* b); expr_ref mk_sub(expr* a, expr* b);
expr_ref mk_add(expr* a, expr* b); expr_ref mk_add(expr* a, expr* b);
expr_ref mk_len(expr* s); expr_ref mk_len(expr* s);
ptr_vector<expr> m_ensure_todo;
void ensure_enodes(expr* e);
enode* get_root(expr* a) { return ensure_enode(a)->get_root(); } enode* get_root(expr* a) { return ensure_enode(a)->get_root(); }
dependency* mk_join(dependency* deps, literal lit); dependency* mk_join(dependency* deps, literal lit);
dependency* mk_join(dependency* deps, literal_vector const& lits); dependency* mk_join(dependency* deps, literal_vector const& lits);