mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix #2504

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-08-21 10:06:33 +08:00
parent 2f60bcbfcb
commit e08abb3213
2 changed files with 16 additions and 12 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/ast/datatype_decl_plugin.cpp
View file

@ -121,6 +121,7 @@ namespace datatype {
}; };
namespace param_size { namespace param_size {
void size::dec_ref() { --m_ref; if (m_ref == 0) dealloc(this); }
size* size::mk_offset(sort_size const& s) { return alloc(offset, s); } size* size::mk_offset(sort_size const& s) { return alloc(offset, s); }
size* size::mk_param(sort_ref& p) { return alloc(sparam, p); } size* size::mk_param(sort_ref& p) { return alloc(sparam, p); }
size* size::mk_plus(size* a1, size* a2) { return alloc(plus, a1, a2); } size* size::mk_plus(size* a1, size* a2) { return alloc(plus, a1, a2); }
@ -545,7 +546,9 @@ namespace datatype {
void plugin::remove(symbol const& s) { void plugin::remove(symbol const& s) {
def* d = nullptr; def* d = nullptr;
if (m_defs.find(s, d)) dealloc(d); if (m_defs.find(s, d)) {
dealloc(d);
}
m_defs.remove(s); m_defs.remove(s);
} }
@ -722,14 +725,13 @@ namespace datatype {
if (is_datatype(s)) { if (is_datatype(s)) {
param_size::size* sz; param_size::size* sz;
obj_map<sort, param_size::size*> S; obj_map<sort, param_size::size*> S;
sref_vector<param_size::size> refs;
unsigned n = get_datatype_num_parameter_sorts(s); unsigned n = get_datatype_num_parameter_sorts(s);
def & d = get_def(s->get_name()); def & d = get_def(s->get_name());
SASSERT(n == d.params().size()); SASSERT(n == d.params().size());
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);
refs.push_back(sz); 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();
@ -737,7 +739,7 @@ namespace datatype {
d.set_sort_size(param_size::size::mk_offset(sort_size::mk_infinite())); d.set_sort_size(param_size::size::mk_offset(sort_size::mk_infinite()));
ss = d.sort_size(); ss = d.sort_size();
} }
return ss->subst(S); return ss->subst(S);
} }
array_util autil(m); array_util autil(m);
if (autil.is_array(s)) { if (autil.is_array(s)) {
@ -821,6 +823,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();
} }
} }

17
src/ast/datatype_decl_plugin.h
View file

@ -108,7 +108,7 @@ namespace datatype {
size(): m_ref(0) {} size(): m_ref(0) {}
virtual ~size() {} virtual ~size() {}
void inc_ref() { ++m_ref; } void inc_ref() { ++m_ref; }
void dec_ref() { --m_ref; if (m_ref == 0) dealloc(this); } void dec_ref();
static size* mk_offset(sort_size const& s); static size* mk_offset(sort_size const& s);
static size* mk_param(sort_ref& p); static size* mk_param(sort_ref& p);
static size* mk_plus(size* a1, size* a2); static size* mk_plus(size* a1, size* a2);
@ -159,13 +159,13 @@ namespace datatype {
}; };
class def { class def {
ast_manager& m; ast_manager& m;
util& m_util; util& m_util;
symbol m_name; symbol m_name;
unsigned m_class_id; unsigned m_class_id;
param_size::size* m_sort_size; param_size::size* m_sort_size;
sort_ref_vector m_params; sort_ref_vector m_params;
mutable sort_ref m_sort; mutable sort_ref m_sort;
ptr_vector<constructor> m_constructors; ptr_vector<constructor> m_constructors;
public: public:
def(ast_manager& m, util& u, symbol const& n, unsigned class_id, unsigned num_params, sort * const* params): def(ast_manager& m, util& u, symbol const& n, unsigned class_id, unsigned num_params, sort * const* params):
@ -304,6 +304,7 @@ namespace datatype {
obj_map<sort, bool> m_is_enum; obj_map<sort, bool> m_is_enum;
mutable obj_map<sort, bool> m_is_fully_interp; mutable obj_map<sort, bool> m_is_fully_interp;
mutable ast_ref_vector m_asts; mutable ast_ref_vector m_asts;
sref_vector<param_size::size> m_refs;
ptr_vector<ptr_vector<func_decl> > m_vectors; ptr_vector<ptr_vector<func_decl> > m_vectors;
unsigned m_start; unsigned m_start;
mutable ptr_vector<sort> m_fully_interp_trail; mutable ptr_vector<sort> m_fully_interp_trail;