Skip to content

Commit

Permalink
#5952
Browse files Browse the repository at this point in the history
  • Loading branch information
@NikolajBjorner
NikolajBjorner committed Apr 8, 2022
1 parent babac78 commit 1346a16
Show file tree
Hide file tree
Showing 4 changed files with 54 additions and 24 deletions.
1 change: 1 addition & 0 deletions src/cmd_context/cmd_context.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1636,6 +1636,7 @@ void cmd_context::pop(unsigned n) {
restore_aux_pdecls(s.m_aux_pdecls_lim);
restore_assertions(s.m_assertions_lim);
restore_psort_inst(s.m_psort_inst_stack_lim);
m_dt_eh.get()->reset();
m_mcs.shrink(m_mcs.size() - n);
m_scopes.shrink(new_lvl);
if (!m_global_decls)
Expand Down
1 change: 1 addition & 0 deletions src/cmd_context/cmd_context.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -267,6 +267,7 @@ class cmd_context : public progress_callback, public tactic_manager, public ast_
cmd_context & m_owner;
datatype_util m_dt_util;
public:
void reset() { m_dt_util.reset(); }
dt_eh(cmd_context & owner);
~dt_eh() override;
void operator()(sort * dt, pdecl* pd) override;
Expand Down
59 changes: 42 additions & 17 deletions src/cmd_context/pdecl.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -156,8 +156,8 @@ class psort_sort : public psort {
return false;
return m_sort == static_cast<psort_sort const *>(other)->m_sort;
}
void display(std::ostream & out) const override {
out << m_sort->get_name();
std::ostream& display(std::ostream & out) const override {
return out << m_sort->get_name();
}
};

Expand All @@ -180,8 +180,8 @@ class psort_var : public psort {
get_num_params() == other->get_num_params() &&
m_idx == static_cast<psort_var const *>(other)->m_idx;
}
void display(std::ostream & out) const override {
out << "s_" << m_idx;
std::ostream& display(std::ostream & out) const override {
return out << "s_" << m_idx;
}
unsigned idx() const { return m_idx; }
};
Expand Down Expand Up @@ -254,7 +254,7 @@ class psort_app : public psort {
}
return true;
}
void display(std::ostream & out) const override {
std::ostream& display(std::ostream & out) const override {
if (m_args.empty()) {
out << m_decl->get_name();
}
Expand All @@ -267,6 +267,7 @@ class psort_app : public psort {
}
out << ")";
}
return out;
}
};

Expand Down Expand Up @@ -342,12 +343,12 @@ void display_sort_args(std::ostream & out, unsigned num_params) {
out << ") ";
}

