From e079af9d0d372e3490e034ace4cb323dac7a7ec1 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 1 Jun 2020 19:51:39 +0100 Subject: [PATCH] add context::internalize() API that takes multiple expressions at once (#4488) --- src/smt/smt_context.h | 12 +++++--- src/smt/smt_internalizer.cpp | 57 +++++++++++++++++++++++------------ src/smt/theory_array_full.cpp | 2 +- src/smt/theory_bv.cpp | 26 ++++++++-------- src/smt/theory_fpa.cpp | 12 ++------ 5 files changed, 60 insertions(+), 49 deletions(-) diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index a766ca1a54c..d3fd26446e1 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -741,7 +741,12 @@ namespace smt { bool should_internalize_rec(expr* e) const; - void top_sort_expr(expr * n, svector & sorted_exprs); + void top_sort_expr(expr* const* exprs, unsigned num_exprs, svector & sorted_exprs); + + void internalize_rec(expr * n, bool gate_ctx); + + void internalize_deep(expr * n); + void internalize_deep(expr* const* n, unsigned num_exprs); void assert_default(expr * n, proof * pr); @@ -868,6 +873,7 @@ namespace smt { void ensure_internalized(expr* e); void internalize(expr * n, bool gate_ctx); + void internalize(expr* const* exprs, unsigned num_exprs, bool gate_ctx); void internalize(expr * n, bool gate_ctx, unsigned generation); @@ -906,10 +912,6 @@ namespace smt { public: - void internalize_rec(expr * n, bool gate_ctx); - - void internalize_deep(expr * n); - // helper function for trail void undo_th_case_split(literal l); diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 55018d3f1c3..a198984529a 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -152,11 +152,9 @@ namespace smt { return visited; } - void context::top_sort_expr(expr * n, svector & sorted_exprs) { - ts_todo.reset(); + void context::top_sort_expr(expr* const* exprs, unsigned num_exprs, svector & sorted_exprs) { tcolors.reset(); fcolors.reset(); - ts_todo.push_back(expr_bool_pair(n, true)); while (!ts_todo.empty()) { expr_bool_pair & p = ts_todo.back(); expr * curr = p.first; @@ -166,12 +164,14 @@ namespace smt { set_color(tcolors, fcolors, curr, gate_ctx, Grey); ts_visit_children(curr, gate_ctx, ts_todo); break; - case Grey: + case Grey: { SASSERT(ts_visit_children(curr, gate_ctx, ts_todo)); set_color(tcolors, fcolors, curr, gate_ctx, Black); - if (n != curr && !m.is_not(curr)) + auto end = exprs + num_exprs; + if (std::find(exprs, end, curr) == end && !m.is_not(curr) && should_internalize_rec(curr)) sorted_exprs.push_back(expr_bool_pair(curr, gate_ctx)); break; + } case Black: ts_todo.pop_back(); break; @@ -189,23 +189,33 @@ namespace smt { 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) { - 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 - // 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);); - svector 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) { - expr* e = kv.first; - if (should_internalize_rec(e)) - internalize_rec(e, kv.second); + + void context::internalize_deep(expr* const* exprs, unsigned num_exprs) { + ts_todo.reset(); + for (unsigned i = 0; i < num_exprs; ++i) { + expr * n = exprs[i]; + 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 + // 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);); + ts_todo.push_back(expr_bool_pair(n, true)); } } + + svector sorted_exprs; + top_sort_expr(exprs, num_exprs, sorted_exprs); + TRACE("deep_internalize", for (auto & kv : sorted_exprs) tout << "#" << kv.first->get_id() << " " << kv.second << "\n"; ); + for (auto & kv : sorted_exprs) { + expr* e = kv.first; + SASSERT(should_internalize_rec(e)); + internalize_rec(e, kv.second); + } + } + void context::internalize_deep(expr* n) { + expr * v[1] = { n }; + internalize_deep(v, 1); } /** @@ -343,6 +353,13 @@ namespace smt { internalize_rec(n, gate_ctx); } + void context::internalize(expr* const* exprs, unsigned num_exprs, bool gate_ctx) { + internalize_deep(exprs, num_exprs); + for (unsigned i = 0; i < num_exprs; ++i) { + internalize_rec(exprs[i], gate_ctx); + } + } + void context::internalize_rec(expr * n, bool gate_ctx) { TRACE("internalize", tout << "internalizing:\n" << mk_pp(n, m) << "\n";); TRACE("internalize_bug", tout << "internalizing:\n" << mk_bounded_pp(n, m) << "\n";); diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp index c6e4c106d41..8679c4dd9ee 100644 --- a/src/smt/theory_array_full.cpp +++ b/src/smt/theory_array_full.cpp @@ -398,7 +398,7 @@ namespace smt { if (!is_default(n) && !is_select(n) && !is_map(n) && !is_const(n) && !is_as_array(n)){ return; } - if (!ctx.e_internalized(n)) ctx.internalize(n, false);; + ctx.ensure_internalized(n); enode* node = ctx.get_enode(n); if (is_select(n)) { enode * arg = ctx.get_enode(n->get_arg(0)); diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 6e96b0b0129..4ec312541da 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -23,6 +23,7 @@ Revision History: #include "ast/bv_decl_plugin.h" #include "smt/smt_model_generator.h" #include "util/stats.h" +#include "util/vector.h" #define WATCH_DISEQ 0 @@ -142,9 +143,7 @@ namespace smt { } void theory_bv::process_args(app * n) { - for (expr* arg : *n) { - ctx.internalize(arg, false); - } + ctx.internalize(n->get_args(), n->get_num_args(), false); } enode * theory_bv::mk_enode(app * n) { @@ -312,13 +311,16 @@ namespace smt { unsigned sz = bits.size(); SASSERT(get_bv_size(n) == sz); m_bits[v].reset(); + + ptr_vector bits_exprs; + for (unsigned i = 0; i < sz; ++i) + bits_exprs.push_back(bits.get(i)); + ctx.internalize(bits_exprs.c_ptr(), sz, true); + for (unsigned i = 0; i < sz; i++) { expr * bit = bits.get(i); - expr_ref s_bit(m); - simplify_bit(bit, s_bit); - ctx.internalize(s_bit, true); - literal l = ctx.get_literal(s_bit.get()); - TRACE("init_bits", tout << "bit " << i << " of #" << n->get_owner_id() << "\n" << mk_ll_pp(s_bit, m) << "\n";); + literal l = ctx.get_literal(bit); + TRACE("init_bits", tout << "bit " << i << " of #" << n->get_owner_id() << "\n" << mk_ll_pp(bit, m) << "\n";); add_bit(v, l); } find_wpos(v); @@ -983,9 +985,7 @@ namespace smt { } bool theory_bv::internalize_carry(app * n, bool gate_ctx) { - ctx.internalize(n->get_arg(0), true); - ctx.internalize(n->get_arg(1), true); - ctx.internalize(n->get_arg(2), true); + ctx.internalize(n->get_args(), 3, true); bool is_new_var = false; bool_var v; if (!ctx.b_internalized(n)) { @@ -1016,9 +1016,7 @@ namespace smt { } bool theory_bv::internalize_xor3(app * n, bool gate_ctx) { - ctx.internalize(n->get_arg(0), true); - ctx.internalize(n->get_arg(1), true); - ctx.internalize(n->get_arg(2), true); + ctx.internalize(n->get_args(), 3, true); bool is_new_var = false; bool_var v; if (!ctx.b_internalized(n)) { diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 7c97dbc52f9..dadff152ae8 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -415,9 +415,7 @@ namespace smt { if (ctx.b_internalized(atom)) return true; - unsigned num_args = atom->get_num_args(); - for (unsigned i = 0; i < num_args; i++) - ctx.internalize(atom->get_arg(i), false); + ctx.internalize(atom->get_args(), atom->get_num_args(), false); literal l(ctx.mk_bool_var(atom)); ctx.set_var_theory(l.var(), get_id()); @@ -436,9 +434,7 @@ namespace smt { SASSERT(term->get_family_id() == get_family_id()); SASSERT(!ctx.e_internalized(term)); - unsigned num_args = term->get_num_args(); - for (unsigned i = 0; i < num_args; i++) - ctx.internalize(term->get_arg(i), false); + ctx.internalize(term->get_args(), term->get_num_args(), false); enode * e = ctx.mk_enode(term, false, false, true); @@ -697,9 +693,7 @@ namespace smt { } enode* theory_fpa::ensure_enode(expr* e) { - if (!ctx.e_internalized(e)) { - ctx.internalize(e, false); - } + ctx.ensure_internalized(e); enode* n = ctx.get_enode(e); ctx.mark_as_relevant(n); return n;