mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

fix #1266 by bypassing topological ordering on theory symbols

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-09-24 09:19:51 -07:00
parent 2751cbc270
commit 7a15de374a
1 changed files with 9 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/smt/smt_internalizer.cpp
View file

@ -198,11 +198,19 @@ namespace smt {
if (get_depth(n) > DEEP_EXPR_THRESHOLD) {
// if the expression is deep, then execute topological sort to avoid
// stack overflow.
// a caveat is that theory internalizers do rely on recursive descent so
// internalization over these follows top-down
TRACE("deep_internalize", tout << "expression is deep: #" << n->get_id() << "\n" << mk_ll_pp(n, m_manager););
svector<expr_bool_pair> sorted_exprs;
top_sort_expr(n, sorted_exprs);
TRACE("deep_internalize", for (auto & kv : sorted_exprs) tout << "#" << kv.first->get_id() << " " << kv.second << "\n"; );
for (auto & kv : sorted_exprs) internalize(kv.first, kv.second);
for (auto & kv : sorted_exprs) {
expr* e = kv.first;
if (!is_app(e) ||
to_app(e)->get_family_id() == null_family_id ||
to_app(e)->get_family_id() == m_manager.get_basic_family_id())
internalize(e, kv.second);
}
}
SASSERT(m_manager.is_bool(n));
if (is_gate(m_manager, n)) {