From 02e71c7d23627fc19b2a91b3d537daa1bad65673 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 7 Oct 2019 16:21:54 -0700 Subject: [PATCH] fix #2650, use datatype constructor producing smallest possible tree whenever possible Signed-off-by: Nikolaj Bjorner --- src/ast/datatype_decl_plugin.cpp | 63 +++++++++++++++----------------- src/ast/datatype_decl_plugin.h | 6 +-- src/nlsat/nlsat_evaluator.cpp | 2 +- src/nlsat/nlsat_solver.cpp | 20 +++++++++- src/smt/theory_datatype.cpp | 5 ++- 5 files changed, 55 insertions(+), 41 deletions(-) diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 06af112c1..22f328988 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -1105,20 +1105,16 @@ namespace datatype { */ func_decl * util::get_non_rec_constructor(sort * ty) { SASSERT(is_datatype(ty)); - func_decl * r = nullptr; - if (m_datatype2nonrec_constructor.find(ty, r)) - return r; - r = nullptr; + cnstr_depth cd; + if (m_datatype2nonrec_constructor.find(ty, cd)) + return cd.first; ptr_vector forbidden_set; forbidden_set.push_back(ty); TRACE("util_bug", tout << "invoke get-non-rec: " << sort_ref(ty, m) << "\n";); - r = get_non_rec_constructor_core(ty, forbidden_set); + cd = get_non_rec_constructor_core(ty, forbidden_set); SASSERT(forbidden_set.back() == ty); - SASSERT(r); - m_asts.push_back(ty); - m_asts.push_back(r); - m_datatype2nonrec_constructor.insert(ty, r); - return r; + SASSERT(cd.first); + return cd.first; } /** @@ -1126,7 +1122,7 @@ namespace datatype { each T_i is not a datatype or it is a datatype t not in forbidden_set, and get_non_rec_constructor_core(T_i, forbidden_set union { T_i }) */ - func_decl * util::get_non_rec_constructor_core(sort * ty, ptr_vector & forbidden_set) { + util::cnstr_depth util::get_non_rec_constructor_core(sort * ty, ptr_vector & forbidden_set) { // We must select a constructor c(T_1, ..., T_n):T such that // 1) T_i's are not recursive // If there is no such constructor, then we select one that @@ -1135,6 +1131,9 @@ namespace datatype { ptr_vector const& constructors = *get_datatype_constructors(ty); unsigned sz = constructors.size(); array_util autil(m); + cnstr_depth result(nullptr, 0); + if (m_datatype2nonrec_constructor.find(ty, result)) + return result; TRACE("util_bug", tout << "get-non-rec constructor: " << sort_ref(ty, m) << "\n"; tout << "forbidden: "; for (sort* s : forbidden_set) tout << sort_ref(s, m) << " "; @@ -1142,25 +1141,12 @@ namespace datatype { tout << "constructors: " << sz << "\n"; for (func_decl* f : constructors) tout << func_decl_ref(f, m) << "\n"; ); - // step 1) - unsigned start = ++m_start; - for (unsigned j = 0; j < sz; ++j) { - func_decl * c = constructors[(j + start) % sz]; - TRACE("util_bug", tout << "checking " << sort_ref(ty, m) << ": " << func_decl_ref(c, m) << "\n";); - unsigned num_args = c->get_arity(); - unsigned i = 0; - for (; i < num_args && !is_datatype(autil.get_array_range_rec(c->get_domain(i))); i++); - if (i == num_args) { - TRACE("util_bug", tout << "found non-rec " << func_decl_ref(c, m) << "\n";); - return c; - } - } - // step 2) - for (unsigned j = 0; j < sz; ++j) { - func_decl * c = constructors[(j + start) % sz]; - TRACE("util_bug", tout << "non_rec_constructor c: " << j << " " << func_decl_ref(c, m) << "\n";); + unsigned min_depth = INT_MAX; + for (func_decl * c : constructors) { + TRACE("util_bug", tout << "non_rec_constructor c: " << func_decl_ref(c, m) << "\n";); unsigned num_args = c->get_arity(); unsigned i = 0; + unsigned max_depth = 0; for (; i < num_args; i++) { sort * T_i = autil.get_array_range_rec(c->get_domain(i)); TRACE("util_bug", tout << "c: " << i << " " << sort_ref(T_i, m) << "\n";); @@ -1173,17 +1159,26 @@ namespace datatype { break; } forbidden_set.push_back(T_i); - func_decl * nested_c = get_non_rec_constructor_core(T_i, forbidden_set); + cnstr_depth nested_c = get_non_rec_constructor_core(T_i, forbidden_set); SASSERT(forbidden_set.back() == T_i); forbidden_set.pop_back(); - if (nested_c == nullptr) + if (nested_c.first == nullptr) break; - TRACE("util_bug", tout << "nested_c: " << nested_c->get_name() << "\n";); + TRACE("util_bug", tout << "nested_c: " << nested_c.first->get_name() << "\n";); + max_depth = std::max(nested_c.second + 1, max_depth); + } + if (i == num_args && max_depth < min_depth) { + result.first = c; + result.second = max_depth; + min_depth = max_depth; } - if (i == num_args) - return c; } - return nullptr; + if (result.first) { + m_asts.push_back(result.first); + m_asts.push_back(ty); + m_datatype2nonrec_constructor.insert(ty, result); + } + return result; } unsigned util::get_constructor_idx(func_decl * f) const { diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index 42a706904..cb139953b 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -292,10 +292,10 @@ namespace datatype { ast_manager & m; family_id m_family_id; mutable decl::plugin* m_plugin; - + typedef std::pair cnstr_depth; obj_map *> m_datatype2constructors; - obj_map m_datatype2nonrec_constructor; + obj_map m_datatype2nonrec_constructor; obj_map *> m_constructor2accessors; obj_map m_constructor2recognizer; obj_map m_recognizer2constructor; @@ -309,7 +309,7 @@ namespace datatype { unsigned m_start; mutable ptr_vector m_fully_interp_trail; - func_decl * get_non_rec_constructor_core(sort * ty, ptr_vector & forbidden_set); + cnstr_depth get_non_rec_constructor_core(sort * ty, ptr_vector & forbidden_set); friend class decl::plugin; diff --git a/src/nlsat/nlsat_evaluator.cpp b/src/nlsat/nlsat_evaluator.cpp index 81e8cf536..081351f06 100644 --- a/src/nlsat/nlsat_evaluator.cpp +++ b/src/nlsat/nlsat_evaluator.cpp @@ -423,7 +423,7 @@ namespace nlsat { scoped_anum_vector & roots = m_tmp_values; roots.reset(); m_am.isolate_roots(polynomial_ref(a->p(), m_pm), undef_var_assignment(m_assignment, a->x()), roots); - TRACE("nlsat", + TRACE("nlsat_evaluator", m_solver.display(tout << (neg?"!":""), *a); tout << "\n"; if (roots.empty()) { tout << "No roots\n"; diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 67aa219c3..4cbc80411 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -826,6 +826,24 @@ namespace nlsat { } IF_VERBOSE(0, verbose_stream() << "check\n";); lbool r = checker.check(); + if (r == l_true) { + for (bool_var b : tr) { + literal lit(b, false); + IF_VERBOSE(0, checker.display(verbose_stream(), lit) << " := " << checker.value(lit) << "\n"); + TRACE("nlsat", checker.display(tout, lit) << " := " << checker.value(lit) << "\n";); + } + for (clause* c : m_learned) { + bool found = false; + for (literal lit: *c) { + literal tlit(tr[lit.var()], lit.sign()); + found |= checker.value(tlit) == l_true; + } + if (!found) { + IF_VERBOSE(0, display(verbose_stream() << "violdated clause: ", *c) << "\n"); + TRACE("nlsat", display(tout << "violdated clause: ", *c) << "\n";); + } + } + } VERIFY(r == l_false); for (bool_var b : tr) { checker.dec_ref(b); @@ -1738,7 +1756,7 @@ namespace nlsat { tout << "new valid clause:\n"; display(tout, m_lazy_clause.size(), m_lazy_clause.c_ptr()) << "\n";); - if (m_check_lemmas && false) { + if (false && m_check_lemmas) { check_lemma(m_lazy_clause.size(), m_lazy_clause.c_ptr(), true, nullptr); } diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index d8266f2bb..b4bcfa146 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -885,6 +885,7 @@ namespace smt { unassigned_idx = idx; num_unassigned++; } + TRACE("datatype", tout << "propagate " << num_unassigned << " eqs: " << eqs.size() << "\n";); if (num_unassigned == 0) { // conflict SASSERT(!lits.empty()); @@ -938,13 +939,13 @@ namespace smt { enode * n = get_enode(v); sort * s = m.get_sort(n->get_owner()); func_decl * non_rec_c = m_util.get_non_rec_constructor(s); - TRACE("datatype_bug", tout << "non_rec_c: " << non_rec_c->get_name() << "\n";); unsigned non_rec_idx = m_util.get_constructor_idx(non_rec_c); var_data * d = m_var_data[v]; SASSERT(d->m_constructor == nullptr); func_decl * r = nullptr; m_stats.m_splits++; + TRACE("datatype_bug", tout << "non_rec_c: " << non_rec_c->get_name() << " #rec: " << d->m_recognizers.size() << "\n";); if (d->m_recognizers.empty()) { r = m_util.get_constructor_is(non_rec_c); @@ -987,7 +988,7 @@ namespace smt { return; // all recognizers are asserted to false... conflict will be detected... } } - SASSERT(r != 0); + SASSERT(r != nullptr); app * r_app = m.mk_app(r, n->get_owner()); TRACE("datatype", tout << "creating split: " << mk_pp(r_app, m) << "\n";); ctx.internalize(r_app, false);