mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

perf(datatype): whole-graph implementation of occurs_check

Browse source
This commit is contained in:
Simon Cruanes 2018-04-02 17:17:21 -05:00
parent 2ee1e358b6
commit 9df140343a
4 changed files with 135 additions and 70 deletions

7
src/smt/smt_enode.h
View file

@ -171,6 +171,9 @@ namespace smt {
m_interpreted = true;
}
inline bool equal(const enode & other) const {
return m_owner == other.m_owner;
}
void del_eh(ast_manager & m, bool update_children_parent = true);
@ -423,5 +426,9 @@ namespace smt {
};
inline bool operator==(const smt::enode & e1, const smt::enode & e2) {
return e1.equal(e2);
}
#endif /* SMT_ENODE_H_ */

1
src/smt/smt_types.h
View file

@ -47,7 +47,6 @@ namespace smt {
typedef ptr_vector<enode> enode_vector;
typedef std::pair<enode *, enode *> enode_pair;
typedef svector<enode_pair> enode_pair_vector;
typedef ptr_hashtable<enode, obj_ptr_hash<enode>, deref_eq<enode> > enode_tbl;
class context;

136
src/smt/theory_datatype.cpp
View file

@ -389,14 +389,13 @@ namespace smt {
final_check_status theory_datatype::final_check_eh() {
int num_vars = get_num_vars();
final_check_status r = FC_DONE;
init_final_check();
final_check_st _guard(this); // RAII for managing state
for (int v = 0; v < num_vars; v++) {
if (v == static_cast<int>(m_find.find(v))) {
enode * node = get_enode(v);
if (occurs_check(node)) {
// conflict was detected...
// return...
cleanup_final_check();
return FC_CONTINUE;
}
if (m_params.m_dt_lazy_splits > 0) {
@ -409,10 +408,62 @@ namespace smt {
}
}
}
cleanup_final_check();
return r;
}
// explain the cycle root -> … -> app -> root
void theory_datatype::occurs_check_explain(enode * app, enode * const root) {
TRACE("datatype", tout << "occurs_check_explain " << mk_bounded_pp(app->get_owner(), get_manager()) << " <-> " << mk_bounded_pp(root->get_owner(), get_manager()) << "\n";);
enode* app_parent = nullptr;
while (app->get_root() != root->get_root()) {
theory_var v = app->get_root()->get_th_var(get_id());
SASSERT(v != null_theory_var);
v = m_find.find(v);
var_data * d = m_var_data[v];
SASSERT(d->m_constructor);
if (app != d->m_constructor)
m_used_eqs.push_back(enode_pair(app, d->m_constructor));
bool found = m_parent.find(app, app_parent);
SASSERT(found);
app = app_parent;
}
SASSERT(app->get_root() == root->get_root());
if (app != root)
m_used_eqs.push_back(enode_pair(app, root));
}
// start exploring subgraph below `app`
bool theory_datatype::occurs_check_enter(enode * app) {
oc_mark_on_stack(app);
theory_var v = app->get_root()->get_th_var(get_id());
if (v != null_theory_var) {
v = m_find.find(v);
var_data * d = m_var_data[v];
if (d->m_constructor) {
unsigned num_args = d->m_constructor->get_num_args();
for (unsigned i = 0; i < num_args; i++) {
enode * arg = d->m_constructor->get_arg(i);
if (oc_cycle_free(arg)) {
return false;
}
if (oc_on_stack(arg)) {
// arg was explored before app, and is still on the stack: cycle
occurs_check_explain(app, arg);
return true;
}
// explore `arg` (with parent `app`)
if (m_util.is_datatype(get_manager().get_sort(arg->get_owner()))) {
m_parent.insert(arg, app);
oc_push_stack(arg);
}
}
}
}
return false;
}
/**
\brief Check if n can be reached starting from n and following equalities and constructors.
For example, occur_check(a1) returns true in the following set of equalities:
@ -421,68 +472,47 @@ namespace smt {
a3 = cons(v3, a1)
*/
bool theory_datatype::occurs_check(enode * n) {
TRACE("datatype", tout << "occurs check: #" << n->get_owner_id() << "\n";);
m_to_unmark.reset();
m_used_eqs.reset();
m_main = n;
bool res = occurs_check_core(m_main);
unmark_enodes(m_to_unmark.size(), m_to_unmark.c_ptr());
TRACE("datatype", tout << "occurs check: #" << n->get_owner_id() << " " << mk_bounded_pp(n->get_owner(), get_manager()) << "\n";);
m_stats.m_occurs_check++;
bool res = false;
oc_push_stack(n);
// DFS traversal from `n`. Look at top element and explore it.
while (!res && !m_stack.empty()) {
stack_op op = m_stack.back().first;
enode * app = m_stack.back().second;
m_stack.pop_back();
if (oc_cycle_free(app)) continue;
TRACE("datatype", tout << "occurs check loop: #" << app->get_owner_id() << " " << mk_bounded_pp(app->get_owner(), get_manager()) << (op==ENTER?" enter":" exit")<< "\n";);
switch (op) {
case ENTER:
res = occurs_check_enter(app) || res;
break;
case EXIT:
oc_mark_cycle_free(app);
break;
}
}
if (res) {
// m_used_eqs should contain conflict
context & ctx = get_context();
region & r = ctx.get_region();
ctx.set_conflict(ctx.mk_justification(ext_theory_conflict_justification(get_id(), r, 0, nullptr, m_used_eqs.size(), m_used_eqs.c_ptr())));
TRACE("occurs_check",
TRACE("datatype",
tout << "occurs_check: true\n";
for (enode_pair const& p : m_used_eqs) {
tout << "eq: #" << p.first->get_owner_id() << " #" << p.second->get_owner_id() << "\n";
tout << mk_bounded_pp(p.first->get_owner(), get_manager()) << " " << mk_bounded_pp(p.second->get_owner(), get_manager()) << "\n";
});
} else {
oc_mark_cycle_free(n);
}
return res;
}
/**
\brief Auxiliary method for occurs_check.
TODO: improve performance.
*/
bool theory_datatype::occurs_check_core(enode * app) {
if (oc_cycle_free(app) || oc_explored(app))
return false;
m_stats.m_occurs_check++;
oc_mark_explore(app);
TRACE("datatype", tout << "occurs check_core: #" << app->get_owner_id() << " #" << m_main->get_owner_id() << "\n";);
theory_var v = app->get_root()->get_th_var(get_id());
if (v != null_theory_var) {
v = m_find.find(v);
var_data * d = m_var_data[v];
if (d->m_constructor) {
if (app != d->m_constructor)
m_used_eqs.push_back(enode_pair(app, d->m_constructor));
unsigned num_args = d->m_constructor->get_num_args();
for (unsigned i = 0; i < num_args; i++) {
enode * arg = d->m_constructor->get_arg(i);
if (arg->get_root() == m_main->get_root()) {
if (arg != m_main)
m_used_eqs.push_back(enode_pair(arg, m_main));
return true;
}
if (m_util.is_datatype(get_manager().get_sort(arg->get_owner())) && occurs_check_core(arg))
return true;
}
if (app != d->m_constructor) {
SASSERT(m_used_eqs.back().first == app);
SASSERT(m_used_eqs.back().second == d->m_constructor);
m_used_eqs.pop_back();
}
}
}
return false;
}
void theory_datatype::reset_eh() {
m_trail_stack.reset();

61
src/smt/theory_datatype.h
View file

@ -26,7 +26,6 @@ Revision History:
#include "smt/proto_model/datatype_factory.h"
namespace smt {
class theory_datatype : public theory {
typedef trail_stack<theory_datatype> th_trail_stack;
typedef union_find<theory_datatype> th_union_find;
@ -73,27 +72,57 @@ namespace smt {
void propagate_recognizer(theory_var v, enode * r);
void sign_recognizer_conflict(enode * c, enode * r);
ptr_vector<enode> m_to_unmark;
ptr_vector<enode> m_to_unmark2;
enode_pair_vector m_used_eqs;
enode * m_main;
typedef enum { ENTER, EXIT } stack_op;
typedef map<enode*, enode*, obj_ptr_hash<enode>, deref_eq<enode> > parent_tbl;
typedef std::pair<stack_op, enode*> stack_entry;
void oc_mark_explore(enode * n) { n->set_mark(); m_to_unmark.push_back(n); }
bool oc_explored(enode * n) const { n->is_marked(); }
ptr_vector<enode> m_to_unmark;
ptr_vector<enode> m_to_unmark2;
enode_pair_vector m_used_eqs; // conflict, if any
parent_tbl m_parent; // parent explanation for occurs_check
svector<stack_entry> m_stack; // stack for DFS for occurs_check
void oc_mark_cycle_free(enode * n) { n->set_mark2(); m_to_unmark2.push_back(n); }
bool oc_cycle_free(enode * n) const { n->is_marked2(); }
void oc_mark_on_stack(enode * n) {
n = n->get_root();
n->set_mark();
m_to_unmark.push_back(n); }
bool oc_on_stack(enode * n) const { return n->get_root()->is_marked(); }
void init_final_check() {
m_to_unmark2.reset();
}
void cleanup_final_check() {
unmark_enodes2(m_to_unmark2.size(), m_to_unmark2.c_ptr());
m_to_unmark2.reset();
void oc_mark_cycle_free(enode * n) {
n = n->get_root();
n->set_mark2();
m_to_unmark2.push_back(n); }
bool oc_cycle_free(enode * n) const { return n->get_root()->is_marked2(); }
void oc_push_stack(enode * n) {
m_stack.push_back(std::make_pair(EXIT, n));
m_stack.push_back(std::make_pair(ENTER, n));
}
// class for managing state of final_check
class final_check_st {
theory_datatype * th;
public:
final_check_st(theory_datatype * th) : th(th) {
th->m_to_unmark2.reset();
th->m_to_unmark.reset();
th->m_used_eqs.reset();
th->m_stack.reset();
th->m_parent.reset();
}
~final_check_st() {
unmark_enodes(th->m_to_unmark.size(), th->m_to_unmark.c_ptr());
unmark_enodes2(th->m_to_unmark2.size(), th->m_to_unmark2.c_ptr());
th->m_to_unmark.reset();
th->m_to_unmark2.reset();
th->m_stack.reset();
th->m_parent.reset();
}
};
bool occurs_check(enode * n);
bool occurs_check_core(enode * n);
bool occurs_check_enter(enode * n);
void occurs_check_explain(enode * top, enode * root);
void mk_split(theory_var v);