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

fix #7309

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-07-28 13:18:08 +02:00
parent 5f6bb3db3e
commit f94500c3ca
2 changed files with 79 additions and 65 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

103
src/ast/datatype_decl_plugin.cpp
View file

@ -231,6 +231,24 @@ namespace datatype {
} }
m_defs.reset(); m_defs.reset();
m_util = nullptr; // force deletion m_util = nullptr; // force deletion
dealloc(m_asts);
std::for_each(m_vectors.begin(), m_vectors.end(), delete_proc<ptr_vector<func_decl> >());
}
void plugin::reset() {
m_datatype2constructors.reset();
m_datatype2nonrec_constructor.reset();
m_constructor2accessors.reset();
m_constructor2recognizer.reset();
m_recognizer2constructor.reset();
m_accessor2constructor.reset();
m_is_recursive.reset();
m_is_enum.reset();
std::for_each(m_vectors.begin(), m_vectors.end(), delete_proc<ptr_vector<func_decl> >());
m_vectors.reset();
dealloc(m_asts);
m_asts = nullptr;
++m_start;
} }
util & plugin::u() const { util & plugin::u() const {
@ -578,6 +596,7 @@ namespace datatype {
if (m_defs.find(s, d)) if (m_defs.find(s, d))
dealloc(d); dealloc(d);
m_defs.remove(s); m_defs.remove(s);
reset();
} }
bool plugin::is_value_visit(bool unique, expr * arg, ptr_buffer<app> & todo) const { bool plugin::is_value_visit(bool unique, expr * arg, ptr_buffer<app> & todo) const {
@ -799,7 +818,7 @@ namespace datatype {
for (unsigned i = 0; i < n; ++i) { for (unsigned i = 0; i < n; ++i) {
sort* ps = get_datatype_parameter_sort(s, i); sort* ps = get_datatype_parameter_sort(s, i);
sz = get_sort_size(params, ps); sz = get_sort_size(params, ps);
m_refs.push_back(sz); plugin().m_refs.push_back(sz);
S.insert(d.params().get(i), sz); S.insert(d.params().get(i), sz);
} }
auto ss = d.sort_size(); auto ss = d.sort_size();
@ -896,7 +915,7 @@ namespace datatype {
} }
TRACE("datatype", tout << "set sort size " << s << "\n";); TRACE("datatype", tout << "set sort size " << s << "\n";);
d.set_sort_size(param_size::size::mk_plus(s_add)); d.set_sort_size(param_size::size::mk_plus(s_add));
m_refs.reset(); plugin().m_refs.reset();
} }
} }
@ -1008,9 +1027,7 @@ namespace datatype {
util::util(ast_manager & m): util::util(ast_manager & m):
m(m), m(m),
m_family_id(null_family_id), m_family_id(null_family_id),
m_plugin(nullptr), m_plugin(nullptr) {
m_asts(m),
m_start(0) {
} }
@ -1027,24 +1044,24 @@ namespace datatype {
util::~util() { util::~util() {
std::for_each(m_vectors.begin(), m_vectors.end(), delete_proc<ptr_vector<func_decl> >());
} }
ptr_vector<func_decl> const * util::get_datatype_constructors(sort * ty) { ptr_vector<func_decl> const * util::get_datatype_constructors(sort * ty) {
SASSERT(is_datatype(ty)); SASSERT(is_datatype(ty));
ptr_vector<func_decl> * r = nullptr; ptr_vector<func_decl> * r = nullptr;
if (m_datatype2constructors.find(ty, r)) if (plugin().m_datatype2constructors.find(ty, r))
return r; return r;
r = alloc(ptr_vector<func_decl>); r = alloc(ptr_vector<func_decl>);
m_asts.push_back(ty); plugin().add_ast(ty);
m_vectors.push_back(r); plugin().m_vectors.push_back(r);
m_datatype2constructors.insert(ty, r); plugin().m_datatype2constructors.insert(ty, r);
if (!is_declared(ty)) if (!is_declared(ty))
m.raise_exception("datatype constructors have not been created"); m.raise_exception("datatype constructors have not been created");
def const& d = get_def(ty); def const& d = get_def(ty);
for (constructor const* c : d) { for (constructor const* c : d) {
func_decl_ref f = c->instantiate(ty); func_decl_ref f = c->instantiate(ty);
m_asts.push_back(f); plugin().add_ast(f);
r->push_back(f); r->push_back(f);
} }
return r; return r;
@ -1053,13 +1070,13 @@ namespace datatype {
ptr_vector<func_decl> const * util::get_constructor_accessors(func_decl * con) { ptr_vector<func_decl> const * util::get_constructor_accessors(func_decl * con) {
SASSERT(is_constructor(con)); SASSERT(is_constructor(con));
ptr_vector<func_decl> * res = nullptr; ptr_vector<func_decl> * res = nullptr;
if (m_constructor2accessors.find(con, res)) { if (plugin().m_constructor2accessors.find(con, res)) {
return res; return res;
} }
res = alloc(ptr_vector<func_decl>); res = alloc(ptr_vector<func_decl>);
m_asts.push_back(con); plugin().add_ast(con);
m_vectors.push_back(res); plugin().m_vectors.push_back(res);
m_constructor2accessors.insert(con, res); plugin().m_constructor2accessors.insert(con, res);
sort * datatype = con->get_range(); sort * datatype = con->get_range();
def const& d = get_def(datatype); def const& d = get_def(datatype);
for (constructor const* c : d) { for (constructor const* c : d) {
@ -1067,7 +1084,7 @@ namespace datatype {
for (accessor const* a : *c) { for (accessor const* a : *c) {
func_decl_ref fn = a->instantiate(datatype); func_decl_ref fn = a->instantiate(datatype);
res->push_back(fn); res->push_back(fn);
m_asts.push_back(fn); plugin().add_ast(fn);
} }
break; break;
} }
@ -1086,7 +1103,7 @@ namespace datatype {
func_decl * util::get_constructor_recognizer(func_decl * con) { func_decl * util::get_constructor_recognizer(func_decl * con) {
SASSERT(is_constructor(con)); SASSERT(is_constructor(con));
func_decl * d = nullptr; func_decl * d = nullptr;
if (m_constructor2recognizer.find(con, d)) if (plugin().m_constructor2recognizer.find(con, d))
return d; return d;
sort * datatype = con->get_range(); sort * datatype = con->get_range();
def const& dd = get_def(datatype); def const& dd = get_def(datatype);
@ -1097,9 +1114,9 @@ namespace datatype {
parameter ps[2] = { parameter(con), parameter(r) }; parameter ps[2] = { parameter(con), parameter(r) };
d = m.mk_func_decl(fid(), OP_DT_RECOGNISER, 2, ps, 1, &datatype); d = m.mk_func_decl(fid(), OP_DT_RECOGNISER, 2, ps, 1, &datatype);
SASSERT(d); SASSERT(d);
m_asts.push_back(con); plugin().add_ast(con);
m_asts.push_back(d); plugin().add_ast(d);
m_constructor2recognizer.insert(con, d); plugin().m_constructor2recognizer.insert(con, d);
return d; return d;
} }
@ -1120,10 +1137,10 @@ namespace datatype {
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;
if (!m_is_recursive.find(ty, r)) { if (!plugin().m_is_recursive.find(ty, r)) {
r = is_recursive_core(ty); r = is_recursive_core(ty);
m_is_recursive.insert(ty, r); plugin().m_is_recursive.insert(ty, r);
m_asts.push_back(ty); plugin().add_ast(ty);
} }
return r; return r;
} }
@ -1147,21 +1164,21 @@ namespace datatype {
if (!is_datatype(s)) if (!is_datatype(s))
return false; return false;
bool r = false; bool r = false;
if (m_is_enum.find(s, r)) if (plugin().m_is_enum.find(s, r))
return r; return r;
ptr_vector<func_decl> const& cnstrs = *get_datatype_constructors(s); ptr_vector<func_decl> const& cnstrs = *get_datatype_constructors(s);
r = true; r = true;
for (unsigned i = 0; r && i < cnstrs.size(); ++i) for (unsigned i = 0; r && i < cnstrs.size(); ++i)
r = cnstrs[i]->get_arity() == 0; r = cnstrs[i]->get_arity() == 0;
m_is_enum.insert(s, r); plugin().m_is_enum.insert(s, r);
m_asts.push_back(s); plugin().add_ast(s);
return r; return r;
} }
func_decl * util::get_accessor_constructor(func_decl * accessor) { func_decl * util::get_accessor_constructor(func_decl * accessor) {
SASSERT(is_accessor(accessor)); SASSERT(is_accessor(accessor));
func_decl * r = nullptr; func_decl * r = nullptr;
if (m_accessor2constructor.find(accessor, r)) if (plugin().m_accessor2constructor.find(accessor, r))
return r; return r;
sort * datatype = accessor->get_domain(0); sort * datatype = accessor->get_domain(0);
symbol c_id = accessor->get_parameter(1).get_symbol(); symbol c_id = accessor->get_parameter(1).get_symbol();
@ -1174,26 +1191,15 @@ namespace datatype {
} }
} }
r = fn; r = fn;
m_accessor2constructor.insert(accessor, r); plugin().m_accessor2constructor.insert(accessor, r);
m_asts.push_back(accessor); plugin().add_ast(accessor);
m_asts.push_back(r); plugin().add_ast(r);
return r; return r;
} }
void util::reset() { void util::reset() {
m_datatype2constructors.reset(); plugin().reset();
m_datatype2nonrec_constructor.reset();
m_constructor2accessors.reset();
m_constructor2recognizer.reset();
m_recognizer2constructor.reset();
m_accessor2constructor.reset();
m_is_recursive.reset();
m_is_enum.reset();
std::for_each(m_vectors.begin(), m_vectors.end(), delete_proc<ptr_vector<func_decl> >());
m_vectors.reset();
m_asts.reset();
++m_start;
} }
@ -1205,7 +1211,7 @@ namespace datatype {
func_decl * util::get_non_rec_constructor(sort * ty) { func_decl * util::get_non_rec_constructor(sort * ty) {
SASSERT(is_datatype(ty)); SASSERT(is_datatype(ty));
cnstr_depth cd; cnstr_depth cd;
if (m_datatype2nonrec_constructor.find(ty, cd)) if (plugin().m_datatype2nonrec_constructor.find(ty, cd))
return cd.first; return cd.first;
ptr_vector<sort> forbidden_set; ptr_vector<sort> forbidden_set;
forbidden_set.push_back(ty); forbidden_set.push_back(ty);
@ -1222,7 +1228,7 @@ namespace datatype {
each T_i is not a datatype or it is a datatype t not in forbidden_set, each T_i is not a datatype or it is a datatype t not in forbidden_set,
and get_non_rec_constructor_core(T_i, forbidden_set union { T_i }) and get_non_rec_constructor_core(T_i, forbidden_set union { T_i })
*/ */
util::cnstr_depth util::get_non_rec_constructor_core(sort * ty, ptr_vector<sort> & forbidden_set) { cnstr_depth util::get_non_rec_constructor_core(sort * ty, ptr_vector<sort> & forbidden_set) {
// We must select a constructor c(T_1, ..., T_n):T such that // We must select a constructor c(T_1, ..., T_n):T such that
// 1) T_i's are not recursive // 1) T_i's are not recursive
// If there is no such constructor, then we select one that // If there is no such constructor, then we select one that
@ -1231,7 +1237,7 @@ namespace datatype {
ptr_vector<func_decl> const& constructors = *get_datatype_constructors(ty); ptr_vector<func_decl> const& constructors = *get_datatype_constructors(ty);
array_util autil(m); array_util autil(m);
cnstr_depth result(nullptr, 0); cnstr_depth result(nullptr, 0);
if (m_datatype2nonrec_constructor.find(ty, result)) if (plugin().m_datatype2nonrec_constructor.find(ty, result))
return result; return result;
TRACE("util_bug", tout << "get-non-rec constructor: " << sort_ref(ty, m) << "\n"; TRACE("util_bug", tout << "get-non-rec constructor: " << sort_ref(ty, m) << "\n";
tout << "forbidden: "; tout << "forbidden: ";
@ -1273,9 +1279,9 @@ namespace datatype {
} }
} }
if (result.first) { if (result.first) {
m_asts.push_back(result.first); plugin().add_ast(result.first);
m_asts.push_back(ty); plugin().add_ast(ty);
m_datatype2nonrec_constructor.insert(ty, result); plugin().m_datatype2nonrec_constructor.insert(ty, result);
} }
return result; return result;
} }
@ -1291,6 +1297,7 @@ namespace datatype {
IF_VERBOSE(0, verbose_stream() << f->get_name() << "\n"); IF_VERBOSE(0, verbose_stream() << f->get_name() << "\n");
for (constructor* c : d) for (constructor* c : d)
IF_VERBOSE(0, verbose_stream() << "!= " << c->name() << "\n"); IF_VERBOSE(0, verbose_stream() << "!= " << c->name() << "\n");
return UINT_MAX;
SASSERT(false); SASSERT(false);
UNREACHABLE(); UNREACHABLE();
return 0; return 0;

41
src/ast/datatype_decl_plugin.h
View file

@ -198,6 +198,8 @@ namespace datatype {
def* translate(ast_translation& tr, util& u); def* translate(ast_translation& tr, util& u);
}; };
typedef std::pair<func_decl*, unsigned> cnstr_depth;
namespace decl { namespace decl {
class plugin : public decl_plugin { class plugin : public decl_plugin {
@ -213,6 +215,24 @@ namespace datatype {
void log_axiom_definitions(symbol const& s, sort * new_sort); void log_axiom_definitions(symbol const& s, sort * new_sort);
friend class util;
obj_map<sort, ptr_vector<func_decl>*> m_datatype2constructors;
obj_map<sort, cnstr_depth> m_datatype2nonrec_constructor;
obj_map<func_decl, ptr_vector<func_decl>*> m_constructor2accessors;
obj_map<func_decl, func_decl*> m_constructor2recognizer;
obj_map<func_decl, func_decl*> m_recognizer2constructor;
obj_map<func_decl, func_decl*> m_accessor2constructor;
obj_map<sort, bool> m_is_recursive;
obj_map<sort, bool> m_is_enum;
mutable obj_map<sort, bool> m_is_fully_interp;
mutable ast_ref_vector * m_asts = nullptr;
sref_vector<param_size::size> m_refs;
ptr_vector<ptr_vector<func_decl> > m_vectors;
unsigned m_start = 0;
mutable ptr_vector<sort> m_fully_interp_trail;
void add_ast(ast* a) const { if (!m_asts) m_asts = alloc(ast_ref_vector, *m_manager); m_asts->push_back(a); }
public: public:
plugin(): m_id_counter(0), m_class_id(0), m_has_nested_rec(false) {} plugin(): m_id_counter(0), m_class_id(0), m_has_nested_rec(false) {}
~plugin() override; ~plugin() override;
@ -259,6 +279,8 @@ namespace datatype {
bool has_nested_rec() const { return m_has_nested_rec; } bool has_nested_rec() const { return m_has_nested_rec; }
void reset();
private: private:
bool is_value_visit(bool unique, expr * arg, ptr_buffer<app> & todo) const; bool is_value_visit(bool unique, expr * arg, ptr_buffer<app> & todo) const;
bool is_value_aux(bool unique, app * arg) const; bool is_value_aux(bool unique, app * arg) const;
@ -295,25 +317,10 @@ namespace datatype {
ast_manager & m; ast_manager & m;
mutable family_id m_family_id; mutable family_id m_family_id;
mutable decl::plugin* m_plugin; mutable decl::plugin* m_plugin;
typedef std::pair<func_decl*, unsigned> cnstr_depth;
family_id fid() const; family_id fid() const;
obj_map<sort, ptr_vector<func_decl> *> m_datatype2constructors;
obj_map<sort, cnstr_depth> m_datatype2nonrec_constructor;
obj_map<func_decl, ptr_vector<func_decl> *> m_constructor2accessors;
obj_map<func_decl, func_decl *> m_constructor2recognizer;
obj_map<func_decl, func_decl *> m_recognizer2constructor;
obj_map<func_decl, func_decl *> m_accessor2constructor;
obj_map<sort, bool> m_is_recursive;
obj_map<sort, bool> m_is_enum;
mutable obj_map<sort, bool> m_is_fully_interp;
mutable ast_ref_vector m_asts;
sref_vector<param_size::size> m_refs;
ptr_vector<ptr_vector<func_decl> > m_vectors;
unsigned m_start;
mutable ptr_vector<sort> m_fully_interp_trail;
cnstr_depth get_non_rec_constructor_core(sort * ty, ptr_vector<sort> & forbidden_set); cnstr_depth get_non_rec_constructor_core(sort * ty, ptr_vector<sort> & forbidden_set);
friend class decl::plugin; friend class decl::plugin;