From 2ebab021f2c781a5ca4f6f0626e40a13dcab05ca Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 23 May 2021 13:42:15 -0700 Subject: [PATCH] fix #5297 --- src/ast/datatype_decl_plugin.cpp | 11 +++++++++++ src/ast/datatype_decl_plugin.h | 1 + src/model/array_factory.cpp | 19 ++++++++++++------- src/model/array_factory.h | 1 + src/model/datatype_factory.cpp | 24 ++++++++++++++++-------- 5 files changed, 41 insertions(+), 15 deletions(-) diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 7190d5bf98a..72d39290e3d 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -1082,6 +1082,14 @@ namespace datatype { return r; } + bool util::is_recursive_array(sort* a) { + array_util autil(m); + if (!autil.is_array(a)) + return false; + a = autil.get_array_range_rec(a); + return is_datatype(a) && is_recursive(a); + } + bool util::is_enum_sort(sort* s) { if (!is_datatype(s)) { return false; @@ -1243,6 +1251,9 @@ namespace datatype { defined together in the same mutually recursive definition. */ bool util::are_siblings(sort * s1, sort * s2) { + array_util autil(m); + s1 = autil.get_array_range_rec(s1); + s2 = autil.get_array_range_rec(s2); if (!is_datatype(s1) || !is_datatype(s2)) { return s1 == s2; } diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index 34e1b5db4ae..90d49e44906 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -330,6 +330,7 @@ namespace datatype { bool is_datatype(sort const* s) const { return is_sort_of(s, fid(), DATATYPE_SORT); } bool is_enum_sort(sort* s); bool is_recursive(sort * ty); + bool is_recursive_array(sort * ty); bool is_constructor(func_decl * f) const { return is_decl_of(f, fid(), OP_DT_CONSTRUCTOR); } bool is_recognizer(func_decl * f) const { return is_recognizer0(f) || is_is(f); } bool is_recognizer0(func_decl * f) const { return is_decl_of(f, fid(), OP_DT_RECOGNISER); } diff --git a/src/model/array_factory.cpp b/src/model/array_factory.cpp index b68d708a115..da3278b4333 100644 --- a/src/model/array_factory.cpp +++ b/src/model/array_factory.cpp @@ -132,13 +132,18 @@ expr * array_factory::get_fresh_value(sort * s) { return get_some_value(s); } sort * range = get_array_range(s); - expr * range_val = m_model.get_fresh_value(range); - if (range_val != nullptr) { - // easy case - func_interp * fi; - expr * val = mk_array_interp(s, fi); - fi->set_else(range_val); - return val; + expr* range_val = nullptr; + + if (!m_recursive_fresh) { + flet _recursive(m_recursive_fresh, true); + range_val = m_model.get_fresh_value(range); + if (range_val != nullptr) { + // easy case + func_interp* fi; + expr* val = mk_array_interp(s, fi); + fi->set_else(range_val); + return val; + } } TRACE("array_factory_bug", tout << "array fresh value: using fresh index, range: " << mk_pp(range, m_manager) << "\n";); diff --git a/src/model/array_factory.h b/src/model/array_factory.h index a213850f27b..a2ec07f8898 100644 --- a/src/model/array_factory.h +++ b/src/model/array_factory.h @@ -28,6 +28,7 @@ class array_factory : public struct_factory { expr * mk_array_interp(sort * s, func_interp * & fi); void get_some_args_for(sort * s, ptr_buffer & args); bool mk_two_diff_values_for(sort * s); + bool m_recursive_fresh { false }; public: array_factory(ast_manager & m, model_core & md); diff --git a/src/model/datatype_factory.cpp b/src/model/datatype_factory.cpp index e59ae14f21c..b5e769d2e6b 100644 --- a/src/model/datatype_factory.cpp +++ b/src/model/datatype_factory.cpp @@ -27,6 +27,8 @@ datatype_factory::datatype_factory(ast_manager & m, model_core & md): } expr * datatype_factory::get_some_value(sort * s) { + if (!m_util.is_datatype(s)) + return m_model.get_some_value(s); value_set * set = nullptr; if (m_sort2value_set.find(s, set) && !set->empty()) return *(set->begin()); @@ -77,6 +79,8 @@ bool datatype_factory::is_subterm_of_last_value(app* e) { It also updates m_last_fresh_value */ expr * datatype_factory::get_almost_fresh_value(sort * s) { + if (!m_util.is_datatype(s)) + return m_model.get_some_value(s); value_set * set = get_value_set(s); if (set->empty()) { expr * val = get_some_value(s); @@ -136,6 +140,8 @@ expr * datatype_factory::get_almost_fresh_value(sort * s) { expr * datatype_factory::get_fresh_value(sort * s) { + if (!m_util.is_datatype(s)) + return m_model.get_fresh_value(s); TRACE("datatype", tout << "generating fresh value for: " << s->get_name() << "\n";); value_set * set = get_value_set(s); // Approach 0) @@ -162,7 +168,9 @@ expr * datatype_factory::get_fresh_value(sort * s) { unsigned num = constructor->get_arity(); for (unsigned i = 0; i < num; i++) { sort * s_arg = constructor->get_domain(i); - if (!found_fresh_arg && (!m_util.is_recursive(s) || !m_util.is_datatype(s_arg) || !m_util.are_siblings(s, s_arg))) { + if (!found_fresh_arg && + !m_util.is_recursive_array(s_arg) && + (!m_util.is_recursive(s) || !m_util.is_datatype(s_arg) || !m_util.are_siblings(s, s_arg))) { expr * new_arg = m_model.get_fresh_value(s_arg); if (new_arg != nullptr) { found_fresh_arg = true; @@ -191,7 +199,7 @@ expr * datatype_factory::get_fresh_value(sort * s) { // search for constructor... unsigned num_iterations = 0; if (m_util.is_recursive(s)) { - while(true) { + while (true) { ++num_iterations; TRACE("datatype", tout << mk_pp(get_last_fresh_value(s), m_manager) << "\n";); ptr_vector const & constructors = *m_util.get_datatype_constructors(s); @@ -207,15 +215,15 @@ expr * datatype_factory::get_fresh_value(sort * s) { << m_util.are_siblings(s, s_arg) << " is_datatype " << m_util.is_datatype(s_arg) << " found_sibling " << found_sibling << "\n";); - if (!found_sibling && m_util.is_datatype(s_arg) && m_util.are_siblings(s, s_arg)) { + if (!found_sibling && m_util.are_siblings(s, s_arg)) { found_sibling = true; expr * maybe_new_arg = nullptr; - if (num_iterations <= 1) { - maybe_new_arg = get_almost_fresh_value(s_arg); - } - else { + if (!m_util.is_datatype(s_arg)) + maybe_new_arg = m_model.get_fresh_value(s_arg); + else if (num_iterations <= 1) + maybe_new_arg = get_almost_fresh_value(s_arg); + else maybe_new_arg = get_fresh_value(s_arg); - } if (!maybe_new_arg) { TRACE("datatype", tout << "no argument found for " << mk_pp(s_arg, m_manager) << "\n";);