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

add check for contravariance to fix #2256

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-05-22 12:25:36 +04:00
parent 082a0f4df4
commit faf4ba8309
2 changed files with 47 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

45
src/ast/datatype_decl_plugin.cpp
View file

@ -446,6 +446,9 @@ namespace datatype {
if (!u().is_well_founded(sorts.size(), sorts.c_ptr())) { if (!u().is_well_founded(sorts.size(), sorts.c_ptr())) {
m_manager->raise_exception("datatype is not well-founded"); m_manager->raise_exception("datatype is not well-founded");
} }
if (!u().is_covariant(sorts.size(), sorts.c_ptr())) {
m_manager->raise_exception("datatype is not co-variant");
}
u().compute_datatype_size_functions(m_def_block); u().compute_datatype_size_functions(m_def_block);
for (symbol const& s : m_def_block) { for (symbol const& s : m_def_block) {
@ -851,6 +854,48 @@ namespace datatype {
return num_well_founded == num_types; return num_well_founded == num_types;
} }
/**
\brief Return true if the inductive datatype is co-variant.
Pre-condition: The given argument constrains the parameters of an inductive datatype.
*/
bool util::is_covariant(unsigned num_types, sort* const* sorts) const {
ast_mark mark;
ptr_vector<sort> subsorts;
for (unsigned tid = 0; tid < num_types; tid++) {
mark.mark(sorts[tid], true);
}
for (unsigned tid = 0; tid < num_types; tid++) {
sort* s = sorts[tid];
def const& d = get_def(s);
for (constructor const* c : d) {
for (accessor const* a : *c) {
if (!is_covariant(mark, subsorts, a->range())) {
return false;
}
}
}
}
return true;
}
bool util::is_covariant(ast_mark& mark, ptr_vector<sort>& subsorts, sort* s) const {
array_util autil(m);
if (!autil.is_array(s)) {
return true;
}
unsigned n = get_array_arity(s);
subsorts.reset();
for (unsigned i = 0; i < n; ++i) {
get_subsorts(get_array_domain(s, i), subsorts);
}
for (sort* r : subsorts) {
if (mark.is_marked(r)) return false;
}
return is_covariant(mark, subsorts, get_array_range(s));
}
def const& util::get_def(sort* s) const { def const& util::get_def(sort* s) const {
return m_plugin->get_def(s); return m_plugin->get_def(s);
} }

2
src/ast/datatype_decl_plugin.h
View file

@ -314,6 +314,8 @@ namespace datatype {
void compute_datatype_size_functions(svector<symbol> const& names); void compute_datatype_size_functions(svector<symbol> const& names);
param_size::size* get_sort_size(sort_ref_vector const& params, sort* s); param_size::size* get_sort_size(sort_ref_vector const& params, sort* s);
bool is_well_founded(unsigned num_types, sort* const* sorts); bool is_well_founded(unsigned num_types, sort* const* sorts);
bool is_covariant(unsigned num_types, sort* const* sorts) const;
bool is_covariant(ast_mark& mark, ptr_vector<sort>& subsorts, sort* s) const;
def& get_def(symbol const& s) { return m_plugin->get_def(s); } def& get_def(symbol const& s) { return m_plugin->get_def(s); }
void get_subsorts(sort* s, ptr_vector<sort>& sorts) const; void get_subsorts(sort* s, ptr_vector<sort>& sorts) const;