mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

fix #5297

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-05-23 13:42:15 -07:00
parent 8919fa4970
commit 2ebab021f2
5 changed files with 41 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/ast/datatype_decl_plugin.cpp
View file

@ -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;
}

1
src/ast/datatype_decl_plugin.h
View file

@ -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); }

19
src/model/array_factory.cpp
View file

@ -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";);

1
src/model/array_factory.h
View file

@ -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);

24
src/model/datatype_factory.cpp
View file

@ -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";);