Skip to content

Commit

Permalink
#close 5363
Browse files Browse the repository at this point in the history 
Force in-lining auxiliary functions so that model values can be used by SPACER to retrieve counter-examples. This fixes the issue of terminating without a trace. It does not address inefficiency involved with invoking satisfiability checks to retrieve models during trace construction.
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Jun 22, 2021
1 parent 55daa24 commit d5c6abe
Show file tree
Hide file tree
Showing 3 changed files with 32 additions and 29 deletions.
10 changes: 4 additions & 6 deletions src/model/func_interp.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -369,16 +369,14 @@ expr_ref func_interp::get_array_interp_core(func_decl * f) const {
if (m_else == nullptr)
return r;
ptr_vector<sort> domain;
for (sort* s : *f) {
domain.push_back(s);
}
for (sort* s : *f)
domain.push_back(s);

bool ground = is_ground(m_else);
for (func_entry * curr : m_entries) {
ground &= is_ground(curr->get_result());
for (unsigned i = 0; i < m_arity; i++) {
ground &= is_ground(curr->get_arg(i));
}
for (unsigned i = 0; i < m_arity; i++)
ground &= is_ground(curr->get_arg(i));
}
if (!ground) {
r = get_interp();
Expand Down
41 changes: 23 additions & 18 deletions src/model/model.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -224,7 +224,7 @@ struct model::top_sort : public ::top_sort<func_decl> {
}
};

void model::compress() {
void model::compress(bool force_inline) {
if (m_cleaned) return;

// stratify m_finterp and m_decls in a topological sort
Expand All @@ -238,7 +238,7 @@ void model::compress() {
collect_deps(ts);
ts.topological_sort();
for (func_decl * f : ts.top_sorted()) {
cleanup_interp(ts, f);
cleanup_interp(ts, f, force_inline);
}

func_decl_set removed;
Expand Down Expand Up @@ -332,23 +332,23 @@ model::func_decl_set* model::collect_deps(top_sort& ts, func_interp * fi) {
\brief Inline interpretations of skolem functions
*/

void model::cleanup_interp(top_sort& ts, func_decl* f) {
void model::cleanup_interp(top_sort& ts, func_decl* f, bool force_inline) {
unsigned pid = ts.partition_id(f);
expr * e1 = get_const_interp(f);
if (e1) {
expr_ref e2 = cleanup_expr(ts, e1, pid);
expr_ref e2 = cleanup_expr(ts, e1, pid, force_inline);
if (e2 != e1)
register_decl(f, e2);
return;
}
func_interp* fi = get_func_interp(f);
if (fi) {
e1 = fi->get_else();
expr_ref e2 = cleanup_expr(ts, e1, pid);
expr_ref e2 = cleanup_expr(ts, e1, pid, force_inline);
if (e1 != e2)
fi->set_else(e2);
for (auto& fe : *fi) {
e2 = cleanup_expr(ts, fe->get_result(), pid);
e2 = cleanup_expr(ts, fe->get_result(), pid, force_inline);
if (e2 != fe->get_result()) {
fi->insert_entry(fe->get_args(), e2);
}
Expand Down Expand Up @@ -382,21 +382,26 @@ void model::collect_occs(top_sort& ts, expr* e) {
for_each_ast(collector, e, true);
}

bool model::can_inline_def(top_sort& ts, func_decl* f) {
bool model::can_inline_def(top_sort& ts, func_decl* f, bool force_inline) {
if (ts.occur_count(f) <= 1) return true;
func_interp* fi = get_func_interp(f);
if (!fi) return false;
if (fi->get_else() == nullptr) return false;
if (m_inline) return true;
if (!fi)
return false;
if (fi->get_else() == nullptr)
return false;
if (m_inline)
return true;
expr* e = fi->get_else();
obj_hashtable<expr> subs;
ptr_buffer<expr> todo;
todo.push_back(e);
while (!todo.empty()) {
if (fi->num_entries() + subs.size() > 8) return false;
if (!force_inline && fi->num_entries() + subs.size() > 8)
return false;
expr* e = todo.back();
todo.pop_back();
if (subs.contains(e)) continue;
if (subs.contains(e))
continue;
subs.insert(e);
if (is_app(e)) {
for (expr* arg : *to_app(e)) {
Expand All @@ -411,7 +416,7 @@ bool model::can_inline_def(top_sort& ts, func_decl* f) {
}


expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition) {
expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition, bool force_inline) {
if (!e) return expr_ref(nullptr, m);

TRACE("model", tout << "cleaning up:\n" << mk_pp(e, m) << "\n";);
Expand Down Expand Up @@ -455,7 +460,7 @@ expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition)
if (autil.is_as_array(a)) {
func_decl* f = autil.get_as_array_func_decl(a);
// only expand auxiliary definitions that occur once.
if (can_inline_def(ts, f)) {
if (can_inline_def(ts, f, force_inline)) {
fi = get_func_interp(f);
if (fi) {
new_t = fi->get_array_interp(f);
Expand All @@ -467,7 +472,7 @@ expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition)
if (new_t) {
// noop
}
else if (f->is_skolem() && can_inline_def(ts, f) && (fi = get_func_interp(f)) &&
else if (f->is_skolem() && can_inline_def(ts, f, force_inline) && (fi = get_func_interp(f)) &&
fi->get_interp() && (!ts.partition_ids().find(f, pid) || pid != current_partition)) {
var_subst vs(m, false);
new_t = vs(fi->get_interp(), args.size(), args.data());
Expand Down Expand Up @@ -526,15 +531,15 @@ expr_ref model::unfold_as_array(expr* e) {
}


expr_ref model::get_inlined_const_interp(func_decl* f) {
expr_ref model::get_inlined_const_interp(func_decl* f, bool force_inline) {
expr* v = get_const_interp(f);
if (!v) return expr_ref(nullptr, m);
top_sort st(m);
expr_ref result1(v, m);
expr_ref result2 = cleanup_expr(st, v, UINT_MAX);
expr_ref result2 = cleanup_expr(st, v, UINT_MAX, force_inline);
while (result1 != result2) {
result1 = result2;
result2 = cleanup_expr(st, result1, UINT_MAX);
result2 = cleanup_expr(st, result1, UINT_MAX, force_inline);
}
return result2;
}
Expand Down
10 changes: 5 additions & 5 deletions src/model/model.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -50,10 +50,10 @@ class model : public model_core {
void collect_deps(top_sort& ts);
void collect_occs(top_sort& ts, func_decl* f);
void collect_occs(top_sort& ts, expr* e);
void cleanup_interp(top_sort& ts, func_decl * f);
expr_ref cleanup_expr(top_sort& ts, expr* e, unsigned current_partition);
void cleanup_interp(top_sort& ts, func_decl * f, bool force_inline);
expr_ref cleanup_expr(top_sort& ts, expr* e, unsigned current_partition, bool force_inline);
void remove_decls(ptr_vector<func_decl> & decls, func_decl_set const & s);
bool can_inline_def(top_sort& ts, func_decl* f);
bool can_inline_def(top_sort& ts, func_decl* f, bool force_inline);
value_factory* get_factory(sort* s);

public:
Expand All @@ -78,7 +78,7 @@ class model : public model_core {
sort * get_uninterpreted_sort(unsigned idx) const override;
bool has_uninterpreted_sort(sort * s) const;

expr_ref get_inlined_const_interp(func_decl* f);
expr_ref get_inlined_const_interp(func_decl* f, bool force_inline);
expr_ref unfold_as_array(expr* e);

//
Expand All @@ -90,7 +90,7 @@ class model : public model_core {
//
model * translate(ast_translation & translator) const;

void compress();
void compress(bool force_inline = false);

void set_model_completion(bool f) { m_mev.set_model_completion(f); }
void updt_params(params_ref const & p);
Expand Down

0 comments on commit d5c6abe

Please sign in to comment.