mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 21:31:22 +00:00
Code Activity

fix #3060

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-02-20 21:05:21 -08:00
parent 84b12dddac
commit 1aea0d2c8b
2 changed files with 21 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

31
src/cmd_context/pdecl.cpp
View file

@ -145,7 +145,7 @@ class psort_sort : public psort {
bool check_num_params(pdecl * other) const override { return true; } bool check_num_params(pdecl * other) const override { return true; }
size_t obj_size() const override { return sizeof(psort_sort); } size_t obj_size() const override { return sizeof(psort_sort); }
sort * get_sort() const { return m_sort; } sort * get_sort() const { return m_sort; }
sort * instantiate(pdecl_manager & m, sort * const * s) override { return m_sort; } sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override { return m_sort; }
public: public:
~psort_sort() override {} ~psort_sort() override {}
bool is_sort_wrapper() const override { return true; } bool is_sort_wrapper() const override { return true; }
@ -165,7 +165,10 @@ class psort_var : public psort {
friend class pdecl_manager; friend class pdecl_manager;
unsigned m_idx; unsigned m_idx;
psort_var(unsigned id, unsigned num_params, unsigned idx):psort(id, num_params), m_idx(idx) { SASSERT(idx < num_params); } psort_var(unsigned id, unsigned num_params, unsigned idx):psort(id, num_params), m_idx(idx) { SASSERT(idx < num_params); }
sort * instantiate(pdecl_manager & m, sort * const * s) override { return s[m_idx]; } sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override {
if (n <= m_idx) throw default_exception("type parameter was not declared");
return s[m_idx];
}
size_t obj_size() const override { return sizeof(psort_var); } size_t obj_size() const override { return sizeof(psort_var); }
public: public:
~psort_var() override {} ~psort_var() override {}
@ -214,14 +217,14 @@ class psort_app : public psort {
unsigned operator()(psort_app const * d, unsigned idx) const { return d->m_args[idx]->hash(); } unsigned operator()(psort_app const * d, unsigned idx) const { return d->m_args[idx]->hash(); }
}; };
sort * instantiate(pdecl_manager & m, sort * const * s) override { sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override {
sort * r = find(s); sort * r = find(s);
if (r) if (r)
return r; return r;
sort_ref_buffer args_i(m.m()); sort_ref_buffer args_i(m.m());
unsigned sz = m_args.size(); unsigned sz = m_args.size();
for (unsigned i = 0; i < sz; i++) { for (unsigned i = 0; i < sz; i++) {
sort * a = m_args[i]->instantiate(m, s); sort * a = m_args[i]->instantiate(m, n, s);
args_i.push_back(a); args_i.push_back(a);
} }
r = m_decl->instantiate(m, args_i.size(), args_i.c_ptr()); r = m_decl->instantiate(m, args_i.size(), args_i.c_ptr());
@ -321,7 +324,7 @@ sort * psort_user_decl::instantiate(pdecl_manager & m, unsigned n, sort * const
r = m.m().mk_uninterpreted_sort(m_name, ps.size(), ps.c_ptr()); r = m.m().mk_uninterpreted_sort(m_name, ps.size(), ps.c_ptr());
} }
else { else {
r = m_def->instantiate(m, s); r = m_def->instantiate(m, n, s);
} }
cache(m, s, r); cache(m, s, r);
m.save_info(r, this, n, s); m.save_info(r, this, n, s);
@ -457,10 +460,10 @@ bool paccessor_decl::fix_missing_refs(dictionary<int> const & symbol2idx, symbol
return false; return false;
} }
accessor_decl * paccessor_decl::instantiate_decl(pdecl_manager & m, sort * const * s) { accessor_decl * paccessor_decl::instantiate_decl(pdecl_manager & m, unsigned n, sort * const * s) {
switch (m_type.kind()) { switch (m_type.kind()) {
case PTR_REC_REF: return mk_accessor_decl(m.m(), m_name, type_ref(m_type.get_idx())); case PTR_REC_REF: return mk_accessor_decl(m.m(), m_name, type_ref(m_type.get_idx()));
case PTR_PSORT: return mk_accessor_decl(m.m(), m_name, type_ref(m_type.get_psort()->instantiate(m, s))); case PTR_PSORT: return mk_accessor_decl(m.m(), m_name, type_ref(m_type.get_psort()->instantiate(m, n, s)));
default: default:
// missing refs must have been eliminated. // missing refs must have been eliminated.
UNREACHABLE(); UNREACHABLE();
@ -504,10 +507,10 @@ bool pconstructor_decl::fix_missing_refs(dictionary<int> const & symbol2idx, sym
return true; return true;
} }
constructor_decl * pconstructor_decl::instantiate_decl(pdecl_manager & m, sort * const * s) { constructor_decl * pconstructor_decl::instantiate_decl(pdecl_manager & m, unsigned n, sort * const * s) {
ptr_buffer<accessor_decl> as; ptr_buffer<accessor_decl> as;
for (paccessor_decl* a : m_accessors) for (paccessor_decl* a : m_accessors)
as.push_back(a->instantiate_decl(m, s)); as.push_back(a->instantiate_decl(m, n, s));
return mk_constructor_decl(m_name, m_recogniser_name, as.size(), as.c_ptr()); return mk_constructor_decl(m_name, m_recogniser_name, as.size(), as.c_ptr());
} }
@ -564,10 +567,10 @@ bool pdatatype_decl::fix_missing_refs(dictionary<int> const & symbol2idx, symbol
return true; return true;
} }
datatype_decl * pdatatype_decl::instantiate_decl(pdecl_manager & m, sort * const * s) { datatype_decl * pdatatype_decl::instantiate_decl(pdecl_manager & m, unsigned n, sort * const * s) {
ptr_buffer<constructor_decl> cs; ptr_buffer<constructor_decl> cs;
for (auto c : m_constructors) { for (auto c : m_constructors) {
cs.push_back(c->instantiate_decl(m, s)); cs.push_back(c->instantiate_decl(m, n, s));
} }
datatype_util util(m.m()); datatype_util util(m.m());
return mk_datatype_decl(util, m_name, m_num_params, s, cs.size(), cs.c_ptr()); return mk_datatype_decl(util, m_name, m_num_params, s, cs.size(), cs.c_ptr());
@ -638,7 +641,7 @@ bool pdatatype_decl::commit(pdecl_manager& m) {
ps.push_back(m.m().mk_uninterpreted_sort(symbol(i), 0, nullptr)); ps.push_back(m.m().mk_uninterpreted_sort(symbol(i), 0, nullptr));
} }
datatype_decl_buffer dts; datatype_decl_buffer dts;
dts.m_buffer.push_back(instantiate_decl(m, ps.c_ptr())); dts.m_buffer.push_back(instantiate_decl(m, ps.size(), ps.c_ptr()));
datatype_decl * d_ptr = dts.m_buffer[0]; datatype_decl * d_ptr = dts.m_buffer[0];
sort_ref_vector sorts(m.m()); sort_ref_vector sorts(m.m());
bool is_ok = m.get_dt_plugin()->mk_datatypes(1, &d_ptr, m_num_params, ps.c_ptr(), sorts); bool is_ok = m.get_dt_plugin()->mk_datatypes(1, &d_ptr, m_num_params, ps.c_ptr(), sorts);
@ -716,7 +719,7 @@ bool pdatatypes_decl::commit(pdecl_manager& m) {
for (unsigned i = 0; i < d->get_num_params(); ++i) { for (unsigned i = 0; i < d->get_num_params(); ++i) {
ps.push_back(m.m().mk_uninterpreted_sort(symbol(i), 0, nullptr)); ps.push_back(m.m().mk_uninterpreted_sort(symbol(i), 0, nullptr));
} }
dts.m_buffer.push_back(d->instantiate_decl(m, ps.c_ptr())); dts.m_buffer.push_back(d->instantiate_decl(m, ps.size(), ps.c_ptr()));
} }
sort_ref_vector sorts(m.m()); sort_ref_vector sorts(m.m());
bool is_ok = m.get_dt_plugin()->mk_datatypes(m_datatypes.size(), dts.m_buffer.c_ptr(), 0, nullptr, sorts); bool is_ok = m.get_dt_plugin()->mk_datatypes(m_datatypes.size(), dts.m_buffer.c_ptr(), 0, nullptr, sorts);
@ -937,7 +940,7 @@ psort_decl * pdecl_manager::mk_psort_builtin_decl(symbol const & n, family_id fi
sort * pdecl_manager::instantiate(psort * p, unsigned num, sort * const * args) { sort * pdecl_manager::instantiate(psort * p, unsigned num, sort * const * args) {
// ignoring stack overflows... sorts are not deeply nested // ignoring stack overflows... sorts are not deeply nested
return p->instantiate(*this, args); return p->instantiate(*this, num, args);
} }

8
src/cmd_context/pdecl.h
View file

@ -72,7 +72,7 @@ protected:
virtual sort * find(sort * const * s) const; virtual sort * find(sort * const * s) const;
public: public:
virtual bool is_sort_wrapper() const { return false; } virtual bool is_sort_wrapper() const { return false; }
virtual sort * instantiate(pdecl_manager & m, sort * const * s) { return nullptr; } virtual sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) { return nullptr; }
// we use hash-consing for psorts. // we use hash-consing for psorts.
virtual char const * hcons_kind() const { UNREACHABLE(); return nullptr; } virtual char const * hcons_kind() const { UNREACHABLE(); return nullptr; }
virtual unsigned hcons_hash() const { UNREACHABLE(); return 0; } virtual unsigned hcons_hash() const { UNREACHABLE(); return 0; }
@ -194,7 +194,7 @@ class paccessor_decl : public pdecl {
size_t obj_size() const override { return sizeof(paccessor_decl); } size_t obj_size() const override { return sizeof(paccessor_decl); }
bool has_missing_refs(symbol & missing) const; bool has_missing_refs(symbol & missing) const;
bool fix_missing_refs(dictionary<int> const & symbol2idx, symbol & missing); bool fix_missing_refs(dictionary<int> const & symbol2idx, symbol & missing);
accessor_decl * instantiate_decl(pdecl_manager & m, sort * const * s); accessor_decl * instantiate_decl(pdecl_manager & m, unsigned n, sort * const * s);
symbol const & get_name() const { return m_name; } symbol const & get_name() const { return m_name; }
ptype const & get_type() const { return m_type; } ptype const & get_type() const { return m_type; }
~paccessor_decl() override {} ~paccessor_decl() override {}
@ -217,7 +217,7 @@ class pconstructor_decl : public pdecl {
bool fix_missing_refs(dictionary<int> const & symbol2idx, symbol & missing); bool fix_missing_refs(dictionary<int> const & symbol2idx, symbol & missing);
symbol const & get_name() const { return m_name; } symbol const & get_name() const { return m_name; }
symbol const & get_recognizer_name() const { return m_recogniser_name; } symbol const & get_recognizer_name() const { return m_recogniser_name; }
constructor_decl * instantiate_decl(pdecl_manager & m, sort * const * s); constructor_decl * instantiate_decl(pdecl_manager & m, unsigned n, sort * const * s);
~pconstructor_decl() override {} ~pconstructor_decl() override {}
public: public:
void display(std::ostream & out) const override { pdecl::display(out); } void display(std::ostream & out) const override { pdecl::display(out); }
@ -234,7 +234,7 @@ class pdatatype_decl : public psort_decl {
void finalize(pdecl_manager & m) override; void finalize(pdecl_manager & m) override;
size_t obj_size() const override { return sizeof(pdatatype_decl); } size_t obj_size() const override { return sizeof(pdatatype_decl); }
bool fix_missing_refs(dictionary<int> const & symbol2idx, symbol & missing); bool fix_missing_refs(dictionary<int> const & symbol2idx, symbol & missing);
datatype_decl * instantiate_decl(pdecl_manager & m, sort * const * s); datatype_decl * instantiate_decl(pdecl_manager & m, unsigned n, sort * const * s);
~pdatatype_decl() override {} ~pdatatype_decl() override {}
public: public:
sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override; sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override;