mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

Merge branch 'master' of https://github.com/Z3Prover/z3

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-10-09 19:18:46 +01:00
commit e0db65bb1d
21 changed files with 319 additions and 137 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/c++/z3++.h
View file

@ -140,7 +140,7 @@ namespace z3 {
class context {
bool m_enable_exceptions;
Z3_context m_ctx;
static void error_handler(Z3_context /*c*/, Z3_error_code /*e*/) { /* do nothing */ }
static void Z3_API error_handler(Z3_context /*c*/, Z3_error_code /*e*/) { /* do nothing */ }
void init(config & c) {
m_ctx = Z3_mk_context_rc(c);
m_enable_exceptions = true;

3
src/ast/ast.cpp
View file

@ -471,6 +471,9 @@ bool compare_nodes(ast const * n1, ast const * n2) {
compare_arrays(to_quantifier(n1)->get_decl_sorts(),
to_quantifier(n2)->get_decl_sorts(),
to_quantifier(n1)->get_num_decls()) &&
compare_arrays(to_quantifier(n1)->get_decl_names(),
to_quantifier(n2)->get_decl_names(),
to_quantifier(n1)->get_num_decls()) &&
to_quantifier(n1)->get_expr() == to_quantifier(n2)->get_expr() &&
to_quantifier(n1)->get_weight() == to_quantifier(n2)->get_weight() &&
to_quantifier(n1)->get_num_patterns() == to_quantifier(n2)->get_num_patterns() &&

9
src/ast/expr_abstract.cpp
View file

@ -19,6 +19,7 @@ Notes:
#include "ast/expr_abstract.h"
#include "util/map.h"
#include "ast/ast_pp.h"
void expr_abstractor::operator()(unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result) {
@ -109,6 +110,9 @@ void expr_abstractor::operator()(unsigned base, unsigned num_bound, expr* const*
void expr_abstract(ast_manager& m, unsigned base, unsigned num_bound, expr* const* bound, expr* n, expr_ref& result) {
expr_abstractor abs(m);
abs(base, num_bound, bound, n, result);
TRACE("expr_abstract",
tout << expr_ref(n, m) << "\n";
tout << result << "\n";);
}
expr_ref mk_quantifier(bool is_forall, ast_manager& m, unsigned num_bound, app* const* bound, expr* n) {
@ -123,6 +127,11 @@ expr_ref mk_quantifier(bool is_forall, ast_manager& m, unsigned num_bound, app*
}
result = m.mk_quantifier(is_forall, num_bound, sorts.c_ptr(), names.c_ptr(), result);
}
TRACE("expr_abstract",
tout << expr_ref(n, m) << "\n";
for (unsigned i = 0; i < num_bound; ++i) tout << expr_ref(bound[i], m) << " ";
tout << "\n";
tout << result << "\n";);
return result;
}

10
src/ast/expr_substitution.cpp
View file

@ -16,8 +16,9 @@ Author:
Notes:
--*/
#include "ast/expr_substitution.h"
#include "util/ref_util.h"
#include "ast/expr_substitution.h"
#include "ast/ast_pp.h"
typedef obj_map<expr, proof*> expr2proof;
typedef obj_map<expr, expr_dependency*> expr2expr_dependency;
@ -56,6 +57,13 @@ expr_substitution::~expr_substitution() {
reset();
}
std::ostream& expr_substitution::display(std::ostream& out) {
for (auto & kv : m_subst) {
out << mk_pp(kv.m_key, m()) << " |-> " << mk_pp(kv.m_value, m()) << "\n";
}
return out;
}
void expr_substitution::insert(expr * c, expr * def, proof * def_pr, expr_dependency * def_dep) {
obj_map<expr, expr*>::obj_map_entry * entry = m_subst.insert_if_not_there2(c, 0);
if (entry->get_data().m_value == 0) {

3
src/ast/expr_substitution.h
View file

@ -50,6 +50,8 @@ public:
bool contains(expr * s);
void reset();
void cleanup();
std::ostream& display(std::ostream& out);
};
class scoped_expr_substitution {
@ -84,6 +86,7 @@ public:
bool find(expr * s, expr * & def, proof * & def_pr, expr_dependency * & def_dep) { return m_subst.find(s, def, def_pr, def_dep); }
bool contains(expr * s) { return m_subst.contains(s); }
void cleanup() { m_subst.cleanup(); }
std::ostream& display(std::ostream& out) { return m_subst.display(out); }
};
#endif

6
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -1180,8 +1180,6 @@ void fpa2bv_converter::mk_abs(sort * s, expr_ref & x, expr_ref & result) {
void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 2);
unsigned ebits = m_util.get_ebits(f->get_range());
unsigned sbits = m_util.get_sbits(f->get_range());
expr * x = args[0], * y = args[1];
@ -1227,8 +1225,6 @@ void fpa2bv_converter::mk_min(func_decl * f, unsigned num, expr * const * args,
void fpa2bv_converter::mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
SASSERT(num == 2);
unsigned ebits = m_util.get_ebits(f->get_range());
unsigned sbits = m_util.get_sbits(f->get_range());
expr * x = args[0], *y = args[1];
@ -3081,8 +3077,6 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const *
mk_is_nan(x, x_is_nan);
sort * fp_srt = m.get_sort(x);
unsigned ebits = m_util.get_ebits(fp_srt);
unsigned sbits = m_util.get_sbits(fp_srt);
expr_ref unspec(m);
mk_to_ieee_bv_unspecified(f, num, args, unspec);

4
src/interp/iz3mgr.h
View file

@ -96,7 +96,7 @@ class ast_r : public ast_i {
ast_r(const ast_r &other) : ast_i(other) {
_m = other._m;
_m->inc_ref(_ast);
if (_m) _m->inc_ref(_ast);
}
ast_r &operator=(const ast_r &other) {
@ -104,7 +104,7 @@ class ast_r : public ast_i {
_m->dec_ref(_ast);
_ast = other._ast;
_m = other._m;
_m->inc_ref(_ast);
if (_m) _m->inc_ref(_ast);
return *this;
}

12
src/model/model_core.cpp
View file

@ -86,18 +86,22 @@ void model_core::register_decl(func_decl * d, func_interp * fi) {
void model_core::unregister_decl(func_decl * d) {
decl2expr::obj_map_entry * ec = m_interp.find_core(d);
if (ec && ec->get_data().m_value != 0) {
m_manager.dec_ref(ec->get_data().m_key);
m_manager.dec_ref(ec->get_data().m_value);
auto k = ec->get_data().m_key;
auto v = ec->get_data().m_value;
m_interp.remove(d);
m_const_decls.erase(d);
m_manager.dec_ref(k);
m_manager.dec_ref(v);
return;
}
decl2finterp::obj_map_entry * ef = m_finterp.find_core(d);
if (ef && ef->get_data().m_value != 0) {
m_manager.dec_ref(ef->get_data().m_key);
dealloc(ef->get_data().m_value);
auto k = ef->get_data().m_key;
auto v = ef->get_data().m_value;
m_finterp.remove(d);
m_func_decls.erase(d);
m_manager.dec_ref(k);
dealloc(v);
}
}

3
src/muz/rel/tbv.cpp
View file

@ -74,8 +74,7 @@ tbv* tbv_manager::allocate(tbv const& bv) {
}
tbv* tbv_manager::allocate(uint64 val) {
tbv* v = allocate0();
for (unsigned bit = num_tbits(); bit > 0;) {
--bit;
for (unsigned bit = std::min(64u, num_tbits()); bit-- > 0;) {
if (val & (1ULL << bit)) {
set(*v, bit, BIT_1);
} else {

138
src/tactic/core/dom_simplify_tactic.cpp
View file

@ -91,21 +91,27 @@ bool expr_dominators::compute_dominators() {
unsigned iterations = 1;
while (change) {
change = false;
TRACE("simplify",
for (auto & kv : m_doms) {
tout << expr_ref(kv.m_key, m) << " |-> " << expr_ref(kv.m_value, m) << "\n";
});
SASSERT(m_post2expr.empty() || m_post2expr.back() == e);
for (unsigned i = 0; i + 1 < m_post2expr.size(); ++i) {
expr * child = m_post2expr[i];
ptr_vector<expr> const& p = m_parents[child];
SASSERT(!p.empty());
expr * new_idom = 0, *idom2 = 0;
for (unsigned j = 0; j < p.size(); ++j) {
if (!new_idom) {
m_doms.find(p[j], new_idom);
}
else if (m_doms.find(p[j], idom2)) {
new_idom = intersect(new_idom, idom2);
for (expr * pred : p) {
if (m_doms.contains(pred)) {
new_idom = !new_idom ? pred : intersect(new_idom, pred);
}
}
if (new_idom && (!m_doms.find(child, idom2) || idom2 != new_idom)) {
if (!new_idom) {
m_doms.insert(child, p[0]);
change = true;
}
else if (!m_doms.find(child, idom2) || idom2 != new_idom) {
m_doms.insert(child, new_idom);
change = true;
}
@ -130,6 +136,7 @@ bool expr_dominators::compile(expr * e) {
compute_post_order();
if (!compute_dominators()) return false;
extract_tree();
TRACE("simplify", display(tout););
return true;
}
@ -147,11 +154,31 @@ void expr_dominators::reset() {
m_root.reset();
}
std::ostream& expr_dominators::display(std::ostream& out) {
return display(out, 0, m_root);
}
std::ostream& expr_dominators::display(std::ostream& out, unsigned indent, expr* r) {
for (unsigned i = 0; i < indent; ++i) out << " ";
out << expr_ref(r, m);
if (m_tree.contains(r)) {
for (expr* child : m_tree[r]) {
if (child != r)
display(out, indent + 1, child);
}
}
out << "\n";
return out;
}
// -----------------------
// dom_simplify_tactic
dom_simplify_tactic::~dom_simplify_tactic() {
dealloc(m_simplifier);
}
tactic * dom_simplify_tactic::translate(ast_manager & m) {
return alloc(dom_simplify_tactic, m, m_simplifier->translate(m), m_params);
}
@ -183,32 +210,31 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) {
expr * c = 0, *t = 0, *e = 0;
VERIFY(m.is_ite(ite, c, t, e));
unsigned old_lvl = scope_level();
expr_ref new_c = simplify(c);
expr_ref new_c = simplify_arg(c);
if (m.is_true(new_c)) {
r = simplify(t);
r = simplify_arg(t);
}
else if (m.is_false(new_c) || !assert_expr(new_c, false)) {
r = simplify(e);
r = simplify_arg(e);
}
else {
for (expr * child : tree(ite)) {
if (is_subexpr(child, t) && !is_subexpr(child, e)) {
simplify(child);
simplify_rec(child);
}
}
pop(scope_level() - old_lvl);
expr_ref new_t = simplify(t);
expr_ref new_t = simplify_arg(t);
if (!assert_expr(new_c, true)) {
return new_t;
}
for (expr * child : tree(ite)) {
if (is_subexpr(child, e) && !is_subexpr(child, t)) {
simplify(child);
simplify_rec(child);
}
}
pop(scope_level() - old_lvl);
expr_ref new_e = simplify(e);
expr_ref new_e = simplify_arg(e);
if (c == new_c && t == new_t && e == new_e) {
r = ite;
}
@ -223,9 +249,22 @@ expr_ref dom_simplify_tactic::simplify_ite(app * ite) {
return r;
}
expr_ref dom_simplify_tactic::simplify(expr * e0) {
expr_ref dom_simplify_tactic::simplify_arg(expr * e) {
expr_ref r(m);
r = get_cached(e);
(*m_simplifier)(r);
TRACE("simplify", tout << "depth: " << m_depth << " " << mk_pp(e, m) << " -> " << r << "\n";);
return r;
}
/**
\brief simplify e recursively.
*/
expr_ref dom_simplify_tactic::simplify_rec(expr * e0) {
expr_ref r(m);
expr* e = 0;
TRACE("simplify", tout << "depth: " << m_depth << " " << mk_pp(e0, m) << "\n";);
if (!m_result.find(e0, e)) {
e = e0;
}
@ -245,12 +284,12 @@ expr_ref dom_simplify_tactic::simplify(expr * e0) {
}
else {
for (expr * child : tree(e)) {
simplify(child);
simplify_rec(child);
}
if (is_app(e)) {
m_args.reset();
for (expr* arg : *to_app(e)) {
m_args.push_back(get_cached(arg)); // TBD is cache really applied to all sub-terms?
m_args.push_back(simplify_arg(arg));
}
r = m.mk_app(to_app(e)->get_decl(), m_args.size(), m_args.c_ptr());
}
@ -281,18 +320,30 @@ expr_ref dom_simplify_tactic::simplify_and_or(bool is_and, app * e) {
};
expr_ref_vector args(m);
for (expr * arg : *e) {
for (expr * child : tree(arg)) {
if (is_subexpr_arg(child, arg)) {
simplify(child);
}
}
r = simplify(arg);
args.push_back(r);
if (!assert_expr(simplify(arg), !is_and)) {
r = is_and ? m.mk_false() : m.mk_true();
return r;
if (m_forward) {
for (expr * arg : *e) {
#define _SIMP_ARG(arg) \
for (expr * child : tree(arg)) { \
if (is_subexpr_arg(child, arg)) { \
simplify_rec(child); \
} \
} \
r = simplify_arg(arg); \
args.push_back(r); \
if (!assert_expr(r, !is_and)) { \
r = is_and ? m.mk_false() : m.mk_true(); \
return r; \
}
_SIMP_ARG(arg);
}
}
else {
for (unsigned i = e->get_num_args(); i > 0; ) {
--i;
expr* arg = e->get_arg(i);
_SIMP_ARG(arg);
}
args.reverse();
}
pop(scope_level() - old_lvl);
r = is_and ? mk_and(args) : mk_or(args);
@ -319,13 +370,15 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
change = false;
// go forwards
m_forward = true;
if (!init(g)) return;
unsigned sz = g.size();
for (unsigned i = 0; !g.inconsistent() && i < sz; ++i) {
expr_ref r = simplify(g.form(i));
expr_ref r = simplify_rec(g.form(i));
if (i < sz - 1 && !m.is_true(r) && !m.is_false(r) && !g.dep(i) && !g.proofs_enabled() && !assert_expr(r, false)) {
r = m.mk_false();
}
CTRACE("simplify", r != g.form(i), tout << r << " " << mk_pp(g.form(i), m) << "\n";);
change |= r != g.form(i);
proof* new_pr = 0;
if (g.proofs_enabled()) {
@ -336,15 +389,17 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
pop(scope_level());
// go backwards
m_forward = false;
if (!init(g)) return;
sz = g.size();
for (unsigned i = sz; !g.inconsistent() && i > 0; ) {
--i;
expr_ref r = simplify(g.form(i));
expr_ref r = simplify_rec(g.form(i));
if (i > 0 && !m.is_true(r) && !m.is_false(r) && !g.dep(i) && !g.proofs_enabled() && !assert_expr(r, false)) {
r = m.mk_false();
}
change |= r != g.form(i);
CTRACE("simplify", r != g.form(i), tout << r << " " << mk_pp(g.form(i), m) << "\n";);
proof* new_pr = 0;
if (g.proofs_enabled()) {
new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite_star(g.form(i), r, 0, 0));
@ -356,6 +411,12 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
SASSERT(scope_level() == 0);
}
/**
\brief determine if a is dominated by b.
Walk the immediate dominators of a upwards until hitting b or a term that is deeper than b.
Save intermediary results in a cache to avoid recomputations.
*/
bool dom_simplify_tactic::is_subexpr(expr * a, expr * b) {
if (a == b)
return true;
@ -364,14 +425,13 @@ bool dom_simplify_tactic::is_subexpr(expr * a, expr * b) {
if (m_subexpr_cache.find(a, b, r))
return r;
for (expr * e : tree(b)) {
if (is_subexpr(a, e)) {
m_subexpr_cache.insert(a, b, true);
return true;
}
if (get_depth(a) >= get_depth(b)) {
return false;
}
m_subexpr_cache.insert(a, b, false);
return false;
SASSERT(a != idom(a) && get_depth(idom(a)) > get_depth(a));
r = is_subexpr(idom(a), b);
m_subexpr_cache.insert(a, b, r);
return r;
}
ptr_vector<expr> const & dom_simplify_tactic::tree(expr * e) {

17
src/tactic/core/dom_simplify_tactic.h
View file

@ -48,6 +48,8 @@ private:
bool compute_dominators();
void extract_tree();
std::ostream& display(std::ostream& out, unsigned indent, expr* r);
public:
expr_dominators(ast_manager& m): m(m), m_root(m) {}
@ -55,7 +57,9 @@ public:
bool compile(unsigned sz, expr * const* es);
tree_t const& get_tree() { return m_tree; }
void reset();
expr* idom(expr *e) const { return m_doms[e]; }
std::ostream& display(std::ostream& out);
};
class dom_simplifier {
@ -83,8 +87,6 @@ class dom_simplifier {
};
class dom_simplify_tactic : public tactic {
public:
private:
ast_manager& m;
dom_simplifier* m_simplifier;
params_ref m_params;
@ -96,8 +98,10 @@ private:
unsigned m_max_depth;
ptr_vector<expr> m_empty;
obj_pair_map<expr, expr, bool> m_subexpr_cache;
bool m_forward;
expr_ref simplify(expr* t);
expr_ref simplify_rec(expr* t);
expr_ref simplify_arg(expr* t);
expr_ref simplify_ite(app * ite);
expr_ref simplify_and(app * ite) { return simplify_and_or(true, ite); }
expr_ref simplify_or(app * ite) { return simplify_and_or(false, ite); }
@ -110,6 +114,7 @@ private:
void cache(expr *t, expr* r) { m_result.insert(t, r); m_trail.push_back(r); }
ptr_vector<expr> const & tree(expr * e);
expr* idom(expr *e) const { return m_dominators.idom(e); }
unsigned scope_level() { return m_scope_level; }
void pop(unsigned n) { SASSERT(n <= m_scope_level); m_scope_level -= n; m_simplifier->pop(n); }
@ -122,10 +127,10 @@ public:
m(m), m_simplifier(s), m_params(p),
m_trail(m), m_args(m),
m_dominators(m),
m_scope_level(0), m_depth(0), m_max_depth(1024) {}
m_scope_level(0), m_depth(0), m_max_depth(1024), m_forward(true) {}
virtual ~dom_simplify_tactic() {}
virtual ~dom_simplify_tactic();
virtual tactic * translate(ast_manager & m);
virtual void updt_params(params_ref const & p) {}

1
src/util/lp/indexed_vector_instances.cpp
View file

@ -33,6 +33,7 @@ template void indexed_vector<unsigned>::resize(unsigned int);
template void indexed_vector<mpq>::set_value(const mpq&, unsigned int);
template void indexed_vector<unsigned>::set_value(const unsigned&, unsigned int);
#ifdef Z3DEBUG
template bool indexed_vector<unsigned>::is_OK() const;
template bool indexed_vector<double>::is_OK() const;
template bool indexed_vector<mpq>::is_OK() const;
template bool indexed_vector<lp::numeric_pair<mpq> >::is_OK() const;

5
src/util/mpz.cpp
View file

@ -558,14 +558,13 @@ void mpz_manager<SYNCH>::big_rem(mpz const & a, mpz const & b, mpz & c) {
template<bool SYNCH>
void mpz_manager<SYNCH>::gcd(mpz const & a, mpz const & b, mpz & c) {
if (is_small(a) && is_small(b)) {
COMPILE_TIME_ASSERT(sizeof(a.m_val) == sizeof(int));
if (is_small(a) && is_small(b) && a.m_val != INT_MIN && b.m_val != INT_MIN) {
int _a = a.m_val;
int _b = b.m_val;
if (_a < 0) _a = -_a;
if (_b < 0) _b = -_b;
unsigned r = u_gcd(_a, _b);
// Remark: r is (INT_MAX + 1)
// If a == b == INT_MIN
set(c, r);
}
else {