diff --git a/src/ast/CMakeLists.txt b/src/ast/CMakeLists.txt index 0a14d9473..47ed2def8 100644 --- a/src/ast/CMakeLists.txt +++ b/src/ast/CMakeLists.txt @@ -14,6 +14,7 @@ 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.cpp b/src/ast/ast.cpp index c1ff04ada..1a35e710a 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -188,18 +188,14 @@ decl_info::decl_info(decl_info const& other) : void decl_info::init_eh(ast_manager & m) { - vector::iterator it = m_parameters.begin(); - vector::iterator end = m_parameters.end(); - for (; it != end; ++it) { - it->init_eh(m); + for (parameter & p : m_parameters) { + p.init_eh(m); } } void decl_info::del_eh(ast_manager & m) { - vector::iterator it = m_parameters.begin(); - vector::iterator end = m_parameters.end(); - for (; it != end; ++it) { - it->del_eh(m, m_family_id); + for (parameter & p : m_parameters) { + p.del_eh(m, m_family_id); } } @@ -1935,6 +1931,35 @@ sort * ast_manager::mk_sort(symbol const & name, sort_info * info) { return register_node(new_node); } +sort * ast_manager::substitute(sort* s, unsigned n, sort * const * src, sort * const * dst) { + for (unsigned i = 0; i < n; ++i) { + if (s == src[i]) return dst[i]; + } + + vector ps; + bool change = false; + sort_ref_vector sorts(*this); + for (unsigned i = 0; i < s->get_num_parameters(); ++i) { + parameter const& p = s->get_parameter(i); + if (p.is_ast()) { + SASSERT(is_sort(p.get_ast())); + change = true; + sorts.push_back(substitute(to_sort(p.get_ast()), n, src, dst)); + ps.push_back(parameter(sorts.back())); + } + else { + ps.push_back(p); + } + } + if (!change) { + return s; + } + decl_info dinfo(s->get_family_id(), s->get_decl_kind(), ps.size(), ps.c_ptr(), s->private_parameters()); + sort_info sinfo(dinfo, s->get_num_elements()); + return mk_sort(s->get_name(), &sinfo); +} + + sort * ast_manager::mk_uninterpreted_sort(symbol const & name, unsigned num_parameters, parameter const * parameters) { user_sort_plugin * plugin = get_user_sort_plugin(); decl_kind kind = plugin->register_name(name); @@ -2580,7 +2605,7 @@ expr * ast_manager::get_some_value(sort * s) { return mk_model_value(0, s); } -bool ast_manager::is_fully_interp(sort const * s) const { +bool ast_manager::is_fully_interp(sort * s) const { if (is_uninterp(s)) return false; family_id fid = s->get_family_id(); diff --git a/src/ast/ast.h b/src/ast/ast.h index 699268bd0..a1e31f46f 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -335,13 +335,17 @@ public: unsigned num_parameters = 0, parameter const * parameters = 0, bool private_parameters = false): decl_info(family_id, k, num_parameters, parameters, private_parameters), m_num_elements(num_elements) { } - sort_info(sort_info const& other) : decl_info(other), m_num_elements(other.m_num_elements) { + sort_info(sort_info const& other) : decl_info(other), m_num_elements(other.m_num_elements) { } + sort_info(decl_info const& di, sort_size const& num_elements) : + decl_info(di), m_num_elements(num_elements) {} + ~sort_info() {} bool is_infinite() const { return m_num_elements.is_infinite(); } bool is_very_big() const { return m_num_elements.is_very_big(); } sort_size const & get_num_elements() const { return m_num_elements; } + void set_num_elements(sort_size const& s) { m_num_elements = s; } }; std::ostream & operator<<(std::ostream & out, sort_info const & info); @@ -567,6 +571,7 @@ public: bool is_very_big() const { return get_info() == 0 || get_info()->is_very_big(); } bool is_sort_of(family_id fid, decl_kind k) const { return get_family_id() == fid && get_decl_kind() == k; } sort_size const & get_num_elements() const { return get_info()->get_num_elements(); } + void set_num_elements(sort_size const& s) { get_info()->set_num_elements(s); } unsigned get_size() const { return get_obj_size(); } }; @@ -988,7 +993,7 @@ public: // Return true if the interpreted sort s does not depend on uninterpreted sorts. // This may be the case, for example, for array and datatype sorts. - virtual bool is_fully_interp(sort const * s) const { return true; } + virtual bool is_fully_interp(sort * s) const { return true; } // Event handlers for deleting/translating PARAM_EXTERNAL virtual void del(parameter const & p) {} @@ -1655,6 +1660,8 @@ public: sort * mk_sort(family_id fid, decl_kind k, unsigned num_parameters = 0, parameter const * parameters = 0); + sort * substitute(sort* s, unsigned n, sort * const * src, sort * const * dst); + sort * mk_bool_sort() const { return m_bool_sort; } sort * mk_proof_sort() const { return m_proof_sort; } @@ -1667,7 +1674,7 @@ public: \brief A sort is "fully" interpreted if it is interpreted, and doesn't depend on other uninterpreted sorts. */ - bool is_fully_interp(sort const * s) const; + bool is_fully_interp(sort * s) const; func_decl * mk_func_decl(family_id fid, decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range = 0); diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp index b4f30767f..446992105 100644 --- a/src/ast/datatype_decl_plugin.cpp +++ b/src/ast/datatype_decl_plugin.cpp @@ -675,7 +675,7 @@ expr * datatype_decl_plugin::get_some_value(sort * s) { return m_manager->mk_app(c, args.size(), args.c_ptr()); } -bool datatype_decl_plugin::is_fully_interp(sort const * s) const { +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(); diff --git a/src/ast/datatype_decl_plugin.h b/src/ast/datatype_decl_plugin.h index 3d008ad9c..dcd352471 100644 --- a/src/ast/datatype_decl_plugin.h +++ b/src/ast/datatype_decl_plugin.h @@ -150,7 +150,7 @@ public: virtual expr * get_some_value(sort * s); - virtual bool is_fully_interp(sort const * s) const; + virtual bool is_fully_interp(sort * s) const; virtual bool is_value(app* e) const; diff --git a/src/ast/datatype_decl_plugin2.cpp b/src/ast/datatype_decl_plugin2.cpp new file mode 100644 index 000000000..4e60abcce --- /dev/null +++ b/src/ast/datatype_decl_plugin2.cpp @@ -0,0 +1,819 @@ +/*++ +Copyright (c) 2006 Microsoft Corporation + +Module Name: + + datatype_decl_plugin.cpp + +Abstract: + + + +Author: + + Leonardo de Moura (leonardo) 2008-01-10. + +Revision History: + + // compute sort sizes and insert them. + // have a notion of pre-sort or just attach sort size after declaration. + +--*/ +#include "ast/datatype_decl_plugin2.h" +#include "util/warning.h" +#include "ast/ast_smt2_pp.h" + +namespace datatype { + + func_decl_ref accessor::instantiate(sort_ref_vector const& ps) const { + unsigned n = ps.size(); + 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(); } + + util& constructor::u() const { return m_def->u(); } + + func_decl_ref constructor::instantiate(sort_ref_vector const& ps) const { + 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); + } + + sort_ref def::instantiate(sort_ref_vector const& sorts) const { + sort_ref s(m); + if (!m_sort) { + vector ps; + 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(), sorts.c_ptr(), m_params.c_ptr()), m); + } + + enum status { + GRAY, + BLACK + }; + + 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); + if (m_util.get() == 0) { + m_util = alloc(util, *m_manager); + } + return *(m_util.get()); + } + + struct invalid_datatype {}; + + sort * plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) { + try { + if (k != DATATYPE_SORT) { + throw invalid_datatype(); + } + if (num_parameters < 1) { + 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)); + // compute datatype size + sort_size ts = u().get_datatype_size(s); + s->set_num_elements(ts); + 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); + } + + + func_decl * decl::plugin::mk_constructor(unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) { + ast_manager& m = *m_manager; + SASSERT(num_parameters == 1 && parameters[0].is_symbol() && range && u().is_datatype(range)); + if (num_parameters != 1 || !parameters[0].is_symbol() || !range || !u().is_datatype(range)) { + m_manager->raise_exception("invalid parameters for datatype constructor"); + } + // 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; + SASSERT(arity == 1 && num_parameters == 1 && parameters[0].is_ast() && is_func_decl(parameters[0].get_ast())); + SASSERT(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; + symbol name = to_func_decl(parameters[0].get_ast())->get_name(); + return m.mk_func_decl(name, arity, domain, range); + } + + func_decl * decl::plugin::mk_accessor(unsigned num_parameters, parameter const * parameters, + unsigned arity, sort * const * domain, sort * range) + { + ast_manager& m = *m_manager; + SASSERT(arity == 1 && num_parameters == 2 && parameters[0].is_symbol() && parameters[0].is_symbol()); + SASSERT(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); + } + + 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_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::add(symbol const& name, unsigned n, sort * const * params) { + ast_manager& m = *m_manager; + def* d = alloc(def, m, u(), name, m_class_id, n, params); + m_defs.insert(name, d); + m_def_block.push_back(name); + return *d; + } + + 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)); + } + if (!u().is_well_founded(sorts.size(), sorts.c_ptr())) { + m_manager->raise_exception("datatype is not well-founded"); + } + } + + void plugin::del(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) { + 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; + } + + /** + \brief Return the size of the inductive datatype. + Pre-condition: The given argument constains the parameters of an inductive datatype. + */ + sort_size util::get_datatype_size(sort* s0) { + obj_map already_found; + obj_map szs; + ptr_vector todo; + todo.push_back(s0); + status st; + while (!todo.empty()) { + sort* s = todo.back(); + if (already_found.find(s, st) && st == BLACK) { + todo.pop_back(); + continue; + } + already_found.insert(s, GRAY); + bool is_very_big = false; + bool can_process = true; + def const& d = get_def(s); + for (constructor const& c : d) { + for (accessor const& a : c) { + func_decl_ref ac = a.instantiate(s); + sort* r = ac->get_range(); + if (is_datatype(r)) { + if (already_found.find(r, st)) { + // type is infinite + if (st == GRAY) return sort_size(); + } + else { + todo.push_back(r); + can_process = false; + } + } + else if (r->is_infinite()) { + // type is infinite + return sort_size(); + } + else if (r->is_very_big()) { + is_very_big = true; + } + } + } + + if (can_process) { + todo.pop_back(); + already_found.insert(s, BLACK); + if (is_very_big) { + szs.insert(s, sort_size::mk_very_big()); + } + else { + // the type is not infinite nor the number of elements is infinite... + // computing the number of elements + rational num; + def const& d = get_def(s); + for (constructor const& c : d) { + rational c_num(1); + for (accessor const& a : c) { + func_decl_ref ac = a.instantiate(s); + sort* r = ac->get_range(); + if (szs.contains(r)) { + c_num *= rational(szs[r].size(), rational::ui64()); + } + else { + SASSERT(!r->is_infinite() && !r->is_very_big()); + c_num *= rational(r->get_num_elements().size(), rational::ui64()); + } + } + num += c_num; + } + szs.insert(s, sort_size(num)); + } + } + } + return szs[s0]; + } + + + /** + \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)); + } + + 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) { + res->push_back(a.instantiate(datatype)); + } + break; + } + } + return *res; + } + + func_decl * 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(); + parameter ps[1] = { parameter(constructor) }; + d = m.mk_func_decl(m_family_id, OP_DT_RECOGNISER, 1, ps, 1, &datatype); + SASSERT(d); + m_asts.push_back(constructor); + m_asts.push_back(d); + m_constructor2recognizer.insert(constructor, d); + return d; + } + + func_decl * util::get_recognizer_constructor(func_decl * recognizer) { + 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); + 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); + // step 1) + unsigned sz = constructors.size(); + ++m_start; + for (unsigned j = 0; j < sz; ++j) { + func_decl * c = constructors[(j + m_start) % sz]; + unsigned num_args = c->get_arity(); + unsigned i = 0; + for (; i < num_args; i++) { + sort * T_i = c->get_domain(i); + if (is_datatype(T_i)) + break; + } + if (i == num_args) + return c; + } + // step 2) + for (unsigned j = 0; j < sz; ++j) { + func_decl * c = constructors[(j + m_start) % sz]; + TRACE("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("util_bug", tout << "c: " << c->get_name() << " i: " << i << " T_i: " << T_i->get_name() << "\n";); + if (!is_datatype(T_i)) { + TRACE("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("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("util_bug", tout << "nested_c: " << nested_c->get_name() << "\n";); + if (nested_c == 0) + break; + } + if (i == num_args) + return c; + } + return 0; + } + + + /** + \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(); + } + } + + void 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)) { + mark.mark(s1, true); + todo.push_back(s1); + } + } + strm << "\n"; + } + } + } +} diff --git a/src/ast/datatype_decl_plugin2.h b/src/ast/datatype_decl_plugin2.h new file mode 100644 index 000000000..fad7ff174 --- /dev/null +++ b/src/ast/datatype_decl_plugin2.h @@ -0,0 +1,257 @@ +/*++ +Copyright (c) 2006 Microsoft Corporation + +Module Name: + + datatype_decl_plugin.h + +Abstract: + + + +Author: + + Leonardo de Moura (leonardo) 2008-01-09. + +Revision History: + +--*/ +#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" + +namespace datatype { + + class util; + class def; + class accessor; + class constructor; + + enum sort_kind { + DATATYPE_SORT + }; + + enum op_kind { + OP_DT_CONSTRUCTOR, + OP_DT_RECOGNISER, + OP_DT_ACCESSOR, + OP_DT_UPDATE_FIELD, + LAST_DT_OP + }; + + class accessor { + ast_manager& m; + symbol m_name; + sort_ref m_domain; + sort_ref m_range; + constructor* m_constructor; + public: + accessor(ast_manager& m, symbol const& n): + m(m), + m_name(n), + m_domain(m), + m_range(m) + {} + sort* range() const { return m_range; } + 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; + }; + + class constructor { + ast_manager& m; + symbol m_name; + vector m_accessors; + def* m_def; + public: + constructor(ast_manager& m, symbol n): m(m), m_name(n) {} + void add(accessor& a) { m_accessors.push_back(a); a.attach(this); } + symbol const& name() const { return m_name; } + vector const& accessors() const { return m_accessors; } + vector::const_iterator begin() const { return m_accessors.begin(); } + vector::const_iterator end() const { 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; + }; + + class def { + ast_manager& m; + util& m_util; + symbol m_name; + unsigned m_class_id; + sort_ref_vector m_params; + mutable sort_ref m_sort; + 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_params(m, num_params, params), + m_sort(m) + {} + 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; + vector const& constructors() const { return m_constructors; } + vector::const_iterator begin() const { return m_constructors.begin(); } + vector::const_iterator end() const { return m_constructors.end(); } + sort_ref_vector const& params() const { return m_params; } + util& u() const { return m_util; } + }; + + 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; + 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& add(symbol const& name, unsigned n, sort * const * params); + + void del(symbol const& d); + + def const& get_def(sort* s) const { def* d = 0; VERIFY(m_defs.find(datatype_name(s), d)); return *d; } + + 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); + + 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; + + + 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; + 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); + func_decl * get_constructor(sort * ty, unsigned c_id); + + friend class decl::plugin; + + bool is_recursive_core(sort * s) const; + sort_size get_datatype_size(sort* s0); + bool is_well_founded(unsigned num_types, sort* const* sorts); + def const& get_def(sort* s) const; + void get_subsorts(sort* s, ptr_vector& sorts) const; + + public: + util(ast_manager & m); + ~util(); + ast_manager & get_manager() const { return m; } + 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_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); + 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); + 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(); + void display_datatype(sort *s, std::ostream& strm); + bool is_fully_interp(sort * s) const; + sort_ref_vector datatype_params(sort * s) const; + }; + +}; + +#endif /* DATATYPE_DECL_PLUGIN_H_ */ + diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 4dfd69ddd..c1ef61938 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -35,6 +35,7 @@ void arith_rewriter::updt_local_params(params_ref const & _p) { m_mul2power = p.mul_to_power(); m_elim_rem = p.elim_rem(); m_expand_tan = p.expand_tan(); + m_expand_eqs = p.expand_eqs(); set_sort_sums(p.sort_sums()); } @@ -454,7 +455,20 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin st = BR_DONE; } } - if (st == BR_DONE && arg1 == orig_arg1 && arg2 == orig_arg2) { + if (kind == EQ && m_expand_eqs) { + result = m().mk_and(m_util.mk_le(arg1, arg2), m_util.mk_ge(arg1, arg2)); + return BR_REWRITE2; + } + else if (is_numeral(arg2, a2) && is_neg_poly(arg1, new_arg1)) { + a2.neg(); + new_arg2 = m_util.mk_numeral(a2, m_util.is_int(new_arg1)); + switch (kind) { + case LE: result = m_util.mk_ge(new_arg1, new_arg2); return BR_DONE; + case GE: result = m_util.mk_le(new_arg1, new_arg2); return BR_DONE; + case EQ: result = m_util.mk_eq(new_arg1, new_arg2); return BR_DONE; + } + } + else if (st == BR_DONE && arg1 == orig_arg1 && arg2 == orig_arg2) { // Nothing new; return BR_FAILED to avoid rewriting loops. return BR_FAILED; } @@ -494,6 +508,56 @@ br_status arith_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result return mk_le_ge_eq_core(arg1, arg2, EQ, result); } +expr_ref arith_rewriter::neg_monomial(expr* e) const { + expr_ref_vector args(m()); + rational a1; + if (is_app(e) & m_util.is_mul(e)) { + if (is_numeral(to_app(e)->get_arg(0), a1)) { + if (!a1.is_minus_one()) { + args.push_back(m_util.mk_numeral(-a1, m_util.is_int(e))); + } + args.append(to_app(e)->get_num_args() - 1, to_app(e)->get_args() + 1); + } + else { + args.push_back(m_util.mk_numeral(rational(-1), m_util.is_int(e))); + args.append(to_app(e)->get_num_args(), to_app(e)->get_args()); + } + } + else { + args.push_back(m_util.mk_numeral(rational(-1), m_util.is_int(e))); + args.push_back(e); + } + if (args.size() == 1) { + return expr_ref(args.back(), m()); + } + else { + return expr_ref(m_util.mk_mul(args.size(), args.c_ptr()), m()); + } +} + +bool arith_rewriter::is_neg_poly(expr* t, expr_ref& neg) const { + rational r; + if (m_util.is_mul(t) && is_numeral(to_app(t)->get_arg(0), r) && r.is_neg()) { + neg = neg_monomial(t); + return true; + } + + if (!m_util.is_add(t)) { + return false; + } + expr * t2 = to_app(t)->get_arg(0); + + if (m_util.is_mul(t2) && is_numeral(to_app(t2)->get_arg(0), r) && r.is_neg()) { + expr_ref_vector args1(m()); + for (expr* e1 : *to_app(t)) { + args1.push_back(neg_monomial(e1)); + } + neg = m_util.mk_add(args1.size(), args1.c_ptr()); + return true; + } + return false; +} + bool arith_rewriter::is_anum_simp_target(unsigned num_args, expr * const * args) { if (!m_anum_simp) return false; diff --git a/src/ast/rewriter/arith_rewriter.h b/src/ast/rewriter/arith_rewriter.h index 5d9fb1d66..352cb5a6c 100644 --- a/src/ast/rewriter/arith_rewriter.h +++ b/src/ast/rewriter/arith_rewriter.h @@ -55,6 +55,7 @@ class arith_rewriter : public poly_rewriter { bool m_push_to_real; bool m_anum_simp; bool m_elim_rem; + bool m_expand_eqs; unsigned m_max_degree; void get_coeffs_gcd(expr * t, numeral & g, bool & first, unsigned & num_consts); @@ -88,6 +89,8 @@ class arith_rewriter : public poly_rewriter { bool is_2_pi_integer_offset(expr * t, expr * & m); bool is_pi_integer(expr * t); bool is_pi_integer_offset(expr * t, expr * & m); + bool is_neg_poly(expr* e, expr_ref& neg) const; + expr_ref neg_monomial(expr * e) const; expr * mk_sin_value(rational const & k); app * mk_sqrt(rational const & k); diff --git a/src/ast/rewriter/arith_rewriter_params.pyg b/src/ast/rewriter/arith_rewriter_params.pyg index 8a41d838d..94ada1b6d 100644 --- a/src/ast/rewriter/arith_rewriter_params.pyg +++ b/src/ast/rewriter/arith_rewriter_params.pyg @@ -12,4 +12,5 @@ def_module_params(module_name='rewriter', ("arith_lhs", BOOL, False, "all monomials are moved to the left-hand-side, and the right-hand-side is just a constant."), ("elim_to_real", BOOL, False, "eliminate to_real from arithmetic predicates that contain only integers."), ("push_to_real", BOOL, True, "distribute to_real over * and +."), + ("expand_eqs", BOOL, False, "expand equalities into two inequalities"), ("elim_rem", BOOL, False, "replace (rem x y) with (ite (>= y 0) (mod x y) (- (mod x y)))."))) diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp index 6ecf26bd8..fb2004c77 100644 --- a/src/smt/asserted_formulas.cpp +++ b/src/smt/asserted_formulas.cpp @@ -123,6 +123,8 @@ void asserted_formulas::set_eliminate_and(bool flag) { p.set_bool("arith_lhs", true); p.set_bool("sort_sums", true); p.set_bool("rewrite_patterns", true); + p.set_bool("expand_eqs", m_params.m_arith_expand_eqs); + p.set_bool("gcd_rounding", true); m_rewriter.updt_params(p); flush_cache(); } diff --git a/src/smt/params/theory_arith_params.cpp b/src/smt/params/theory_arith_params.cpp index ab80f0c67..9b8aa9b81 100644 --- a/src/smt/params/theory_arith_params.cpp +++ b/src/smt/params/theory_arith_params.cpp @@ -18,6 +18,7 @@ Revision History: --*/ #include "smt/params/theory_arith_params.h" #include "smt/params/smt_params_helper.hpp" +#include "ast/rewriter/arith_rewriter_params.hpp" void theory_arith_params::updt_params(params_ref const & _p) { smt_params_helper p(_p); @@ -36,6 +37,8 @@ void theory_arith_params::updt_params(params_ref const & _p) { m_arith_bound_prop = static_cast(p.arith_propagation_mode()); m_arith_dump_lemmas = p.arith_dump_lemmas(); m_arith_reflect = p.arith_reflect(); + arith_rewriter_params ap(_p); + m_arith_expand_eqs = ap.expand_eqs(); } diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index 806d6706b..beb1acf63 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -437,10 +437,7 @@ namespace smt { ctx.set_conflict(ctx.mk_justification(ext_theory_conflict_justification(get_id(), r, 0, 0, m_used_eqs.size(), m_used_eqs.c_ptr()))); TRACE("occurs_check", tout << "occurs_check: true\n"; - enode_pair_vector::const_iterator it = m_used_eqs.begin(); - enode_pair_vector::const_iterator end = m_used_eqs.end(); - for(; it != end; ++it) { - enode_pair const & p = *it; + for (enode_pair const& p : m_used_eqs) { tout << "eq: #" << p.first->get_owner_id() << " #" << p.second->get_owner_id() << "\n"; tout << mk_bounded_pp(p.first->get_owner(), get_manager()) << " " << mk_bounded_pp(p.second->get_owner(), get_manager()) << "\n"; }); @@ -613,11 +610,9 @@ namespace smt { d1->m_constructor = d2->m_constructor; } } - ptr_vector::iterator it = d2->m_recognizers.begin(); - ptr_vector::iterator end = d2->m_recognizers.end(); - for (; it != end; ++it) - if (*it) - add_recognizer(v1, *it); + for (enode* e : d2->m_recognizers) + if (e) + add_recognizer(v1, e); } void theory_datatype::unmerge_eh(theory_var v1, theory_var v2) { diff --git a/src/util/symbol_table.h b/src/util/symbol_table.h index ea848d991..818cb7584 100644 --- a/src/util/symbol_table.h +++ b/src/util/symbol_table.h @@ -182,29 +182,20 @@ public: } void append(symbol_table const& other) { - typename sym_table::iterator it = other.m_sym_table.begin(); - typename sym_table::iterator end = other.m_sym_table.end(); - - for (; it != end; ++it) { - insert((*it).m_key, (*it).m_data); + for (auto const& kv : other.m_sym_table) { + insert(kv.m_key, kv.m_data); } } void get_range(vector& range) const { - typename sym_table::iterator it = m_sym_table.begin(); - typename sym_table::iterator end = m_sym_table.end(); - - for (; it != end; ++it) { - range.push_back((*it).m_data); + for (auto kv : m_sym_table) { + range.push_back(kv.m_data); } } void get_dom(svector& dom) const { - typename sym_table::iterator it = m_sym_table.begin(); - typename sym_table::iterator end = m_sym_table.end(); - - for (; it != end; ++it) { - dom.push_back((*it).m_key); + for (auto kv : m_sym_table) { + dom.push_back(kv.m_key); } } };