| 42 | #define ARRAY_SORT_STR "Array" |
| 43 | |
| 44 | sort * array_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) { |
| 45 | |
| 46 | if (k == _SET_SORT) { |
| 47 | if (num_parameters != 1) { |
| 48 | m_manager->raise_exception("invalid array sort definition, invalid number of parameters"); |
| 49 | return nullptr; |
| 50 | } |
| 51 | parameter params[2] = { parameter(parameters[0]), parameter(m_manager->mk_bool_sort()) }; |
| 52 | return mk_sort(ARRAY_SORT, 2, params); |
| 53 | } |
| 54 | SASSERT(k == ARRAY_SORT); |
| 55 | if (num_parameters < 2) { |
| 56 | m_manager->raise_exception("invalid array sort definition, invalid number of parameters"); |
| 57 | return nullptr; |
| 58 | } |
| 59 | |
| 60 | for (unsigned i = 0; i < num_parameters; ++i) { |
| 61 | if (!parameters[i].is_ast() || !is_sort(parameters[i].get_ast())) { |
| 62 | m_manager->raise_exception("invalid array sort definition, parameter is not a sort"); |
| 63 | return nullptr; |
| 64 | } |
| 65 | } |
| 66 | sort * range = to_sort(parameters[num_parameters - 1].get_ast()); |
| 67 | TRACE(array_decl_plugin_bug, tout << mk_pp(range, *m_manager) << "\n";); |
| 68 | if (!range->is_infinite() && !range->is_very_big() && (1 == range->get_num_elements().size())) { |
| 69 | return m_manager->mk_sort(symbol(ARRAY_SORT_STR), sort_info(m_family_id, ARRAY_SORT, 1, |
| 70 | num_parameters, parameters)); |
| 71 | } |
| 72 | bool is_infinite = false; |
| 73 | bool is_very_big = false; |
| 74 | for (unsigned i = 0; i < num_parameters; ++i) { |
| 75 | sort * s = to_sort(parameters[i].get_ast()); |
| 76 | if (s->is_infinite()) { |
| 77 | is_infinite = true; |
| 78 | } |
| 79 | if (s->is_very_big()) { |
| 80 | is_very_big = true; |
| 81 | } |
| 82 | } |
| 83 | if (is_infinite) { |
| 84 | return m_manager->mk_sort(symbol(ARRAY_SORT_STR), sort_info(m_family_id, ARRAY_SORT, num_parameters, parameters)); |
| 85 | } |
| 86 | else if (is_very_big) { |
| 87 | return m_manager->mk_sort(symbol(ARRAY_SORT_STR), sort_info(m_family_id, ARRAY_SORT, sort_size::mk_very_big(), |
| 88 | num_parameters, parameters)); |
| 89 | } |
| 90 | else { |
| 91 | rational domain_sz(1); |
| 92 | rational num_elements; |
| 93 | for (unsigned i = 0; i < num_parameters - 1; ++i) { |
| 94 | domain_sz *= rational(to_sort(parameters[i].get_ast())->get_num_elements().size(),rational::ui64()); |
| 95 | } |
| 96 | if (domain_sz <= rational(128)) { |
| 97 | num_elements = rational(range->get_num_elements().size(),rational::ui64()); |
| 98 | num_elements = power(num_elements, static_cast<int>(domain_sz.get_int64())); |
| 99 | } |
| 100 | |
| 101 | if (domain_sz > rational(128) || !num_elements.is_uint64()) { |
no test coverage detected