From 442e47dfced2b010b47b27401d8ba6c892b1f230 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 17 Jan 2019 16:34:26 -0800 Subject: [PATCH] fix datatype occurs check bug reported by Gerhard Schellhorn Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 1 - src/smt/smt_conflict_resolution.cpp | 8 ++--- src/smt/smt_context.cpp | 2 ++ src/smt/smt_context_pp.cpp | 2 +- src/smt/theory_datatype.cpp | 49 ++++++++++++++++++----------- src/smt/theory_datatype.h | 3 +- 6 files changed, 40 insertions(+), 25 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 1f2f40941..a974e8b78 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -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); diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index 93c172bf1..7fdfbf9aa 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -311,7 +311,7 @@ namespace smt { bool_var var = antecedent.var(); unsigned lvl = m_ctx.get_assign_level(var); SASSERT(var < static_cast(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); diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 3c601f400..38a25c874 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -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; } diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 4eb997c2e..72cc2404c 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -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"; } diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index 6aa49efae..e907b4462 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -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); diff --git a/src/smt/theory_datatype.h b/src/smt/theory_datatype.h index 010e78cb3..67cf5cfee 100644 --- a/src/smt/theory_datatype.h +++ b/src/smt/theory_datatype.h @@ -73,7 +73,7 @@ namespace smt { void sign_recognizer_conflict(enode * c, enode * r); typedef enum { ENTER, EXIT } stack_op; - typedef map, ptr_eq > parent_tbl; + typedef obj_map parent_tbl; typedef std::pair stack_entry; ptr_vector 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);