void psort_user_decl::display(std::ostream & out) const {
std::ostream& psort_user_decl::display(std::ostream & out) const {
out << "(declare-sort " << m_name;
display_sort_args(out, m_num_params);
if (m_def)
m_def->display(out);
out << ")";
return out << ")";
}

// -------------------
Expand All @@ -364,8 +365,8 @@ sort * psort_dt_decl::instantiate(pdecl_manager & m, unsigned n, sort * const *
return m.instantiate_datatype(this, m_name, n, s);
}

void psort_dt_decl::display(std::ostream & out) const {
out << "(datatype-sort " << m_name << ")";
std::ostream& psort_dt_decl::display(std::ostream & out) const {
return out << "(datatype-sort " << m_name << ")";
}

// -------------------
Expand Down Expand Up @@ -410,8 +411,8 @@ sort * psort_builtin_decl::instantiate(pdecl_manager & m, unsigned n, unsigned c
}
}

void psort_builtin_decl::display(std::ostream & out) const {
out << "(declare-builtin-sort " << m_name << ")";
std::ostream& psort_builtin_decl::display(std::ostream & out) const {
return out << "(declare-builtin-sort " << m_name << ")";
}

void ptype::display(std::ostream & out, pdatatype_decl const * const * dts) const {
Expand Down Expand Up @@ -615,7 +616,7 @@ sort * pdatatype_decl::instantiate(pdecl_manager & m, unsigned n, sort * const *
}


void pdatatype_decl::display(std::ostream & out) const {
std::ostream& pdatatype_decl::display(std::ostream & out) const {
out << "(declare-datatype " << m_name;
display_sort_args(out, m_num_params);
bool first = true;
Expand All @@ -631,7 +632,7 @@ void pdatatype_decl::display(std::ostream & out) const {
}
first = false;
}
out << ")";
return out << ")";
}

bool pdatatype_decl::commit(pdecl_manager& m) {
Expand All @@ -645,9 +646,11 @@ bool pdatatype_decl::commit(pdecl_manager& m) {
datatype_decl * d_ptr = dts.m_buffer[0];
sort_ref_vector sorts(m.m());
bool is_ok = m.get_dt_plugin()->mk_datatypes(1, &d_ptr, m_num_params, ps.data(), sorts);
m.notify_mk_datatype(m_name);
if (is_ok && m_num_params == 0) {
m.notify_new_dt(sorts.get(0), this);
}

return is_ok;
}

Expand Down Expand Up @@ -722,6 +725,7 @@ void pdecl_manager::notify_datatype(sort *r, psort_decl* p, unsigned n, sort* co

void pdecl_manager::push() {
m_notified_lim.push_back(m_notified_trail.size());
m_datatypes_lim.push_back(m_datatypes_trail.size());
}

void pdecl_manager::pop(unsigned n) {
Expand All @@ -732,6 +736,16 @@ void pdecl_manager::pop(unsigned n) {
}
m_notified_trail.shrink(new_sz);
m_notified_lim.shrink(m_notified_lim.size() - n);

new_sz = m_datatypes_lim[m_datatypes_lim.size() - n];
if (new_sz != m_datatypes_trail.size()) {
datatype_util util(m());
for (unsigned i = m_datatypes_trail.size(); i-- > new_sz; )
util.plugin().remove(m_datatypes_trail[i]);
}
m_datatypes_trail.shrink(new_sz);
m_datatypes_lim.shrink(m_datatypes_lim.size() - n);

}

bool pdatatypes_decl::instantiate(pdecl_manager & m, sort * const * s) {
Expand All @@ -751,16 +765,24 @@ bool pdatatypes_decl::commit(pdecl_manager& m) {
sort_ref_vector sorts(m.m());
bool is_ok = m.get_dt_plugin()->mk_datatypes(m_datatypes.size(), dts.m_buffer.data(), 0, nullptr, sorts);
if (is_ok) {
for (pdatatype_decl* d : m_datatypes) {
m.notify_mk_datatype(d->get_name());
}
for (unsigned i = 0; i < m_datatypes.size(); ++i) {
pdatatype_decl* d = m_datatypes[i];
if (d->get_num_params() == 0) {
if (d->get_num_params() == 0)
m.notify_new_dt(sorts.get(i), this);
}
}
}

return is_ok;
}

void pdecl_manager::notify_mk_datatype(symbol const& name) {
m_datatypes_trail.push_back(name);
}


struct pdecl_manager::sort_info {
psort_decl * m_decl;

Expand Down Expand Up @@ -985,16 +1007,19 @@ void pdecl_manager::del_decl_core(pdecl * p) {
}

void pdecl_manager::del_decl(pdecl * p) {
TRACE("pdecl_manager", tout << "del psort "; p->display(tout); tout << "\n";);
TRACE("pdecl_manager", tout << "del psort "; p->display(tout); tout << "\n";);
if (p->is_psort()) {
psort * _p = static_cast<psort*>(p);
if (_p->is_sort_wrapper()) {
m_sort2psort.erase(static_cast<psort_sort*>(_p)->get_sort());
sort* s = static_cast<psort_sort*>(_p)->get_sort();
m_sort2psort.erase(s);
}
else {
m_table.erase(_p);
}

}

del_decl_core(p);
}

Expand Down
17 changes: 10 additions & 7 deletions src/cmd_context/pdecl.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -45,7 +45,7 @@ class pdecl {
unsigned get_id() const { return m_id; }
unsigned get_ref_count() const { return m_ref_count; }
unsigned hash() const { return m_id; }
virtual void display(std::ostream & out) const {}
virtual std::ostream& display(std::ostream & out) const { return out;}
virtual void reset_cache(pdecl_manager& m) {}
};

Expand Down Expand Up @@ -123,7 +123,7 @@ class psort_user_decl : public psort_decl {
~psort_user_decl() override {}
public:
sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override;
void display(std::ostream & out) const override;
std::ostream& display(std::ostream & out) const override;
};

class psort_builtin_decl : public psort_decl {
Expand All @@ -137,7 +137,7 @@ class psort_builtin_decl : public psort_decl {
public:
sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override;
sort * instantiate(pdecl_manager & m, unsigned n, unsigned const * s) override;
void display(std::ostream & out) const override;
std::ostream& display(std::ostream & out) const override;
};

class psort_dt_decl : public psort_decl {
Expand All @@ -148,7 +148,7 @@ class psort_dt_decl : public psort_decl {
~psort_dt_decl() override {}
public:
sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override;
void display(std::ostream & out) const override;
std::ostream& display(std::ostream & out) const override;
};


Expand Down Expand Up @@ -198,7 +198,7 @@ class paccessor_decl : public pdecl {
ptype const & get_type() const { return m_type; }
~paccessor_decl() override {}
public:
void display(std::ostream & out) const override { pdecl::display(out); }
std::ostream& display(std::ostream & out) const override { pdecl::display(out); return out; }
void display(std::ostream & out, pdatatype_decl const * const * dts) const;
};

Expand All @@ -219,7 +219,7 @@ class pconstructor_decl : public pdecl {
constructor_decl * instantiate_decl(pdecl_manager & m, unsigned n, sort * const * s);
~pconstructor_decl() override {}
public:
void display(std::ostream & out) const override { pdecl::display(out); }
std::ostream& display(std::ostream & out) const override { pdecl::display(out); return out; }
void display(std::ostream & out, pdatatype_decl const * const * dts) const;
};

Expand All @@ -237,7 +237,7 @@ class pdatatype_decl : public psort_decl {
~pdatatype_decl() override {}
public:
sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s) override;
void display(std::ostream & out) const override;
std::ostream& display(std::ostream & out) const override;
bool has_missing_refs(symbol & missing) const;
bool has_duplicate_accessors(symbol & repeated) const;
bool commit(pdecl_manager& m);
Expand Down Expand Up @@ -289,6 +289,8 @@ class pdecl_manager {
obj_hashtable<sort> m_notified;
ptr_vector<sort> m_notified_trail;
unsigned_vector m_notified_lim;
svector<symbol> m_datatypes_trail;
unsigned_vector m_datatypes_lim;

void init_list();
void del_decl_core(pdecl * p);
Expand Down Expand Up @@ -319,6 +321,7 @@ class pdecl_manager {
sort * instantiate_datatype(psort_decl* p, symbol const& name, unsigned n, sort * const* s);
sort * instantiate(psort * s, unsigned num, sort * const * args);
void notify_datatype(sort *r, psort_decl* p, unsigned n, sort* const* s);
void notify_mk_datatype(symbol const& name);
void push();
void pop(unsigned n);

Expand Down

0 comments on commit 1346a16

Please sign in to comment.