mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 02:42:02 +00:00
Code Activity

fix #2276

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-05-14 19:20:55 +02:00
parent c42d590db3
commit f989e4eb38
3 changed files with 12 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/ast/datatype_decl_plugin.cpp
View file

@ -960,6 +960,11 @@ namespace datatype {
return to_func_decl(recognizer->get_parameter(0).get_ast()); return to_func_decl(recognizer->get_parameter(0).get_ast());
} }
func_decl * util::get_update_accessor(func_decl * updt) const {
SASSERT(is_update_field(updt));
return to_func_decl(updt->get_parameter(0).get_ast());
}
bool util::is_recursive(sort * ty) { bool util::is_recursive(sort * ty) {
SASSERT(is_datatype(ty)); SASSERT(is_datatype(ty));
bool r = false; bool r = false;

1
src/ast/datatype_decl_plugin.h
View file

@ -350,6 +350,7 @@ namespace datatype {
ptr_vector<func_decl> const * get_constructor_accessors(func_decl * constructor); ptr_vector<func_decl> const * get_constructor_accessors(func_decl * constructor);
func_decl * get_accessor_constructor(func_decl * accessor); func_decl * get_accessor_constructor(func_decl * accessor);
func_decl * get_recognizer_constructor(func_decl * recognizer) const; func_decl * get_recognizer_constructor(func_decl * recognizer) const;
func_decl * get_update_accessor(func_decl * update) const;
family_id get_family_id() const { return m_family_id; } family_id get_family_id() const { return m_family_id; }
bool are_siblings(sort * s1, sort * s2); bool are_siblings(sort * s1, sort * s2);
bool is_func_decl(op_kind k, unsigned num_params, parameter const* params, func_decl* f); bool is_func_decl(op_kind k, unsigned num_params, parameter const* params, func_decl* f);

11
src/ast/rewriter/datatype_rewriter.cpp
View file

@ -70,17 +70,18 @@ br_status datatype_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr
return BR_FAILED; return BR_FAILED;
app * a = to_app(args[0]); app * a = to_app(args[0]);
func_decl * c_decl = a->get_decl(); func_decl * c_decl = a->get_decl();
if (c_decl != m_util.get_accessor_constructor(f)) { func_decl * acc = m_util.get_update_accessor(f);
if (c_decl != m_util.get_accessor_constructor(acc)) {
result = a; result = a;
return BR_DONE; return BR_DONE;
} }
ptr_vector<func_decl> const & acc = *m_util.get_constructor_accessors(c_decl); ptr_vector<func_decl> const & accs = *m_util.get_constructor_accessors(c_decl);
SASSERT(acc.size() == a->get_num_args()); SASSERT(accs.size() == a->get_num_args());
unsigned num = acc.size(); unsigned num = accs.size();
ptr_buffer<expr> new_args; ptr_buffer<expr> new_args;
for (unsigned i = 0; i < num; ++i) { for (unsigned i = 0; i < num; ++i) {
if (f == acc[i]) { if (acc == accs[i]) {
new_args.push_back(args[1]); new_args.push_back(args[1]);
} }
else { else {