From 070c699ffcfd2c1ffe10ac40825de13cdb195cd9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 10 Sep 2017 15:32:53 +0300 Subject: [PATCH] remove V2 reference Signed-off-by: Nikolaj Bjorner --- src/ast/CMakeLists.txt | 1 - src/ast/ast_smt2_pp.cpp | 2 - src/ast/ast_smt_pp.cpp | 71 - src/ast/datatype_decl_plugin.cpp | 2003 ++++++++++++++--------------- src/ast/datatype_decl_plugin.h | 582 ++++++--- src/ast/datatype_decl_plugin2.cpp | 1077 ---------------- src/ast/datatype_decl_plugin2.h | 439 ------- src/cmd_context/pdecl.cpp | 62 - src/cmd_context/pdecl.h | 4 - src/parsers/smt2/smt2parser.cpp | 32 +- 10 files changed, 1377 insertions(+), 2896 deletions(-) delete mode 100644 src/ast/datatype_decl_plugin2.cpp delete mode 100644 src/ast/datatype_decl_plugin2.h diff --git a/src/ast/CMakeLists.txt b/src/ast/CMakeLists.txt index 47ed2def8..0a14d9473 100644 --- a/src/ast/CMakeLists.txt +++ b/src/ast/CMakeLists.txt @@ -14,7 +14,6 @@ z3_add_component(ast ast_util.cpp bv_decl_plugin.cpp datatype_decl_plugin.cpp - datatype_decl_plugin2.cpp decl_collector.cpp dl_decl_plugin.cpp expr2polynomial.cpp diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index c69cafc71..abb4ae959 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -434,7 +434,6 @@ format_ns::format * smt2_pp_environment::pp_sort(sort * s) { fs.push_back(pp_sort(to_sort(s->get_parameter(0).get_ast()))); return mk_seq1(m, fs.begin(), fs.end(), f2f(), get_sutil().is_seq(s)?"Seq":"RegEx"); } -#ifdef DATATYPE_V2 if (get_dtutil().is_datatype(s)) { unsigned sz = get_dtutil().get_datatype_num_parameter_sorts(s); if (sz > 0) { @@ -445,7 +444,6 @@ format_ns::format * smt2_pp_environment::pp_sort(sort * s) { return mk_seq1(m, fs.begin(), fs.end(), f2f(), s->get_name().str().c_str()); } } -#endif return format_ns::mk_string(get_manager(), s->get_name().str().c_str()); } diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp index 1c3b4aeb2..906fd054b 100644 --- a/src/ast/ast_smt_pp.cpp +++ b/src/ast/ast_smt_pp.cpp @@ -204,19 +204,13 @@ class smt_printer { void pp_decl(func_decl* d) { symbol sym = m_renaming.get_symbol(d->get_name()); if (d->get_family_id() == m_dt_fid) { -#ifdef DATATYPE_V2 - std::cout << "printing " << sym << "\n"; datatype_util util(m_manager); if (util.is_recognizer(d)) { - std::cout << d->get_num_parameters() << "\n"; visit_params(false, sym, d->get_num_parameters(), d->get_parameters()); } else { m_out << sym; } -#else - m_out << sym; -#endif } else if (m_manager.is_ite(d)) { m_out << "ite"; @@ -314,9 +308,6 @@ class smt_printer { sym = "Array"; } else if (s->is_sort_of(m_dt_fid, DATATYPE_SORT)) { -#ifndef DATATYPE_V2 - m_out << m_renaming.get_symbol(s->get_name()); -#else datatype_util util(m_manager); unsigned num_sorts = util.get_datatype_num_parameter_sorts(s); if (num_sorts > 0) { @@ -330,7 +321,6 @@ class smt_printer { } m_out << ")"; } -#endif return; } else { @@ -787,8 +777,6 @@ public: datatype_util util(m_manager); SASSERT(util.is_datatype(s)); -#ifdef DATATYPE_V2 - sort_ref_vector ps(m_manager); ptr_vector defs; util.get_defs(s, defs); @@ -839,65 +827,6 @@ public: m_out << ")"; } m_out << "))"; -#else - - ptr_vector rec_sorts; - - rec_sorts.push_back(s); - mark.mark(s, true); - - // collect siblings and sorts that have not already been printed. - for (unsigned h = 0; h < rec_sorts.size(); ++h) { - s = rec_sorts[h]; - ptr_vector const& decls = *util.get_datatype_constructors(s); - - for (unsigned i = 0; i < decls.size(); ++i) { - func_decl* f = decls[i]; - for (unsigned j = 0; j < f->get_arity(); ++j) { - sort* s2 = f->get_domain(j); - if (!mark.is_marked(s2)) { - if (m_manager.is_uninterp(s2)) { - pp_sort_decl(mark, s2); - } - else if (!util.is_datatype(s2)) { - // skip - } - else if (util.are_siblings(s, s2)) { - rec_sorts.push_back(s2); - mark.mark(s2, true); - } - else { - pp_sort_decl(mark, s2); - } - } - } - } - } - - m_out << "(declare-datatypes () ("; - bool first_sort = true; - for (sort * s : rec_sorts) { - if (!first_sort) m_out << " "; else first_sort = false; - - m_out << "("; - m_out << m_renaming.get_symbol(s->get_name()); - m_out << " "; - bool first_constr = true; - for (func_decl* f : *util.get_datatype_constructors(s)) { - if (!first_constr) m_out << " "; else first_constr = false; - m_out << "("; - m_out << m_renaming.get_symbol(f->get_name()); - for (func_decl* a : *util.get_constructor_accessors(f)) { - m_out << " (" << m_renaming.get_symbol(a->get_name()) << " "; - visit_sort(a->get_range()); - m_out << ")"; - } - m_out << ")"; - } - m_out << ")"; - } - m_out << "))"; -#endif newline(); } diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index 1090b3ff1..566487e60 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -1,5 +1,5 @@ /*++ -Copyright (c) 2006 Microsoft Corporation +Copyright (c) 2017 Microsoft Corporation Module Name: @@ -11,321 +11,703 @@ Abstract: Author: - Leonardo de Moura (leonardo) 2008-01-10. + Nikolaj Bjorner (nbjorner) 2017-9-1 Revision History: --*/ -#include "ast/datatype_decl_plugin.h" + #include "util/warning.h" +#include "ast/array_decl_plugin.h" +#include "ast/datatype_decl_plugin.h" #include "ast/ast_smt2_pp.h" +#include "ast/ast_translation.h" -#ifndef DATATYPE_V2 -/** - \brief Auxiliary class used to declare inductive datatypes. -*/ -class accessor_decl { - symbol m_name; - type_ref m_type; -public: - accessor_decl(const symbol & n, type_ref r):m_name(n), m_type(r) {} - symbol const & get_name() const { return m_name; } - type_ref const & get_type() const { return m_type; } -}; +namespace datatype { -accessor_decl * mk_accessor_decl(ast_manager& m, symbol const & n, type_ref const & t) { - return alloc(accessor_decl, n, t); -} - -void del_accessor_decl(accessor_decl * d) { - dealloc(d); -} - -void del_accessor_decls(unsigned num, accessor_decl * const * as) { - for (unsigned i = 0; i < num; i++) - del_accessor_decl(as[i]); -} - -/** - \brief Auxiliary class used to declare inductive datatypes. -*/ -class constructor_decl { - symbol m_name; - symbol m_recogniser_name; - ptr_vector m_accessors; -public: - constructor_decl(const symbol & n, const symbol & r, unsigned num_accessors, accessor_decl * const * accessors): - m_name(n), m_recogniser_name(r), m_accessors(num_accessors, accessors) {} - ~constructor_decl() { - std::for_each(m_accessors.begin(), m_accessors.end(), delete_proc()); - } - symbol const & get_name() const { return m_name; } - symbol const & get_recognizer_name() const { return m_recogniser_name; } - ptr_vector const & get_accessors() const { return m_accessors; } -}; - -constructor_decl * mk_constructor_decl(symbol const & n, symbol const & r, unsigned num_accessors, accessor_decl * const * accessors) { - return alloc(constructor_decl, n, r, num_accessors, accessors); -} - -void del_constructor_decl(constructor_decl * d) { - dealloc(d); -} - -void del_constructor_decls(unsigned num, constructor_decl * const * cs) { - for (unsigned i = 0; i < num; i++) - del_constructor_decl(cs[i]); -} - -/** - \brief Auxiliary class used to declare inductive datatypes. -*/ -class datatype_decl { - symbol m_name; - ptr_vector m_constructors; -public: - datatype_decl(const symbol & n, unsigned num_constructors, constructor_decl * const * constructors): - m_name(n), m_constructors(num_constructors, constructors) { - } - ~datatype_decl() { - std::for_each(m_constructors.begin(), m_constructors.end(), delete_proc()); - } - symbol const & get_name() const { return m_name; } - ptr_vector const & get_constructors() const { return m_constructors; } -}; - -datatype_decl * mk_datatype_decl(datatype_util&, symbol const & n, unsigned num_params, sort * const* params, unsigned num_constructors, constructor_decl * const * cs) { - return alloc(datatype_decl, n, num_constructors, cs); -} - -void del_datatype_decl(datatype_decl * d) { - dealloc(d); -} - -void del_datatype_decls(unsigned num, datatype_decl * const * ds) { - for (unsigned i = 0; i < num; i++) - del_datatype_decl(ds[i]); -} - -typedef buffer bool_buffer; - -struct invalid_datatype {}; - -static parameter const & read(unsigned num_parameters, parameter const * parameters, unsigned idx, bool_buffer & read_pos) { - if (idx >= num_parameters) { - throw invalid_datatype(); - } - if (idx >= read_pos.size()) { - read_pos.resize(idx+1, false); - } - read_pos[idx] = true; - return parameters[idx]; -} - -static int read_int(unsigned num_parameters, parameter const * parameters, unsigned idx, bool_buffer & read_pos) { - const parameter & r = read(num_parameters, parameters, idx, read_pos); - if (!r.is_int()) { - TRACE("datatype", tout << "expected integer parameter at position " << idx << " got: " << r << "\n";); - throw invalid_datatype(); - } - return r.get_int(); -} - -static symbol read_symbol(unsigned num_parameters, parameter const * parameters, unsigned idx, bool_buffer & read_pos) { - parameter const & r = read(num_parameters, parameters, idx, read_pos); - if (!r.is_symbol()) { - TRACE("datatype", tout << "expected symol parameter at position " << idx << " got: " << r << "\n";); - throw invalid_datatype(); - } - return r.get_symbol(); -} - -static sort* read_sort(unsigned num_parameters, parameter const * parameters, unsigned idx, bool_buffer & read_pos) { - parameter const & r = read(num_parameters, parameters, idx, read_pos); - if (!r.is_ast()) { - TRACE("datatype", tout << "expected ast parameter at position " << idx << " got: " << r << "\n";); - throw invalid_datatype(); - } - ast* a = r.get_ast(); - if (!is_sort(a)) { - throw invalid_datatype(); - } - return to_sort(a); -} - -enum status { - WHITE, - GRAY, - BLACK -}; - -/** - \brief Return true if the inductive datatype is recursive. - Pre-condition: The given argument constains the parameters of an inductive datatype. -*/ -static bool is_recursive_datatype(parameter const * parameters) { - unsigned num_types = parameters[0].get_int(); - unsigned top_tid = parameters[1].get_int(); - buffer already_found(num_types, WHITE); - buffer todo; - todo.push_back(top_tid); - while (!todo.empty()) { - unsigned tid = todo.back(); - if (already_found[tid] == BLACK) { - todo.pop_back(); - continue; + void accessor::fix_range(sort_ref_vector const& dts) { + if (!m_range) { + m_range = dts[m_index]; } - already_found[tid] = GRAY; - unsigned o = datatype_decl_plugin::constructor_offset(parameters, tid); // constructor offset - unsigned num_constructors = parameters[o].get_int(); - bool can_process = true; - for (unsigned s = 1; s <= num_constructors; s++) { - unsigned k_i = parameters[o + s].get_int(); - unsigned num_accessors = parameters[k_i + 2].get_int(); - for (unsigned r = 0; r < num_accessors; r++) { - parameter const & a_type = parameters[k_i + 4 + 2*r]; - if (a_type.is_int()) { - unsigned tid_prime = a_type.get_int(); - switch (already_found[tid_prime]) { - case WHITE: - todo.push_back(tid_prime); - can_process = false; - break; - case GRAY: - // type is recursive - return true; - case BLACK: - break; + } + + func_decl_ref accessor::instantiate(sort_ref_vector const& ps) const { + ast_manager& m = ps.get_manager(); + unsigned n = ps.size(); + SASSERT(m_range); + SASSERT(n == get_def().params().size()); + sort_ref range(m.substitute(m_range, n, get_def().params().c_ptr(), ps.c_ptr()), m); + sort_ref src(get_def().instantiate(ps)); + sort* srcs[1] = { src.get() }; + parameter pas[2] = { parameter(name()), parameter(get_constructor().name()) }; + return func_decl_ref(m.mk_func_decl(u().get_family_id(), OP_DT_ACCESSOR, 2, pas, 1, srcs, range), m); + } + + func_decl_ref accessor::instantiate(sort* dt) const { + sort_ref_vector sorts = get_def().u().datatype_params(dt); + return instantiate(sorts); + } + + def const& accessor::get_def() const { return m_constructor->get_def(); } + util& accessor::u() const { return m_constructor->u(); } + accessor* accessor::translate(ast_translation& tr) { + return alloc(accessor, tr.to(), name(), to_sort(tr(m_range.get()))); + } + + constructor::~constructor() { + for (accessor* a : m_accessors) dealloc(a); + m_accessors.reset(); + } + util& constructor::u() const { return m_def->u(); } + + func_decl_ref constructor::instantiate(sort_ref_vector const& ps) const { + ast_manager& m = ps.get_manager(); + sort_ref_vector domain(m); + for (accessor const* a : accessors()) { + domain.push_back(a->instantiate(ps)->get_range()); + } + sort_ref range = get_def().instantiate(ps); + parameter pas[1] = { parameter(name()) }; + return func_decl_ref(m.mk_func_decl(u().get_family_id(), OP_DT_CONSTRUCTOR, 1, pas, domain.size(), domain.c_ptr(), range), m); + } + + func_decl_ref constructor::instantiate(sort* dt) const { + sort_ref_vector sorts = get_def().u().datatype_params(dt); + return instantiate(sorts); + } + + constructor* constructor::translate(ast_translation& tr) { + constructor* result = alloc(constructor, m_name, m_recognizer); + for (accessor* a : *this) { + result->add(a->translate(tr)); + } + return result; + } + + + 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 ps; + ps.push_back(parameter(m_name)); + for (sort * s : m_params) ps.push_back(parameter(s)); + m_sort = m.mk_sort(u().get_family_id(), DATATYPE_SORT, ps.size(), ps.c_ptr()); + } + if (sorts.empty()) { + return m_sort; + } + return sort_ref(m.substitute(m_sort, sorts.size(), m_params.c_ptr(), sorts.c_ptr()), m); + } + + def* def::translate(ast_translation& tr, util& u) { + SASSERT(&u.get_manager() == &tr.to()); + sort_ref_vector ps(tr.to()); + for (sort* p : m_params) { + ps.push_back(to_sort(tr(p))); + } + def* result = alloc(def, tr.to(), u, m_name, m_class_id, ps.size(), ps.c_ptr()); + for (constructor* c : *this) { + result->add(c->translate(tr)); + } + if (m_sort) result->m_sort = to_sort(tr(m_sort.get())); + return result; + } + + enum status { + GRAY, + BLACK + }; + + namespace param_size { + 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_plus(size* a1, size* a2) { return alloc(plus, a1, a2); } + size* size::mk_times(size* a1, size* a2) { return alloc(times, a1, a2); } + size* size::mk_times(ptr_vector& szs) { + if (szs.empty()) return mk_offset(sort_size(1)); + if (szs.size() == 1) return szs[0]; + size* r = szs[0]; + for (unsigned i = 1; i < szs.size(); ++i) { + r = mk_times(r, szs[i]); + } + return r; + } + size* size::mk_plus(ptr_vector& szs) { + if (szs.empty()) return mk_offset(sort_size(0)); + if (szs.size() == 1) return szs[0]; + size* r = szs[0]; + for (unsigned i = 1; i < szs.size(); ++i) { + r = mk_plus(r, szs[i]); + } + return r; + } + size* size::mk_power(size* a1, size* a2) { return alloc(power, a1, a2); } + } + + namespace decl { + + plugin::~plugin() { + finalize(); + } + + void plugin::finalize() { + for (auto& kv : m_defs) { + dealloc(kv.m_value); + } + m_defs.reset(); + m_util = 0; // force deletion + } + + util & plugin::u() const { + SASSERT(m_manager); + SASSERT(m_family_id != null_family_id); + if (m_util.get() == 0) { + m_util = alloc(util, *m_manager); + } + return *(m_util.get()); + } + + void plugin::inherit(decl_plugin* other_p, ast_translation& tr) { + plugin* p = dynamic_cast(other_p); + svector names; + ptr_vector new_defs; + SASSERT(p); + for (auto& kv : p->m_defs) { + def* d = kv.m_value; + if (!m_defs.contains(kv.m_key)) { + names.push_back(kv.m_key); + new_defs.push_back(d->translate(tr, u())); + } + } + for (def* d : new_defs) + m_defs.insert(d->name(), d); + m_class_id = m_defs.size(); + u().compute_datatype_size_functions(names); + } + + + struct invalid_datatype {}; + + sort * plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) { + try { + if (k != DATATYPE_SORT) { + TRACE("datatype", tout << "invalid kind parameter to datatype\n";); + throw invalid_datatype(); + } + if (num_parameters < 1) { + TRACE("datatype", tout << "at least one parameter expected to datatype declaration\n";); + throw invalid_datatype(); + } + parameter const & name = parameters[0]; + if (!name.is_symbol()) { + TRACE("datatype", tout << "expected symol parameter at position " << 0 << " got: " << name << "\n";); + throw invalid_datatype(); + } + for (unsigned i = 1; i < num_parameters; ++i) { + parameter const& s = parameters[i]; + if (!s.is_ast() || !is_sort(s.get_ast())) { + TRACE("datatype", tout << "expected sort parameter at position " << i << " got: " << s << "\n";); + throw invalid_datatype(); + } + } + + sort* s = m_manager->mk_sort(name.get_symbol(), + sort_info(m_family_id, k, num_parameters, parameters, true)); + def* d = 0; + if (m_defs.find(s->get_name(), d) && d->sort_size()) { + obj_map S; + for (unsigned i = 0; i + 1 < num_parameters; ++i) { + sort* r = to_sort(parameters[i + 1].get_ast()); + S.insert(d->params()[i], r->get_num_elements()); + } + sort_size ts = d->sort_size()->eval(S); + TRACE("datatype", tout << name << " has size " << ts << "\n";); + s->set_num_elements(ts); + } + else { + TRACE("datatype", tout << "not setting size for " << name << "\n";); + } + return s; + } + catch (invalid_datatype) { + m_manager->raise_exception("invalid datatype"); + return 0; + } + } + + func_decl * plugin::mk_update_field( + unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) { + decl_kind k = OP_DT_UPDATE_FIELD; + ast_manager& m = *m_manager; + + if (num_parameters != 1 || !parameters[0].is_ast()) { + m.raise_exception("invalid parameters for datatype field update"); + return 0; + } + if (arity != 2) { + m.raise_exception("invalid number of arguments for datatype field update"); + return 0; + } + func_decl* acc = 0; + if (is_func_decl(parameters[0].get_ast())) { + acc = to_func_decl(parameters[0].get_ast()); + } + if (acc && !u().is_accessor(acc)) { + acc = 0; + } + if (!acc) { + m.raise_exception("datatype field update requires a datatype accessor as the second argument"); + return 0; + } + sort* dom = acc->get_domain(0); + sort* rng = acc->get_range(); + if (dom != domain[0]) { + m.raise_exception("first argument to field update should be a data-type"); + return 0; + } + if (rng != domain[1]) { + std::ostringstream buffer; + buffer << "second argument to field update should be " << mk_ismt2_pp(rng, m) + << " instead of " << mk_ismt2_pp(domain[1], m); + m.raise_exception(buffer.str().c_str()); + return 0; + } + range = domain[0]; + func_decl_info info(m_family_id, k, num_parameters, parameters); + return m.mk_func_decl(symbol("update-field"), arity, domain, range, info); + } + +#define VALIDATE_PARAM(_pred_) if (!(_pred_)) m_manager->raise_exception("invalid parameter to datatype function " #_pred_); + + func_decl * decl::plugin::mk_constructor(unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) { + ast_manager& m = *m_manager; + VALIDATE_PARAM(num_parameters == 1 && parameters[0].is_symbol() && range && u().is_datatype(range)); + // we blindly trust other conditions are met, including domain types. + symbol name = parameters[0].get_symbol(); + func_decl_info info(m_family_id, OP_DT_CONSTRUCTOR, num_parameters, parameters); + info.m_private_parameters = true; + return m.mk_func_decl(name, arity, domain, range, info); + } + + func_decl * decl::plugin::mk_recognizer(unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort *) { + ast_manager& m = *m_manager; + VALIDATE_PARAM(arity == 1 && num_parameters == 2 && parameters[1].is_symbol() && parameters[0].is_ast() && is_func_decl(parameters[0].get_ast())); + VALIDATE_PARAM(u().is_datatype(domain[0])); + // blindly trust that parameter is a constructor + sort* range = m_manager->mk_bool_sort(); + func_decl_info info(m_family_id, OP_DT_RECOGNISER, num_parameters, parameters); + info.m_private_parameters = true; + return m.mk_func_decl(symbol(parameters[1].get_symbol()), arity, domain, range, info); + } + + func_decl * decl::plugin::mk_is(unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort *) { + ast_manager& m = *m_manager; + VALIDATE_PARAM(arity == 1 && num_parameters == 1 && parameters[0].is_ast() && is_func_decl(parameters[0].get_ast())); + VALIDATE_PARAM(u().is_datatype(domain[0])); + // blindly trust that parameter is a constructor + sort* range = m_manager->mk_bool_sort(); + func_decl_info info(m_family_id, OP_DT_IS, num_parameters, parameters); + info.m_private_parameters = true; + return m.mk_func_decl(symbol("is"), arity, domain, range, info); + } + + func_decl * decl::plugin::mk_accessor(unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) + { + ast_manager& m = *m_manager; + VALIDATE_PARAM(arity == 1 && num_parameters == 2 && parameters[0].is_symbol() && parameters[1].is_symbol()); + VALIDATE_PARAM(u().is_datatype(domain[0])); + SASSERT(range); + func_decl_info info(m_family_id, OP_DT_ACCESSOR, num_parameters, parameters); + info.m_private_parameters = true; + symbol name = parameters[0].get_symbol(); + return m.mk_func_decl(name, arity, domain, range, info); + } + + func_decl * decl::plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) { + switch (k) { + case OP_DT_CONSTRUCTOR: + return mk_constructor(num_parameters, parameters, arity, domain, range); + case OP_DT_RECOGNISER: + return mk_recognizer(num_parameters, parameters, arity, domain, range); + case OP_DT_IS: + return mk_is(num_parameters, parameters, arity, domain, range); + case OP_DT_ACCESSOR: + return mk_accessor(num_parameters, parameters, arity, domain, range); + case OP_DT_UPDATE_FIELD: + return mk_update_field(num_parameters, parameters, arity, domain, range); + default: + m_manager->raise_exception("invalid datatype operator kind"); + return 0; + } + } + + def* plugin::mk(symbol const& name, unsigned n, sort * const * params) { + ast_manager& m = *m_manager; + return alloc(def, m, u(), name, m_class_id, n, params); + } + + + 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]; + sort_ref_vector ps(m); + sorts.push_back(d.instantiate(ps)); + } + for (symbol const& s : m_def_block) { + def& d = *m_defs[s]; + for (constructor* c : d) { + for (accessor* a : *c) { + a->fix_range(sorts); } } } - } - if (can_process) { - already_found[tid] = BLACK; - todo.pop_back(); - } - } - return false; -} + if (!u().is_well_founded(sorts.size(), sorts.c_ptr())) { + m_manager->raise_exception("datatype is not well-founded"); + } -/** - \brief Return the size of the inductive datatype. - Pre-condition: The given argument constains the parameters of an inductive datatype. -*/ -static sort_size get_datatype_size(parameter const * parameters) { - unsigned num_types = parameters[0].get_int(); - unsigned top_tid = parameters[1].get_int(); - buffer szs(num_types, sort_size()); - buffer already_found(num_types, WHITE); - buffer todo; - todo.push_back(top_tid); - while (!todo.empty()) { - unsigned tid = todo.back(); - if (already_found[tid] == BLACK) { - todo.pop_back(); - continue; - } - already_found[tid] = GRAY; - unsigned o = datatype_decl_plugin::constructor_offset(parameters, tid); - unsigned num_constructors = parameters[o].get_int(); - bool is_very_big = false; - bool can_process = true; - for (unsigned s = 1; s <= num_constructors; s++) { - unsigned k_i = parameters[o+s].get_int(); - unsigned num_accessors = parameters[k_i+2].get_int(); - for (unsigned r = 0; r < num_accessors; r++) { - parameter const & a_type = parameters[k_i+4 + 2*r]; - if (a_type.is_int()) { - int tid_prime = a_type.get_int(); - switch (already_found[tid_prime]) { - case WHITE: - todo.push_back(tid_prime); - can_process = false; - break; - case GRAY: - // type is recursive - return sort_size(); - case BLACK: - break; - } - } - else { - SASSERT(a_type.is_ast()); - sort * ty = to_sort(a_type.get_ast()); - if (ty->is_infinite()) { - // type is infinite - return sort_size(); - } - else if (ty->is_very_big()) { - is_very_big = true; - } - } + 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); } } - if (can_process) { - todo.pop_back(); - already_found[tid] = BLACK; - if (is_very_big) { - szs[tid] = sort_size::mk_very_big(); + + bool plugin::mk_datatypes(unsigned num_datatypes, def * const * datatypes, unsigned num_params, sort* const* sort_params, sort_ref_vector & new_sorts) { + begin_def_block(); + for (unsigned i = 0; i < num_datatypes; ++i) { + def* d = 0; + TRACE("datatype", tout << "declaring " << datatypes[i]->name() << "\n";); + if (m_defs.find(datatypes[i]->name(), d)) { + TRACE("datatype", tout << "delete previous version for " << datatypes[i]->name() << "\n";); + dealloc(d); + } + m_defs.insert(datatypes[i]->name(), datatypes[i]); + m_def_block.push_back(datatypes[i]->name()); + } + end_def_block(); + sort_ref_vector ps(*m_manager); + for (symbol const& s : m_def_block) { + new_sorts.push_back(m_defs[s]->instantiate(ps)); + } + return true; + } + + void plugin::remove(symbol const& s) { + def* d = 0; + if (m_defs.find(s, d)) dealloc(d); + m_defs.remove(s); + } + + bool plugin::is_value_visit(expr * arg, ptr_buffer & todo) const { + if (!is_app(arg)) + return false; + family_id fid = to_app(arg)->get_family_id(); + if (fid == m_family_id) { + if (!u().is_constructor(to_app(arg))) + return false; + if (to_app(arg)->get_num_args() == 0) + return true; + todo.push_back(to_app(arg)); + return true; } else { - // the type is not infinite nor the number of elements is infinite... - // computing the number of elements - rational num; - for (unsigned s = 1; s <= num_constructors; s++) { - unsigned k_i = parameters[o+s].get_int(); - unsigned num_accessors = parameters[k_i+2].get_int(); - rational c_num(1); - for (unsigned r = 0; r < num_accessors; r++) { - parameter const & a_type = parameters[k_i+4 + 2*r]; - if (a_type.is_int()) { - int tid_prime = a_type.get_int(); - SASSERT(!szs[tid_prime].is_infinite() && !szs[tid_prime].is_very_big()); - c_num *= rational(szs[tid_prime].size(),rational::ui64()); - } - else { - SASSERT(a_type.is_ast()); - sort * ty = to_sort(a_type.get_ast()); - SASSERT(!ty->is_infinite() && !ty->is_very_big()); - c_num *= rational(ty->get_num_elements().size(), rational::ui64()); - } - } - num += c_num; - } - szs[tid] = sort_size(num); + return m_manager->is_value(arg); + } + } + + bool plugin::is_value(app * e) const { + TRACE("dt_is_value", tout << "checking\n" << mk_ismt2_pp(e, *m_manager) << "\n";); + if (!u().is_constructor(e)) + return false; + if (e->get_num_args() == 0) + return true; + // REMARK: if the following check is too expensive, we should + // cache the values in the decl::plugin. + ptr_buffer todo; + // potentially expensive check for common sub-expressions. + for (expr* arg : *e) { + if (!is_value_visit(arg, todo)) { + TRACE("dt_is_value", tout << "not-value:\n" << mk_ismt2_pp(arg, *m_manager) << "\n";); + return false; + } + } + while (!todo.empty()) { + app * curr = todo.back(); + SASSERT(u().is_constructor(curr)); + todo.pop_back(); + for (expr* arg : *curr) { + if (!is_value_visit(arg, todo)) { + TRACE("dt_is_value", tout << "not-value:\n" << mk_ismt2_pp(arg, *m_manager) << "\n";); + return false; + } + } + } + return true; + } + + void plugin::get_op_names(svector & op_names, symbol const & logic) { + op_names.push_back(builtin_name("is", OP_DT_IS)); + if (logic == symbol::null) { + op_names.push_back(builtin_name("update-field", OP_DT_UPDATE_FIELD)); } } - } - return szs[top_tid]; -} -/** - \brief Return true if the inductive datatype is well-founded. - Pre-condition: The given argument constains the parameters of an inductive datatype. -*/ -static bool is_well_founded(parameter const * parameters) { - unsigned num_types = parameters[0].get_int(); - buffer well_founded(num_types, false); - unsigned num_well_founded = 0; - bool changed; - do { - changed = false; - for (unsigned tid = 0; tid < num_types; tid++) { - if (!well_founded[tid]) { - unsigned o = datatype_decl_plugin::constructor_offset(parameters, tid); // constructor offset - unsigned num_constructors = parameters[o].get_int(); - for (unsigned s = 1; s <= num_constructors; s++) { - unsigned k_i = parameters[o + s].get_int(); - unsigned num_accessors = parameters[k_i + 2].get_int(); - unsigned r = 0; - for (; r < num_accessors; r++) { - parameter const & a_type = parameters[k_i + 4 + 2*r]; - if (a_type.is_int() && !well_founded[a_type.get_int()]) { + expr * plugin::get_some_value(sort * s) { + SASSERT(u().is_datatype(s)); + func_decl * c = u().get_non_rec_constructor(s); + ptr_buffer args; + for (unsigned i = 0; i < c->get_arity(); i++) { + args.push_back(m_manager->get_some_value(c->get_domain(i))); + } + return m_manager->mk_app(c, args.size(), args.c_ptr()); + } + + bool plugin::is_fully_interp(sort * s) const { + return u().is_fully_interp(s); + } + } + + sort_ref_vector util::datatype_params(sort * s) const { + SASSERT(is_datatype(s)); + sort_ref_vector result(m); + for (unsigned i = 1; i < s->get_num_parameters(); ++i) { + result.push_back(to_sort(s->get_parameter(i).get_ast())); + } + return result; + } + + + bool util::is_fully_interp(sort * s) const { + SASSERT(is_datatype(s)); + bool fi = true; + return fi; + if (m_is_fully_interp.find(s, fi)) { + return fi; + } + unsigned sz = m_fully_interp_trail.size(); + m_is_fully_interp.insert(s, true); + def const& d = get_def(s); + bool is_interp = true; + m_fully_interp_trail.push_back(s); + for (constructor const* c : d) { + for (accessor const* a : *c) { + func_decl_ref ac = a->instantiate(s); + sort* r = ac->get_range(); + if (!m.is_fully_interp(r)) { + is_interp = false; + break; + } + } + if (!is_interp) break; + } + for (unsigned i = sz; i < m_fully_interp_trail.size(); ++i) { + m_is_fully_interp.remove(m_fully_interp_trail[i]); + } + m_fully_interp_trail.shrink(sz); + m_is_fully_interp.insert(s, is_interp); + m_asts.push_back(s); + return true; + } + + /** + \brief Return true if the inductive datatype is recursive. + */ + bool util::is_recursive_core(sort* s) const { + obj_map already_found; + ptr_vector todo, subsorts; + todo.push_back(s); + status st; + while (!todo.empty()) { + s = todo.back(); + if (already_found.find(s, st) && st == BLACK) { + todo.pop_back(); + continue; + } + already_found.insert(s, GRAY); + def const& d = get_def(s); + bool can_process = true; + for (constructor const* c : d) { + for (accessor const* a : *c) { + sort* d = a->range(); + // check if d is a datatype sort + subsorts.reset(); + get_subsorts(d, subsorts); + for (sort * s2 : subsorts) { + if (is_datatype(s2)) { + if (already_found.find(s2, st)) { + // type is recursive + if (st == GRAY) return true; + } + else { + todo.push_back(s2); + can_process = false; + } + } + } + } + } + if (can_process) { + already_found.insert(s, BLACK); + todo.pop_back(); + } + } + return false; + } + + unsigned util::get_datatype_num_parameter_sorts(sort * ty) { + SASSERT(ty->get_num_parameters() >= 1); + return ty->get_num_parameters() - 1; + } + + sort* util::get_datatype_parameter_sort(sort * ty, unsigned idx) { + SASSERT(idx < get_datatype_num_parameter_sorts(ty)); + return to_sort(ty->get_parameter(idx+1).get_ast()); + } + + param_size::size* util::get_sort_size(sort_ref_vector const& params, sort* s) { + if (params.empty()) { + return param_size::size::mk_offset(s->get_num_elements()); + } + if (is_datatype(s)) { + param_size::size* sz; + obj_map S; + unsigned n = get_datatype_num_parameter_sorts(s); + for (unsigned i = 0; i < n; ++i) { + sort* ps = get_datatype_parameter_sort(s, i); + sz = get_sort_size(params, ps); + sz->inc_ref(); + S.insert(ps, sz); + } + def & d = get_def(s->get_name()); + sz = d.sort_size()->subst(S); + for (auto & kv : S) { + kv.m_value->dec_ref(); + } + return sz; + } + array_util autil(m); + if (autil.is_array(s)) { + unsigned n = get_array_arity(s); + ptr_vector szs; + for (unsigned i = 0; i < n; ++i) { + szs.push_back(get_sort_size(params, get_array_domain(s, i))); + } + param_size::size* sz1 = param_size::size::mk_times(szs); + param_size::size* sz2 = get_sort_size(params, get_array_range(s)); + return param_size::size::mk_power(sz2, sz1); + } + for (sort* p : params) { + if (s == p) { + sort_ref sr(s, m); + return param_size::size::mk_param(sr); + } + } + return param_size::size::mk_offset(s->get_num_elements()); + } + + bool util::is_declared(sort* s) const { + return m_plugin->is_declared(s); + } + + void util::compute_datatype_size_functions(svector const& names) { + map already_found; + map szs; + + svector todo(names); + 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; + } + already_found.insert(s, GRAY); + bool is_infinite = false; + bool can_process = true; + def& d = get_def(s); + for (constructor const* c : d) { + for (accessor const* a : *c) { + sort* r = a->range(); + if (is_datatype(r)) { + symbol s2 = r->get_name(); + if (already_found.find(s2, st)) { + // type is infinite + if (st == GRAY) { + is_infinite = true; + } + } + else if (names.contains(s2)) { + todo.push_back(s2); + can_process = false; + } + } + } + } + if (!can_process) { + continue; + } + todo.pop_back(); + already_found.insert(s, BLACK); + if (is_infinite) { + d.set_sort_size(param_size::size::mk_offset(sort_size::mk_infinite())); + continue; + } + + ptr_vector s_add; + for (constructor const* c : d) { + ptr_vector s_mul; + for (accessor const* a : *c) { + s_mul.push_back(get_sort_size(d.params(), a->range())); + } + s_add.push_back(param_size::size::mk_times(s_mul)); + } + d.set_sort_size(param_size::size::mk_plus(s_add)); + } + } + + + /** + \brief Return true if the inductive datatype is well-founded. + Pre-condition: The given argument constains the parameters of an inductive datatype. + */ + bool util::is_well_founded(unsigned num_types, sort* const* sorts) { + buffer well_founded(num_types, false); + obj_map sort2id; + for (unsigned i = 0; i < num_types; ++i) { + sort2id.insert(sorts[i], i); + } + unsigned num_well_founded = 0, id = 0; + bool changed; + do { + changed = false; + for (unsigned tid = 0; tid < num_types; tid++) { + if (well_founded[tid]) { + continue; + } + sort* s = sorts[tid]; + def const& d = get_def(s); + for (constructor const* c : d) { + bool found_nonwf = false; + for (accessor const* a : *c) { + if (sort2id.find(a->range(), id) && !well_founded[id]) { + found_nonwf = true; break; } } - if (r == num_accessors) { + if (!found_nonwf) { changed = true; well_founded[tid] = true; num_well_founded++; @@ -333,759 +715,358 @@ static bool is_well_founded(parameter const * parameters) { } } } - } - } while(changed && num_well_founded < num_types); - unsigned tid = parameters[1].get_int(); - return well_founded[tid]; -} - -datatype_decl_plugin::~datatype_decl_plugin() { - SASSERT(m_util.get() == 0); -} - -void datatype_decl_plugin::finalize() { - m_util = 0; // force deletion -} - -datatype_util & datatype_decl_plugin::get_util() const { - SASSERT(m_manager); - if (m_util.get() == 0) { - m_util = alloc(datatype_util, *m_manager); + } + while(changed && num_well_founded < num_types); + return num_well_founded == num_types; } - return *(m_util.get()); -} - -sort * datatype_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) { - try { - if (k != DATATYPE_SORT) { - throw invalid_datatype(); - } - buffer found; - unsigned num_types = read_int(num_parameters, parameters, 0, found); - if (num_types == 0) { - throw invalid_datatype(); - } - unsigned tid = read_int(num_parameters, parameters, 1, found); - unsigned num_sort_params = read_int(num_parameters, parameters, 2, found); - for (unsigned j = 0; j < num_sort_params; ++j) { - read_sort(num_parameters, parameters, 3 + j, found); - } - unsigned c_offset = constructor_offset(parameters); - for (unsigned j = 0; j < num_types; j++) { - read_symbol(num_parameters, parameters, c_offset + 2*j, found); // type name - unsigned o = read_int(num_parameters, parameters, c_offset + 2*j + 1, found); - unsigned num_constructors = read_int(num_parameters, parameters, o, found); - if (num_constructors == 0) { - throw invalid_datatype(); + def const& util::get_def(sort* s) const { + return m_plugin->get_def(s); + } + + void util::get_subsorts(sort* s, ptr_vector& sorts) const { + sorts.push_back(s); + for (unsigned i = 0; i < s->get_num_parameters(); ++i) { + parameter const& p = s->get_parameter(i); + if (p.is_ast() && is_sort(p.get_ast())) { + get_subsorts(to_sort(p.get_ast()), sorts); } - for (unsigned s = 1; s <= num_constructors; s++) { - unsigned k_i = read_int(num_parameters, parameters, o + s, found); - read_symbol(num_parameters, parameters, k_i, found); // constructor name - read_symbol(num_parameters, parameters, k_i + 1, found); // recognizer name - unsigned num_accessors = read_int(num_parameters, parameters, k_i + 2, found); - unsigned first_accessor = k_i+3; - for (unsigned r = 0; r < num_accessors; r++) { - read_symbol(num_parameters, parameters, first_accessor + 2*r, found); // accessor name - parameter const & a_type = read(num_parameters, parameters, first_accessor + 2*r + 1, found); // accessort type - if (!a_type.is_int() && !a_type.is_ast()) { - throw invalid_datatype(); - } - if (a_type.is_ast() && !is_sort(a_type.get_ast())) { - throw invalid_datatype(); - } + } + } + + + util::util(ast_manager & m): + m(m), + m_family_id(m.mk_family_id("datatype")), + m_asts(m), + m_start(0) { + m_plugin = dynamic_cast(m.get_plugin(m_family_id)); + SASSERT(m_plugin); + } + + util::~util() { + std::for_each(m_vectors.begin(), m_vectors.end(), delete_proc >()); + } + + ptr_vector const * util::get_datatype_constructors(sort * ty) { + SASSERT(is_datatype(ty)); + ptr_vector * r = 0; + if (m_datatype2constructors.find(ty, r)) + return r; + r = alloc(ptr_vector); + m_asts.push_back(ty); + m_vectors.push_back(r); + m_datatype2constructors.insert(ty, r); + def const& d = get_def(ty); + for (constructor const* c : d) { + func_decl_ref f = c->instantiate(ty); + m_asts.push_back(f); + r->push_back(f); + } + return r; + } + + ptr_vector const * util::get_constructor_accessors(func_decl * con) { + SASSERT(is_constructor(con)); + ptr_vector * res = 0; + if (m_constructor2accessors.find(con, res)) { + return res; + } + res = alloc(ptr_vector); + m_asts.push_back(con); + m_vectors.push_back(res); + 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); } + break; } } - // check if there is no garbage - if (found.size() != num_parameters || std::find(found.begin(), found.end(), false) != found.end()) { - throw invalid_datatype(); - } + return res; + } - if (!is_well_founded(parameters)) { - m_manager->raise_exception("datatype is not well-founded"); - return 0; - } - - // compute datatype size - sort_size ts = get_datatype_size(parameters); - symbol const & tname = parameters[c_offset + 2*tid].get_symbol(); - return m_manager->mk_sort(tname, - sort_info(m_family_id, k, ts, num_parameters, parameters, true)); - } - catch (invalid_datatype) { - m_manager->raise_exception("invalid datatype"); - return 0; - } -} - -static sort * get_other_datatype(ast_manager & m, family_id datatype_fid, sort * source_datatype, unsigned tid) { - SASSERT(source_datatype->get_family_id() == datatype_fid); - SASSERT(source_datatype->get_decl_kind() == DATATYPE_SORT); - if (tid == static_cast(source_datatype->get_parameter(1).get_int())) { - return source_datatype; - } - buffer p; - unsigned n = source_datatype->get_num_parameters(); - for (unsigned i = 0; i < n; i++) { - p.push_back(source_datatype->get_parameter(i)); - } - p[1] = parameter(tid); - return m.mk_sort(datatype_fid, DATATYPE_SORT, n, p.c_ptr()); -} - -static sort * get_type(ast_manager & m, family_id datatype_fid, sort * source_datatype, parameter const & p) { - SASSERT(p.is_ast() || p.is_int()); - if (p.is_ast()) { - return to_sort(p.get_ast()); - } - else { - return get_other_datatype(m, datatype_fid, source_datatype, p.get_int()); - } -} - -func_decl * datatype_decl_plugin::mk_update_field( - unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range) { - decl_kind k = OP_DT_UPDATE_FIELD; - ast_manager& m = *m_manager; - - if (num_parameters != 1 || !parameters[0].is_ast()) { - m.raise_exception("invalid parameters for datatype field update"); - return 0; - } - if (arity != 2) { - m.raise_exception("invalid number of arguments for datatype field update"); - return 0; - } - func_decl* acc = 0; - if (is_func_decl(parameters[0].get_ast())) { - acc = to_func_decl(parameters[0].get_ast()); - } - if (acc && !get_util().is_accessor(acc)) { - acc = 0; - } - if (!acc) { - m.raise_exception("datatype field update requires a datatype accessor as the second argument"); - return 0; - } - sort* dom = acc->get_domain(0); - sort* rng = acc->get_range(); - if (dom != domain[0]) { - m.raise_exception("first argument to field update should be a data-type"); - return 0; - } - if (rng != domain[1]) { - std::ostringstream buffer; - buffer << "second argument to field update should be " << mk_ismt2_pp(rng, m) - << " instead of " << mk_ismt2_pp(domain[1], m); - m.raise_exception(buffer.str().c_str()); - return 0; - } - range = domain[0]; - func_decl_info info(m_family_id, k, num_parameters, parameters); - return m.mk_func_decl(symbol("update-field"), arity, domain, range, info); -} - -func_decl * datatype_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range) { - - if (k == OP_DT_UPDATE_FIELD) { - return mk_update_field(num_parameters, parameters, arity, domain, range); - } - if (num_parameters < 2 || !parameters[0].is_ast() || !is_sort(parameters[0].get_ast())) { - m_manager->raise_exception("invalid parameters for datatype operator"); - return 0; - } - sort * datatype = to_sort(parameters[0].get_ast()); - if (datatype->get_family_id() != m_family_id || - datatype->get_decl_kind() != DATATYPE_SORT) { - m_manager->raise_exception("invalid parameters for datatype operator"); - return 0; - } - for (unsigned i = 1; i < num_parameters; i++) { - if (!parameters[i].is_int()) { - m_manager->raise_exception("invalid parameters for datatype operator"); - return 0; - } - } - unsigned c_idx = parameters[1].get_int(); - unsigned tid = datatype->get_parameter(1).get_int(); - unsigned o = datatype_decl_plugin::constructor_offset(datatype, tid); - unsigned num_constructors = datatype->get_parameter(o).get_int(); - if (c_idx >= num_constructors) { - m_manager->raise_exception("invalid parameters for datatype operator"); - return 0; - } - unsigned k_i = datatype->get_parameter(o + 1 + c_idx).get_int(); - - switch (k) { - case OP_DT_CONSTRUCTOR: - if (num_parameters != 2) { - m_manager->raise_exception("invalid parameters for datatype constructor"); - return 0; - } - else { - symbol c_name = datatype->get_parameter(k_i).get_symbol(); - unsigned num_accessors = datatype->get_parameter(k_i + 2).get_int(); - if (num_accessors != arity) { - m_manager->raise_exception("invalid domain size for datatype constructor"); - return 0; + func_decl * util::get_constructor_recognizer(func_decl * con) { + SASSERT(is_constructor(con)); + func_decl * d = 0; + if (m_constructor2recognizer.find(con, d)) + return d; + sort * datatype = con->get_range(); + def const& dd = get_def(datatype); + symbol r; + for (constructor const* c : dd) { + if (c->name() == con->get_name()) { + r = c->recognizer(); } + } + parameter ps[2] = { parameter(con), parameter(r) }; + d = m.mk_func_decl(m_family_id, OP_DT_RECOGNISER, 2, ps, 1, &datatype); + SASSERT(d); + m_asts.push_back(con); + m_asts.push_back(d); + m_constructor2recognizer.insert(con, d); + return d; + } - // - // the reference count to domain could be 0. - // we need to ensure that creating a temporary - // copy of the same type causes a free. - // - sort_ref_vector domain_check(*m_manager); + func_decl * util::get_recognizer_constructor(func_decl * recognizer) const { + SASSERT(is_recognizer(recognizer)); + return to_func_decl(recognizer->get_parameter(0).get_ast()); + } - for (unsigned r = 0; r < num_accessors; r++) { - sort_ref ty(*m_manager); - ty = get_type(*m_manager, m_family_id, datatype, datatype->get_parameter(k_i + 4 + 2*r)); - domain_check.push_back(ty); - if (ty != domain[r]) { - m_manager->raise_exception("invalid domain for datatype constructor"); - return 0; + bool util::is_recursive(sort * ty) { + SASSERT(is_datatype(ty)); + bool r = false; + if (!m_is_recursive.find(ty, r)) { + r = is_recursive_core(ty); + m_is_recursive.insert(ty, r); + m_asts.push_back(ty); + } + return r; + } + + bool util::is_enum_sort(sort* s) { + if (!is_datatype(s)) { + return false; + } + bool r = false; + if (m_is_enum.find(s, r)) + return r; + ptr_vector 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); + return r; + } + + func_decl * util::get_accessor_constructor(func_decl * accessor) { + SASSERT(is_accessor(accessor)); + func_decl * r = 0; + if (m_accessor2constructor.find(accessor, r)) + return r; + sort * datatype = accessor->get_domain(0); + symbol c_id = accessor->get_parameter(1).get_symbol(); + def const& d = get_def(datatype); + func_decl_ref fn(m); + for (constructor const* c : d) { + if (c->name() == c_id) { + fn = c->instantiate(datatype); + break; + } + } + r = fn; + m_accessor2constructor.insert(accessor, r); + m_asts.push_back(accessor); + m_asts.push_back(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 >()); + m_vectors.reset(); + m_asts.reset(); + ++m_start; + } + + + /** + \brief Return a constructor mk(T_1, ... T_n) + where each T_i is not a datatype or it is a datatype that contains + a constructor that will not contain directly or indirectly an element of the given sort. + */ + func_decl * util::get_non_rec_constructor(sort * ty) { + SASSERT(is_datatype(ty)); + func_decl * r = 0; + if (m_datatype2nonrec_constructor.find(ty, r)) + return r; + r = 0; + ptr_vector forbidden_set; + forbidden_set.push_back(ty); + TRACE("util_bug", tout << "invoke get-non-rec: " << sort_ref(ty, m) << "\n";); + r = get_non_rec_constructor_core(ty, forbidden_set); + SASSERT(forbidden_set.back() == ty); + SASSERT(r); + m_asts.push_back(ty); + m_asts.push_back(r); + m_datatype2nonrec_constructor.insert(ty, r); + return r; + } + + /** + \brief Return a constructor mk(T_1, ..., T_n) where + 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 }) + */ + func_decl * util::get_non_rec_constructor_core(sort * ty, ptr_vector & 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 + // 2) each type T_i is not recursive or contains a constructor that does not depend on T + + ptr_vector const& constructors = *get_datatype_constructors(ty); + unsigned sz = constructors.size(); + TRACE("util_bug", tout << "get-non-rec constructor: " << sort_ref(ty, m) << "\n"; + tout << "forbidden: "; + for (sort* s : forbidden_set) tout << sort_ref(s, m) << " "; + tout << "\n"; + tout << "constructors: " << sz << "\n"; + for (func_decl* f : constructors) tout << func_decl_ref(f, m) << "\n"; + ); + // step 1) + unsigned start = ++m_start; + for (unsigned j = 0; j < sz; ++j) { + func_decl * c = constructors[(j + start) % sz]; + TRACE("util_bug", tout << "checking " << sort_ref(ty, m) << ": " << func_decl_ref(c, m) << "\n";); + unsigned num_args = c->get_arity(); + unsigned i = 0; + for (; i < num_args && !is_datatype(c->get_domain(i)); i++); + if (i == num_args) { + TRACE("util_bug", tout << "found non-rec " << func_decl_ref(c, m) << "\n";); + return c; + } + } + // step 2) + for (unsigned j = 0; j < sz; ++j) { + func_decl * c = constructors[(j + start) % sz]; + TRACE("util_bug", tout << "non_rec_constructor c: " << j << " " << func_decl_ref(c, m) << "\n";); + unsigned num_args = c->get_arity(); + unsigned i = 0; + for (; i < num_args; i++) { + sort * T_i = c->get_domain(i); + TRACE("util_bug", tout << "c: " << i << " " << sort_ref(T_i, m) << "\n";); + if (!is_datatype(T_i)) { + TRACE("util_bug", tout << sort_ref(T_i, m) << " is not a datatype\n";); + continue; } + if (std::find(forbidden_set.begin(), forbidden_set.end(), T_i) != forbidden_set.end()) { + TRACE("util_bug", tout << sort_ref(T_i, m) << " is in forbidden_set\n";); + break; + } + forbidden_set.push_back(T_i); + func_decl * nested_c = get_non_rec_constructor_core(T_i, forbidden_set); + SASSERT(forbidden_set.back() == T_i); + forbidden_set.pop_back(); + if (nested_c == 0) + break; + TRACE("util_bug", tout << "nested_c: " << nested_c->get_name() << "\n";); + } + if (i == num_args) + return c; + } + return 0; + } + unsigned util::get_constructor_idx(func_decl * f) const { + unsigned idx = 0; + def const& d = get_def(f->get_range()); + for (constructor* c : d) { + if (c->name() == f->get_name()) { + return idx; } - func_decl_info info(m_family_id, k, num_parameters, parameters); - info.m_private_parameters = true; - SASSERT(info.private_parameters()); - return m_manager->mk_func_decl(c_name, arity, domain, datatype, info); + ++idx; } - case OP_DT_RECOGNISER: - if (num_parameters != 2 || arity != 1 || domain[0] != datatype) { - m_manager->raise_exception("invalid parameters for datatype recogniser"); - return 0; - } - else { - symbol r_name = datatype->get_parameter(k_i + 1).get_symbol(); - sort * b = m_manager->mk_bool_sort(); - func_decl_info info(m_family_id, k, num_parameters, parameters); - info.m_private_parameters = true; - SASSERT(info.private_parameters()); - return m_manager->mk_func_decl(r_name, arity, domain, b, info); - } - case OP_DT_ACCESSOR: - if (num_parameters != 3 || arity != 1 || domain[0] != datatype) { - m_manager->raise_exception("invalid parameters for datatype accessor"); - return 0; - } - else { - unsigned a_idx = parameters[2].get_int(); - unsigned num_accessors = datatype->get_parameter(k_i + 2).get_int(); - if (a_idx >= num_accessors) { - m_manager->raise_exception("invalid datatype accessor"); - return 0; - } - symbol a_name = datatype->get_parameter(k_i + 3 + 2*a_idx).get_symbol(); - sort * a_type = get_type(*m_manager, m_family_id, datatype, datatype->get_parameter(k_i + 4 + 2*a_idx)); - func_decl_info info(m_family_id, k, num_parameters, parameters); - info.m_private_parameters = true; - SASSERT(info.private_parameters()); - return m_manager->mk_func_decl(a_name, arity, domain, a_type, info); - } - break; - case OP_DT_UPDATE_FIELD: UNREACHABLE(); return 0; - default: - m_manager->raise_exception("invalid datatype operator kind"); - return 0; } -} -bool datatype_decl_plugin::mk_datatypes(unsigned num_datatypes, datatype_decl * const * datatypes, unsigned num_params, sort* const* sort_params, sort_ref_vector & new_types) { - buffer p; - p.push_back(parameter(num_datatypes)); - p.push_back(parameter(-1)); - p.push_back(parameter(num_params)); - for (unsigned i = 0; i < num_params; ++i) { - p.push_back(parameter(sort_params[i])); + unsigned util::get_recognizer_constructor_idx(func_decl * f) const { + return get_constructor_idx(get_recognizer_constructor(f)); } - - unsigned c_offset = constructor_offset(p.c_ptr()); - for (unsigned i = 0; i < num_datatypes; i++) { - p.push_back(parameter(datatypes[i]->get_name())); - p.push_back(parameter(-1)); // offset is unknown at this point - } - for (unsigned i = 0; i < num_datatypes; i++) { - p[c_offset + 1 + 2*i] = parameter(p.size()); // save offset to constructor table - ptr_vector const & constructors = datatypes[i]->get_constructors(); - unsigned num_constructors = constructors.size(); - p.push_back(parameter(num_constructors)); - for (unsigned j = 0; j < num_constructors; j++) { - p.push_back(parameter(-1)); // offset is unknown at this point + + /** + \brief Two datatype sorts s1 and s2 are siblings if they were + defined together in the same mutually recursive definition. + */ + bool util::are_siblings(sort * s1, sort * s2) { + if (!is_datatype(s1) || !is_datatype(s2)) { + return s1 == s2; + } + else { + return get_def(s1).id() == get_def(s2).id(); } } - for (unsigned i = 0; i < num_datatypes; i++) { - unsigned o = constructor_offset(p.c_ptr(), i); - ptr_vector const & constructors = datatypes[i]->get_constructors(); - unsigned num_constructors = constructors.size(); - for (unsigned j = 0; j < num_constructors; j++) { - p[o+1+j] = parameter(p.size()); // save offset to constructor definition - constructor_decl * c = constructors[j]; - p.push_back(parameter(c->get_name())); - p.push_back(parameter(c->get_recognizer_name())); - ptr_vector const & accessors = c->get_accessors(); - unsigned num_accessors = accessors.size(); - p.push_back(parameter(num_accessors)); - for (unsigned k = 0; k < num_accessors; k++) { - accessor_decl * a = accessors[k]; - p.push_back(parameter(a->get_name())); - type_ref const & ty = a->get_type(); - if (ty.is_idx()) { - if (static_cast(ty.get_idx()) >= num_datatypes) { - TRACE("datatype", tout << "Index out of bounds: " << ty.get_idx() << "\n";); - return false; + + unsigned util::get_datatype_num_constructors(sort * ty) { + def const& d = get_def(ty->get_name()); + return d.constructors().size(); + } + + void util::get_defs(sort* s0, ptr_vector& defs) { + svector mark; + ptr_buffer todo; + todo.push_back(s0); + mark.push_back(s0->get_name()); + while (!todo.empty()) { + sort* s = todo.back(); + todo.pop_back(); + defs.push_back(&m_plugin->get_def(s->get_name())); + def const& d = get_def(s); + for (constructor* c : d) { + for (accessor* a : *c) { + sort* s = a->range(); + if (are_siblings(s0, s) && !mark.contains(s->get_name())) { + mark.push_back(s->get_name()); + todo.push_back(s); } - p.push_back(parameter(ty.get_idx())); - } - else { - p.push_back(parameter(ty.get_sort())); } } } } - for (unsigned i = 0; i < num_datatypes; i++) { - p[1] = parameter(i); - TRACE("datatype", tout << "new datatype parameters:\n"; - for (unsigned j = 0; j < p.size(); j++) { - tout << "p[" << j << "] -> " << p[j] << "\n"; - }); - sort * ty = mk_sort(DATATYPE_SORT, p.size(), p.c_ptr()); - if (ty == 0) { - TRACE("datatype", tout << "Failed to create datatype sort from parameters\n";); - return false; - } - new_types.push_back(ty); - } - return true; -} -expr * datatype_decl_plugin::get_some_value(sort * s) { - SASSERT(s->is_sort_of(m_family_id, DATATYPE_SORT)); - datatype_util & util = get_util(); - func_decl * c = util.get_non_rec_constructor(s); - ptr_buffer args; - for (unsigned i = 0; i < c->get_arity(); i++) { - args.push_back(m_manager->get_some_value(c->get_domain(i))); - } - return m_manager->mk_app(c, args.size(), args.c_ptr()); -} + void util::display_datatype(sort *s0, std::ostream& out) { + ast_mark mark; + ptr_buffer todo; + SASSERT(is_datatype(s0)); + out << s0->get_name() << " where\n"; + todo.push_back(s0); + mark.mark(s0, true); + while (!todo.empty()) { + sort* s = todo.back(); + todo.pop_back(); + out << s->get_name() << " =\n"; -bool datatype_decl_plugin::is_fully_interp(sort * s) const { - SASSERT(s->is_sort_of(m_family_id, DATATYPE_SORT)); - parameter const * parameters = s->get_parameters(); - unsigned num_types = parameters[0].get_int(); - for (unsigned tid = 0; tid < num_types; tid++) { - unsigned o = datatype_decl_plugin::constructor_offset(s, tid); - unsigned num_constructors = parameters[o].get_int(); - for (unsigned si = 1; si <= num_constructors; si++) { - unsigned k_i = parameters[o + si].get_int(); - unsigned num_accessors = parameters[k_i + 2].get_int(); - unsigned r = 0; - for (; r < num_accessors; r++) { - parameter const & a_type = parameters[k_i + 4 + 2*r]; - if (a_type.is_int()) - continue; - SASSERT(a_type.is_ast()); - sort * arg_s = to_sort(a_type.get_ast()); - if (!m_manager->is_fully_interp(arg_s)) - return false; - } - } - } - return true; -} - -bool datatype_decl_plugin::is_value_visit(expr * arg, ptr_buffer & todo) const { - if (!is_app(arg)) - return false; - family_id fid = to_app(arg)->get_family_id(); - if (fid == m_family_id) { - if (!get_util().is_constructor(to_app(arg))) - return false; - if (to_app(arg)->get_num_args() == 0) - return true; - todo.push_back(to_app(arg)); - return true; - } - else { - return m_manager->is_value(arg); - } -} - -unsigned datatype_decl_plugin::constructor_offset(sort const* s) { - return constructor_offset(s->get_parameters()); -} - -unsigned datatype_decl_plugin::constructor_offset(parameter const& p) { - return 3 + p.get_int(); -} - -unsigned datatype_decl_plugin::constructor_offset(parameter const* ps) { - return constructor_offset(ps[2]); -} - -unsigned datatype_decl_plugin::constructor_offset(sort const* s, unsigned tid) { - unsigned c_offset = constructor_offset(s->get_parameters()); - return s->get_parameter(c_offset + 1 + 2*tid).get_int(); -} - -unsigned datatype_decl_plugin::constructor_offset(parameter const* ps, unsigned tid) { - unsigned c_offset = constructor_offset(ps[2]); - return ps[c_offset + 1 + 2*tid].get_int(); -} - -bool datatype_decl_plugin::is_value(app * e) const { - TRACE("dt_is_value", tout << "checking\n" << mk_ismt2_pp(e, *m_manager) << "\n";); - if (!get_util().is_constructor(e)) - return false; - if (e->get_num_args() == 0) - return true; - // REMARK: if the following check is too expensive, we should - // cache the values in the datatype_decl_plugin. - ptr_buffer todo; - // potentially expensive check for common sub-expressions. - for (unsigned i = 0; i < e->get_num_args(); i++) { - if (!is_value_visit(e->get_arg(i), todo)) { - TRACE("dt_is_value", tout << "not-value:\n" << mk_ismt2_pp(e->get_arg(i), *m_manager) << "\n";); - return false; - } - } - while (!todo.empty()) { - app * curr = todo.back(); - SASSERT(get_util().is_constructor(curr)); - todo.pop_back(); - for (unsigned i = 0; i < curr->get_num_args(); i++) { - if (!is_value_visit(curr->get_arg(i), todo)) { - TRACE("dt_is_value", tout << "not-value:\n" << mk_ismt2_pp(curr->get_arg(i), *m_manager) << "\n";); - return false; - } - } - } - return true; -} - -void datatype_decl_plugin::get_op_names(svector & op_names, symbol const & logic) { - if (logic == symbol::null) { - op_names.push_back(builtin_name("update-field", OP_DT_UPDATE_FIELD)); - } -} - - -datatype_util::datatype_util(ast_manager & m): - m_manager(m), - m_family_id(m.mk_family_id("datatype")), - m_asts(m), - m_start(0) { -} - -datatype_util::~datatype_util() { - std::for_each(m_vectors.begin(), m_vectors.end(), delete_proc >()); -} - -func_decl * datatype_util::get_constructor(sort * ty, unsigned c_id) { - unsigned tid = ty->get_parameter(1).get_int(); - unsigned o = datatype_decl_plugin::constructor_offset(ty, tid); - unsigned k_i = ty->get_parameter(o + c_id + 1).get_int(); - unsigned num_accessors = ty->get_parameter(k_i + 2).get_int(); - parameter p[2] = { parameter(ty), parameter(c_id) }; - ptr_buffer domain; - for (unsigned r = 0; r < num_accessors; r++) { - domain.push_back(get_type(m_manager, m_family_id, ty, ty->get_parameter(k_i + 4 + 2*r))); - } - func_decl * d = m_manager.mk_func_decl(m_family_id, OP_DT_CONSTRUCTOR, 2, p, domain.size(), domain.c_ptr()); - SASSERT(d); - return d; -} - -ptr_vector const * datatype_util::get_datatype_constructors(sort * ty) { - SASSERT(is_datatype(ty)); - ptr_vector * r = 0; - if (m_datatype2constructors.find(ty, r)) - return r; - r = alloc(ptr_vector); - m_asts.push_back(ty); - m_vectors.push_back(r); - m_datatype2constructors.insert(ty, r); - unsigned tid = ty->get_parameter(1).get_int(); - unsigned o = datatype_decl_plugin::constructor_offset(ty, tid); - unsigned num_constructors = ty->get_parameter(o).get_int(); - for (unsigned c_id = 0; c_id < num_constructors; c_id++) { - func_decl * c = get_constructor(ty, c_id); - m_asts.push_back(c); - r->push_back(c); - } - return r; -} - -/** - \brief Return a constructor mk(T_1, ... T_n) - where each T_i is not a datatype or it is a datatype that contains - a constructor that will not contain directly or indirectly an element of the given sort. -*/ -func_decl * datatype_util::get_non_rec_constructor(sort * ty) { - SASSERT(is_datatype(ty)); - func_decl * r = 0; - if (m_datatype2nonrec_constructor.find(ty, r)) - return r; - r = 0; - ptr_vector forbidden_set; - forbidden_set.push_back(ty); - r = get_non_rec_constructor_core(ty, forbidden_set); - SASSERT(forbidden_set.back() == ty); - SASSERT(r); - m_asts.push_back(ty); - m_asts.push_back(r); - m_datatype2nonrec_constructor.insert(ty, r); - return r; -} - -/** - \brief Return a constructor mk(T_1, ..., T_n) where - 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 }) -*/ -func_decl * datatype_util::get_non_rec_constructor_core(sort * ty, ptr_vector & 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 - // 2) each type T_i is not recursive or contains a constructor that does not depend on T - ptr_vector const & constructors = *get_datatype_constructors(ty); - // step 1) - unsigned sz = constructors.size(); - unsigned start = ++m_start; - for (unsigned j = 0; j < sz; ++j) { - func_decl * c = constructors[(j + start) % sz]; - unsigned num_args = c->get_arity(); - unsigned i = 0; - for (; i < num_args && !is_datatype(c->get_domain(i)); i++) {}; - if (i == num_args) - return c; - } - // step 2) - for (unsigned j = 0; j < sz; ++j) { - func_decl * c = (*constructors)[(j + start) % sz]; - TRACE("datatype_util_bug", tout << "non_rec_constructor c: " << c->get_name() << "\n";); - unsigned num_args = c->get_arity(); - unsigned i = 0; - for (; i < num_args; i++) { - sort * T_i = c->get_domain(i); - TRACE("datatype_util_bug", tout << "c: " << c->get_name() << " i: " << i << " T_i: " << T_i->get_name() << "\n";); - if (!is_datatype(T_i)) { - TRACE("datatype_util_bug", tout << "T_i is not a datatype\n";); - continue; - } - if (std::find(forbidden_set.begin(), forbidden_set.end(), T_i) != forbidden_set.end()) { - TRACE("datatype_util_bug", tout << "T_i is in forbidden_set\n";); - break; - } - forbidden_set.push_back(T_i); - func_decl * nested_c = get_non_rec_constructor_core(T_i, forbidden_set); - SASSERT(forbidden_set.back() == T_i); - forbidden_set.pop_back(); - TRACE("datatype_util_bug", tout << "nested_c: " << nested_c->get_name() << "\n";); - if (nested_c == 0) - break; - } - if (i == num_args) - return c; - } - return 0; -} - -func_decl * datatype_util::get_constructor_recognizer(func_decl * constructor) { - SASSERT(is_constructor(constructor)); - func_decl * d = 0; - if (m_constructor2recognizer.find(constructor, d)) - return d; - sort * datatype = constructor->get_range(); - d = m_manager.mk_func_decl(m_family_id, OP_DT_RECOGNISER, 2, constructor->get_parameters(), 1, &datatype); - SASSERT(d); - m_asts.push_back(constructor); - m_asts.push_back(d); - m_constructor2recognizer.insert(constructor, d); - return d; -} - -ptr_vector const * datatype_util::get_constructor_accessors(func_decl * constructor) { - SASSERT(is_constructor(constructor)); - ptr_vector * res = 0; - if (m_constructor2accessors.find(constructor, res)) - return res; - res = alloc(ptr_vector); - m_asts.push_back(constructor); - m_vectors.push_back(res); - m_constructor2accessors.insert(constructor, res); - unsigned c_id = constructor->get_parameter(1).get_int(); - sort * datatype = constructor->get_range(); - unsigned tid = datatype->get_parameter(1).get_int(); - unsigned o = datatype_decl_plugin::constructor_offset(datatype, tid); - unsigned k_i = datatype->get_parameter(o + c_id + 1).get_int(); - unsigned num_accessors = datatype->get_parameter(k_i+2).get_int(); - parameter p[3] = { parameter(datatype), parameter(c_id), parameter(-1) }; - for (unsigned r = 0; r < num_accessors; r++) { - p[2] = parameter(r); - func_decl * d = m_manager.mk_func_decl(m_family_id, OP_DT_ACCESSOR, 3, p, 1, &datatype); - SASSERT(d); - m_asts.push_back(d); - res->push_back(d); - } - return res; -} - -func_decl * datatype_util::get_accessor_constructor(func_decl * accessor) { - SASSERT(is_accessor(accessor)); - func_decl * r = 0; - if (m_accessor2constructor.find(accessor, r)) - return r; - sort * datatype = to_sort(accessor->get_parameter(0).get_ast()); - unsigned c_id = accessor->get_parameter(1).get_int(); - r = get_constructor(datatype, c_id); - m_accessor2constructor.insert(accessor, r); - m_asts.push_back(accessor); - m_asts.push_back(r); - return r; -} - -func_decl * datatype_util::get_recognizer_constructor(func_decl * recognizer) { - SASSERT(is_recognizer(recognizer)); - func_decl * r = 0; - if (m_recognizer2constructor.find(recognizer, r)) - return r; - sort * datatype = to_sort(recognizer->get_parameter(0).get_ast()); - unsigned c_id = recognizer->get_parameter(1).get_int(); - r = get_constructor(datatype, c_id); - m_recognizer2constructor.insert(recognizer, r); - m_asts.push_back(recognizer); - m_asts.push_back(r); - return r; -} - -bool datatype_util::is_recursive(sort * ty) { - SASSERT(is_datatype(ty)); - bool r = false; - if (m_is_recursive.find(ty, r)) - return r; - r = is_recursive_datatype(ty->get_parameters()); - m_is_recursive.insert(ty, r); - m_asts.push_back(ty); - return r; -} - - -bool datatype_util::is_enum_sort(sort* s) { - if (!is_datatype(s)) { - return false; - } - bool r = false; - if (m_is_enum.find(s, r)) - return r; - ptr_vector 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); - return r; -} - - -void datatype_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 >()); - m_vectors.reset(); - m_asts.reset(); - ++m_start; -} - -/** - \brief Two datatype sorts s1 and s2 are siblings if they were - defined together in the same mutually recursive definition. -*/ -bool datatype_util::are_siblings(sort * s1, sort * s2) { - SASSERT(is_datatype(s1)); - SASSERT(is_datatype(s2)); - if (s1 == s2) - return true; - if (s1->get_num_parameters() != s2->get_num_parameters()) - return false; - unsigned num_params = s1->get_num_parameters(); - if (s1->get_parameter(0) != s2->get_parameter(0)) - return false; - // position 1 contains the IDX of the datatype in a mutually recursive definition. - for (unsigned i = 2; i < num_params; i++) { - if (s1->get_parameter(i) != s2->get_parameter(i)) - return false; - } - return true; -} - -void datatype_util::display_datatype(sort *s0, std::ostream& strm) { - ast_mark mark; - ptr_buffer todo; - SASSERT(is_datatype(s0)); - strm << s0->get_name() << " where\n"; - todo.push_back(s0); - mark.mark(s0, true); - while (!todo.empty()) { - sort* s = todo.back(); - todo.pop_back(); - strm << s->get_name() << " =\n"; - - ptr_vector const & cnstrs = *get_datatype_constructors(s); - for (unsigned i = 0; i < cnstrs.size(); ++i) { - func_decl* cns = cnstrs[i]; - func_decl* rec = get_constructor_recognizer(cns); - strm << " " << cns->get_name() << " :: " << rec->get_name() << " :: "; - ptr_vector const & accs = *get_constructor_accessors(cns); - for (unsigned j = 0; j < accs.size(); ++j) { - func_decl* acc = accs[j]; - sort* s1 = acc->get_range(); - strm << "(" << acc->get_name() << ": " << s1->get_name() << ") "; - if (is_datatype(s1) && are_siblings(s1, s0) && !mark.is_marked(s1)) { + ptr_vector const& cnstrs = *get_datatype_constructors(s); + for (unsigned i = 0; i < cnstrs.size(); ++i) { + func_decl* cns = cnstrs[i]; + func_decl* rec = get_constructor_recognizer(cns); + out << " " << cns->get_name() << " :: " << rec->get_name() << " :: "; + ptr_vector const & accs = *get_constructor_accessors(cns); + for (unsigned j = 0; j < accs.size(); ++j) { + func_decl* acc = accs[j]; + sort* s1 = acc->get_range(); + out << "(" << acc->get_name() << ": " << s1->get_name() << ") "; + if (is_datatype(s1) && are_siblings(s1, s0) && !mark.is_marked(s1)) { mark.mark(s1, true); todo.push_back(s1); - } + } + } + out << "\n"; } - strm << "\n"; } } - } -bool datatype_util::is_func_decl(datatype_op_kind k, unsigned num_params, parameter const* params, func_decl* f) { - bool eq = - f->get_decl_kind() == k && - f->get_family_id() == m_family_id && - f->get_num_parameters() == num_params; - for (unsigned i = 0; eq && i < num_params; ++i) { - eq = params[i] == f->get_parameter(i); +datatype_decl * mk_datatype_decl(datatype_util& u, symbol const & n, unsigned num_params, sort*const* params, unsigned num_constructors, constructor_decl * const * cs) { + datatype::decl::plugin* p = u.get_plugin(); + datatype::def* d = p->mk(n, num_params, params); + for (unsigned i = 0; i < num_constructors; ++i) { + d->add(cs[i]); } - return eq; + return d; } - -bool datatype_util::is_constructor_of(unsigned num_params, parameter const* params, func_decl* f) { - return - num_params == 2 && - m_family_id == f->get_family_id() && - OP_DT_CONSTRUCTOR == f->get_decl_kind() && - 2 == f->get_num_parameters() && - params[0] == f->get_parameter(0) && - params[1] == f->get_parameter(1); -} - - -#endif diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index 840329dda..515ca6e20 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -1,5 +1,5 @@ /*++ -Copyright (c) 2006 Microsoft Corporation +Copyright (c) 2017 Microsoft Corporation Module Name: @@ -11,55 +11,390 @@ Abstract: Author: - Leonardo de Moura (leonardo) 2008-01-09. + Nikolaj Bjorner (nbjorner) 2017-9-1 Revision History: ---*/ -#define DATATYPE_V2 -#ifdef DATATYPE_V2 -#include "ast/datatype_decl_plugin2.h" -#else + rewritten to support SMTLIB-2.6 parameters from + Leonardo de Moura (leonardo) 2008-01-09. +--*/ #ifndef DATATYPE_DECL_PLUGIN_H_ #define DATATYPE_DECL_PLUGIN_H_ - #include "ast/ast.h" -#include "util/tptr.h" #include "util/buffer.h" +#include "util/symbol_table.h" #include "util/obj_hashtable.h" -enum datatype_sort_kind { + +enum sort_kind { DATATYPE_SORT }; -enum datatype_op_kind { +enum op_kind { OP_DT_CONSTRUCTOR, OP_DT_RECOGNISER, - OP_DT_ACCESSOR, + OP_DT_IS, + OP_DT_ACCESSOR, OP_DT_UPDATE_FIELD, LAST_DT_OP }; -/** - \brief Auxiliary class used to declare inductive datatypes. - It may be a sort or an integer. If it is an integer, - then it represents a reference to a recursive type. +namespace datatype { - For example, consider the datatypes - Datatype - Tree = tree(value:Real, children:TreeList) - TreeList = cons_t(first_t:Tree, rest_t:Tree) - | nil_t - End - - The recursive occurrences of Tree and TreeList will have idx 0 and - 1 respectively. + class util; + class def; + class accessor; + class constructor; + + + class accessor { + symbol m_name; + sort_ref m_range; + unsigned m_index; // reference to recursive data-type may only get resolved after all mutually recursive data-types are procssed. + constructor* m_constructor; + public: + accessor(ast_manager& m, symbol const& n, sort* range): + m_name(n), + m_range(range, m), + m_index(UINT_MAX) + {} + accessor(ast_manager& m, symbol const& n, unsigned index): + m_name(n), + m_range(m), + m_index(index) + {} + sort* range() const { return m_range; } + void fix_range(sort_ref_vector const& dts); + symbol const& name() const { return m_name; } + func_decl_ref instantiate(sort_ref_vector const& ps) const; + func_decl_ref instantiate(sort* dt) const; + void attach(constructor* d) { m_constructor = d; } + constructor const& get_constructor() const { return *m_constructor; } + def const& get_def() const; + util& u() const; + accessor* translate(ast_translation& tr); + }; + + class constructor { + symbol m_name; + symbol m_recognizer; + ptr_vector m_accessors; + def* m_def; + public: + constructor(symbol n, symbol const& r): m_name(n), m_recognizer(r) {} + ~constructor(); + void add(accessor* a) { m_accessors.push_back(a); a->attach(this); } + symbol const& name() const { return m_name; } + symbol const& recognizer() const { return m_recognizer; } + ptr_vector const& accessors() const { return m_accessors; } + ptr_vector::const_iterator begin() const { return m_accessors.begin(); } + ptr_vector::const_iterator end() const { return m_accessors.end(); } + ptr_vector::iterator begin() { return m_accessors.begin(); } + ptr_vector::iterator end() { return m_accessors.end(); } + func_decl_ref instantiate(sort_ref_vector const& ps) const; + func_decl_ref instantiate(sort* dt) const; + void attach(def* d) { m_def = d; } + def const& get_def() const { return *m_def; } + util& u() const; + constructor* translate(ast_translation& tr); + }; + + namespace param_size { + class size { + unsigned m_ref; + public: + size(): m_ref(0) {} + virtual ~size() {} + void inc_ref() { ++m_ref; } + void dec_ref() { --m_ref; if (m_ref == 0) dealloc(this); } + static size* mk_offset(sort_size const& s); + static size* mk_param(sort_ref& p); + static size* mk_plus(size* a1, size* a2); + static size* mk_times(size* a1, size* a2); + static size* mk_plus(ptr_vector& szs); + static size* mk_times(ptr_vector& szs); + static size* mk_power(size* a1, size* a2); + + virtual size* subst(obj_map& S) = 0; + virtual sort_size eval(obj_map const& S) = 0; + + }; + struct offset : public size { + sort_size m_offset; + offset(sort_size const& s): m_offset(s) {} + virtual ~offset() {} + virtual size* subst(obj_map& S) { return this; } + virtual sort_size eval(obj_map const& S) { return m_offset; } + }; + struct plus : public size { + size* m_arg1, *m_arg2; + plus(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref();} + virtual ~plus() { m_arg1->dec_ref(); m_arg2->dec_ref(); } + virtual size* subst(obj_map& S) { return mk_plus(m_arg1->subst(S), m_arg2->subst(S)); } + virtual sort_size eval(obj_map const& S) { + sort_size s1 = m_arg1->eval(S); + sort_size s2 = m_arg2->eval(S); + if (s1.is_infinite()) return s1; + if (s2.is_infinite()) return s2; + if (s1.is_very_big()) return s1; + if (s2.is_very_big()) return s2; + rational r = rational(s1.size(), rational::ui64()) + rational(s2.size(), rational::ui64()); + return sort_size(r); + } + }; + struct times : public size { + size* m_arg1, *m_arg2; + times(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref(); } + virtual ~times() { m_arg1->dec_ref(); m_arg2->dec_ref(); } + virtual size* subst(obj_map& S) { return mk_times(m_arg1->subst(S), m_arg2->subst(S)); } + virtual sort_size eval(obj_map const& S) { + sort_size s1 = m_arg1->eval(S); + sort_size s2 = m_arg2->eval(S); + if (s1.is_infinite()) return s1; + if (s2.is_infinite()) return s2; + if (s1.is_very_big()) return s1; + if (s2.is_very_big()) return s2; + rational r = rational(s1.size(), rational::ui64()) * rational(s2.size(), rational::ui64()); + return sort_size(r); + } + }; + struct power : public size { + size* m_arg1, *m_arg2; + power(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref(); } + virtual ~power() { m_arg1->dec_ref(); m_arg2->dec_ref(); } + virtual size* subst(obj_map& S) { return mk_power(m_arg1->subst(S), m_arg2->subst(S)); } + virtual sort_size eval(obj_map const& S) { + sort_size s1 = m_arg1->eval(S); + sort_size s2 = m_arg2->eval(S); + // s1^s2 + if (s1.is_infinite()) return s1; + if (s2.is_infinite()) return s2; + if (s1.is_very_big()) return s1; + if (s2.is_very_big()) return s2; + if (s1.size() == 1) return s1; + if (s2.size() == 1) return s1; + if (s1.size() > (2 << 20) || s2.size() > 10) return sort_size::mk_very_big(); + rational r = ::power(rational(s1.size(), rational::ui64()), static_cast(s2.size())); + return sort_size(r); + } + }; + struct sparam : public size { + sort_ref m_param; + sparam(sort_ref& p): m_param(p) {} + virtual ~sparam() {} + virtual size* subst(obj_map& S) { return S[m_param]; } + virtual sort_size eval(obj_map const& S) { return S[m_param]; } + }; + }; + + class def { + ast_manager& m; + util& m_util; + symbol m_name; + unsigned m_class_id; + param_size::size* m_sort_size; + sort_ref_vector m_params; + mutable sort_ref m_sort; + ptr_vector m_constructors; + public: + def(ast_manager& m, util& u, symbol const& n, unsigned class_id, unsigned num_params, sort * const* params): + m(m), + m_util(u), + m_name(n), + m_class_id(class_id), + m_sort_size(0), + m_params(m, num_params, params), + m_sort(m) + {} + ~def() { + if (m_sort_size) m_sort_size->dec_ref(); + for (constructor* c : m_constructors) dealloc(c); + m_constructors.reset(); + } + void add(constructor* c) { + m_constructors.push_back(c); + c->attach(this); + } + symbol const& name() const { return m_name; } + unsigned id() const { return m_class_id; } + sort_ref instantiate(sort_ref_vector const& ps) const; + ptr_vector const& constructors() const { return m_constructors; } + ptr_vector::const_iterator begin() const { return m_constructors.begin(); } + ptr_vector::const_iterator end() const { return m_constructors.end(); } + ptr_vector::iterator begin() { return m_constructors.begin(); } + ptr_vector::iterator end() { return m_constructors.end(); } + 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(); m_sort = 0; } + def* translate(ast_translation& tr, util& u); + }; + + namespace decl { + + class plugin : public decl_plugin { + mutable scoped_ptr m_util; + map m_defs; + svector m_def_block; + unsigned m_class_id; + util & u() const; + + virtual void inherit(decl_plugin* other_p, ast_translation& tr); + + public: + plugin(): m_class_id(0) {} + virtual ~plugin(); + + virtual void finalize(); + + virtual decl_plugin * mk_fresh() { return alloc(plugin); } + + virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters); + + virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); + + virtual expr * get_some_value(sort * s); + + virtual bool is_fully_interp(sort * s) const; + + virtual bool is_value(app* e) const; + + virtual bool is_unique_value(app * e) const { return is_value(e); } + + virtual void get_op_names(svector & op_names, symbol const & logic); + + void begin_def_block() { m_class_id++; m_def_block.reset(); } + + void end_def_block(); + + def* mk(symbol const& name, unsigned n, sort * const * params); + + void remove(symbol const& d); + + bool mk_datatypes(unsigned num_datatypes, def * const * datatypes, unsigned num_params, sort* const* sort_params, sort_ref_vector & new_sorts); + + def const& get_def(sort* s) const { return *(m_defs[datatype_name(s)]); } + def& get_def(symbol const& s) { return *(m_defs[s]); } + bool is_declared(sort* s) const { return m_defs.contains(datatype_name(s)); } + private: + bool is_value_visit(expr * arg, ptr_buffer & todo) const; + + func_decl * mk_update_field( + unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); + + func_decl * mk_constructor( + unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); + + func_decl * mk_accessor( + unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); + + func_decl * mk_recognizer( + unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); + + func_decl * mk_is( + unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range); + + symbol datatype_name(sort * s) const { + //SASSERT(u().is_datatype(s)); + return s->get_parameter(0).get_symbol(); + } + + }; + } + + class util { + ast_manager & m; + family_id m_family_id; + mutable decl::plugin* m_plugin; + + + obj_map *> m_datatype2constructors; + obj_map m_datatype2nonrec_constructor; + obj_map *> m_constructor2accessors; + obj_map m_constructor2recognizer; + obj_map m_recognizer2constructor; + obj_map m_accessor2constructor; + obj_map m_is_recursive; + obj_map m_is_enum; + mutable obj_map m_is_fully_interp; + mutable ast_ref_vector m_asts; + ptr_vector > m_vectors; + unsigned m_start; + mutable ptr_vector m_fully_interp_trail; + + func_decl * get_non_rec_constructor_core(sort * ty, ptr_vector & forbidden_set); + + friend class decl::plugin; + + bool is_recursive_core(sort * s) const; + sort_size get_datatype_size(sort* s0); + void compute_datatype_size_functions(svector const& names); + param_size::size* get_sort_size(sort_ref_vector const& params, sort* s); + bool is_well_founded(unsigned num_types, sort* const* sorts); + def& get_def(symbol const& s) { return m_plugin->get_def(s); } + void get_subsorts(sort* s, ptr_vector& sorts) const; + + public: + util(ast_manager & m); + ~util(); + ast_manager & get_manager() const { return m; } + // sort * mk_datatype_sort(symbol const& name, unsigned n, sort* const* params); + bool is_datatype(sort const* s) const { return is_sort_of(s, m_family_id, DATATYPE_SORT); } + bool is_enum_sort(sort* s); + bool is_recursive(sort * ty); + bool is_constructor(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_CONSTRUCTOR); } + bool is_recognizer(func_decl * f) const { return is_recognizer0(f) || is_is(f); } + bool is_recognizer0(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_RECOGNISER); } + bool is_is(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_IS); } + bool is_accessor(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_ACCESSOR); } + bool is_update_field(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_UPDATE_FIELD); } + bool is_constructor(app * f) const { return is_app_of(f, m_family_id, OP_DT_CONSTRUCTOR); } + bool is_recognizer0(app * f) const { return is_app_of(f, m_family_id, OP_DT_RECOGNISER);} + bool is_is(app * f) const { return is_app_of(f, m_family_id, OP_DT_IS);} + bool is_recognizer(app * f) const { return is_recognizer0(f) || is_is(f); } + bool is_accessor(app * f) const { return is_app_of(f, m_family_id, OP_DT_ACCESSOR); } + bool is_update_field(app * f) const { return is_app_of(f, m_family_id, OP_DT_UPDATE_FIELD); } + ptr_vector const * get_datatype_constructors(sort * ty); + unsigned get_datatype_num_constructors(sort * ty); + unsigned get_datatype_num_parameter_sorts(sort * ty); + sort* get_datatype_parameter_sort(sort * ty, unsigned idx); + func_decl * get_non_rec_constructor(sort * ty); + func_decl * get_constructor_recognizer(func_decl * constructor); + ptr_vector const * get_constructor_accessors(func_decl * constructor); + func_decl * get_accessor_constructor(func_decl * accessor); + func_decl * get_recognizer_constructor(func_decl * recognizer) const; + family_id get_family_id() const { return m_family_id; } + bool are_siblings(sort * s1, sort * s2); + bool is_func_decl(op_kind k, unsigned num_params, parameter const* params, func_decl* f); + bool is_constructor_of(unsigned num_params, parameter const* params, func_decl* f); + void reset(); + bool is_declared(sort* s) const; + void display_datatype(sort *s, std::ostream& strm); + bool is_fully_interp(sort * s) const; + sort_ref_vector datatype_params(sort * s) const; + unsigned get_constructor_idx(func_decl * f) const; + unsigned get_recognizer_constructor_idx(func_decl * f) const; + decl::plugin* get_plugin() { return m_plugin; } + void get_defs(sort* s, ptr_vector& defs); + def const& get_def(sort* s) const; + }; + +}; + +typedef datatype::accessor accessor_decl; +typedef datatype::constructor constructor_decl; +typedef datatype::def datatype_decl; +typedef datatype::decl::plugin datatype_decl_plugin; +typedef datatype::util datatype_util; - This is a transient value, it is only used to declare a set of - recursive datatypes. -*/ class type_ref { void * m_data; public: @@ -73,178 +408,29 @@ public: int get_idx() const { return UNBOXINT(m_data); } }; -class accessor_decl; -class constructor_decl; -class datatype_decl; -class datatype_util; +inline accessor_decl * mk_accessor_decl(ast_manager& m, symbol const & n, type_ref const & t) { + if (t.is_idx()) { + return alloc(accessor_decl, m, n, t.get_idx()); + } + else { + return alloc(accessor_decl, m, n, t.get_sort()); + } +} + +inline constructor_decl * mk_constructor_decl(symbol const & n, symbol const & r, unsigned num_accessors, accessor_decl * * acs) { + constructor_decl* c = alloc(constructor_decl, n, r); + for (unsigned i = 0; i < num_accessors; ++i) { + c->add(acs[i]); + } + return c; +} + + -accessor_decl * mk_accessor_decl(ast_manager& m, symbol const & n, type_ref const & t); -// Remark: the constructor becomes the owner of the accessor_decls -constructor_decl * mk_constructor_decl(symbol const & n, symbol const & r, unsigned num_accessors, accessor_decl * const * acs); // Remark: the datatype becomes the owner of the constructor_decls -datatype_decl * mk_datatype_decl(datatype_util& u, symbol const & n, unsigned num_params, sort * const* params, unsigned num_constructors, constructor_decl * const * cs); -void del_datatype_decl(datatype_decl * d); -void del_datatype_decls(unsigned num, datatype_decl * const * ds); +datatype_decl * mk_datatype_decl(datatype_util& u, symbol const & n, unsigned num_params, sort*const* params, unsigned num_constructors, constructor_decl * const * cs); +inline void del_datatype_decl(datatype_decl * d) {} +inline void del_datatype_decls(unsigned num, datatype_decl * const * ds) {} -class datatype_decl_plugin : public decl_plugin { - mutable scoped_ptr m_util; - datatype_util & get_util() const; -public: - datatype_decl_plugin() {} - - virtual ~datatype_decl_plugin(); - virtual void finalize(); - - virtual decl_plugin * mk_fresh() { return alloc(datatype_decl_plugin); } - - - /** - Contract for sort: - parameters[0] - (int) n - number of recursive types. - parameters[1] - (int) i - index 0..n-1 of which type is defined. - - parameters[2] - (int) p - number of type parameters. - - for j = 0..p-1 - parameters[3 + j] - (sort) s - type parameter - - c_offset := 3 + p - for j in 0..n-1 - parameters[c_offset + 2*j] - (symbol) name of the type - parameters[c_offset + 2*j + 1] - (int) o - offset where the constructors are defined. - - for each offset o at parameters[2 + 2*j + 1] for some j in 0..n-1 - parameters[o] - (int) m - number of constructors - parameters[o+1] - (int) k_1 - offset for constructor definition - ... - parameters[o+m] - (int) k_m - offset for constructor definition - - for each offset k_i at parameters[o+s] for some s in 0..m-1 - parameters[k_i] - (symbol) name of the constructor - parameters[k_i+1] - (symbol) name of the recognizer - parameters[k_i+2] - (int) m' - number of accessors - parameters[k_i+3+2*r] - (symbol) name of the r accessor - parameters[k_i+3+2*r+1] - (int or type_ast) type of the accessor. If integer, then the value must be in [0..n-1], and it - represents an reference to the recursive type. - - The idea with the additional offsets is that - access to relevant constructors and types can be performed using - a few address calculations. - */ - virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters); - - /** - Contract for constructors - parameters[0] - (ast) datatype ast. - parmaeters[1] - (int) constructor idx. - Contract for accessors - parameters[0] - (ast) datatype ast. - parameters[1] - (int) constructor idx. - parameters[2] - (int) accessor idx. - Contract for tester - parameters[0] - (ast) datatype ast. - parameters[1] - (int) constructor idx. - */ - virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range); - - bool mk_datatypes(unsigned num_datatypes, datatype_decl * const * datatypes, unsigned num_params, sort* const* sort_params, sort_ref_vector & new_sorts); - - virtual expr * get_some_value(sort * s); - - virtual bool is_fully_interp(sort * s) const; - - virtual bool is_value(app* e) const; - - virtual bool is_unique_value(app * e) const { return is_value(e); } - - virtual void get_op_names(svector & op_names, symbol const & logic); - - static unsigned constructor_offset(sort const* s); - static unsigned constructor_offset(parameter const& p); - static unsigned constructor_offset(parameter const* ps); - - static unsigned constructor_offset(sort const* s, unsigned tid); - static unsigned constructor_offset(parameter const* ps, unsigned tid); - -private: - bool is_value_visit(expr * arg, ptr_buffer & todo) const; - - func_decl * mk_update_field( - unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range); -}; - -class datatype_util { - ast_manager & m_manager; - family_id m_family_id; - - func_decl * get_constructor(sort * ty, unsigned c_id) const; - - obj_map *> m_datatype2constructors; - obj_map m_datatype2nonrec_constructor; - obj_map *> m_constructor2accessors; - obj_map m_constructor2recognizer; - obj_map m_recognizer2constructor; - obj_map m_accessor2constructor; - obj_map m_is_recursive; - obj_map m_is_enum; - ast_ref_vector m_asts; - ptr_vector > m_vectors; - unsigned m_start; - - func_decl * get_non_rec_constructor_core(sort * ty, ptr_vector & forbidden_set); - func_decl * get_constructor(sort * ty, unsigned c_id); - -public: - datatype_util(ast_manager & m); - ~datatype_util(); - ast_manager & get_manager() const { return m_manager; } - bool is_datatype(sort * s) const { return is_sort_of(s, m_family_id, DATATYPE_SORT); } - bool is_enum_sort(sort* s); - - bool is_recursive(sort * ty); - bool is_constructor(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_CONSTRUCTOR); } - bool is_recognizer(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_RECOGNISER); } - bool is_accessor(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_ACCESSOR); } - bool is_update_field(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_UPDATE_FIELD); } - bool is_constructor(app * f) const { return is_app_of(f, m_family_id, OP_DT_CONSTRUCTOR); } - bool is_recognizer(app * f) const { return is_app_of(f, m_family_id, OP_DT_RECOGNISER); } - bool is_accessor(app * f) const { return is_app_of(f, m_family_id, OP_DT_ACCESSOR); } - bool is_update_field(app * f) const { return is_app_of(f, m_family_id, OP_DT_UPDATE_FIELD); } - ptr_vector const * get_datatype_constructors(sort * ty); - unsigned get_datatype_num_constructors(sort * ty) { - SASSERT(is_datatype(ty)); - unsigned tid = ty->get_parameter(1).get_int(); - unsigned o = datatype_decl_plugin::constructor_offset(ty, tid); - return ty->get_parameter(o).get_int(); - } - unsigned get_datatype_num_parameter_sorts(sort * ty) { - SASSERT(is_datatype(ty)); - return ty->get_parameter(2).get_int(); - } - sort* get_datatype_parameter_sort(sort * ty, unsigned idx) { - SASSERT(is_datatype(ty)); - SASSERT(idx < get_datatype_num_parameter_sorts(ty)); - return to_sort(ty->get_parameter(3 + idx).get_ast()); - } - unsigned get_constructor_idx(func_decl * f) const { SASSERT(is_constructor(f)); return f->get_parameter(1).get_int(); } - unsigned get_recognizer_constructor_idx(func_decl * f) const { SASSERT(is_recognizer(f)); return f->get_parameter(1).get_int(); } - func_decl * get_non_rec_constructor(sort * ty); - func_decl * get_constructor_recognizer(func_decl * constructor); - ptr_vector const * get_constructor_accessors(func_decl * constructor); - func_decl * get_accessor_constructor(func_decl * accessor); - func_decl * get_recognizer_constructor(func_decl * recognizer); - family_id get_family_id() const { return m_family_id; } - bool are_siblings(sort * s1, sort * s2); - bool is_func_decl(datatype_op_kind k, unsigned num_params, parameter const* params, func_decl* f); - bool is_constructor_of(unsigned num_params, parameter const* params, func_decl* f); - void reset(); - void display_datatype(sort *s, std::ostream& strm); - - -}; #endif /* DATATYPE_DECL_PLUGIN_H_ */ - -#endif /* DATATYPE_V2 */ diff --git a/src/ast/datatype_decl_plugin2.cpp b/src/ast/datatype_decl_plugin2.cpp deleted file mode 100644 index 743a08e98..000000000 --- a/src/ast/datatype_decl_plugin2.cpp +++ /dev/null @@ -1,1077 +0,0 @@ -/*++ -Copyright (c) 2017 Microsoft Corporation - -Module Name: - - datatype_decl_plugin.cpp - -Abstract: - - - -Author: - - Nikolaj Bjorner (nbjorner) 2017-9-1 - -Revision History: - ---*/ - -#include "ast/datatype_decl_plugin.h" - -#ifdef DATATYPE_V2 -#include "util/warning.h" -#include "ast/datatype_decl_plugin2.h" -#include "ast/array_decl_plugin.h" -#include "ast/ast_smt2_pp.h" -#include "ast/ast_translation.h" - - -namespace datatype { - - void accessor::fix_range(sort_ref_vector const& dts) { - if (!m_range) { - m_range = dts[m_index]; - } - } - - func_decl_ref accessor::instantiate(sort_ref_vector const& ps) const { - ast_manager& m = ps.get_manager(); - unsigned n = ps.size(); - SASSERT(m_range); - SASSERT(n == get_def().params().size()); - sort_ref range(m.substitute(m_range, n, get_def().params().c_ptr(), ps.c_ptr()), m); - sort_ref src(get_def().instantiate(ps)); - sort* srcs[1] = { src.get() }; - parameter pas[2] = { parameter(name()), parameter(get_constructor().name()) }; - return func_decl_ref(m.mk_func_decl(u().get_family_id(), OP_DT_ACCESSOR, 2, pas, 1, srcs, range), m); - } - - func_decl_ref accessor::instantiate(sort* dt) const { - sort_ref_vector sorts = get_def().u().datatype_params(dt); - return instantiate(sorts); - } - - def const& accessor::get_def() const { return m_constructor->get_def(); } - util& accessor::u() const { return m_constructor->u(); } - accessor* accessor::translate(ast_translation& tr) { - return alloc(accessor, tr.to(), name(), to_sort(tr(m_range.get()))); - } - - constructor::~constructor() { - for (accessor* a : m_accessors) dealloc(a); - m_accessors.reset(); - } - util& constructor::u() const { return m_def->u(); } - - func_decl_ref constructor::instantiate(sort_ref_vector const& ps) const { - ast_manager& m = ps.get_manager(); - sort_ref_vector domain(m); - for (accessor const* a : accessors()) { - domain.push_back(a->instantiate(ps)->get_range()); - } - sort_ref range = get_def().instantiate(ps); - parameter pas[1] = { parameter(name()) }; - return func_decl_ref(m.mk_func_decl(u().get_family_id(), OP_DT_CONSTRUCTOR, 1, pas, domain.size(), domain.c_ptr(), range), m); - } - - func_decl_ref constructor::instantiate(sort* dt) const { - sort_ref_vector sorts = get_def().u().datatype_params(dt); - return instantiate(sorts); - } - - constructor* constructor::translate(ast_translation& tr) { - constructor* result = alloc(constructor, m_name, m_recognizer); - for (accessor* a : *this) { - result->add(a->translate(tr)); - } - return result; - } - - - 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 ps; - ps.push_back(parameter(m_name)); - for (sort * s : m_params) ps.push_back(parameter(s)); - m_sort = m.mk_sort(u().get_family_id(), DATATYPE_SORT, ps.size(), ps.c_ptr()); - } - if (sorts.empty()) { - return m_sort; - } - return sort_ref(m.substitute(m_sort, sorts.size(), m_params.c_ptr(), sorts.c_ptr()), m); - } - - def* def::translate(ast_translation& tr, util& u) { - SASSERT(&u.get_manager() == &tr.to()); - sort_ref_vector ps(tr.to()); - for (sort* p : m_params) { - ps.push_back(to_sort(tr(p))); - } - def* result = alloc(def, tr.to(), u, m_name, m_class_id, ps.size(), ps.c_ptr()); - for (constructor* c : *this) { - result->add(c->translate(tr)); - } - if (m_sort) result->m_sort = to_sort(tr(m_sort.get())); - return result; - } - - enum status { - GRAY, - BLACK - }; - - namespace param_size { - 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_plus(size* a1, size* a2) { return alloc(plus, a1, a2); } - size* size::mk_times(size* a1, size* a2) { return alloc(times, a1, a2); } - size* size::mk_times(ptr_vector& szs) { - if (szs.empty()) return mk_offset(sort_size(1)); - if (szs.size() == 1) return szs[0]; - size* r = szs[0]; - for (unsigned i = 1; i < szs.size(); ++i) { - r = mk_times(r, szs[i]); - } - return r; - } - size* size::mk_plus(ptr_vector& szs) { - if (szs.empty()) return mk_offset(sort_size(0)); - if (szs.size() == 1) return szs[0]; - size* r = szs[0]; - for (unsigned i = 1; i < szs.size(); ++i) { - r = mk_plus(r, szs[i]); - } - return r; - } - size* size::mk_power(size* a1, size* a2) { return alloc(power, a1, a2); } - } - - namespace decl { - - plugin::~plugin() { - finalize(); - } - - void plugin::finalize() { - for (auto& kv : m_defs) { - dealloc(kv.m_value); - } - m_defs.reset(); - m_util = 0; // force deletion - } - - util & plugin::u() const { - SASSERT(m_manager); - SASSERT(m_family_id != null_family_id); - if (m_util.get() == 0) { - m_util = alloc(util, *m_manager); - } - return *(m_util.get()); - } - - void plugin::inherit(decl_plugin* other_p, ast_translation& tr) { - plugin* p = dynamic_cast(other_p); - svector names; - ptr_vector new_defs; - SASSERT(p); - for (auto& kv : p->m_defs) { - def* d = kv.m_value; - if (!m_defs.contains(kv.m_key)) { - names.push_back(kv.m_key); - new_defs.push_back(d->translate(tr, u())); - } - } - for (def* d : new_defs) - m_defs.insert(d->name(), d); - m_class_id = m_defs.size(); - u().compute_datatype_size_functions(names); - } - - - struct invalid_datatype {}; - - sort * plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) { - try { - if (k != DATATYPE_SORT) { - TRACE("datatype", tout << "invalid kind parameter to datatype\n";); - throw invalid_datatype(); - } - if (num_parameters < 1) { - TRACE("datatype", tout << "at least one parameter expected to datatype declaration\n";); - throw invalid_datatype(); - } - parameter const & name = parameters[0]; - if (!name.is_symbol()) { - TRACE("datatype", tout << "expected symol parameter at position " << 0 << " got: " << name << "\n";); - throw invalid_datatype(); - } - for (unsigned i = 1; i < num_parameters; ++i) { - parameter const& s = parameters[i]; - if (!s.is_ast() || !is_sort(s.get_ast())) { - TRACE("datatype", tout << "expected sort parameter at position " << i << " got: " << s << "\n";); - throw invalid_datatype(); - } - } - - sort* s = m_manager->mk_sort(name.get_symbol(), - sort_info(m_family_id, k, num_parameters, parameters, true)); - def* d = 0; - if (m_defs.find(s->get_name(), d) && d->sort_size()) { - obj_map S; - for (unsigned i = 0; i + 1 < num_parameters; ++i) { - sort* r = to_sort(parameters[i + 1].get_ast()); - S.insert(d->params()[i], r->get_num_elements()); - } - sort_size ts = d->sort_size()->eval(S); - TRACE("datatype", tout << name << " has size " << ts << "\n";); - s->set_num_elements(ts); - } - else { - TRACE("datatype", tout << "not setting size for " << name << "\n";); - } - return s; - } - catch (invalid_datatype) { - m_manager->raise_exception("invalid datatype"); - return 0; - } - } - - func_decl * plugin::mk_update_field( - unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range) { - decl_kind k = OP_DT_UPDATE_FIELD; - ast_manager& m = *m_manager; - - if (num_parameters != 1 || !parameters[0].is_ast()) { - m.raise_exception("invalid parameters for datatype field update"); - return 0; - } - if (arity != 2) { - m.raise_exception("invalid number of arguments for datatype field update"); - return 0; - } - func_decl* acc = 0; - if (is_func_decl(parameters[0].get_ast())) { - acc = to_func_decl(parameters[0].get_ast()); - } - if (acc && !u().is_accessor(acc)) { - acc = 0; - } - if (!acc) { - m.raise_exception("datatype field update requires a datatype accessor as the second argument"); - return 0; - } - sort* dom = acc->get_domain(0); - sort* rng = acc->get_range(); - if (dom != domain[0]) { - m.raise_exception("first argument to field update should be a data-type"); - return 0; - } - if (rng != domain[1]) { - std::ostringstream buffer; - buffer << "second argument to field update should be " << mk_ismt2_pp(rng, m) - << " instead of " << mk_ismt2_pp(domain[1], m); - m.raise_exception(buffer.str().c_str()); - return 0; - } - range = domain[0]; - func_decl_info info(m_family_id, k, num_parameters, parameters); - return m.mk_func_decl(symbol("update-field"), arity, domain, range, info); - } - -#define VALIDATE_PARAM(_pred_) if (!(_pred_)) m_manager->raise_exception("invalid parameter to datatype function " #_pred_); - - func_decl * decl::plugin::mk_constructor(unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range) { - ast_manager& m = *m_manager; - VALIDATE_PARAM(num_parameters == 1 && parameters[0].is_symbol() && range && u().is_datatype(range)); - // we blindly trust other conditions are met, including domain types. - symbol name = parameters[0].get_symbol(); - func_decl_info info(m_family_id, OP_DT_CONSTRUCTOR, num_parameters, parameters); - info.m_private_parameters = true; - return m.mk_func_decl(name, arity, domain, range, info); - } - - func_decl * decl::plugin::mk_recognizer(unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort *) { - ast_manager& m = *m_manager; - VALIDATE_PARAM(arity == 1 && num_parameters == 2 && parameters[1].is_symbol() && parameters[0].is_ast() && is_func_decl(parameters[0].get_ast())); - VALIDATE_PARAM(u().is_datatype(domain[0])); - // blindly trust that parameter is a constructor - sort* range = m_manager->mk_bool_sort(); - func_decl_info info(m_family_id, OP_DT_RECOGNISER, num_parameters, parameters); - info.m_private_parameters = true; - return m.mk_func_decl(symbol(parameters[1].get_symbol()), arity, domain, range, info); - } - - func_decl * decl::plugin::mk_is(unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort *) { - ast_manager& m = *m_manager; - VALIDATE_PARAM(arity == 1 && num_parameters == 1 && parameters[0].is_ast() && is_func_decl(parameters[0].get_ast())); - VALIDATE_PARAM(u().is_datatype(domain[0])); - // blindly trust that parameter is a constructor - sort* range = m_manager->mk_bool_sort(); - func_decl_info info(m_family_id, OP_DT_IS, num_parameters, parameters); - info.m_private_parameters = true; - return m.mk_func_decl(symbol("is"), arity, domain, range, info); - } - - func_decl * decl::plugin::mk_accessor(unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range) - { - ast_manager& m = *m_manager; - VALIDATE_PARAM(arity == 1 && num_parameters == 2 && parameters[0].is_symbol() && parameters[1].is_symbol()); - VALIDATE_PARAM(u().is_datatype(domain[0])); - SASSERT(range); - func_decl_info info(m_family_id, OP_DT_ACCESSOR, num_parameters, parameters); - info.m_private_parameters = true; - symbol name = parameters[0].get_symbol(); - return m.mk_func_decl(name, arity, domain, range, info); - } - - func_decl * decl::plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range) { - switch (k) { - case OP_DT_CONSTRUCTOR: - return mk_constructor(num_parameters, parameters, arity, domain, range); - case OP_DT_RECOGNISER: - return mk_recognizer(num_parameters, parameters, arity, domain, range); - case OP_DT_IS: - return mk_is(num_parameters, parameters, arity, domain, range); - case OP_DT_ACCESSOR: - return mk_accessor(num_parameters, parameters, arity, domain, range); - case OP_DT_UPDATE_FIELD: - return mk_update_field(num_parameters, parameters, arity, domain, range); - default: - m_manager->raise_exception("invalid datatype operator kind"); - return 0; - } - } - - def* plugin::mk(symbol const& name, unsigned n, sort * const * params) { - ast_manager& m = *m_manager; - return alloc(def, m, u(), name, m_class_id, n, params); - } - - - 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]; - sort_ref_vector ps(m); - sorts.push_back(d.instantiate(ps)); - } - for (symbol const& s : m_def_block) { - def& d = *m_defs[s]; - for (constructor* c : d) { - for (accessor* a : *c) { - a->fix_range(sorts); - } - } - } - 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) { - begin_def_block(); - for (unsigned i = 0; i < num_datatypes; ++i) { - def* d = 0; - TRACE("datatype", tout << "declaring " << datatypes[i]->name() << "\n";); - if (m_defs.find(datatypes[i]->name(), d)) { - TRACE("datatype", tout << "delete previous version for " << datatypes[i]->name() << "\n";); - dealloc(d); - } - m_defs.insert(datatypes[i]->name(), datatypes[i]); - m_def_block.push_back(datatypes[i]->name()); - } - end_def_block(); - sort_ref_vector ps(*m_manager); - for (symbol const& s : m_def_block) { - new_sorts.push_back(m_defs[s]->instantiate(ps)); - } - return true; - } - - void plugin::remove(symbol const& s) { - def* d = 0; - if (m_defs.find(s, d)) dealloc(d); - m_defs.remove(s); - } - - bool plugin::is_value_visit(expr * arg, ptr_buffer & todo) const { - if (!is_app(arg)) - return false; - family_id fid = to_app(arg)->get_family_id(); - if (fid == m_family_id) { - if (!u().is_constructor(to_app(arg))) - return false; - if (to_app(arg)->get_num_args() == 0) - return true; - todo.push_back(to_app(arg)); - return true; - } - else { - return m_manager->is_value(arg); - } - } - - bool plugin::is_value(app * e) const { - TRACE("dt_is_value", tout << "checking\n" << mk_ismt2_pp(e, *m_manager) << "\n";); - if (!u().is_constructor(e)) - return false; - if (e->get_num_args() == 0) - return true; - // REMARK: if the following check is too expensive, we should - // cache the values in the decl::plugin. - ptr_buffer todo; - // potentially expensive check for common sub-expressions. - for (expr* arg : *e) { - if (!is_value_visit(arg, todo)) { - TRACE("dt_is_value", tout << "not-value:\n" << mk_ismt2_pp(arg, *m_manager) << "\n";); - return false; - } - } - while (!todo.empty()) { - app * curr = todo.back(); - SASSERT(u().is_constructor(curr)); - todo.pop_back(); - for (expr* arg : *curr) { - if (!is_value_visit(arg, todo)) { - TRACE("dt_is_value", tout << "not-value:\n" << mk_ismt2_pp(arg, *m_manager) << "\n";); - return false; - } - } - } - return true; - } - - void plugin::get_op_names(svector & op_names, symbol const & logic) { - op_names.push_back(builtin_name("is", OP_DT_IS)); - if (logic == symbol::null) { - op_names.push_back(builtin_name("update-field", OP_DT_UPDATE_FIELD)); - } - } - - expr * plugin::get_some_value(sort * s) { - SASSERT(u().is_datatype(s)); - func_decl * c = u().get_non_rec_constructor(s); - ptr_buffer args; - for (unsigned i = 0; i < c->get_arity(); i++) { - args.push_back(m_manager->get_some_value(c->get_domain(i))); - } - return m_manager->mk_app(c, args.size(), args.c_ptr()); - } - - bool plugin::is_fully_interp(sort * s) const { - return u().is_fully_interp(s); - } - } - - sort_ref_vector util::datatype_params(sort * s) const { - SASSERT(is_datatype(s)); - sort_ref_vector result(m); - for (unsigned i = 1; i < s->get_num_parameters(); ++i) { - result.push_back(to_sort(s->get_parameter(i).get_ast())); - } - return result; - } - - - bool util::is_fully_interp(sort * s) const { - SASSERT(is_datatype(s)); - bool fi = true; - return fi; - if (m_is_fully_interp.find(s, fi)) { - return fi; - } - unsigned sz = m_fully_interp_trail.size(); - m_is_fully_interp.insert(s, true); - def const& d = get_def(s); - bool is_interp = true; - m_fully_interp_trail.push_back(s); - for (constructor const* c : d) { - for (accessor const* a : *c) { - func_decl_ref ac = a->instantiate(s); - sort* r = ac->get_range(); - if (!m.is_fully_interp(r)) { - is_interp = false; - break; - } - } - if (!is_interp) break; - } - for (unsigned i = sz; i < m_fully_interp_trail.size(); ++i) { - m_is_fully_interp.remove(m_fully_interp_trail[i]); - } - m_fully_interp_trail.shrink(sz); - m_is_fully_interp.insert(s, is_interp); - m_asts.push_back(s); - return true; - } - - /** - \brief Return true if the inductive datatype is recursive. - */ - bool util::is_recursive_core(sort* s) const { - obj_map already_found; - ptr_vector todo, subsorts; - todo.push_back(s); - status st; - while (!todo.empty()) { - s = todo.back(); - if (already_found.find(s, st) && st == BLACK) { - todo.pop_back(); - continue; - } - already_found.insert(s, GRAY); - def const& d = get_def(s); - bool can_process = true; - for (constructor const* c : d) { - for (accessor const* a : *c) { - sort* d = a->range(); - // check if d is a datatype sort - subsorts.reset(); - get_subsorts(d, subsorts); - for (sort * s2 : subsorts) { - if (is_datatype(s2)) { - if (already_found.find(s2, st)) { - // type is recursive - if (st == GRAY) return true; - } - else { - todo.push_back(s2); - can_process = false; - } - } - } - } - } - if (can_process) { - already_found.insert(s, BLACK); - todo.pop_back(); - } - } - return false; - } - - unsigned util::get_datatype_num_parameter_sorts(sort * ty) { - SASSERT(ty->get_num_parameters() >= 1); - return ty->get_num_parameters() - 1; - } - - sort* util::get_datatype_parameter_sort(sort * ty, unsigned idx) { - SASSERT(idx < get_datatype_num_parameter_sorts(ty)); - return to_sort(ty->get_parameter(idx+1).get_ast()); - } - - param_size::size* util::get_sort_size(sort_ref_vector const& params, sort* s) { - if (params.empty()) { - return param_size::size::mk_offset(s->get_num_elements()); - } - if (is_datatype(s)) { - param_size::size* sz; - obj_map S; - unsigned n = get_datatype_num_parameter_sorts(s); - for (unsigned i = 0; i < n; ++i) { - sort* ps = get_datatype_parameter_sort(s, i); - sz = get_sort_size(params, ps); - sz->inc_ref(); - S.insert(ps, sz); - } - def & d = get_def(s->get_name()); - sz = d.sort_size()->subst(S); - for (auto & kv : S) { - kv.m_value->dec_ref(); - } - return sz; - } - array_util autil(m); - if (autil.is_array(s)) { - unsigned n = get_array_arity(s); - ptr_vector szs; - for (unsigned i = 0; i < n; ++i) { - szs.push_back(get_sort_size(params, get_array_domain(s, i))); - } - param_size::size* sz1 = param_size::size::mk_times(szs); - param_size::size* sz2 = get_sort_size(params, get_array_range(s)); - return param_size::size::mk_power(sz2, sz1); - } - for (sort* p : params) { - if (s == p) { - sort_ref sr(s, m); - return param_size::size::mk_param(sr); - } - } - return param_size::size::mk_offset(s->get_num_elements()); - } - - bool util::is_declared(sort* s) const { - return m_plugin->is_declared(s); - } - - void util::compute_datatype_size_functions(svector const& names) { - map already_found; - map szs; - - svector todo(names); - 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; - } - already_found.insert(s, GRAY); - bool is_infinite = false; - bool can_process = true; - def& d = get_def(s); - for (constructor const* c : d) { - for (accessor const* a : *c) { - sort* r = a->range(); - if (is_datatype(r)) { - symbol s2 = r->get_name(); - if (already_found.find(s2, st)) { - // type is infinite - if (st == GRAY) { - is_infinite = true; - } - } - else if (names.contains(s2)) { - todo.push_back(s2); - can_process = false; - } - } - } - } - if (!can_process) { - continue; - } - todo.pop_back(); - already_found.insert(s, BLACK); - if (is_infinite) { - d.set_sort_size(param_size::size::mk_offset(sort_size::mk_infinite())); - continue; - } - - ptr_vector s_add; - for (constructor const* c : d) { - ptr_vector s_mul; - for (accessor const* a : *c) { - s_mul.push_back(get_sort_size(d.params(), a->range())); - } - s_add.push_back(param_size::size::mk_times(s_mul)); - } - d.set_sort_size(param_size::size::mk_plus(s_add)); - } - } - - - /** - \brief Return true if the inductive datatype is well-founded. - Pre-condition: The given argument constains the parameters of an inductive datatype. - */ - bool util::is_well_founded(unsigned num_types, sort* const* sorts) { - buffer well_founded(num_types, false); - obj_map sort2id; - for (unsigned i = 0; i < num_types; ++i) { - sort2id.insert(sorts[i], i); - } - unsigned num_well_founded = 0, id = 0; - bool changed; - do { - changed = false; - for (unsigned tid = 0; tid < num_types; tid++) { - if (well_founded[tid]) { - continue; - } - sort* s = sorts[tid]; - def const& d = get_def(s); - for (constructor const* c : d) { - bool found_nonwf = false; - for (accessor const* a : *c) { - if (sort2id.find(a->range(), id) && !well_founded[id]) { - found_nonwf = true; - break; - } - } - if (!found_nonwf) { - changed = true; - well_founded[tid] = true; - num_well_founded++; - break; - } - } - } - } - while(changed && num_well_founded < num_types); - return num_well_founded == num_types; - } - - def const& util::get_def(sort* s) const { - return m_plugin->get_def(s); - } - - void util::get_subsorts(sort* s, ptr_vector& sorts) const { - sorts.push_back(s); - for (unsigned i = 0; i < s->get_num_parameters(); ++i) { - parameter const& p = s->get_parameter(i); - if (p.is_ast() && is_sort(p.get_ast())) { - get_subsorts(to_sort(p.get_ast()), sorts); - } - } - } - - - util::util(ast_manager & m): - m(m), - m_family_id(m.mk_family_id("datatype")), - m_asts(m), - m_start(0) { - m_plugin = dynamic_cast(m.get_plugin(m_family_id)); - SASSERT(m_plugin); - } - - util::~util() { - std::for_each(m_vectors.begin(), m_vectors.end(), delete_proc >()); - } - - ptr_vector const * util::get_datatype_constructors(sort * ty) { - SASSERT(is_datatype(ty)); - ptr_vector * r = 0; - if (m_datatype2constructors.find(ty, r)) - return r; - r = alloc(ptr_vector); - m_asts.push_back(ty); - m_vectors.push_back(r); - m_datatype2constructors.insert(ty, r); - def const& d = get_def(ty); - for (constructor const* c : d) { - func_decl_ref f = c->instantiate(ty); - m_asts.push_back(f); - r->push_back(f); - } - return r; - } - - ptr_vector const * util::get_constructor_accessors(func_decl * con) { - SASSERT(is_constructor(con)); - ptr_vector * res = 0; - if (m_constructor2accessors.find(con, res)) { - return res; - } - res = alloc(ptr_vector); - m_asts.push_back(con); - m_vectors.push_back(res); - 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); - } - break; - } - } - return res; - } - - func_decl * util::get_constructor_recognizer(func_decl * con) { - SASSERT(is_constructor(con)); - func_decl * d = 0; - if (m_constructor2recognizer.find(con, d)) - return d; - sort * datatype = con->get_range(); - def const& dd = get_def(datatype); - symbol r; - for (constructor const* c : dd) { - if (c->name() == con->get_name()) { - r = c->recognizer(); - } - } - parameter ps[2] = { parameter(con), parameter(r) }; - d = m.mk_func_decl(m_family_id, OP_DT_RECOGNISER, 2, ps, 1, &datatype); - SASSERT(d); - m_asts.push_back(con); - m_asts.push_back(d); - m_constructor2recognizer.insert(con, d); - return d; - } - - func_decl * util::get_recognizer_constructor(func_decl * recognizer) const { - SASSERT(is_recognizer(recognizer)); - return to_func_decl(recognizer->get_parameter(0).get_ast()); - } - - bool util::is_recursive(sort * ty) { - SASSERT(is_datatype(ty)); - bool r = false; - if (!m_is_recursive.find(ty, r)) { - r = is_recursive_core(ty); - m_is_recursive.insert(ty, r); - m_asts.push_back(ty); - } - return r; - } - - bool util::is_enum_sort(sort* s) { - if (!is_datatype(s)) { - return false; - } - bool r = false; - if (m_is_enum.find(s, r)) - return r; - ptr_vector 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); - return r; - } - - func_decl * util::get_accessor_constructor(func_decl * accessor) { - SASSERT(is_accessor(accessor)); - func_decl * r = 0; - if (m_accessor2constructor.find(accessor, r)) - return r; - sort * datatype = accessor->get_domain(0); - symbol c_id = accessor->get_parameter(1).get_symbol(); - def const& d = get_def(datatype); - func_decl_ref fn(m); - for (constructor const* c : d) { - if (c->name() == c_id) { - fn = c->instantiate(datatype); - break; - } - } - r = fn; - m_accessor2constructor.insert(accessor, r); - m_asts.push_back(accessor); - m_asts.push_back(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 >()); - m_vectors.reset(); - m_asts.reset(); - ++m_start; - } - - - /** - \brief Return a constructor mk(T_1, ... T_n) - where each T_i is not a datatype or it is a datatype that contains - a constructor that will not contain directly or indirectly an element of the given sort. - */ - func_decl * util::get_non_rec_constructor(sort * ty) { - SASSERT(is_datatype(ty)); - func_decl * r = 0; - if (m_datatype2nonrec_constructor.find(ty, r)) - return r; - r = 0; - ptr_vector forbidden_set; - forbidden_set.push_back(ty); - TRACE("util_bug", tout << "invoke get-non-rec: " << sort_ref(ty, m) << "\n";); - r = get_non_rec_constructor_core(ty, forbidden_set); - SASSERT(forbidden_set.back() == ty); - SASSERT(r); - m_asts.push_back(ty); - m_asts.push_back(r); - m_datatype2nonrec_constructor.insert(ty, r); - return r; - } - - /** - \brief Return a constructor mk(T_1, ..., T_n) where - 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 }) - */ - func_decl * util::get_non_rec_constructor_core(sort * ty, ptr_vector & 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 - // 2) each type T_i is not recursive or contains a constructor that does not depend on T - - ptr_vector const& constructors = *get_datatype_constructors(ty); - unsigned sz = constructors.size(); - TRACE("util_bug", tout << "get-non-rec constructor: " << sort_ref(ty, m) << "\n"; - tout << "forbidden: "; - for (sort* s : forbidden_set) tout << sort_ref(s, m) << " "; - tout << "\n"; - tout << "constructors: " << sz << "\n"; - for (func_decl* f : constructors) tout << func_decl_ref(f, m) << "\n"; - ); - // step 1) - unsigned start = ++m_start; - for (unsigned j = 0; j < sz; ++j) { - func_decl * c = constructors[(j + start) % sz]; - TRACE("util_bug", tout << "checking " << sort_ref(ty, m) << ": " << func_decl_ref(c, m) << "\n";); - unsigned num_args = c->get_arity(); - unsigned i = 0; - for (; i < num_args && !is_datatype(c->get_domain(i)); i++); - if (i == num_args) { - TRACE("util_bug", tout << "found non-rec " << func_decl_ref(c, m) << "\n";); - return c; - } - } - // step 2) - for (unsigned j = 0; j < sz; ++j) { - func_decl * c = constructors[(j + start) % sz]; - TRACE("util_bug", tout << "non_rec_constructor c: " << j << " " << func_decl_ref(c, m) << "\n";); - unsigned num_args = c->get_arity(); - unsigned i = 0; - for (; i < num_args; i++) { - sort * T_i = c->get_domain(i); - TRACE("util_bug", tout << "c: " << i << " " << sort_ref(T_i, m) << "\n";); - if (!is_datatype(T_i)) { - TRACE("util_bug", tout << sort_ref(T_i, m) << " is not a datatype\n";); - continue; - } - if (std::find(forbidden_set.begin(), forbidden_set.end(), T_i) != forbidden_set.end()) { - TRACE("util_bug", tout << sort_ref(T_i, m) << " is in forbidden_set\n";); - break; - } - forbidden_set.push_back(T_i); - func_decl * nested_c = get_non_rec_constructor_core(T_i, forbidden_set); - SASSERT(forbidden_set.back() == T_i); - forbidden_set.pop_back(); - if (nested_c == 0) - break; - TRACE("util_bug", tout << "nested_c: " << nested_c->get_name() << "\n";); - } - if (i == num_args) - return c; - } - return 0; - } - - unsigned util::get_constructor_idx(func_decl * f) const { - unsigned idx = 0; - def const& d = get_def(f->get_range()); - for (constructor* c : d) { - if (c->name() == f->get_name()) { - return idx; - } - ++idx; - } - UNREACHABLE(); - return 0; - } - - unsigned util::get_recognizer_constructor_idx(func_decl * f) const { - return get_constructor_idx(get_recognizer_constructor(f)); - } - - /** - \brief Two datatype sorts s1 and s2 are siblings if they were - defined together in the same mutually recursive definition. - */ - bool util::are_siblings(sort * s1, sort * s2) { - if (!is_datatype(s1) || !is_datatype(s2)) { - return s1 == s2; - } - else { - return get_def(s1).id() == get_def(s2).id(); - } - } - - unsigned util::get_datatype_num_constructors(sort * ty) { - def const& d = get_def(ty->get_name()); - return d.constructors().size(); - } - - void util::get_defs(sort* s0, ptr_vector& defs) { - svector mark; - ptr_buffer todo; - todo.push_back(s0); - mark.push_back(s0->get_name()); - while (!todo.empty()) { - sort* s = todo.back(); - todo.pop_back(); - defs.push_back(&m_plugin->get_def(s->get_name())); - def const& d = get_def(s); - for (constructor* c : d) { - for (accessor* a : *c) { - sort* s = a->range(); - if (are_siblings(s0, s) && !mark.contains(s->get_name())) { - mark.push_back(s->get_name()); - todo.push_back(s); - } - } - } - } - } - - void util::display_datatype(sort *s0, std::ostream& out) { - ast_mark mark; - ptr_buffer todo; - SASSERT(is_datatype(s0)); - out << s0->get_name() << " where\n"; - todo.push_back(s0); - mark.mark(s0, true); - while (!todo.empty()) { - sort* s = todo.back(); - todo.pop_back(); - out << s->get_name() << " =\n"; - - ptr_vector const& cnstrs = *get_datatype_constructors(s); - for (unsigned i = 0; i < cnstrs.size(); ++i) { - func_decl* cns = cnstrs[i]; - func_decl* rec = get_constructor_recognizer(cns); - out << " " << cns->get_name() << " :: " << rec->get_name() << " :: "; - ptr_vector const & accs = *get_constructor_accessors(cns); - for (unsigned j = 0; j < accs.size(); ++j) { - func_decl* acc = accs[j]; - sort* s1 = acc->get_range(); - out << "(" << acc->get_name() << ": " << s1->get_name() << ") "; - if (is_datatype(s1) && are_siblings(s1, s0) && !mark.is_marked(s1)) { - mark.mark(s1, true); - todo.push_back(s1); - } - } - out << "\n"; - } - } - } -} - -datatype_decl * mk_datatype_decl(datatype_util& u, symbol const & n, unsigned num_params, sort*const* params, unsigned num_constructors, constructor_decl * const * cs) { - datatype::decl::plugin* p = u.get_plugin(); - datatype::def* d = p->mk(n, num_params, params); - for (unsigned i = 0; i < num_constructors; ++i) { - d->add(cs[i]); - } - return d; -} - -#endif diff --git a/src/ast/datatype_decl_plugin2.h b/src/ast/datatype_decl_plugin2.h deleted file mode 100644 index 364ba9350..000000000 --- a/src/ast/datatype_decl_plugin2.h +++ /dev/null @@ -1,439 +0,0 @@ -/*++ -Copyright (c) 2017 Microsoft Corporation - -Module Name: - - datatype_decl_plugin.h - -Abstract: - - - -Author: - - Nikolaj Bjorner (nbjorner) 2017-9-1 - -Revision History: - - rewritten to support SMTLIB-2.6 parameters from - Leonardo de Moura (leonardo) 2008-01-09. - ---*/ -#ifndef DATATYPE_DECL_PLUGIN2_H_ -#define DATATYPE_DECL_PLUGIN2_H_ - -#include "ast/ast.h" -#include "util/buffer.h" -#include "util/symbol_table.h" -#include "util/obj_hashtable.h" - -#ifdef DATATYPE_V2 - - enum sort_kind { - DATATYPE_SORT - }; - - enum op_kind { - OP_DT_CONSTRUCTOR, - OP_DT_RECOGNISER, - OP_DT_IS, - OP_DT_ACCESSOR, - OP_DT_UPDATE_FIELD, - LAST_DT_OP - }; - -namespace datatype { - - class util; - class def; - class accessor; - class constructor; - - - class accessor { - symbol m_name; - sort_ref m_range; - unsigned m_index; // reference to recursive data-type may only get resolved after all mutually recursive data-types are procssed. - constructor* m_constructor; - public: - accessor(ast_manager& m, symbol const& n, sort* range): - m_name(n), - m_range(range, m), - m_index(UINT_MAX) - {} - accessor(ast_manager& m, symbol const& n, unsigned index): - m_name(n), - m_range(m), - m_index(index) - {} - sort* range() const { return m_range; } - void fix_range(sort_ref_vector const& dts); - symbol const& name() const { return m_name; } - func_decl_ref instantiate(sort_ref_vector const& ps) const; - func_decl_ref instantiate(sort* dt) const; - void attach(constructor* d) { m_constructor = d; } - constructor const& get_constructor() const { return *m_constructor; } - def const& get_def() const; - util& u() const; - accessor* translate(ast_translation& tr); - }; - - class constructor { - symbol m_name; - symbol m_recognizer; - ptr_vector m_accessors; - def* m_def; - public: - constructor(symbol n, symbol const& r): m_name(n), m_recognizer(r) {} - ~constructor(); - void add(accessor* a) { m_accessors.push_back(a); a->attach(this); } - symbol const& name() const { return m_name; } - symbol const& recognizer() const { return m_recognizer; } - ptr_vector const& accessors() const { return m_accessors; } - ptr_vector::const_iterator begin() const { return m_accessors.begin(); } - ptr_vector::const_iterator end() const { return m_accessors.end(); } - ptr_vector::iterator begin() { return m_accessors.begin(); } - ptr_vector::iterator end() { return m_accessors.end(); } - func_decl_ref instantiate(sort_ref_vector const& ps) const; - func_decl_ref instantiate(sort* dt) const; - void attach(def* d) { m_def = d; } - def const& get_def() const { return *m_def; } - util& u() const; - constructor* translate(ast_translation& tr); - }; - - namespace param_size { - class size { - unsigned m_ref; - public: - size(): m_ref(0) {} - virtual ~size() {} - void inc_ref() { ++m_ref; } - void dec_ref() { --m_ref; if (m_ref == 0) dealloc(this); } - static size* mk_offset(sort_size const& s); - static size* mk_param(sort_ref& p); - static size* mk_plus(size* a1, size* a2); - static size* mk_times(size* a1, size* a2); - static size* mk_plus(ptr_vector& szs); - static size* mk_times(ptr_vector& szs); - static size* mk_power(size* a1, size* a2); - - virtual size* subst(obj_map& S) = 0; - virtual sort_size eval(obj_map const& S) = 0; - - }; - struct offset : public size { - sort_size m_offset; - offset(sort_size const& s): m_offset(s) {} - virtual ~offset() {} - virtual size* subst(obj_map& S) { return this; } - virtual sort_size eval(obj_map const& S) { return m_offset; } - }; - struct plus : public size { - size* m_arg1, *m_arg2; - plus(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref();} - virtual ~plus() { m_arg1->dec_ref(); m_arg2->dec_ref(); } - virtual size* subst(obj_map& S) { return mk_plus(m_arg1->subst(S), m_arg2->subst(S)); } - virtual sort_size eval(obj_map const& S) { - sort_size s1 = m_arg1->eval(S); - sort_size s2 = m_arg2->eval(S); - if (s1.is_infinite()) return s1; - if (s2.is_infinite()) return s2; - if (s1.is_very_big()) return s1; - if (s2.is_very_big()) return s2; - rational r = rational(s1.size(), rational::ui64()) + rational(s2.size(), rational::ui64()); - return sort_size(r); - } - }; - struct times : public size { - size* m_arg1, *m_arg2; - times(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref(); } - virtual ~times() { m_arg1->dec_ref(); m_arg2->dec_ref(); } - virtual size* subst(obj_map& S) { return mk_times(m_arg1->subst(S), m_arg2->subst(S)); } - virtual sort_size eval(obj_map const& S) { - sort_size s1 = m_arg1->eval(S); - sort_size s2 = m_arg2->eval(S); - if (s1.is_infinite()) return s1; - if (s2.is_infinite()) return s2; - if (s1.is_very_big()) return s1; - if (s2.is_very_big()) return s2; - rational r = rational(s1.size(), rational::ui64()) * rational(s2.size(), rational::ui64()); - return sort_size(r); - } - }; - struct power : public size { - size* m_arg1, *m_arg2; - power(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref(); } - virtual ~power() { m_arg1->dec_ref(); m_arg2->dec_ref(); } - virtual size* subst(obj_map& S) { return mk_power(m_arg1->subst(S), m_arg2->subst(S)); } - virtual sort_size eval(obj_map const& S) { - sort_size s1 = m_arg1->eval(S); - sort_size s2 = m_arg2->eval(S); - // s1^s2 - if (s1.is_infinite()) return s1; - if (s2.is_infinite()) return s2; - if (s1.is_very_big()) return s1; - if (s2.is_very_big()) return s2; - if (s1.size() == 1) return s1; - if (s2.size() == 1) return s1; - if (s1.size() > (2 << 20) || s2.size() > 10) return sort_size::mk_very_big(); - rational r = ::power(rational(s1.size(), rational::ui64()), static_cast(s2.size())); - return sort_size(r); - } - }; - struct sparam : public size { - sort_ref m_param; - sparam(sort_ref& p): m_param(p) {} - virtual ~sparam() {} - virtual size* subst(obj_map& S) { return S[m_param]; } - virtual sort_size eval(obj_map const& S) { return S[m_param]; } - }; - }; - - class def { - ast_manager& m; - util& m_util; - symbol m_name; - unsigned m_class_id; - param_size::size* m_sort_size; - sort_ref_vector m_params; - mutable sort_ref m_sort; - ptr_vector m_constructors; - public: - def(ast_manager& m, util& u, symbol const& n, unsigned class_id, unsigned num_params, sort * const* params): - m(m), - m_util(u), - m_name(n), - m_class_id(class_id), - m_sort_size(0), - m_params(m, num_params, params), - m_sort(m) - {} - ~def() { - if (m_sort_size) m_sort_size->dec_ref(); - for (constructor* c : m_constructors) dealloc(c); - m_constructors.reset(); - } - void add(constructor* c) { - m_constructors.push_back(c); - c->attach(this); - } - symbol const& name() const { return m_name; } - unsigned id() const { return m_class_id; } - sort_ref instantiate(sort_ref_vector const& ps) const; - ptr_vector const& constructors() const { return m_constructors; } - ptr_vector::const_iterator begin() const { return m_constructors.begin(); } - ptr_vector::const_iterator end() const { return m_constructors.end(); } - ptr_vector::iterator begin() { return m_constructors.begin(); } - ptr_vector::iterator end() { return m_constructors.end(); } - 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(); m_sort = 0; } - def* translate(ast_translation& tr, util& u); - }; - - namespace decl { - - class plugin : public decl_plugin { - mutable scoped_ptr m_util; - map m_defs; - svector m_def_block; - unsigned m_class_id; - util & u() const; - - virtual void inherit(decl_plugin* other_p, ast_translation& tr); - - public: - plugin(): m_class_id(0) {} - virtual ~plugin(); - - virtual void finalize(); - - virtual decl_plugin * mk_fresh() { return alloc(plugin); } - - virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters); - - virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range); - - virtual expr * get_some_value(sort * s); - - virtual bool is_fully_interp(sort * s) const; - - virtual bool is_value(app* e) const; - - virtual bool is_unique_value(app * e) const { return is_value(e); } - - virtual void get_op_names(svector & op_names, symbol const & logic); - - void begin_def_block() { m_class_id++; m_def_block.reset(); } - - void end_def_block(); - - def* mk(symbol const& name, unsigned n, sort * const * params); - - void remove(symbol const& d); - - bool mk_datatypes(unsigned num_datatypes, def * const * datatypes, unsigned num_params, sort* const* sort_params, sort_ref_vector & new_sorts); - - def const& get_def(sort* s) const { return *(m_defs[datatype_name(s)]); } - def& get_def(symbol const& s) { return *(m_defs[s]); } - bool is_declared(sort* s) const { return m_defs.contains(datatype_name(s)); } - private: - bool is_value_visit(expr * arg, ptr_buffer & todo) const; - - func_decl * mk_update_field( - unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range); - - func_decl * mk_constructor( - unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range); - - func_decl * mk_accessor( - unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range); - - func_decl * mk_recognizer( - unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range); - - func_decl * mk_is( - unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range); - - symbol datatype_name(sort * s) const { - //SASSERT(u().is_datatype(s)); - return s->get_parameter(0).get_symbol(); - } - - }; - } - - class util { - ast_manager & m; - family_id m_family_id; - mutable decl::plugin* m_plugin; - - - obj_map *> m_datatype2constructors; - obj_map m_datatype2nonrec_constructor; - obj_map *> m_constructor2accessors; - obj_map m_constructor2recognizer; - obj_map m_recognizer2constructor; - obj_map m_accessor2constructor; - obj_map m_is_recursive; - obj_map m_is_enum; - mutable obj_map m_is_fully_interp; - mutable ast_ref_vector m_asts; - ptr_vector > m_vectors; - unsigned m_start; - mutable ptr_vector m_fully_interp_trail; - - func_decl * get_non_rec_constructor_core(sort * ty, ptr_vector & forbidden_set); - - friend class decl::plugin; - - bool is_recursive_core(sort * s) const; - sort_size get_datatype_size(sort* s0); - void compute_datatype_size_functions(svector const& names); - param_size::size* get_sort_size(sort_ref_vector const& params, sort* s); - bool is_well_founded(unsigned num_types, sort* const* sorts); - def& get_def(symbol const& s) { return m_plugin->get_def(s); } - void get_subsorts(sort* s, ptr_vector& sorts) const; - - public: - util(ast_manager & m); - ~util(); - ast_manager & get_manager() const { return m; } - // sort * mk_datatype_sort(symbol const& name, unsigned n, sort* const* params); - bool is_datatype(sort const* s) const { return is_sort_of(s, m_family_id, DATATYPE_SORT); } - bool is_enum_sort(sort* s); - bool is_recursive(sort * ty); - bool is_constructor(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_CONSTRUCTOR); } - bool is_recognizer(func_decl * f) const { return is_recognizer0(f) || is_is(f); } - bool is_recognizer0(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_RECOGNISER); } - bool is_is(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_IS); } - bool is_accessor(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_ACCESSOR); } - bool is_update_field(func_decl * f) const { return is_decl_of(f, m_family_id, OP_DT_UPDATE_FIELD); } - bool is_constructor(app * f) const { return is_app_of(f, m_family_id, OP_DT_CONSTRUCTOR); } - bool is_recognizer0(app * f) const { return is_app_of(f, m_family_id, OP_DT_RECOGNISER);} - bool is_is(app * f) const { return is_app_of(f, m_family_id, OP_DT_IS);} - bool is_recognizer(app * f) const { return is_recognizer0(f) || is_is(f); } - bool is_accessor(app * f) const { return is_app_of(f, m_family_id, OP_DT_ACCESSOR); } - bool is_update_field(app * f) const { return is_app_of(f, m_family_id, OP_DT_UPDATE_FIELD); } - ptr_vector const * get_datatype_constructors(sort * ty); - unsigned get_datatype_num_constructors(sort * ty); - unsigned get_datatype_num_parameter_sorts(sort * ty); - sort* get_datatype_parameter_sort(sort * ty, unsigned idx); - func_decl * get_non_rec_constructor(sort * ty); - func_decl * get_constructor_recognizer(func_decl * constructor); - ptr_vector const * get_constructor_accessors(func_decl * constructor); - func_decl * get_accessor_constructor(func_decl * accessor); - func_decl * get_recognizer_constructor(func_decl * recognizer) const; - family_id get_family_id() const { return m_family_id; } - bool are_siblings(sort * s1, sort * s2); - bool is_func_decl(op_kind k, unsigned num_params, parameter const* params, func_decl* f); - bool is_constructor_of(unsigned num_params, parameter const* params, func_decl* f); - void reset(); - bool is_declared(sort* s) const; - void display_datatype(sort *s, std::ostream& strm); - bool is_fully_interp(sort * s) const; - sort_ref_vector datatype_params(sort * s) const; - unsigned get_constructor_idx(func_decl * f) const; - unsigned get_recognizer_constructor_idx(func_decl * f) const; - decl::plugin* get_plugin() { return m_plugin; } - void get_defs(sort* s, ptr_vector& defs); - def const& get_def(sort* s) const; - }; - -}; - -typedef datatype::accessor accessor_decl; -typedef datatype::constructor constructor_decl; -typedef datatype::def datatype_decl; -typedef datatype::decl::plugin datatype_decl_plugin; -typedef datatype::util datatype_util; - -class type_ref { - void * m_data; -public: - type_ref():m_data(TAG(void *, static_cast(0), 1)) {} - type_ref(int idx):m_data(BOXINT(void *, idx)) {} - type_ref(sort * s):m_data(TAG(void *, s, 1)) {} - - bool is_idx() const { return GET_TAG(m_data) == 0; } - bool is_sort() const { return GET_TAG(m_data) == 1; } - sort * get_sort() const { return UNTAG(sort *, m_data); } - int get_idx() const { return UNBOXINT(m_data); } -}; - -inline accessor_decl * mk_accessor_decl(ast_manager& m, symbol const & n, type_ref const & t) { - if (t.is_idx()) { - return alloc(accessor_decl, m, n, t.get_idx()); - } - else { - return alloc(accessor_decl, m, n, t.get_sort()); - } -} - -inline constructor_decl * mk_constructor_decl(symbol const & n, symbol const & r, unsigned num_accessors, accessor_decl * * acs) { - constructor_decl* c = alloc(constructor_decl, n, r); - for (unsigned i = 0; i < num_accessors; ++i) { - c->add(acs[i]); - } - return c; -} - - - -// Remark: the datatype becomes the owner of the constructor_decls -datatype_decl * mk_datatype_decl(datatype_util& u, symbol const & n, unsigned num_params, sort*const* params, unsigned num_constructors, constructor_decl * const * cs); -inline void del_datatype_decl(datatype_decl * d) {} -inline void del_datatype_decls(unsigned num, datatype_decl * const * ds) {} - - -#endif /* DATATYPE_DECL_PLUGIN_H_ */ - -#endif /* DATATYPE_V2 */ diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp index 95a6030f3..7eac1f347 100644 --- a/src/cmd_context/pdecl.cpp +++ b/src/cmd_context/pdecl.cpp @@ -355,13 +355,8 @@ psort_dt_decl::psort_dt_decl(unsigned id, unsigned num_params, pdecl_manager & m sort * psort_dt_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * s) { -#ifndef DATATYPE_V2 - UNREACHABLE(); - return 0; -#else SASSERT(n == m_num_params); return m.instantiate_datatype(this, m_name, n, s); -#endif } void psort_dt_decl::display(std::ostream & out) const { @@ -581,7 +576,6 @@ struct datatype_decl_buffer { ~datatype_decl_buffer() { del_datatype_decls(m_buffer.size(), m_buffer.c_ptr()); } }; -#ifdef DATATYPE_V2 sort * pdatatype_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * s) { sort * r = m.instantiate_datatype(this, m_name, n, s); @@ -615,37 +609,6 @@ sort * pdatatype_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * return r; } -#else -sort * pdatatype_decl::instantiate(pdecl_manager & m, unsigned n, sort * const * s) { - SASSERT(m_num_params == n); - sort * r = find(s); - if (r) - return r; - if (m_parent != 0) { - if (m_parent->instantiate(m, s)) { - r = find(s); - SASSERT(r); - return r; - } - } - else { - datatype_decl_buffer dts; - dts.m_buffer.push_back(instantiate_decl(m, s)); - 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, s, sorts); - TRACE("pdatatype_decl", tout << "instantiating " << m_name << " is_ok: " << is_ok << "\n";); - if (is_ok) { - r = sorts.get(0); - cache(m, s, r); - m.save_info(r, this, n, s); - m.notify_new_dt(r, this); - return r; - } - } - return 0; -} -#endif void pdatatype_decl::display(std::ostream & out) const { out << "(declare-datatype " << m_name; @@ -666,7 +629,6 @@ void pdatatype_decl::display(std::ostream & out) const { out << ")"; } -#ifdef DATATYPE_V2 bool pdatatype_decl::commit(pdecl_manager& m) { TRACE("datatype", tout << m_name << "\n";); sort_ref_vector ps(m.m()); @@ -683,7 +645,6 @@ bool pdatatype_decl::commit(pdecl_manager& m) { } return is_ok; } -#endif pdatatypes_decl::pdatatypes_decl(unsigned id, unsigned num_params, pdecl_manager & m, @@ -714,7 +675,6 @@ bool pdatatypes_decl::fix_missing_refs(symbol & missing) { return true; } -#ifdef DATATYPE_V2 sort* pdecl_manager::instantiate_datatype(psort_decl* p, symbol const& name, unsigned n, sort * const* s) { TRACE("datatype", tout << name << " "; for (unsigned i = 0; i < n; ++i) tout << s[i]->get_name() << " "; tout << "\n";); pdecl_manager& m = *this; @@ -746,28 +706,7 @@ bool pdatatypes_decl::instantiate(pdecl_manager & m, sort * const * s) { UNREACHABLE(); return false; } -#else -bool pdatatypes_decl::instantiate(pdecl_manager & m, sort * const * s) { - datatype_decl_buffer dts; - for (auto d : m_datatypes) { - dts.m_buffer.push_back(d->instantiate_decl(m, s)); - } - sort_ref_vector sorts(m.m()); - bool is_ok = m.get_dt_plugin()->mk_datatypes(dts.m_buffer.size(), dts.m_buffer.c_ptr(), m_num_params, s, sorts); - if (!is_ok) - return false; - unsigned i = 0; - for (auto d : m_datatypes) { - sort * new_dt = sorts.get(i++); - d->cache(m, s, new_dt); - m.save_info(new_dt, d, m_num_params, s); - m.notify_new_dt(new_dt, d); - } - return true; -} -#endif -#ifdef DATATYPE_V2 bool pdatatypes_decl::commit(pdecl_manager& m) { datatype_decl_buffer dts; for (pdatatype_decl* d : m_datatypes) { @@ -789,7 +728,6 @@ bool pdatatypes_decl::commit(pdecl_manager& m) { } return is_ok; } -#endif struct pdecl_manager::sort_info { psort_decl * m_decl; diff --git a/src/cmd_context/pdecl.h b/src/cmd_context/pdecl.h index bef723380..c72020827 100644 --- a/src/cmd_context/pdecl.h +++ b/src/cmd_context/pdecl.h @@ -241,9 +241,7 @@ public: virtual void display(std::ostream & out) const; bool has_missing_refs(symbol & missing) const; bool has_duplicate_accessors(symbol & repeated) const; -#ifdef DATATYPE_V2 bool commit(pdecl_manager& m); -#endif }; /** @@ -263,10 +261,8 @@ public: pdatatype_decl const * const * children() const { return m_datatypes.c_ptr(); } pdatatype_decl * const * begin() const { return m_datatypes.begin(); } pdatatype_decl * const * end() const { return m_datatypes.end(); } -#ifdef DATATYPE_V2 // commit declaration bool commit(pdecl_manager& m); -#endif }; class new_datatype_eh { diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index a1304a848..681c3d597 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -877,9 +877,7 @@ namespace smt2 { } else if (sz == 1) { check_missing(new_dt_decls[0], line, pos); -#ifdef DATATYPE_V2 new_dt_decls[0]->commit(pm()); -#endif } else { SASSERT(sz > 1); @@ -892,27 +890,9 @@ namespace smt2 { err_msg += "'"; throw parser_exception(err_msg, line, pos); } -#ifndef DATATYPE_V2 - m_ctx.insert_aux_pdecl(dts.get()); -#else dts->commit(pm()); - m_ctx.insert_aux_pdecl(dts.get()); -#endif + m_ctx.insert_aux_pdecl(dts.get()); } -#ifndef DATATYPE_V2 - for (unsigned i = 0; i < sz; i++) { - pdatatype_decl * d = new_dt_decls[i]; - SASSERT(d != 0); - symbol duplicated; - check_duplicate(d, line, pos); - m_ctx.insert(d); - if (d->get_num_params() == 0) { - // if datatype is not parametric... then force instantiation to register accessor, recognizers and constructors... - sort_ref s(m()); - s = d->instantiate(pm(), 0, 0); - } - } -#else for (unsigned i = 0; i < sz; i++) { pdatatype_decl * d = new_dt_decls[i]; symbol duplicated; @@ -922,7 +902,6 @@ namespace smt2 { m_ctx.insert(d); } } -#endif TRACE("declare_datatypes", tout << "i: " << i << " new_dt_decls.size(): " << sz << "\n"; for (unsigned j = 0; j < new_dt_decls.size(); ++j) tout << new_dt_decls[j]->get_name() << "\n";); m_ctx.print_success(); @@ -952,16 +931,7 @@ namespace smt2 { check_missing(d, line, pos); check_duplicate(d, line, pos); -#ifndef DATATYPE_V2 - m_ctx.insert(d); - if (d->get_num_params() == 0) { - // if datatype is not parametric... then force instantiation to register accessor, recognizers and constructors... - sort_ref s(m()); - s = d->instantiate(pm(), 0, 0); - } -#else d->commit(pm()); -#endif check_rparen_next("invalid end of datatype declaration, ')' expected"); m_ctx.print_success(); }