Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add context::internalize() API that takes multiple expressions at once #4488

Merged
merged 1 commit into from
Jun 1, 2020
Merged

Add context::internalize() API that takes multiple expressions at once #4488

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 7 additions & 5 deletions src/smt/smt_context.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -741,7 +741,12 @@ namespace smt {

bool should_internalize_rec(expr* e) const;

void top_sort_expr(expr * n, svector<expr_bool_pair> & sorted_exprs);
void top_sort_expr(expr* const* exprs, unsigned num_exprs, svector<expr_bool_pair> & 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);

Expand Down Expand Up @@ -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);

Expand Down Expand Up @@ -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);

Expand Down
57 changes: 37 additions & 20 deletions src/smt/smt_internalizer.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -152,11 +152,9 @@ namespace smt {
return visited;
}

void context::top_sort_expr(expr * n, svector<expr_bool_pair> & sorted_exprs) {
ts_todo.reset();
void context::top_sort_expr(expr* const* exprs, unsigned num_exprs, svector<expr_bool_pair> & 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;
Expand All @@ -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;
Expand All @@ -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<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) {
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<expr_bool_pair> 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);
}

/**
Expand Down Expand Up @@ -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";);
Expand Down
2 changes: 1 addition & 1 deletion src/smt/theory_array_full.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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));
Expand Down
26 changes: 12 additions & 14 deletions src/smt/theory_bv.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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) {
Expand Down Expand Up @@ -312,13 +311,16 @@ namespace smt {
unsigned sz = bits.size();
SASSERT(get_bv_size(n) == sz);
m_bits[v].reset();

ptr_vector<expr> 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);
Expand Down Expand Up @@ -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)) {
Expand Down Expand Up @@ -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)) {
Expand Down
12 changes: 3 additions & 9 deletions src/smt/theory_fpa.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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());
Expand All @@ -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);

Expand Down Expand Up @@ -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;
Expand Down