Skip to content

Commit

Permalink
fix #7309
Browse files Browse the repository at this point in the history
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Jul 28, 2024
1 parent 5f6bb3d commit f94500c
Show file tree
Hide file tree
Showing 2 changed files with 79 additions and 65 deletions.
103 changes: 55 additions & 48 deletions src/ast/datatype_decl_plugin.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down Expand Up @@ -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 {
Expand Down Expand Up @@ -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();
Expand Down Expand Up @@ -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();
}
}

Expand Down Expand Up @@ -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) {
}


Expand All @@ -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;
Expand All @@ -1053,21 +1070,21 @@ 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) {
if (c->name() == con->get_name()) {
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;
}
Expand All @@ -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);
Expand All @@ -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;
}

Expand All @@ -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;
}
Expand All @@ -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();
Expand All @@ -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();
}


Expand All @@ -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);
Expand All @@ -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
Expand All @@ -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: ";
Expand Down Expand Up @@ -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;
}
Expand All @@ -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;
Expand Down
41 changes: 24 additions & 17 deletions src/ast/datatype_decl_plugin.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand All @@ -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;
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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;
Expand Down

0 comments on commit f94500c

Please sign in to comment.