mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 12:28:44 +00:00
Code Activity

doctest fix

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-09-03 19:07:02 -07:00
parent 7b9b714979
commit 09386e43e3
3 changed files with 53 additions and 54 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/api/python/z3/z3.py
View file

@ -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)

59
src/ast/datatype_decl_plugin2.cpp
View file

@ -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<param_size::size> s_add;
for (constructor const& c : d) {
for (constructor const* c : d) {
ptr_vector<param_size::size> 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;
}
}

44
src/ast/datatype_decl_plugin2.h
View file

@ -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<accessor> m_accessors;
ptr_vector<accessor> 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<accessor> const& accessors() const { return m_accessors; }
vector<accessor>::const_iterator begin() const { return m_accessors.begin(); }
vector<accessor>::const_iterator end() const { return m_accessors.end(); }
vector<accessor>::iterator begin() { return m_accessors.begin(); }
vector<accessor>::iterator end() { return m_accessors.end(); }
ptr_vector<accessor> const& accessors() const { return m_accessors; }
ptr_vector<accessor>::const_iterator begin() const { return m_accessors.begin(); }
ptr_vector<accessor>::const_iterator end() const { return m_accessors.end(); }
ptr_vector<accessor>::iterator begin() { return m_accessors.begin(); }
ptr_vector<accessor>::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<constructor> m_constructors;
ptr_vector<constructor> 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<constructor> const& constructors() const { return m_constructors; }
vector<constructor>::const_iterator begin() const { return m_constructors.begin(); }
vector<constructor>::const_iterator end() const { return m_constructors.end(); }
vector<constructor>::iterator begin() { return m_constructors.begin(); }
vector<constructor>::iterator end() { return m_constructors.end(); }
ptr_vector<constructor> const& constructors() const { return m_constructors; }
ptr_vector<constructor>::const_iterator begin() const { return m_constructors.begin(); }
ptr_vector<constructor>::const_iterator end() const { return m_constructors.end(); }
ptr_vector<constructor>::iterator begin() { return m_constructors.begin(); }
ptr_vector<constructor>::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; }