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

block deep based on condition for internalization #4192

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-05-31 13:31:04 -07:00
parent 7d4c9e6126
commit c424165d94
2 changed files with 13 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_context.h
View file

@ -739,6 +739,8 @@ namespace smt {
char_vector tcolors; char_vector tcolors;
char_vector fcolors; char_vector fcolors;
bool should_internalize_rec(expr* e) const;
void top_sort_expr(expr * n, svector<expr_bool_pair> & sorted_exprs); void top_sort_expr(expr * n, svector<expr_bool_pair> & sorted_exprs);
void assert_default(expr * n, proof * pr); void assert_default(expr * n, proof * pr);

16
src/smt/smt_internalizer.cpp
View file

@ -109,6 +109,8 @@ namespace smt {
bool context::ts_visit_children(expr * n, bool gate_ctx, svector<expr_bool_pair> & todo) { bool context::ts_visit_children(expr * n, bool gate_ctx, svector<expr_bool_pair> & todo) {
if (is_quantifier(n)) if (is_quantifier(n))
return true; return true;
if (!should_internalize_rec(n))
return true;
SASSERT(is_app(n)); SASSERT(is_app(n));
if (m.is_bool(n)) { if (m.is_bool(n)) {
if (b_internalized(n)) if (b_internalized(n))
@ -181,8 +183,15 @@ namespace smt {
#define DEEP_EXPR_THRESHOLD 1024 #define DEEP_EXPR_THRESHOLD 1024
bool context::should_internalize_rec(expr* e) const {
return !is_app(e) ||
!m.is_bool(e) ||
to_app(e)->get_family_id() == null_family_id ||
to_app(e)->get_family_id() == m.get_basic_family_id();
}
void context::internalize_deep(expr* n) { void context::internalize_deep(expr* n) {
if (!e_internalized(n) && ::get_depth(n) > DEEP_EXPR_THRESHOLD) { if (!e_internalized(n) && ::get_depth(n) > DEEP_EXPR_THRESHOLD && should_internalize_rec(n)) {
// if the expression is deep, then execute topological sort to avoid // if the expression is deep, then execute topological sort to avoid
// stack overflow. // stack overflow.
// a caveat is that theory internalizers do rely on recursive descent so // a caveat is that theory internalizers do rely on recursive descent so
@ -193,10 +202,7 @@ namespace smt {
TRACE("deep_internalize", for (auto & kv : sorted_exprs) tout << "#" << kv.first->get_id() << " " << kv.second << "\n"; ); TRACE("deep_internalize", for (auto & kv : sorted_exprs) tout << "#" << kv.first->get_id() << " " << kv.second << "\n"; );
for (auto & kv : sorted_exprs) { for (auto & kv : sorted_exprs) {
expr* e = kv.first; expr* e = kv.first;
if (!is_app(e) || if (should_internalize_rec(e))
!m.is_bool(e) ||
to_app(e)->get_family_id() == null_family_id ||
to_app(e)->get_family_id() == m.get_basic_family_id())
internalize_rec(e, kv.second); internalize_rec(e, kv.second);
} }
} }