diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 1452a037e..0b5f151be 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -3640,7 +3640,7 @@ def BitVecs(names, bv, ctx=None): >>> Product(x, y, z) 1*x*y*z >>> simplify(Product(x, y, z)) - x*y*z + z*x*y """ ctx = _get_ctx(ctx) if isinstance(names, str): @@ -7647,7 +7647,7 @@ def simplify(a, *arguments, **keywords): >>> simplify(x + 1 + y + x + 1) 2 + 2*x + y >>> simplify((x + 1)*(y + 1), som=True) - 1 + x + y + x*y + 1 + x + y + y*x >>> simplify(Distinct(x, y, 1), blast_distinct=True) And(Not(x == y), Not(x == 1), Not(y == 1)) >>> simplify(And(x == 0, y == 1), elim_and=True) diff --git a/src/ast/datatype_decl_plugin2.cpp b/src/ast/datatype_decl_plugin2.cpp index 8969e02a9..8233da7d9 100644 --- a/src/ast/datatype_decl_plugin2.cpp +++ b/src/ast/datatype_decl_plugin2.cpp @@ -31,6 +31,7 @@ namespace datatype { } func_decl_ref accessor::instantiate(sort_ref_vector const& ps) const { + ast_manager& m = ps.get_manager(); 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); @@ -52,8 +53,8 @@ namespace datatype { 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()); + 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()) }; @@ -293,9 +294,9 @@ namespace datatype { } for (symbol const& s : m_def_block) { def& d = *m_defs[s]; - for (constructor& c : d) { - for (accessor& a : c) { - // a.fix_range(sorts); + for (constructor* c : d) { + for (accessor* a : *c) { + a->fix_range(sorts); } } } @@ -401,9 +402,9 @@ namespace datatype { 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); + 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; @@ -438,9 +439,9 @@ namespace datatype { 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(); + 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); @@ -533,9 +534,9 @@ namespace datatype { 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(); + 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)) { @@ -562,10 +563,10 @@ namespace datatype { } ptr_vector s_add; - for (constructor const& c : d) { + 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())); + 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)); } @@ -594,10 +595,10 @@ namespace datatype { } sort* s = sorts[tid]; def const& d = get_def(s); - for (constructor const& c : d) { + for (constructor const* c : d) { bool found_nonwf = false; - for (accessor const& a : c) { - if (sort2id.find(a.range(), id) && !well_founded[id]) { + for (accessor const* a : *c) { + if (sort2id.find(a->range(), id) && !well_founded[id]) { found_nonwf = true; break; } @@ -652,8 +653,8 @@ namespace datatype { 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); + for (constructor const* c : d) { + func_decl_ref f = c->instantiate(ty); m_asts.push_back(f); r->push_back(f); } @@ -671,10 +672,10 @@ namespace datatype { 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)); + for (constructor const* c : d) { + if (c->name() == con->get_name()) { + for (accessor const* a : *c) { + res->push_back(a->instantiate(datatype)); } break; } @@ -739,9 +740,9 @@ namespace datatype { 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); + for (constructor const* c : d) { + if (c->name() == c_id) { + fn = c->instantiate(datatype); break; } } diff --git a/src/ast/datatype_decl_plugin2.h b/src/ast/datatype_decl_plugin2.h index 13e85b47f..c540b7c1c 100644 --- a/src/ast/datatype_decl_plugin2.h +++ b/src/ast/datatype_decl_plugin2.h @@ -44,22 +44,19 @@ namespace datatype { }; class accessor { - ast_manager& m; symbol m_name; - sort_ref m_range; + sort* 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(m), + accessor(symbol const& n, sort* range): m_name(n), - m_range(range, m), + m_range(range), m_index(UINT_MAX) {} - accessor(ast_manager& m, symbol const& n, unsigned index): - m(m), + accessor(symbol const& n, unsigned index): m_name(n), - m_range(m), + m_range(0), m_index(index) {} sort* range() const { return m_range; } @@ -76,17 +73,18 @@ namespace datatype { class constructor { ast_manager& m; symbol m_name; - vector m_accessors; + ptr_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); } + ~constructor(); + 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(); } - vector::iterator begin() { return m_accessors.begin(); } - vector::iterator end() { return m_accessors.end(); } + 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; } @@ -190,7 +188,7 @@ namespace datatype { param_size::size* m_sort_size; sort_ref_vector m_params; mutable sort_ref m_sort; - vector m_constructors; + 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), @@ -204,18 +202,18 @@ namespace datatype { ~def() { if (m_sort_size) m_sort_size->dec_ref(); } - void add(constructor& c) { + void add(constructor* c) { m_constructors.push_back(c); - c.attach(this); + 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(); } - vector::iterator begin() { return m_constructors.begin(); } - vector::iterator end() { return m_constructors.end(); } + 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; }