mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

fix #1749 by rejecting non-well-founded use of datatype in array

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-07-12 22:45:52 -07:00
parent b7ea90c12b
commit 4915fb080b
4 changed files with 40 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/ast/ast.cpp
View file

@ -1934,8 +1934,7 @@ sort * ast_manager::substitute(sort* s, unsigned n, sort * const * src, sort * c
vector<parameter> ps;
bool change = false;
sort_ref_vector sorts(*this);
for (unsigned i = 0; i < s->get_num_parameters(); ++i) {
parameter const& p = s->get_parameter(i);
for (parameter const& p : s->parameters()) {
if (p.is_ast()) {
SASSERT(is_sort(p.get_ast()));
change = true;
@ -2330,8 +2329,8 @@ bool ast_manager::is_label_lit(expr const * n, buffer<symbol> & names) const {
return false;
}
func_decl const * decl = to_app(n)->get_decl();
for (unsigned i = 0; i < decl->get_num_parameters(); i++)
names.push_back(decl->get_parameter(i).get_symbol());
for (parameter const& p : decl->parameters()) {
names.push_back(p.get_symbol());
return true;
}
@ -2928,8 +2927,8 @@ bool ast_manager::is_quant_inst(expr const* e, expr*& not_q_or_i, ptr_vector<exp
not_q_or_i = to_app(e)->get_arg(0);
func_decl* d = to_app(e)->get_decl();
SASSERT(binding.empty());
for (unsigned i = 0; i < d->get_num_parameters(); ++i) {
binding.push_back(to_expr(d->get_parameter(i).get_ast()));
for (parameter const& p : d->parameters()) {
binding.push_back(to_expr(p.get_ast()));
}
return true;
}

24
src/ast/ast.h
View file

@ -273,6 +273,14 @@ public:
parameter const * get_parameters() const { return m_parameters.begin(); }
bool private_parameters() const { return m_private_parameters; }
struct iterator {
decl_info const& d;
iterator(decl_info const& d) : d(d) {}
parameter const* begin() const { return d.get_parameters(); }
parameter const* end() const { return begin() + d.get_num_parameters(); }
};
iterator parameters() const { return iterator(*this); }
unsigned hash() const;
bool operator==(decl_info const & info) const;
};
@ -571,6 +579,16 @@ public:
parameter const & get_parameter(unsigned idx) const { return m_info->get_parameter(idx); }
parameter const * get_parameters() const { return m_info == nullptr ? nullptr : m_info->get_parameters(); }
bool private_parameters() const { return m_info != nullptr && m_info->private_parameters(); }
struct iterator {
decl const& d;
iterator(decl const& d) : d(d) {}
parameter const* begin() const { return d.get_parameters(); }
parameter const* end() const { return begin() + d.get_num_parameters(); }
};
iterator parameters() const { return iterator(*this); }
};
// -----------------------------------
@ -2401,11 +2419,7 @@ public:
}
void reset() {
ptr_buffer<ast>::iterator it = m_to_unmark.begin();
ptr_buffer<ast>::iterator end = m_to_unmark.end();
for (; it != end; ++it) {
reset_mark(*it);
}
for (ast* a : m_to_unmark) reset_mark(a);
m_to_unmark.reset();
}

28
src/ast/datatype_decl_plugin.cpp
View file

@ -692,6 +692,7 @@ namespace datatype {
}
unsigned num_well_founded = 0, id = 0;
bool changed;
ptr_vector<sort> subsorts;
do {
changed = false;
for (unsigned tid = 0; tid < num_types; tid++) {
@ -701,23 +702,25 @@ namespace datatype {
sort* s = sorts[tid];
def const& d = get_def(s);
for (constructor const* c : d) {
bool found_nonwf = false;
for (accessor const* a : *c) {
if (sort2id.find(a->range(), id) && !well_founded[id]) {
found_nonwf = true;
break;
subsorts.reset();
get_subsorts(a->range(), subsorts);
for (sort* srt : subsorts) {
if (sort2id.find(srt, id) && !well_founded[id]) {
goto next_constructor;
}
}
}
if (!found_nonwf) {
changed = true;
well_founded[tid] = true;
num_well_founded++;
break;
}
changed = true;
well_founded[tid] = true;
num_well_founded++;
break;
next_constructor:
;
}
}
}
while(changed && num_well_founded < num_types);
while (changed && num_well_founded < num_types);
return num_well_founded == num_types;
}
@ -727,8 +730,7 @@ namespace datatype {
void util::get_subsorts(sort* s, ptr_vector<sort>& sorts) const {
sorts.push_back(s);
for (unsigned i = 0; i < s->get_num_parameters(); ++i) {
parameter const& p = s->get_parameter(i);
for (parameter const& p : s->parameters()) {
if (p.is_ast() && is_sort(p.get_ast())) {
get_subsorts(to_sort(p.get_ast()), sorts);
}

3
src/ast/seq_decl_plugin.cpp
View file

@ -376,8 +376,7 @@ bool seq_decl_plugin::match(ptr_vector<sort>& binding, sort* s, sort* sP) {
if (s->get_family_id() == sP->get_family_id() &&
s->get_decl_kind() == sP->get_decl_kind() &&
s->get_num_parameters() == sP->get_num_parameters()) {
for (unsigned i = 0; i < s->get_num_parameters(); ++i) {
parameter const& p = s->get_parameter(i);
for (parameter const& p : s->parameters()) {
if (p.is_ast() && is_sort(p.get_ast())) {
parameter const& p2 = sP->get_parameter(i);
if (!match(binding, to_sort(p.get_ast()), to_sort(p2.get_ast()))) return false;