diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index a4ddbdaed13..c39b09d5ed4 100644
--- a/src/ast/datatype_decl_plugin.cpp
+++ b/src/ast/datatype_decl_plugin.cpp
@@ -231,6 +231,24 @@ namespace datatype {
}
m_defs.reset();
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 {
@@ -578,6 +596,7 @@ namespace datatype {
if (m_defs.find(s, d))
dealloc(d);
m_defs.remove(s);
+ reset();
}
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) {
sort* ps = get_datatype_parameter_sort(s, i);
sz = get_sort_size(params, ps);
- m_refs.push_back(sz);
+ plugin().m_refs.push_back(sz);
S.insert(d.params().get(i), sz);
}
auto ss = d.sort_size();
@@ -896,7 +915,7 @@ namespace datatype {
}
TRACE("datatype", tout << "set sort size " << s << "\n";);
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):
m(m),
m_family_id(null_family_id),
- m_plugin(nullptr),
- m_asts(m),
- m_start(0) {
+ m_plugin(nullptr) {
}
@@ -1027,24 +1044,24 @@ namespace datatype {
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) {
SASSERT(is_datatype(ty));
ptr_vector<func_decl> * r = nullptr;
- if (m_datatype2constructors.find(ty, r))
+ if (plugin().m_datatype2constructors.find(ty, r))
return r;
r = alloc(ptr_vector<func_decl>);
- m_asts.push_back(ty);
- m_vectors.push_back(r);
- m_datatype2constructors.insert(ty, r);
+ plugin().add_ast(ty);
+ plugin().m_vectors.push_back(r);
+ plugin().m_datatype2constructors.insert(ty, r);
if (!is_declared(ty))
m.raise_exception("datatype constructors have not been created");
def const& d = get_def(ty);
for (constructor const* c : d) {
func_decl_ref f = c->instantiate(ty);
- m_asts.push_back(f);
+ plugin().add_ast(f);
r->push_back(f);
}
return r;
@@ -1053,13 +1070,13 @@ namespace datatype {
ptr_vector<func_decl> const * util::get_constructor_accessors(func_decl * con) {
SASSERT(is_constructor(con));
ptr_vector<func_decl> * res = nullptr;
- if (m_constructor2accessors.find(con, res)) {
+ if (plugin().m_constructor2accessors.find(con, res)) {
return res;
}
res = alloc(ptr_vector<func_decl>);
- m_asts.push_back(con);
- m_vectors.push_back(res);
- m_constructor2accessors.insert(con, res);
+ plugin().add_ast(con);
+ plugin().m_vectors.push_back(res);
+ plugin().m_constructor2accessors.insert(con, res);
sort * datatype = con->get_range();
def const& d = get_def(datatype);
for (constructor const* c : d) {
@@ -1067,7 +1084,7 @@ namespace datatype {
for (accessor const* a : *c) {
func_decl_ref fn = a->instantiate(datatype);
res->push_back(fn);
- m_asts.push_back(fn);
+ plugin().add_ast(fn);
}
break;
}
@@ -1086,7 +1103,7 @@ namespace datatype {
func_decl * util::get_constructor_recognizer(func_decl * con) {
SASSERT(is_constructor(con));
func_decl * d = nullptr;
- if (m_constructor2recognizer.find(con, d))
+ if (plugin().m_constructor2recognizer.find(con, d))
return d;
sort * datatype = con->get_range();
def const& dd = get_def(datatype);
@@ -1097,9 +1114,9 @@ namespace datatype {
parameter ps[2] = { parameter(con), parameter(r) };
d = m.mk_func_decl(fid(), OP_DT_RECOGNISER, 2, ps, 1, &datatype);
SASSERT(d);
- m_asts.push_back(con);
- m_asts.push_back(d);
- m_constructor2recognizer.insert(con, d);
+ plugin().add_ast(con);
+ plugin().add_ast(d);
+ plugin().m_constructor2recognizer.insert(con, d);
return d;
}
@@ -1120,10 +1137,10 @@ namespace datatype {
bool util::is_recursive(sort * ty) {
SASSERT(is_datatype(ty));
bool r = false;
- if (!m_is_recursive.find(ty, r)) {
+ if (!plugin().m_is_recursive.find(ty, r)) {
r = is_recursive_core(ty);
- m_is_recursive.insert(ty, r);
- m_asts.push_back(ty);
+ plugin().m_is_recursive.insert(ty, r);
+ plugin().add_ast(ty);
}
return r;
}
@@ -1147,21 +1164,21 @@ namespace datatype {
if (!is_datatype(s))
return false;
bool r = false;
- if (m_is_enum.find(s, r))
+ if (plugin().m_is_enum.find(s, r))
return r;
ptr_vector<func_decl> const& cnstrs = *get_datatype_constructors(s);
r = true;
for (unsigned i = 0; r && i < cnstrs.size(); ++i)
r = cnstrs[i]->get_arity() == 0;
- m_is_enum.insert(s, r);
- m_asts.push_back(s);
+ plugin().m_is_enum.insert(s, r);
+ plugin().add_ast(s);
return r;
}
func_decl * util::get_accessor_constructor(func_decl * accessor) {
SASSERT(is_accessor(accessor));
func_decl * r = nullptr;
- if (m_accessor2constructor.find(accessor, r))
+ if (plugin().m_accessor2constructor.find(accessor, r))
return r;
sort * datatype = accessor->get_domain(0);
symbol c_id = accessor->get_parameter(1).get_symbol();
@@ -1174,26 +1191,15 @@ namespace datatype {
}
}
r = fn;
- m_accessor2constructor.insert(accessor, r);
- m_asts.push_back(accessor);
- m_asts.push_back(r);
+ plugin().m_accessor2constructor.insert(accessor, r);
+ plugin().add_ast(accessor);
+ plugin().add_ast(r);
return r;
}
void util::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();
- m_asts.reset();
- ++m_start;
+ plugin().reset();
}
@@ -1205,7 +1211,7 @@ namespace datatype {
func_decl * util::get_non_rec_constructor(sort * ty) {
SASSERT(is_datatype(ty));
cnstr_depth cd;
- if (m_datatype2nonrec_constructor.find(ty, cd))
+ if (plugin().m_datatype2nonrec_constructor.find(ty, cd))
return cd.first;
ptr_vector<sort> forbidden_set;
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,
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
// 1) T_i's are not recursive
// 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);
array_util autil(m);
cnstr_depth result(nullptr, 0);
- if (m_datatype2nonrec_constructor.find(ty, result))
+ if (plugin().m_datatype2nonrec_constructor.find(ty, result))
return result;
TRACE("util_bug", tout << "get-non-rec constructor: " << sort_ref(ty, m) << "\n";
tout << "forbidden: ";
@@ -1273,9 +1279,9 @@ namespace datatype {
}
}
if (result.first) {
- m_asts.push_back(result.first);
- m_asts.push_back(ty);
- m_datatype2nonrec_constructor.insert(ty, result);
+ plugin().add_ast(result.first);
+ plugin().add_ast(ty);
+ plugin().m_datatype2nonrec_constructor.insert(ty, result);
}
return result;
}
@@ -1291,6 +1297,7 @@ namespace datatype {
IF_VERBOSE(0, verbose_stream() << f->get_name() << "\n");
for (constructor* c : d)
IF_VERBOSE(0, verbose_stream() << "!= " << c->name() << "\n");
+ return UINT_MAX;
SASSERT(false);
UNREACHABLE();
return 0;
diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h
index 341f3669b50..f68dcfbdd79 100644
--- a/src/ast/datatype_decl_plugin.h
+++ b/src/ast/datatype_decl_plugin.h
@@ -198,6 +198,8 @@ namespace datatype {
def* translate(ast_translation& tr, util& u);
};
+ typedef std::pair<func_decl*, unsigned> cnstr_depth;
+
namespace decl {
class plugin : public decl_plugin {
@@ -213,6 +215,24 @@ namespace datatype {
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:
plugin(): m_id_counter(0), m_class_id(0), m_has_nested_rec(false) {}
~plugin() override;
@@ -259,6 +279,8 @@ namespace datatype {
bool has_nested_rec() const { return m_has_nested_rec; }
+ void reset();
+
private:
bool is_value_visit(bool unique, expr * arg, ptr_buffer<app> & todo) const;
bool is_value_aux(bool unique, app * arg) const;
@@ -295,25 +317,10 @@ namespace datatype {
ast_manager & m;
mutable family_id m_family_id;
mutable decl::plugin* m_plugin;
- typedef std::pair<func_decl*, unsigned> cnstr_depth;
+
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);
friend class decl::plugin;