diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index 7190d5bf9..72d39290e 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 34e1b5db4..90d49e449 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 b68d708a1..da3278b43 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<bool> _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 a213850f2..a2ec07f88 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<expr> & 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 e59ae14f2..b5e769d2e 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<func_decl> 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";);