mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

merge

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-09-05 17:24:29 -07:00
parent 1f551f19f5
commit c708691a50
2 changed files with 10 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/ast/datatype_decl_plugin2.cpp
View file

@ -78,6 +78,7 @@ namespace datatype {
sort_ref def::instantiate(sort_ref_vector const& sorts) const {
sort_ref s(m);
TRACE("datatype", tout << "instantiate " << m_name << "\n";);
if (!m_sort) {
vector<parameter> ps;
ps.push_back(parameter(m_name));
@ -315,6 +316,7 @@ namespace datatype {
void plugin::end_def_block() {
ast_manager& m = *m_manager;
sort_ref_vector sorts(m);
for (symbol const& s : m_def_block) {
def const& d = *m_defs[s];
@ -332,7 +334,12 @@ namespace datatype {
if (!u().is_well_founded(sorts.size(), sorts.c_ptr())) {
m_manager->raise_exception("datatype is not well-founded");
}
u().compute_datatype_size_functions(m_def_block);
for (symbol const& s : m_def_block) {
sort_ref_vector ps(m);
m_defs[s]->instantiate(ps);
}
}
bool plugin::mk_datatypes(unsigned num_datatypes, def * const * datatypes, unsigned num_params, sort* const* sort_params, sort_ref_vector & new_sorts) {
@ -579,6 +586,8 @@ namespace datatype {
status st;
while (!todo.empty()) {
symbol s = todo.back();
TRACE("datatype", tout << "Sort size for " << s << "\n";);
if (already_found.find(s, st) && st == BLACK) {
todo.pop_back();
continue;

2
src/ast/datatype_decl_plugin2.h
View file

@ -227,7 +227,7 @@ namespace datatype {
sort_ref_vector const& params() const { return m_params; }
util& u() const { return m_util; }
param_size::size* sort_size() { return m_sort_size; }
void set_sort_size(param_size::size* p) { m_sort_size = p; p->inc_ref(); }
void set_sort_size(param_size::size* p) { m_sort_size = p; p->inc_ref(); m_sort = 0; }
};
namespace decl {