mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Merge pull request #1560 from c-cube/perf-occurs-check
improve performance of occurs check for datatypes
This commit is contained in:
Nikolaj Bjorner
GitHub
commit
9e8192e448
|
|
@ -21,6 +21,7 @@ Revision History:
|
|||
|
||||
#include "util/list.h"
|
||||
#include "util/vector.h"
|
||||
#include "util/hashtable.h"
|
||||
#include "util/lbool.h"
|
||||
|
||||
class model;
|
||||
|
|
|
|||
|
|
@ -389,10 +389,11 @@ namespace smt {
|
|||
final_check_status theory_datatype::final_check_eh() {
|
||||
int num_vars = get_num_vars();
|
||||
final_check_status r = FC_DONE;
|
||||
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)) {
|
||||
if (!oc_cycle_free(node) && occurs_check(node)) {
|
||||
// conflict was detected...
|
||||
// return...
|
||||
return FC_CONTINUE;
|
||||
|
|
@ -410,6 +411,76 @@ namespace smt {
|
|||
return r;
|
||||
}
|
||||
|
||||
// Assuming `app` is equal to a constructor term, return the constructor enode
|
||||
inline enode * theory_datatype::oc_get_cstor(enode * app) {
|
||||
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);
|
||||
return d->m_constructor;
|
||||
}
|
||||
|
||||
// explain the cycle root -> … -> app -> root
|
||||
void theory_datatype::occurs_check_explain(enode * app, enode * 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;
|
||||
|
||||
// first: explain that root=v, given that app=cstor(…,v,…)
|
||||
{
|
||||
enode * app_cstor = oc_get_cstor(app);
|
||||
for (enode * arg : enode::args(app_cstor)) {
|
||||
// found an argument which is equal to root
|
||||
if (arg->get_root() == root->get_root()) {
|
||||
if (arg != root)
|
||||
m_used_eqs.push_back(enode_pair(arg, root));
|
||||
break;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
// now explain app=cstor(…,v,…) where v=root, and recurse with parent of app
|
||||
while (app->get_root() != root->get_root()) {
|
||||
enode * app_cstor = oc_get_cstor(app);
|
||||
if (app != app_cstor)
|
||||
m_used_eqs.push_back(enode_pair(app, app_cstor));
|
||||
app_parent = m_parent[app->get_root()];
|
||||
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) {
|
||||
for (enode * arg : enode::args(d->m_constructor)) {
|
||||
if (oc_cycle_free(arg)) {
|
||||
continue;
|
||||
}
|
||||
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->get_root(), 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:
|
||||
|
|
@ -418,17 +489,39 @@ 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);
|
||||
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";
|
||||
|
|
@ -437,48 +530,6 @@ namespace smt {
|
|||
}
|
||||
return res;
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Auxiliary method for occurs_check.
|
||||
TODO: improve performance.
|
||||
*/
|
||||
bool theory_datatype::occurs_check_core(enode * app) {
|
||||
if (app->is_marked())
|
||||
return false;
|
||||
|
||||
m_stats.m_occurs_check++;
|
||||
app->set_mark();
|
||||
m_to_unmark.push_back(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();
|
||||
|
|
|
|||
|
|
@ -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,11 +72,59 @@ namespace smt {
|
|||
void propagate_recognizer(theory_var v, enode * r);
|
||||
void sign_recognizer_conflict(enode * c, enode * r);
|
||||
|
||||
ptr_vector<enode> m_to_unmark;
|
||||
enode_pair_vector m_used_eqs;
|
||||
enode * m_main;
|
||||
typedef enum { ENTER, EXIT } stack_op;
|
||||
typedef map<enode*, enode*, obj_ptr_hash<enode>, ptr_eq<enode> > parent_tbl;
|
||||
typedef std::pair<stack_op, enode*> stack_entry;
|
||||
|
||||
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_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 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) {
|
||||
SASSERT(th->m_to_unmark.empty());
|
||||
SASSERT(th->m_to_unmark2.empty());
|
||||
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_used_eqs.reset();
|
||||
th->m_stack.reset();
|
||||
th->m_parent.reset();
|
||||
}
|
||||
};
|
||||
|
||||
enode * oc_get_cstor(enode * n);
|
||||
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);
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue