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

move some methods from header to cpp, format fixing, remove special characters

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-04-07 17:34:46 -07:00
parent 2dc92e2b94
commit bab87bfb9b
2 changed files with 50 additions and 41 deletions

56
src/smt/theory_datatype.cpp
View file

@ -36,6 +36,41 @@ namespace smt {
theory_id get_from_theory() const override { return null_theory_id; }
};
theory_datatype::final_check_st::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();
}
theory_datatype::final_check_st::~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();
}
void theory_datatype::oc_mark_on_stack(enode * n) {
n = n->get_root();
n->set_mark();
m_to_unmark.push_back(n);
}
void theory_datatype::oc_mark_cycle_free(enode * n) {
n = n->get_root();
n->set_mark2();
m_to_unmark2.push_back(n);
}
void theory_datatype::oc_push_stack(enode * n) {
m_stack.push_back(std::make_pair(EXIT, n));
m_stack.push_back(std::make_pair(ENTER, n));
}
theory* theory_datatype::mk_fresh(context* new_ctx) {
return alloc(theory_datatype, new_ctx->get_manager(), m_params);
@ -421,25 +456,22 @@ namespace smt {
return d->m_constructor;
}
// explain the cycle root -> … -> app -> root
// 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;
}
for (enode * arg : enode::args(oc_get_cstor(app))) {
// 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
// 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)
@ -447,7 +479,7 @@ namespace smt {
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));

35
src/smt/theory_datatype.h
View file

@ -82,43 +82,20 @@ namespace smt {
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); }
void oc_mark_on_stack(enode * 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); }
void oc_mark_cycle_free(enode * 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));
}
void oc_push_stack(enode * 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();
}
public:
final_check_st(theory_datatype * th);
~final_check_st();
};
enode * oc_get_cstor(enode * n);