mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 21:08:46 +00:00
Code Activity

fix datatype occurs check bug reported by Gerhard Schellhorn

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-01-17 16:34:26 -08:00
parent f2e636c598
commit 442e47dfce
6 changed files with 40 additions and 25 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/ast/ast.cpp
View file

@ -2138,7 +2138,6 @@ app * ast_manager::mk_app_core(func_decl * decl, unsigned num_args, expr * const
app * new_node = nullptr;
unsigned sz = app::get_obj_size(num_args);
void * mem = allocate_node(sz);
try {
if (m_int_real_coercions && coercion_needed(decl, num_args, args)) {
expr_ref_buffer new_args(*this);

8
src/smt/smt_conflict_resolution.cpp
View file

@ -311,7 +311,7 @@ namespace smt {
bool_var var = antecedent.var();
unsigned lvl = m_ctx.get_assign_level(var);
SASSERT(var < static_cast<int>(m_ctx.get_num_bool_vars()));
TRACE("conflict", tout << "processing antecedent (level " << lvl << "):";
TRACE("conflict_", tout << "processing antecedent (level " << lvl << "):";
m_ctx.display_literal(tout, antecedent);
m_ctx.display_detailed_literal(tout << " ", antecedent) << "\n";);
@ -429,7 +429,7 @@ namespace smt {
void conflict_resolution::finalize_resolve(b_justification conflict, literal not_l) {
unmark_justifications(0);
TRACE("conflict", m_ctx.display_literals(tout << "before minimization:\n", m_lemma) << "\n";);
TRACE("conflict", m_ctx.display_literals(tout << "before minimization:\n", m_lemma) << "\n" << m_lemma << "\n";);
TRACE("conflict_verbose",m_ctx.display_literals_verbose(tout << "before minimization:\n", m_lemma) << "\n";);
@ -484,7 +484,7 @@ namespace smt {
unsigned num_marks = 0;
if (not_l != null_literal) {
TRACE("conflict", tout << "not_l: "; m_ctx.display_literal_verbose(tout, not_l); tout << "\n";);
TRACE("conflict", tout << "not_l: "; m_ctx.display_literal_verbose(tout, not_l) << "\n";);
process_antecedent(not_l, num_marks);
}
@ -497,7 +497,7 @@ namespace smt {
}
TRACE("conflict", tout << "processing consequent id: " << idx << " lit: " << consequent << " "; m_ctx.display_literal(tout, consequent);
m_ctx.display_literal_verbose(tout, consequent) << "\n";
m_ctx.display_literal_verbose(tout << " ", consequent) << "\n";
tout << "num_marks: " << num_marks << ", js kind: " << js.get_kind() << " level: " << m_ctx.get_assign_level(consequent) << "\n";
);
SASSERT(js != null_b_justification);

2
src/smt/smt_context.cpp
View file

@ -3918,6 +3918,8 @@ namespace smt {
conflict_lvl > m_search_lvl + 1 &&
!m_manager.proofs_enabled() &&
m_units_to_reassert.size() < m_fparams.m_delay_units_threshold;
TRACE("conflict", tout << delay_forced_restart << "\n";);
if (delay_forced_restart) {
new_lvl = conflict_lvl - 1;
}

2
src/smt/smt_context_pp.cpp
View file

@ -263,7 +263,7 @@ namespace smt {
for (unsigned i = 0; i < sz; i++) {
expr * n = m_b_internalized_stack.get(i);
bool_var v = get_bool_var_of_id(n->get_id());
out << "(#" << n->get_id() << " -> p!" << v << ") ";
out << "(#" << n->get_id() << " -> " << literal(v, false) << ") ";
}
out << "\n";
}

49
src/smt/theory_datatype.cpp
View file

@ -455,33 +455,46 @@ namespace smt {
return d->m_constructor;
}
void theory_datatype::explain_is_child(enode* parent, enode* child) {
enode * parentc = oc_get_cstor(parent);
if (parent != parentc) {
m_used_eqs.push_back(enode_pair(parent, parentc));
}
// collect equalities on all children that may have been used.
bool found = false;
for (enode * arg : enode::args(parentc)) {
// found an argument which is equal to root
if (arg->get_root() == child->get_root()) {
if (arg != child) {
m_used_eqs.push_back(enode_pair(arg, child));
}
found = true;
}
}
VERIFY(found);
}
// 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,...)
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;
}
}
explain_is_child(app, root);
// 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;
enode* parent_app = m_parent[app->get_root()];
explain_is_child(parent_app, app);
SASSERT(is_constructor(parent_app));
app = parent_app;
}
SASSERT(app->get_root() == root->get_root());
if (app != root)
if (app != root) {
m_used_eqs.push_back(enode_pair(app, root));
}
TRACE("datatype",
tout << "occurs_check\n";
@ -706,11 +719,11 @@ namespace smt {
sort * s = recognizer->get_decl()->get_domain(0);
if (d->m_recognizers.empty()) {
SASSERT(m_util.is_datatype(s));
d->m_recognizers.resize(m_util.get_datatype_num_constructors(s));
d->m_recognizers.resize(m_util.get_datatype_num_constructors(s), nullptr);
}
SASSERT(d->m_recognizers.size() == m_util.get_datatype_num_constructors(s));
unsigned c_idx = m_util.get_recognizer_constructor_idx(recognizer->get_decl());
if (d->m_recognizers[c_idx] == 0) {
if (d->m_recognizers[c_idx] == nullptr) {
lbool val = ctx.get_assignment(recognizer);
TRACE("datatype", tout << "adding recognizer to v" << v << " rec: #" << recognizer->get_owner_id() << " val: " << val << "\n";);
if (val == l_true) {
@ -782,7 +795,7 @@ namespace smt {
region & reg = ctx.get_region();
TRACE("datatype_conflict", tout << mk_ismt2_pp(recognizer->get_owner(), get_manager()) << "\n";
for (literal l : lits) {
ctx.display_detailed_literal(tout, l); tout << "\n";
ctx.display_detailed_literal(tout, l) << "\n";
}
for (auto const& p : eqs) {
tout << enode_eq_pp(p, ctx);

3
src/smt/theory_datatype.h
View file

@ -73,7 +73,7 @@ namespace smt {
void sign_recognizer_conflict(enode * c, enode * r);
typedef enum { ENTER, EXIT } stack_op;
typedef map<enode*, enode*, obj_ptr_hash<enode>, ptr_eq<enode> > parent_tbl;
typedef obj_map<enode, enode*> parent_tbl;
typedef std::pair<stack_op, enode*> stack_entry;
ptr_vector<enode> m_to_unmark;
@ -102,6 +102,7 @@ namespace smt {
bool occurs_check(enode * n);
bool occurs_check_enter(enode * n);
void occurs_check_explain(enode * top, enode * root);
void explain_is_child(enode* parent, enode* child);
void mk_split(theory_var v);