Skip to content

Commit

Permalink
add context::internalize() API that takes multiple expressions at once (
Browse files Browse the repository at this point in the history 
#4488)
  • Loading branch information
@nunoplopes
nunoplopes authored Jun 1, 2020
1 parent e634f29 commit e079af9
Show file tree
Hide file tree
Showing 5 changed files with 60 additions and 49 deletions.
12 changes: 7 additions & 5 deletions src/smt/smt_context.h
View file
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
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
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
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
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

0 comments on commit e079af9

Please sign in to comment.