Skip to content

Commit 2ebab02

Browse files
NikolajBjornerNikolajBjorner
committed
fix #5297 
1 parent 8919fa4 commit 2ebab02

5 files changed

Lines changed: 41 additions & 15 deletions

File tree

‎src/ast/datatype_decl_plugin.cpp‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1082,6 +1082,14 @@ namespace datatype {
10821082
return r;
10831083
}
10841084

1085+
bool util::is_recursive_array(sort* a) {
1086+
array_util autil(m);
1087+
if (!autil.is_array(a))
1088+
return false;
1089+
a = autil.get_array_range_rec(a);
1090+
return is_datatype(a) && is_recursive(a);
1091+
}
1092+
10851093
bool util::is_enum_sort(sort* s) {
10861094
if (!is_datatype(s)) {
10871095
return false;
@@ -1243,6 +1251,9 @@ namespace datatype {
12431251
defined together in the same mutually recursive definition.
12441252
*/
12451253
bool util::are_siblings(sort * s1, sort * s2) {
1254+
array_util autil(m);
1255+
s1 = autil.get_array_range_rec(s1);
1256+
s2 = autil.get_array_range_rec(s2);
12461257
if (!is_datatype(s1) || !is_datatype(s2)) {
12471258
return s1 == s2;
12481259
}

‎src/ast/datatype_decl_plugin.h‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -330,6 +330,7 @@ namespace datatype {
330330
bool is_datatype(sort const* s) const { return is_sort_of(s, fid(), DATATYPE_SORT); }
331331
bool is_enum_sort(sort* s);
332332
bool is_recursive(sort * ty);
333+
bool is_recursive_array(sort * ty);
333334
bool is_constructor(func_decl * f) const { return is_decl_of(f, fid(), OP_DT_CONSTRUCTOR); }
334335
bool is_recognizer(func_decl * f) const { return is_recognizer0(f) || is_is(f); }
335336
bool is_recognizer0(func_decl * f) const { return is_decl_of(f, fid(), OP_DT_RECOGNISER); }

‎src/model/array_factory.cpp‎

Lines changed: 12 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -132,13 +132,18 @@ expr * array_factory::get_fresh_value(sort * s) {
132132
return get_some_value(s);
133133
}
134134
sort * range = get_array_range(s);
135-
expr * range_val = m_model.get_fresh_value(range);
136-
if (range_val != nullptr) {
137-
// easy case
138-
func_interp * fi;
139-
expr * val = mk_array_interp(s, fi);
140-
fi->set_else(range_val);
141-
return val;
135+
expr* range_val = nullptr;
136+
137+
if (!m_recursive_fresh) {
138+
flet<bool> _recursive(m_recursive_fresh, true);
139+
range_val = m_model.get_fresh_value(range);
140+
if (range_val != nullptr) {
141+
// easy case
142+
func_interp* fi;
143+
expr* val = mk_array_interp(s, fi);
144+
fi->set_else(range_val);
145+
return val;
146+
}
142147
}
143148

144149
TRACE("array_factory_bug", tout << "array fresh value: using fresh index, range: " << mk_pp(range, m_manager) << "\n";);

‎src/model/array_factory.h‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,7 @@ class array_factory : public struct_factory {
2828
expr * mk_array_interp(sort * s, func_interp * & fi);
2929
void get_some_args_for(sort * s, ptr_buffer<expr> & args);
3030
bool mk_two_diff_values_for(sort * s);
31+
bool m_recursive_fresh { false };
3132
public:
3233
array_factory(ast_manager & m, model_core & md);
3334

‎src/model/datatype_factory.cpp‎

Lines changed: 16 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -27,6 +27,8 @@ datatype_factory::datatype_factory(ast_manager & m, model_core & md):
2727
}
2828

2929
expr * datatype_factory::get_some_value(sort * s) {
30+
if (!m_util.is_datatype(s))
31+
return m_model.get_some_value(s);
3032
value_set * set = nullptr;
3133
if (m_sort2value_set.find(s, set) && !set->empty())
3234
return *(set->begin());
@@ -77,6 +79,8 @@ bool datatype_factory::is_subterm_of_last_value(app* e) {
7779
It also updates m_last_fresh_value
7880
*/
7981
expr * datatype_factory::get_almost_fresh_value(sort * s) {
82+
if (!m_util.is_datatype(s))
83+
return m_model.get_some_value(s);
8084
value_set * set = get_value_set(s);
8185
if (set->empty()) {
8286
expr * val = get_some_value(s);
@@ -136,6 +140,8 @@ expr * datatype_factory::get_almost_fresh_value(sort * s) {
136140

137141

138142
expr * datatype_factory::get_fresh_value(sort * s) {
143+
if (!m_util.is_datatype(s))
144+
return m_model.get_fresh_value(s);
139145
TRACE("datatype", tout << "generating fresh value for: " << s->get_name() << "\n";);
140146
value_set * set = get_value_set(s);
141147
// Approach 0)
@@ -162,7 +168,9 @@ expr * datatype_factory::get_fresh_value(sort * s) {
162168
unsigned num = constructor->get_arity();
163169
for (unsigned i = 0; i < num; i++) {
164170
sort * s_arg = constructor->get_domain(i);
165-
if (!found_fresh_arg && (!m_util.is_recursive(s) || !m_util.is_datatype(s_arg) || !m_util.are_siblings(s, s_arg))) {
171+
if (!found_fresh_arg &&
172+
!m_util.is_recursive_array(s_arg) &&
173+
(!m_util.is_recursive(s) || !m_util.is_datatype(s_arg) || !m_util.are_siblings(s, s_arg))) {
166174
expr * new_arg = m_model.get_fresh_value(s_arg);
167175
if (new_arg != nullptr) {
168176
found_fresh_arg = true;
@@ -191,7 +199,7 @@ expr * datatype_factory::get_fresh_value(sort * s) {
191199
// search for constructor...
192200
unsigned num_iterations = 0;
193201
if (m_util.is_recursive(s)) {
194-
while(true) {
202+
while (true) {
195203
++num_iterations;
196204
TRACE("datatype", tout << mk_pp(get_last_fresh_value(s), m_manager) << "\n";);
197205
ptr_vector<func_decl> const & constructors = *m_util.get_datatype_constructors(s);
@@ -207,15 +215,15 @@ expr * datatype_factory::get_fresh_value(sort * s) {
207215
<< m_util.are_siblings(s, s_arg) << " is_datatype "
208216
<< m_util.is_datatype(s_arg) << " found_sibling "
209217
<< found_sibling << "\n";);
210-
if (!found_sibling && m_util.is_datatype(s_arg) && m_util.are_siblings(s, s_arg)) {
218+
if (!found_sibling && m_util.are_siblings(s, s_arg)) {
211219
found_sibling = true;
212220
expr * maybe_new_arg = nullptr;
213-
if (num_iterations <= 1) {
214-
maybe_new_arg = get_almost_fresh_value(s_arg);
215-
}
216-
else {
221+
if (!m_util.is_datatype(s_arg))
222+
maybe_new_arg = m_model.get_fresh_value(s_arg);
223+
else if (num_iterations <= 1)
224+
maybe_new_arg = get_almost_fresh_value(s_arg);
225+
else
217226
maybe_new_arg = get_fresh_value(s_arg);
218-
}
219227
if (!maybe_new_arg) {
220228
TRACE("datatype",
221229
tout << "no argument found for " << mk_pp(s_arg, m_manager) << "\n";);

0 commit comments

Comments
 (0)