mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

move dominator simplifier functionality to rewriter and simplifier, move bv_bounds simplifier functionality to simplifier

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-01-27 17:11:48 -08:00
parent d4ca7e5374
commit 0f3c56213e
13 changed files with 1456 additions and 1330 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/ast/rewriter/CMakeLists.txt
View file

@ -14,6 +14,7 @@ z3_add_component(rewriter
der.cpp der.cpp
distribute_forall.cpp distribute_forall.cpp
dl_rewriter.cpp dl_rewriter.cpp
dom_simplifier.cpp
elim_bounds.cpp elim_bounds.cpp
enum2bv_rewriter.cpp enum2bv_rewriter.cpp
expr_replacer.cpp expr_replacer.cpp

566
src/ast/rewriter/bv_bounds_base.h Normal file
View file

@ -0,0 +1,566 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
bv_bounds_simplifier.h
Abstract:
Context dependent simplification for bit-vectors
Author:
Nikolaj and Nuno
--*/
#pragma once
namespace bv {
template<typename T, typename Base>
struct interval_tpl : public Base {
T l, h;
unsigned sz = 0;
bool tight = true;
interval_tpl(T const& l, T const& h, unsigned sz, bool tight = false): l(l), h(h), sz(sz), tight(tight) {}
interval_tpl() {}
bool invariant() const {
return
0 <= l && (l <= Base::bound(sz)) &&
0 <= h && (h <= Base::bound(sz)) &&
(!is_wrapped() || l != h + 1);
}
bool is_full() const {
return l == 0 && h == Base::bound(sz);
}
bool is_wrapped() const { return l > h; }
bool is_singleton() const { return l == h; }
bool operator==(const interval_tpl<T, Base>& b) const {
SASSERT(sz == b.sz);
return l == b.l && h == b.h && tight == b.tight;
}
bool operator!=(const interval_tpl& b) const { return !(*this == b); }
bool implies(const interval_tpl<T, Base>& b) const {
if (b.is_full())
return true;
else if (is_full())
return false;
else if (is_wrapped())
// l >= b.l >= b.h >= h
return b.is_wrapped() && h <= b.h && l >= b.l;
else if (b.is_wrapped())
// b.l > b.h >= h >= l
// h >= l >= b.l > b.h
return h <= b.h || l >= b.l;
else
return l >= b.l && h <= b.h;
}
/// return false if intersection is unsat
bool intersect(const interval_tpl<T, Base>& b, interval_tpl& result) const {
if (is_full() || *this == b) {
result = b;
return true;
}
if (b.is_full()) {
result = *this;
return true;
}
if (is_wrapped()) {
if (b.is_wrapped()) {
if (h >= b.l)
result = b;
else if (b.h >= l)
result = *this;
else
result = interval_tpl(std::max(l, b.l), std::min(h, b.h), sz);
}
else
return b.intersect(*this, result);
}
else if (b.is_wrapped()) {
// ... b.h ... l ... h ... b.l ..
if (h < b.l && l > b.h)
return false;
// ... l ... b.l ... h ...
if (h >= b.l && l <= b.h)
result = b;
else if (h >= b.l)
result = interval_tpl(b.l, h, sz);
else {
// ... l .. b.h .. h .. b.l ...
SASSERT(l <= b.h);
result = interval_tpl(l, std::min(h, b.h), sz);
}
} else {
if (l > b.h || h < b.l)
return false;
// 0 .. l.. l' ... h ... h'
result = interval_tpl(std::max(l, b.l), std::min(h, b.h), sz, tight && b.tight);
}
return true;
}
/// return false if negation is empty
bool negate(interval_tpl<T, Base>& result) const {
if (!tight)
result = interval_tpl(Base::zero(), Base::bound(sz), sz, true);
else if (is_full())
return false;
else if (l == 0 && Base::bound(sz) == h)
result = interval_tpl(Base::zero(), Base::bound(sz), sz);
else if (l == 0)
result = interval_tpl(h + 1, Base::bound(sz), sz);
else if (Base::bound(sz) == h)
result = interval_tpl(Base::zero(), l - 1, sz);
else
result = interval_tpl(h + 1, l - 1, sz);
return true;
}
};
struct rinterval_base {
static rational bound(unsigned sz) {
return rational::power_of_two(sz) - 1;
}
static rational zero() { return rational::zero(); }
};
struct rinterval : public interval_tpl<rational, rinterval_base> {
rinterval(rational const& l, rational const& h, unsigned sz, bool tight = false) {
this->l = l; this->h = h; this->sz = sz; this->tight = tight;
}
rinterval() { l = 0; h = 0; tight = true; }
};
struct iinterval_base {
static uint64_t uMaxInt(unsigned sz) {
SASSERT(sz <= 64);
return ULLONG_MAX >> (64u - sz);
}
static uint64_t bound(unsigned sz) { return uMaxInt(sz); }
static uint64_t zero() { return 0; }
};
struct iinterval : public interval_tpl<uint64_t, iinterval_base> {
iinterval(uint64_t l, uint64_t h, unsigned sz, bool tight = false) {
this->l = l; this->h = h; this->sz = sz; this->tight = tight;
}
iinterval() { l = 0; h = 0; sz = 0; tight = true; }
};
struct interval {
bool is_small = true;
iinterval i;
rinterval r;
interval() {}
interval(rational const& l, rational const& h, unsigned sz, bool tight = false) {
if (sz <= 64) {
is_small = true;
i.l = l.get_uint64();
i.h = h.get_uint64();
i.tight = tight;
i.sz = sz;
}
else {
is_small = false;
r.l = l;
r.h = h;
r.tight = tight;
r.sz = sz;
}
}
unsigned size() const {
return is_small ? i.sz : r.sz;
}
bool negate(interval& result) const {
result.is_small = is_small;
if (is_small)
return i.negate(result.i);
else
return r.negate(result.r);
}
bool intersect(interval const& b, interval & result) const {
result.is_small = is_small;
SASSERT(b.is_small == is_small);
if (is_small)
return i.intersect(b.i, result.i);
else
return r.intersect(b.r, result.r);
}
bool operator==(interval const& other) const {
SASSERT(is_small == other.is_small);
return is_small ? i == other.i : r == other.r;
}
bool operator!=(interval const& other) const {
return !(*this == other);
}
bool is_singleton() const { return is_small ? i.is_singleton() : r.is_singleton(); }
bool is_full() const { return is_small ? i.is_full() : r.is_full(); }
bool tight() const { return is_small ? i.tight : r.tight; }
bool implies(const interval& b) const {
SASSERT(is_small == b.is_small);
return is_small ? i.implies(b.i) : r.implies(b.r);
}
rational lo() const { return is_small ? rational(i.l, rational::ui64()) : r.l; }
rational hi() const { return is_small ? rational(i.h, rational::ui64()) : r.h; }
};
inline std::ostream& operator<<(std::ostream& o, const interval& I) {
if (I.is_small)
return o << "[" << I.i.l << ", " << I.i.h << "]";
else
return o << "[" << I.r.l << ", " << I.r.h << "]";
}
struct undo_bound {
expr* e = nullptr;
interval b;
bool fresh = false;
undo_bound(expr* e, const interval& b, bool fresh) : e(e), b(b), fresh(fresh) {}
};
struct bv_bounds_base {
typedef obj_map<expr, interval> map;
typedef obj_map<expr, bool> expr_set;
typedef obj_map<expr, unsigned> expr_cnt;
ast_manager& m;
bv_util m_bv;
vector<undo_bound> m_scopes;
svector<expr_set*> m_expr_vars;
svector<expr_cnt*> m_bound_exprs;
map m_bound;
bool m_propagate_eq = false;
ptr_vector<expr> m_args;
bv_bounds_base(ast_manager& m):m(m), m_bv(m) {}
virtual ~bv_bounds_base() {
for (auto* e : m_expr_vars)
dealloc(e);
for (auto* b : m_bound_exprs)
dealloc(b);
}
bool is_bound(expr *e, expr*& v, interval& b) const {
rational r;
expr *lhs = nullptr, *rhs = nullptr;
unsigned sz;
if (m_bv.is_bv_ule(e, lhs, rhs)) {
if (m_bv.is_numeral(lhs, r, sz)) { // C ule x <=> x uge C
if (m_bv.is_numeral(rhs))
return false;
b = interval(r, rational::power_of_two(sz) - 1, sz, true);
v = rhs;
return true;
}
if (m_bv.is_numeral(rhs, r, sz)) { // x ule C
b = interval(rational::zero(), r, sz, true);
v = lhs;
return true;
}
// TBD: x + s <= x + q
// x + s <= x
// x <= x + q
}
else if (m_bv.is_bv_sle(e, lhs, rhs)) {
if (m_bv.is_numeral(lhs, r, sz)) { // C sle x <=> x sge C
if (m_bv.is_numeral(rhs))
return false;
b = interval(r, rational::power_of_two(sz-1) - 1, sz, true);
v = rhs;
return true;
}
if (m_bv.is_numeral(rhs, r, sz)) { // x sle C
b = interval(rational::power_of_two(sz-1), r, sz, true);
v = lhs;
return true;
}
// TBD: other cases for forbidden intervals
}
else if (m.is_eq(e, lhs, rhs)) {
if (m_bv.is_numeral(rhs))
std::swap(lhs, rhs);
if (m_bv.is_numeral(rhs))
return false;
if (m_bv.is_numeral(lhs, r, sz)) {
unsigned lo, hi;
expr* rhs2;
if (m_bv.is_extract(rhs, lo, hi, rhs2) && r == 0) {
unsigned sz2 = m_bv.get_bv_size(rhs2);
if (sz2 - 1 == hi) {
b = interval(rational::zero(), rational::power_of_two(lo) - 1, sz2, false);
v = rhs2;
return true;
}
}
b = interval(r, r, sz, true);
v = rhs;
return true;
}
}
return false;
}
bool assert_expr_core(expr * t, bool sign) {
while (m.is_not(t, t))
sign = !sign;
interval b;
expr* t1;
if (is_bound(t, t1, b)) {
SASSERT(m_bv.get_bv_size(t1) == b.size());
SASSERT(!m_bv.is_numeral(t1));
if (sign && !b.negate(b))
return false;
TRACE("bv", tout << (sign?"(not ":"") << mk_pp(t, m) << (sign ? ")" : "") << ": " << mk_pp(t1, m) << " in " << b << "\n";);
map::obj_map_entry* e = m_bound.find_core(t1);
if (e) {
interval& old = e->get_data().m_value;
interval intr;
if (!old.intersect(b, intr))
return false;
if (old == intr)
return true;
m_scopes.push_back(undo_bound(t1, old, false));
old = intr;
SASSERT(old.size() == m_bv.get_bv_size(t1));
}
else {
SASSERT(b.size() == m_bv.get_bv_size(t1));
m_bound.insert(t1, b);
m_scopes.push_back(undo_bound(t1, interval(), true));
}
}
return true;
}
//
// x + q <= s <=> x not in [s - q + 1, -q[
// <=> x in [-q, s - q], s != -1
//
// x in [lo, hi]
// q = -lo
// hi = s + lo => s = hi - lo
// hi - lo != -1
//
expr_ref mk_bound(expr* t, rational const& lo, rational const& hi) {
sort* s = t->get_sort();
if (lo == hi + 1)
return expr_ref(m.mk_true(), m);
else
return expr_ref(m_bv.mk_ule(m_bv.mk_bv_add(t, m_bv.mk_numeral(-lo, s)), m_bv.mk_numeral(hi - lo, s)), m);
}
//
// use interval information to rewrite sub-terms x to (0 ++ x[hi:0])
// in other words, identify leading 0s.
//
bool zero_patch(expr* t, expr_ref& result) {
if (!is_app(t))
return false;
if (m_bv.is_extract(t))
return false;
m_args.reset();
bool simplified = false;
interval b;
for (expr* arg : *to_app(t)) {
if (!m_bv.is_bv(arg)) {
m_args.push_back(arg);
continue;
}
if (!m_bv.is_extract(arg) && m_bound.find(arg, b)) {
unsigned num_bits = b.hi().get_num_bits();
unsigned bv_size = m_bv.get_bv_size(arg);
if (0 < num_bits && num_bits < bv_size) {
m_args.push_back(m_bv.mk_concat(m_bv.mk_zero(bv_size - num_bits),
m_bv.mk_extract(num_bits - 1, 0, arg)));
simplified = true;
}
else
m_args.push_back(arg);
}
else
m_args.push_back(arg);
}
if (simplified) {
result = m.mk_app(to_app(t)->get_decl(), m_args);
return true;
}
return false;
}
bool simplify_core(expr* t, expr_ref& result) {
expr* t1;
interval b;
if (m_bound.find(t, b) && b.is_singleton()) {
result = m_bv.mk_numeral(b.lo(), m_bv.get_bv_size(t));
return true;
}
if (zero_patch(t, result))
return result;
if (!m.is_bool(t))
return false;
bool sign = false;
while (m.is_not(t, t))
sign = !sign;
if (!is_bound(t, t1, b))
return false;
if (sign && b.tight()) {
sign = false;
if (!b.negate(b)) {
result = m.mk_false();
return true;
}
}
interval ctx, intr;
result = nullptr;
if (b.is_full() && b.tight())
result = m.mk_true();
else if (!m_bound.find(t1, ctx)) {
}
else if (ctx.implies(b))
result = m.mk_true();
else if (!b.intersect(ctx, intr))
result = m.mk_false();
else if (m_propagate_eq && intr.is_singleton())
result = m.mk_eq(t1, m_bv.mk_numeral(intr.lo(), t1->get_sort()));
else if (false && intr != b)
result = mk_bound(t1, intr.lo(), intr.hi());
else {
TRACE("bv", tout << mk_pp(t, m) << " b: " << b << " ctx: " << ctx << " intr " << intr << "\n");
}
CTRACE("bv", result, tout << mk_pp(t, m) << " " << b << " (ctx: " << ctx << ") (intr: " << intr << "): " << result << "\n";);
if (sign && result)
result = m.mk_not(result);
return result != nullptr;
}
// check if t contains v
ptr_vector<expr> todo;
bool contains(expr* t, expr* v) {
ast_fast_mark1 mark;
todo.push_back(t);
while (!todo.empty()) {
t = todo.back();
todo.pop_back();
if (mark.is_marked(t))
continue;
if (t == v) {
todo.reset();
return true;
}
mark.mark(t);
if (!is_app(t))
continue;
app* a = to_app(t);
todo.append(a->get_num_args(), a->get_args());
}
return false;
}
bool contains_bound(expr* t) {
ast_fast_mark1 mark1;
ast_fast_mark2 mark2;
todo.push_back(t);
while (!todo.empty()) {
t = todo.back();
todo.pop_back();
if (mark1.is_marked(t)) {
continue;
}
mark1.mark(t);
if (!is_app(t)) {
continue;
}
interval b;
expr* e;
if (is_bound(t, e, b)) {
if (mark2.is_marked(e)) {
todo.reset();
return true;
}
mark2.mark(e);
if (m_bound.contains(e)) {
todo.reset();
return true;
}
}
app* a = to_app(t);
todo.append(a->get_num_args(), a->get_args());
}
return false;
}
void pop_core(unsigned num_scopes) {
TRACE("bv", tout << "pop: " << num_scopes << "\n";);
if (m_scopes.empty())
return;
unsigned target = m_scopes.size() - num_scopes;
if (target == 0) {
m_bound.reset();
m_scopes.reset();
return;
}
for (unsigned i = m_scopes.size(); i-- > target; ) {
undo_bound& undo = m_scopes[i];
SASSERT(m_bound.contains(undo.e));
if (undo.fresh)
m_bound.erase(undo.e);
else
m_bound.insert(undo.e, undo.b);
}
m_scopes.shrink(target);
}
};
}

325
src/ast/rewriter/dom_simplifier.cpp Normal file
View file

@ -0,0 +1,325 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
dom_simplifier.cpp
Abstract:
Dominator-based context simplifer.
Author:
Nikolaj and Nuno
--*/
#include "ast/ast_util.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "ast/rewriter/dom_simplifier.h"
/**
\brief compute a post-order traversal for e.
Also populate the set of parents
*/
void expr_dominators::compute_post_order() {
unsigned post_num = 0;
SASSERT(m_post2expr.empty());
SASSERT(m_expr2post.empty());
ast_mark mark;
ptr_vector<expr> todo;
todo.push_back(m_root);
while (!todo.empty()) {
expr* e = todo.back();
if (mark.is_marked(e)) {
todo.pop_back();
continue;
}
if (is_app(e)) {
app* a = to_app(e);
bool done = true;
for (expr* arg : *a) {
if (!mark.is_marked(arg)) {
todo.push_back(arg);
done = false;
}
}
if (done) {
mark.mark(e, true);
m_expr2post.insert(e, post_num++);
m_post2expr.push_back(e);
todo.pop_back();
for (expr* arg : *a) {
add_edge(m_parents, arg, a);
}
}
}
else {
mark.mark(e, true);
todo.pop_back();
}
}
}
expr* expr_dominators::intersect(expr* x, expr * y) {
unsigned n1 = m_expr2post[x];
unsigned n2 = m_expr2post[y];
while (n1 != n2) {
if (n1 < n2) {
x = m_doms[x];
n1 = m_expr2post[x];
}
else if (n1 > n2) {
y = m_doms[y];
n2 = m_expr2post[y];
}
}
SASSERT(x == y);
return x;
}
bool expr_dominators::compute_dominators() {
expr * e = m_root;
SASSERT(m_doms.empty());
m_doms.insert(e, e);
bool change = true;
unsigned iterations = 1;
while (change) {
change = false;
TRACE("simplify",
for (auto & kv : m_doms) {
tout << mk_bounded_pp(kv.m_key, m) << " |-> " << mk_bounded_pp(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];
expr * new_idom = nullptr, *idom2 = nullptr;
for (expr * pred : p) {
if (m_doms.contains(pred)) {
new_idom = !new_idom ? pred : intersect(new_idom, pred);
}
}
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;
}
}
iterations *= 2;
if (change && iterations > m_post2expr.size()) {
return false;
}
}
return true;
}
void expr_dominators::extract_tree() {
for (auto const& kv : m_doms) {
add_edge(m_tree, kv.m_value, kv.m_key);
}
}
bool expr_dominators::compile(expr * e) {
reset();
m_root = e;
compute_post_order();
if (!compute_dominators()) return false;
extract_tree();
TRACE("simplify", display(tout););
return true;
}
bool expr_dominators::compile(unsigned sz, expr * const* es) {
expr_ref e(m.mk_and(sz, es), m);
return compile(e);
}
void expr_dominators::reset() {
m_expr2post.reset();
m_post2expr.reset();
m_parents.reset();
m_doms.reset();
m_tree.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 << r->get_id() << ": " << mk_bounded_pp(r, m, 1) << "\n";
if (m_tree.contains(r)) {
for (expr* child : m_tree[r]) {
if (child != r)
display(out, indent + 1, child);
}
}
return out;
}
// ---------------------
// expr_substitution_simplifier
namespace {
class expr_substitution_simplifier : public dom_simplifier {
ast_manager& m;
expr_substitution m_subst;
scoped_expr_substitution m_scoped_substitution;
obj_map<expr, unsigned> m_expr2depth;
expr_ref_vector m_trail;
// move from asserted_formulas to here..
void compute_depth(expr* e) {
ptr_vector<expr> todo;
todo.push_back(e);
while (!todo.empty()) {
e = todo.back();
unsigned d = 0;
if (m_expr2depth.contains(e)) {
todo.pop_back();
continue;
}
if (is_app(e)) {
app* a = to_app(e);
bool visited = true;
for (expr* arg : *a) {
unsigned d1 = 0;
if (m_expr2depth.find(arg, d1)) {
d = std::max(d, d1);
}
else {
visited = false;
todo.push_back(arg);
}
}
if (!visited) {
continue;
}
}
todo.pop_back();
m_expr2depth.insert(e, d + 1);
}
}
bool is_gt(expr* lhs, expr* rhs) {
if (lhs == rhs) {
return false;
}
if (m.is_value(rhs)) {
return true;
}
SASSERT(is_ground(lhs) && is_ground(rhs));
if (depth(lhs) > depth(rhs)) {
return true;
}
if (depth(lhs) == depth(rhs) && is_app(lhs) && is_app(rhs)) {
app* l = to_app(lhs);
app* r = to_app(rhs);
if (l->get_decl()->get_id() != r->get_decl()->get_id()) {
return l->get_decl()->get_id() > r->get_decl()->get_id();
}
if (l->get_num_args() != r->get_num_args()) {
return l->get_num_args() > r->get_num_args();
}
for (unsigned i = 0; i < l->get_num_args(); ++i) {
if (l->get_arg(i) != r->get_arg(i)) {
return is_gt(l->get_arg(i), r->get_arg(i));
}
}
UNREACHABLE();
}
return false;
}
unsigned depth(expr* e) { return m_expr2depth[e]; }
public:
expr_substitution_simplifier(ast_manager& m): m(m), m_subst(m), m_scoped_substitution(m_subst), m_trail(m) {}
void updt_params(params_ref const & p) override {}
void collect_param_descrs(param_descrs& r) override {}
bool assert_expr(expr * t, bool sign) override {
expr* tt;
if (m.is_not(t, tt))
return assert_expr(tt, !sign);
if (m.is_false(t))
return sign;
if (m.is_true(t))
return !sign;
TRACE("simplify", tout << t->get_id() << ": " << mk_bounded_pp(t, m) << " " << (sign?" - neg":" - pos") << "\n";);
m_scoped_substitution.push();
if (!sign) {
update_substitution(t, nullptr);
}
else {
expr_ref nt(m.mk_not(t), m);
update_substitution(nt, nullptr);
}
return true;
}
void update_substitution(expr* n, proof* pr) {
expr* lhs, *rhs, *n1;
if (is_ground(n) && m.is_eq(n, lhs, rhs)) {
compute_depth(lhs);
compute_depth(rhs);
m_trail.push_back(lhs);
m_trail.push_back(rhs);
if (is_gt(lhs, rhs)) {
TRACE("propagate_values", tout << "insert " << mk_pp(lhs, m) << " -> " << mk_pp(rhs, m) << "\n";);
m_scoped_substitution.insert(lhs, rhs, pr);
return;
}
if (is_gt(rhs, lhs)) {
TRACE("propagate_values", tout << "insert " << mk_pp(rhs, m) << " -> " << mk_pp(lhs, m) << "\n";);
m_scoped_substitution.insert(rhs, lhs, m.mk_symmetry(pr));
return;
}
TRACE("propagate_values", tout << "incompatible " << mk_pp(n, m) << "\n";);
}
if (m.is_not(n, n1)) {
m_scoped_substitution.insert(n1, m.mk_false(), m.mk_iff_false(pr));
}
else {
m_scoped_substitution.insert(n, m.mk_true(), m.mk_iff_true(pr));
}
}
void operator()(expr_ref& r) override { r = m_scoped_substitution.find(r); }
void pop(unsigned num_scopes) override { m_scoped_substitution.pop(num_scopes); }
unsigned scope_level() const override { return m_scoped_substitution.scope_level(); }
dom_simplifier * translate(ast_manager & m) override {
SASSERT(m_subst.empty());
return alloc(expr_substitution_simplifier, m);
}
};
}
dom_simplifier* mk_expr_substitution_simplifier(ast_manager& m) {
return alloc(expr_substitution_simplifier, m);
}

86
src/ast/rewriter/dom_simplifier.h Normal file
View file

@ -0,0 +1,86 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
dom_simplifier.h
Abstract:
Dominator-based context simplifer.
Author:
Nikolaj and Nuno
--*/
#pragma once
#include "ast/ast.h"
#include "ast/expr_substitution.h"
#include "util/obj_pair_hashtable.h"
class expr_dominators {
public:
typedef obj_map<expr, ptr_vector<expr>> tree_t;
private:
ast_manager& m;
expr_ref m_root;
obj_map<expr, unsigned> m_expr2post; // reverse post-order number
ptr_vector<expr> m_post2expr;
tree_t m_parents;
obj_map<expr, expr*> m_doms;
tree_t m_tree;
void add_edge(tree_t& tree, expr * src, expr* dst) {
tree.insert_if_not_there(src, ptr_vector<expr>()).push_back(dst);
}
void compute_post_order();
expr* intersect(expr* x, expr * y);
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) {}
bool compile(expr * e);
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 {
public:
virtual ~dom_simplifier() = default;
/**
\brief assert_expr performs an implicit push
*/
virtual bool assert_expr(expr * t, bool sign) = 0;
/**
\brief apply simplification.
*/
virtual void operator()(expr_ref& r) = 0;
/**
\brief pop scopes accumulated from assertions.
*/
virtual void pop(unsigned num_scopes) = 0;
virtual dom_simplifier * translate(ast_manager & m) = 0;
virtual unsigned scope_level() const = 0;
virtual void updt_params(params_ref const & p) = 0;
virtual void collect_param_descrs(param_descrs& r) = 0;
};
dom_simplifier* mk_expr_substitution_simplifier(ast_manager& m);

2
src/ast/simplifiers/CMakeLists.txt
View file

@ -4,10 +4,12 @@ z3_add_component(simplifiers
bound_manager.cpp bound_manager.cpp
bound_propagator.cpp bound_propagator.cpp
bound_simplifier.cpp bound_simplifier.cpp
bv_bounds_simplifier.cpp
bv_slice.cpp bv_slice.cpp
card2bv.cpp card2bv.cpp
demodulator_simplifier.cpp demodulator_simplifier.cpp
dependent_expr_state.cpp dependent_expr_state.cpp
dominator_simplifier.cpp
distribute_forall.cpp distribute_forall.cpp
elim_unconstrained.cpp elim_unconstrained.cpp
eliminate_predicates.cpp eliminate_predicates.cpp

65
src/ast/simplifiers/bv_bounds_simplifier.cpp Normal file
View file

@ -0,0 +1,65 @@
/*++
Copyright (c) 2022 Microsoft Corporation
Module Name:
bv_bounds_simplifier.h
Author:
Nikolaj Bjorner (nbjorner) 2023-01-27
--*/
#include "ast/simplifiers/bv_bounds_simplifier.h"
#include "ast/simplifiers/dominator_simplifier.h"
#include "ast/rewriter/bv_bounds_base.h"
#include "ast/rewriter/dom_simplifier.h"
class dom_bv_bounds_simplifier : public dom_simplifier, public bv::bv_bounds_base {
params_ref m_params;
public:
dom_bv_bounds_simplifier(ast_manager& m, params_ref const& p) : bv_bounds_base(m), m_params(p) {
updt_params(p);
}
~dom_bv_bounds_simplifier() override {
}
void updt_params(params_ref const & p) override {
m_propagate_eq = p.get_bool("propagate_eq", false);
}
void collect_param_descrs(param_descrs& r) override {
r.insert("propagate-eq", CPK_BOOL, "propagate equalities from inequalities", "false");
}
bool assert_expr(expr * t, bool sign) override {
return assert_expr_core(t, sign);
}
void operator()(expr_ref& r) override {
expr_ref result(m);
simplify_core(r, result);
if (result)
r = result;
}
void pop(unsigned num_scopes) override {
pop_core(num_scopes);
}
dom_simplifier * translate(ast_manager & m) override {
return alloc(dom_bv_bounds_simplifier, m, m_params);
}
unsigned scope_level() const override {
return m_scopes.size();
}
};
dependent_expr_simplifier* mk_bv_bounds_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& s) {
return alloc(dominator_simplifier, m, s, alloc(dom_bv_bounds_simplifier, m, p), p);
}

18
src/ast/simplifiers/bv_bounds_simplifier.h Normal file
View file

@ -0,0 +1,18 @@
/*++
Copyright (c) 2022 Microsoft Corporation
Module Name:
bv_bounds_simplifier.h
Author:
Nikolaj Bjorner (nbjorner) 2023-01-27
--*/
#pragma once
#include "ast/simplifiers/dependent_expr_state.h"
dependent_expr_simplifier * mk_bv_bounds_simplifier(ast_manager & m, params_ref const & p, dependent_expr_state& fmls);

303
src/ast/simplifiers/dominator_simplifier.cpp Normal file
View file

@ -0,0 +1,303 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
dominator_simplifier.cpp
Abstract:
Dominator-based context simplifer.
Author:
Nikolaj and Nuno
--*/
#include "ast/ast_util.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "ast/simplifiers/dominator_simplifier.h"
dominator_simplifier::~dominator_simplifier() {
dealloc(m_simplifier);
}
expr_ref dominator_simplifier::simplify_ite(app * ite) {
expr_ref r(m);
expr * c = nullptr, *t = nullptr, *e = nullptr;
VERIFY(m.is_ite(ite, c, t, e));
unsigned old_lvl = scope_level();
expr_ref new_c = simplify_arg(c);
if (m.is_true(new_c)) {
r = simplify_arg(t);
}
else if (!assert_expr(new_c, false)) {
r = simplify_arg(e);
}
else {
for (expr * child : tree(ite))
if (is_subexpr(child, t) && !is_subexpr(child, e))
simplify_rec(child);
pop(scope_level() - old_lvl);
expr_ref new_t = simplify_arg(t);
reset_cache();
if (!assert_expr(new_c, true)) {
return new_t;
}
for (expr * child : tree(ite))
if (is_subexpr(child, e) && !is_subexpr(child, t))
simplify_rec(child);
pop(scope_level() - old_lvl);
expr_ref new_e = simplify_arg(e);
if (c == new_c && t == new_t && e == new_e) {
r = ite;
}
else if (new_t == new_e) {
r = new_t;
}
else {
TRACE("simplify", tout << new_c << "\n" << new_t << "\n" << new_e << "\n";);
r = m.mk_ite(new_c, new_t, new_e);
}
}
reset_cache();
return r;
}
expr_ref dominator_simplifier::simplify_arg(expr * e) {
expr_ref r(m);
r = get_cached(e);
(*m_simplifier)(r);
CTRACE("simplify", e != r, tout << "depth: " << m_depth << " " << mk_pp(e, m) << " -> " << r << "\n";);
return r;
}
/**
\brief simplify e recursively.
*/
expr_ref dominator_simplifier::simplify_rec(expr * e0) {
expr_ref r(m);
expr* e = nullptr;
if (!m_result.find(e0, e)) {
e = e0;
}
++m_depth;
if (m_depth > m_max_depth) {
r = e;
}
else if (m.is_ite(e)) {
r = simplify_ite(to_app(e));
}
else if (m.is_and(e)) {
r = simplify_and(to_app(e));
}
else if (m.is_or(e)) {
r = simplify_or(to_app(e));
}
else if (m.is_not(e)) {
r = simplify_not(to_app(e));
}
else {
for (expr * child : tree(e)) {
if (child != e)
simplify_rec(child);
}
if (is_app(e)) {
m_args.reset();
for (expr* arg : *to_app(e)) {
// we don't have a way to distinguish between e.g.
// ite(c, f(c), foo) (which should go to ite(c, f(true), foo))
// from and(or(x, y), f(x)), where we do a "trial" with x=false
// Trials are good for boolean formula simplification but not sound
// for fn applications.
m_args.push_back(m.is_bool(arg) ? arg : simplify_arg(arg));
}
r = m.mk_app(to_app(e)->get_decl(), m_args.size(), m_args.data());
}
else {
r = e;
}
}
CTRACE("simplify", e0 != r, tout << "depth before: " << m_depth << " " << mk_pp(e0, m) << " -> " << r << "\n";);
(*m_simplifier)(r);
cache(e0, r);
CTRACE("simplify", e0 != r, tout << "depth: " << m_depth << " " << mk_pp(e0, m) << " -> " << r << "\n";);
--m_depth;
m_subexpr_cache.reset();
return r;
}
expr_ref dominator_simplifier::simplify_and_or(bool is_and, app * e) {
expr_ref r(m);
unsigned old_lvl = scope_level();
auto is_subexpr_arg = [&](expr * child, expr * except) {
if (!is_subexpr(child, except))
return false;
for (expr * arg : *e) {
if (arg != except && is_subexpr(child, arg))
return false;
}
return true;
};
expr_ref_vector args(m);
auto simp_arg = [&](expr* 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)) {
pop(scope_level() - old_lvl);
r = is_and ? m.mk_false() : m.mk_true();
reset_cache();
return true;
}
return false;
};
if (m_forward) {
for (expr * arg : *e) {
if (simp_arg(arg))
return r;
}
}
else {
for (unsigned i = e->get_num_args(); i-- > 0; ) {
if (simp_arg(e->get_arg(i)))
return r;
}
args.reverse();
}
pop(scope_level() - old_lvl);
reset_cache();
return { is_and ? mk_and(args) : mk_or(args), m };
}
expr_ref dominator_simplifier::simplify_not(app * e) {
expr *ee;
ENSURE(m.is_not(e, ee));
unsigned old_lvl = scope_level();
expr_ref t = simplify_rec(ee);
pop(scope_level() - old_lvl);
reset_cache();
return mk_not(t);
}
bool dominator_simplifier::init() {
expr_ref_vector args(m);
for (auto i : indices())
if (!m_fmls[i].dep())
args.push_back(m_fmls[i].fml());
expr_ref fml = mk_and(args);
m_result.reset();
m_trail.reset();
return m_dominators.compile(fml);
}
void dominator_simplifier::reduce() {
m_trail.reset();
m_args.reset();
m_result.reset();
m_dominators.reset();
SASSERT(scope_level() == 0);
bool change = true;
unsigned n = 0;
m_depth = 0;
while (change && n < 10) {
change = false;
++n;
// go forwards
m_forward = true;
if (!init()) return;
for (unsigned i = qhead(); i < qtail() && !m_fmls.inconsistent(); ++i) {
auto [f, p, d] = m_fmls[i]();
if (d)
continue;
expr_ref r = simplify_rec(f);
if (!m.is_true(r) && !m.is_false(r) && !p && !assert_expr(r, false))
r = m.mk_false();
CTRACE("simplify", r != f, tout << r << " " << mk_pp(f, m) << "\n";);
change |= r != f;
proof_ref new_pr(m);
if (p) {
new_pr = m.mk_modus_ponens(p, m.mk_rewrite(f, r));
}
m_fmls.update(i, dependent_expr(m, r, new_pr, d));
}
pop(scope_level());
// go backwards
m_forward = false;
if (!init()) return;
for (unsigned i = qtail(); i-- > qhead() && !m_fmls.inconsistent(); ) {
auto [f, p, d] = m_fmls[i]();
if (d)
continue;
expr_ref r = simplify_rec(f);
if (!m.is_true(r) && !m.is_false(r) && !p && !assert_expr(r, false))
r = m.mk_false();
change |= r != f;
CTRACE("simplify", r != f, tout << r << " " << mk_pp(f, m) << "\n";);
proof_ref new_pr(m);
if (r) {
new_pr = m.mk_rewrite(f, r);
new_pr = m.mk_modus_ponens(p, new_pr);
}
m_fmls.update(i, dependent_expr(m, r, new_pr, d));
}
pop(scope_level());
}
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 dominator_simplifier::is_subexpr(expr * a, expr * b) {
if (a == b)
return true;
bool r;
if (m_subexpr_cache.find(a, b, r))
return r;
if (get_depth(a) >= get_depth(b)) {
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 & dominator_simplifier::tree(expr * e) {
if (auto p = m_dominators.get_tree().find_core(e))
return p->get_data().get_value();
return m_empty;
}

71
src/ast/simplifiers/dominator_simplifier.h Normal file
View file

@ -0,0 +1,71 @@
/*++
Copyright (c) 2023 Microsoft Corporation
Module Name:
dom_simplifier.h
--*/
#pragma once
#include "ast/ast.h"
#include "ast/expr_substitution.h"
#include "ast/rewriter/dom_simplifier.h"
#include "ast/simplifiers/dependent_expr_state.h"
#include "util/obj_pair_hashtable.h"
class dominator_simplifier : public dependent_expr_simplifier {
ast_manager& m;
dom_simplifier* m_simplifier;
params_ref m_params;
expr_ref_vector m_trail, m_args;
obj_map<expr, expr*> m_result;
expr_dominators m_dominators;
unsigned m_depth;
unsigned m_max_depth;
ptr_vector<expr> m_empty;
obj_pair_map<expr, expr, bool> m_subexpr_cache;
bool m_forward;
expr_ref simplify_rec(expr* t);
expr_ref simplify_arg(expr* t);
expr_ref simplify_ite(app * ite);
expr_ref simplify_and(app * e) { return simplify_and_or(true, e); }
expr_ref simplify_or(app * e) { return simplify_and_or(false, e); }
expr_ref simplify_and_or(bool is_and, app * e);
expr_ref simplify_not(app * e);
bool init();
bool is_subexpr(expr * a, expr * b);
expr_ref get_cached(expr* t) { expr* r = nullptr; if (!m_result.find(t, r)) r = t; return expr_ref(r, m); }
void cache(expr *t, expr* r) { m_result.insert(t, r); m_trail.push_back(r); }
void reset_cache() { m_result.reset(); }
ptr_vector<expr> const & tree(expr * e);
expr* idom(expr *e) const { return m_dominators.idom(e); }
unsigned scope_level() { return m_simplifier->scope_level(); }
void pop(unsigned n) { SASSERT(n <= m_simplifier->scope_level()); m_simplifier->pop(n); }
bool assert_expr(expr* f, bool sign) { return m_simplifier->assert_expr(f, sign); }
public:
dominator_simplifier(ast_manager & m, dependent_expr_state& st, dom_simplifier* s, params_ref const & p = params_ref()):
dependent_expr_simplifier(m, st),
m(m), m_simplifier(s), m_params(p),
m_trail(m), m_args(m),
m_dominators(m), m_depth(0), m_max_depth(1024), m_forward(true) {}
~dominator_simplifier() override;
char const* name() const override { return "dom-simplify"; }
void reduce() override;
void updt_params(params_ref const & p) override { m_simplifier->updt_params(p); }
void collect_param_descrs(param_descrs & r) override { m_simplifier->collect_param_descrs(r); }
};

606
src/tactic/bv/bv_bounds_tactic.cpp
View file

@ -18,564 +18,26 @@ Author:
--*/ --*/
#include "tactic/bv/bv_bounds_tactic.h"
#include "tactic/core/ctx_simplify_tactic.h"
#include "tactic/core/dom_simplify_tactic.h"
#include "ast/bv_decl_plugin.h" #include "ast/bv_decl_plugin.h"
#include "ast/ast_pp.h" #include "ast/ast_pp.h"
#include "ast/simplifiers/dominator_simplifier.h"
#include "tactic/bv/bv_bounds_tactic.h"
#include "tactic/core/ctx_simplify_tactic.h"
#include "tactic/dependent_expr_state_tactic.h"
#include "ast/rewriter/bv_bounds_base.h"
#include "ast/simplifiers/bv_bounds_simplifier.h"
#include <climits> #include <climits>
static uint64_t uMaxInt(unsigned sz) {
SASSERT(sz <= 64);
return ULLONG_MAX >> (64u - sz);
}
namespace { namespace {
template<typename T, typename Base>
struct interval_tpl : public Base {
T l, h;
unsigned sz = 0;
bool tight = true;
interval_tpl(T const& l, T const& h, unsigned sz, bool tight = false): l(l), h(h), sz(sz), tight(tight) {} class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier, public bv::bv_bounds_base {
interval_tpl() {}
bool invariant() const {
return
0 <= l && (l <= Base::bound(sz)) &&
0 <= h && (h <= Base::bound(sz)) &&
(!is_wrapped() || l != h + 1);
}
bool is_full() const {
return l == 0 && h == Base::bound(sz);
}
bool is_wrapped() const { return l > h; }
bool is_singleton() const { return l == h; }
bool operator==(const interval_tpl<T, Base>& b) const {
SASSERT(sz == b.sz);
return l == b.l && h == b.h && tight == b.tight;
}
bool operator!=(const interval_tpl& b) const { return !(*this == b); }
bool implies(const interval_tpl<T, Base>& b) const {
if (b.is_full())
return true;
else if (is_full())
return false;
else if (is_wrapped())
// l >= b.l >= b.h >= h
return b.is_wrapped() && h <= b.h && l >= b.l;
else if (b.is_wrapped())
// b.l > b.h >= h >= l
// h >= l >= b.l > b.h
return h <= b.h || l >= b.l;
else
return l >= b.l && h <= b.h;
}
/// return false if intersection is unsat
bool intersect(const interval_tpl<T, Base>& b, interval_tpl& result) const {
if (is_full() || *this == b) {
result = b;
return true;
}
if (b.is_full()) {
result = *this;
return true;
}
if (is_wrapped()) {
if (b.is_wrapped()) {
if (h >= b.l)
result = b;
else if (b.h >= l)
result = *this;
else
result = interval_tpl(std::max(l, b.l), std::min(h, b.h), sz);
}
else
return b.intersect(*this, result);
}
else if (b.is_wrapped()) {
// ... b.h ... l ... h ... b.l ..
if (h < b.l && l > b.h)
return false;
// ... l ... b.l ... h ...
if (h >= b.l && l <= b.h)
result = b;
else if (h >= b.l)
result = interval_tpl(b.l, h, sz);
else {
// ... l .. b.h .. h .. b.l ...
SASSERT(l <= b.h);
result = interval_tpl(l, std::min(h, b.h), sz);
}
} else {
if (l > b.h || h < b.l)
return false;
// 0 .. l.. l' ... h ... h'
result = interval_tpl(std::max(l, b.l), std::min(h, b.h), sz, tight && b.tight);
}
return true;
}
/// return false if negation is empty
bool negate(interval_tpl<T, Base>& result) const {
if (!tight)
result = interval_tpl(Base::zero(), Base::bound(sz), sz, true);
else if (is_full())
return false;
else if (l == 0 && Base::bound(sz) == h)
result = interval_tpl(Base::zero(), Base::bound(sz), sz);
else if (l == 0)
result = interval_tpl(h + 1, Base::bound(sz), sz);
else if (Base::bound(sz) == h)
result = interval_tpl(Base::zero(), l - 1, sz);
else
result = interval_tpl(h + 1, l - 1, sz);
return true;
}
};
struct rinterval_base {
static rational bound(unsigned sz) {
return rational::power_of_two(sz) - 1;
}
static rational zero() { return rational::zero(); }
};
struct rinterval : public interval_tpl<rational, rinterval_base> {
rinterval(rational const& l, rational const& h, unsigned sz, bool tight = false) {
this->l = l; this->h = h; this->sz = sz; this->tight = tight;
}
rinterval() { l = 0; h = 0; tight = true; }
};
struct iinterval_base {
static uint64_t bound(unsigned sz) { return uMaxInt(sz); }
static uint64_t zero() { return 0; }
};
struct iinterval : public interval_tpl<uint64_t, iinterval_base> {
iinterval(uint64_t l, uint64_t h, unsigned sz, bool tight = false) {
this->l = l; this->h = h; this->sz = sz; this->tight = tight;
}
iinterval() { l = 0; h = 0; sz = 0; tight = true; }
};
struct interval {
bool is_small = true;
iinterval i;
rinterval r;
interval() {}
interval(rational const& l, rational const& h, unsigned sz, bool tight = false) {
if (sz <= 64) {
is_small = true;
i.l = l.get_uint64();
i.h = h.get_uint64();
i.tight = tight;
i.sz = sz;
}
else {
is_small = false;
r.l = l;
r.h = h;
r.tight = tight;
r.sz = sz;
}
}
unsigned size() const {
return is_small ? i.sz : r.sz;
}
bool negate(interval& result) const {
result.is_small = is_small;
if (is_small)
return i.negate(result.i);
else
return r.negate(result.r);
}
bool intersect(interval const& b, interval & result) const {
result.is_small = is_small;
SASSERT(b.is_small == is_small);
if (is_small)
return i.intersect(b.i, result.i);
else
return r.intersect(b.r, result.r);
}
bool operator==(interval const& other) const {
SASSERT(is_small == other.is_small);
return is_small ? i == other.i : r == other.r;
}
bool operator!=(interval const& other) const {
return !(*this == other);
}
bool is_singleton() const { return is_small ? i.is_singleton() : r.is_singleton(); }
bool is_full() const { return is_small ? i.is_full() : r.is_full(); }
bool tight() const { return is_small ? i.tight : r.tight; }
bool implies(const interval& b) const {
SASSERT(is_small == b.is_small);
return is_small ? i.implies(b.i) : r.implies(b.r);
}
rational lo() const { return is_small ? rational(i.l, rational::ui64()) : r.l; }
rational hi() const { return is_small ? rational(i.h, rational::ui64()) : r.h; }
};
std::ostream& operator<<(std::ostream& o, const interval& I) {
if (I.is_small)
return o << "[" << I.i.l << ", " << I.i.h << "]";
else
return o << "[" << I.r.l << ", " << I.r.h << "]";
}
struct undo_bound {
expr* e = nullptr;
interval b;
bool fresh = false;
undo_bound(expr* e, const interval& b, bool fresh) : e(e), b(b), fresh(fresh) {}
};
struct bv_bounds_base {
typedef obj_map<expr, interval> map;
typedef obj_map<expr, bool> expr_set;
typedef obj_map<expr, unsigned> expr_cnt;
ast_manager& m;
bv_util m_bv;
vector<undo_bound> m_scopes;
svector<expr_set*> m_expr_vars;
svector<expr_cnt*> m_bound_exprs;
map m_bound;
bool m_propagate_eq = false;
ptr_vector<expr> m_args;
bv_bounds_base(ast_manager& m):m(m), m_bv(m) {}
virtual ~bv_bounds_base() {
for (auto* e : m_expr_vars)
dealloc(e);
for (auto* b : m_bound_exprs)
dealloc(b);
}
bool is_bound(expr *e, expr*& v, interval& b) const {
rational r;
expr *lhs = nullptr, *rhs = nullptr;
unsigned sz;
if (m_bv.is_bv_ule(e, lhs, rhs)) {
if (m_bv.is_numeral(lhs, r, sz)) { // C ule x <=> x uge C
if (m_bv.is_numeral(rhs))
return false;
b = interval(r, rational::power_of_two(sz) - 1, sz, true);
v = rhs;
return true;
}
if (m_bv.is_numeral(rhs, r, sz)) { // x ule C
b = interval(rational::zero(), r, sz, true);
v = lhs;
return true;
}
// TBD: x + s <= x + q
// x + s <= x
// x <= x + q
}
else if (m_bv.is_bv_sle(e, lhs, rhs)) {
if (m_bv.is_numeral(lhs, r, sz)) { // C sle x <=> x sge C
if (m_bv.is_numeral(rhs))
return false;
b = interval(r, rational::power_of_two(sz-1) - 1, sz, true);
v = rhs;
return true;
}
if (m_bv.is_numeral(rhs, r, sz)) { // x sle C
b = interval(rational::power_of_two(sz-1), r, sz, true);
v = lhs;
return true;
}
// TBD: other cases for forbidden intervals
}
else if (m.is_eq(e, lhs, rhs)) {
if (m_bv.is_numeral(rhs))
std::swap(lhs, rhs);
if (m_bv.is_numeral(rhs))
return false;
if (m_bv.is_numeral(lhs, r, sz)) {
unsigned lo, hi;
expr* rhs2;
if (m_bv.is_extract(rhs, lo, hi, rhs2) && r == 0) {
unsigned sz2 = m_bv.get_bv_size(rhs2);
if (sz2 - 1 == hi) {
b = interval(rational::zero(), rational::power_of_two(lo) - 1, sz2, false);
v = rhs2;
return true;
}
}
b = interval(r, r, sz, true);
v = rhs;
return true;
}
}
return false;
}
bool assert_expr_core(expr * t, bool sign) {
while (m.is_not(t, t))
sign = !sign;
interval b;
expr* t1;
if (is_bound(t, t1, b)) {
SASSERT(m_bv.get_bv_size(t1) == b.size());
SASSERT(!m_bv.is_numeral(t1));
if (sign && !b.negate(b))
return false;
TRACE("bv", tout << (sign?"(not ":"") << mk_pp(t, m) << (sign ? ")" : "") << ": " << mk_pp(t1, m) << " in " << b << "\n";);
map::obj_map_entry* e = m_bound.find_core(t1);
if (e) {
interval& old = e->get_data().m_value;
interval intr;
if (!old.intersect(b, intr))
return false;
if (old == intr)
return true;
m_scopes.push_back(undo_bound(t1, old, false));
old = intr;
SASSERT(old.size() == m_bv.get_bv_size(t1));
}
else {
SASSERT(b.size() == m_bv.get_bv_size(t1));
m_bound.insert(t1, b);
m_scopes.push_back(undo_bound(t1, interval(), true));
}
}
return true;
}
//
// x + q <= s <=> x not in [s - q + 1, -q[
// <=> x in [-q, s - q], s != -1
//
// x in [lo, hi]
// q = -lo
// hi = s + lo => s = hi - lo
// hi - lo != -1
//
expr_ref mk_bound(expr* t, rational const& lo, rational const& hi) {
sort* s = t->get_sort();
if (lo == hi + 1)
return expr_ref(m.mk_true(), m);
else
return expr_ref(m_bv.mk_ule(m_bv.mk_bv_add(t, m_bv.mk_numeral(-lo, s)), m_bv.mk_numeral(hi - lo, s)), m);
}
//
// use interval information to rewrite sub-terms x to (0 ++ x[hi:0])
// in other words, identify leading 0s.
//
bool zero_patch(expr* t, expr_ref& result) {
if (!is_app(t))
return false;
if (m_bv.is_extract(t))
return false;
m_args.reset();
bool simplified = false;
interval b;
for (expr* arg : *to_app(t)) {
if (!m_bv.is_bv(arg)) {
m_args.push_back(arg);
continue;
}
if (!m_bv.is_extract(arg) && m_bound.find(arg, b)) {
unsigned num_bits = b.hi().get_num_bits();
unsigned bv_size = m_bv.get_bv_size(arg);
if (0 < num_bits && num_bits < bv_size) {
m_args.push_back(m_bv.mk_concat(m_bv.mk_zero(bv_size - num_bits),
m_bv.mk_extract(num_bits - 1, 0, arg)));
simplified = true;
}
else
m_args.push_back(arg);
}
else
m_args.push_back(arg);
}
if (simplified) {
result = m.mk_app(to_app(t)->get_decl(), m_args);
return true;
}
return false;
}
bool simplify_core(expr* t, expr_ref& result) {
expr* t1;
interval b;
if (m_bound.find(t, b) && b.is_singleton()) {
result = m_bv.mk_numeral(b.lo(), m_bv.get_bv_size(t));
return true;
}
if (zero_patch(t, result))
return result;
if (!m.is_bool(t))
return false;
bool sign = false;
while (m.is_not(t, t))
sign = !sign;
if (!is_bound(t, t1, b))
return false;
if (sign && b.tight()) {
sign = false;
if (!b.negate(b)) {
result = m.mk_false();
return true;
}
}
interval ctx, intr;
result = nullptr;
if (b.is_full() && b.tight())
result = m.mk_true();
else if (!m_bound.find(t1, ctx)) {
}
else if (ctx.implies(b))
result = m.mk_true();
else if (!b.intersect(ctx, intr))
result = m.mk_false();
else if (m_propagate_eq && intr.is_singleton())
result = m.mk_eq(t1, m_bv.mk_numeral(intr.lo(), t1->get_sort()));
else if (false && intr != b)
result = mk_bound(t1, intr.lo(), intr.hi());
else {
TRACE("bv", tout << mk_pp(t, m) << " b: " << b << " ctx: " << ctx << " intr " << intr << "\n");
}
CTRACE("bv", result, tout << mk_pp(t, m) << " " << b << " (ctx: " << ctx << ") (intr: " << intr << "): " << result << "\n";);
if (sign && result)
result = m.mk_not(result);
return result != nullptr;
}
// check if t contains v
ptr_vector<expr> todo;
bool contains(expr* t, expr* v) {
ast_fast_mark1 mark;
todo.push_back(t);
while (!todo.empty()) {
t = todo.back();
todo.pop_back();
if (mark.is_marked(t))
continue;
if (t == v) {
todo.reset();
return true;
}
mark.mark(t);
if (!is_app(t))
continue;
app* a = to_app(t);
todo.append(a->get_num_args(), a->get_args());
}
return false;
}
bool contains_bound(expr* t) {
ast_fast_mark1 mark1;
ast_fast_mark2 mark2;
todo.push_back(t);
while (!todo.empty()) {
t = todo.back();
todo.pop_back();
if (mark1.is_marked(t)) {
continue;
}
mark1.mark(t);
if (!is_app(t)) {
continue;
}
interval b;
expr* e;
if (is_bound(t, e, b)) {
if (mark2.is_marked(e)) {
todo.reset();
return true;
}
mark2.mark(e);
if (m_bound.contains(e)) {
todo.reset();
return true;
}
}
app* a = to_app(t);
todo.append(a->get_num_args(), a->get_args());
}
return false;
}
void pop_core(unsigned num_scopes) {
TRACE("bv", tout << "pop: " << num_scopes << "\n";);
if (m_scopes.empty())
return;
unsigned target = m_scopes.size() - num_scopes;
if (target == 0) {
m_bound.reset();
m_scopes.reset();
return;
}
for (unsigned i = m_scopes.size(); i-- > target; ) {
undo_bound& undo = m_scopes[i];
SASSERT(m_bound.contains(undo.e));
if (undo.fresh)
m_bound.erase(undo.e);
else
m_bound.insert(undo.e, undo.b);
}
m_scopes.shrink(target);
}
};
class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier, public bv_bounds_base {
params_ref m_params; params_ref m_params;
public: public:
bv_bounds_simplifier(ast_manager& m, params_ref const& p) : bv_bounds_base(m), m_params(p) { bv_bounds_simplifier(ast_manager& m, params_ref const& p) : bv::bv_bounds_base(m), m_params(p) {
updt_params(p); updt_params(p);
} }
@ -608,7 +70,7 @@ namespace {
return true; return true;
expr* t1; expr* t1;
interval b; bv::interval b;
// skip common case: single bound constraint without any context for simplification // skip common case: single bound constraint without any context for simplification
if (is_bound(t, t1, b)) if (is_bound(t, t1, b))
return b.is_full() || m_bound.contains(t1); return b.is_full() || m_bound.contains(t1);
@ -629,56 +91,12 @@ namespace {
} }
}; };
class dom_bv_bounds_simplifier : public dom_simplifier, public bv_bounds_base {
params_ref m_params;
public:
dom_bv_bounds_simplifier(ast_manager& m, params_ref const& p) : bv_bounds_base(m), m_params(p) {
updt_params(p);
}
~dom_bv_bounds_simplifier() override {
}
void updt_params(params_ref const & p) override {
m_propagate_eq = p.get_bool("propagate_eq", false);
}
void collect_param_descrs(param_descrs& r) override {
r.insert("propagate-eq", CPK_BOOL, "propagate equalities from inequalities", "false");
}
bool assert_expr(expr * t, bool sign) override {
return assert_expr_core(t, sign);
}
void operator()(expr_ref& r) override {
expr_ref result(m);
simplify_core(r, result);
if (result)
r = result;
}
void pop(unsigned num_scopes) override {
pop_core(num_scopes);
}
dom_simplifier * translate(ast_manager & m) override {
return alloc(dom_bv_bounds_simplifier, m, m_params);
}
unsigned scope_level() const override {
return m_scopes.size();
}
};
} }
tactic * mk_bv_bounds_tactic(ast_manager & m, params_ref const & p) { tactic * mk_bv_bounds_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(ctx_simplify_tactic, m, alloc(bv_bounds_simplifier, m, p), p)); return clean(alloc(ctx_simplify_tactic, m, alloc(bv_bounds_simplifier, m, p), p));
} }
tactic * mk_dom_bv_bounds_tactic(ast_manager & m, params_ref const & p) { tactic* mk_dom_bv_bounds_tactic(ast_manager& m, params_ref const& p) {
return clean(alloc(dom_simplify_tactic, m, alloc(dom_bv_bounds_simplifier, m, p), p)); return alloc(dependent_expr_state_tactic, m, p, mk_bv_bounds_simplifier);
} }

1
src/tactic/core/CMakeLists.txt
View file

@ -6,7 +6,6 @@ z3_add_component(core_tactics
collect_statistics_tactic.cpp collect_statistics_tactic.cpp
ctx_simplify_tactic.cpp ctx_simplify_tactic.cpp
der_tactic.cpp der_tactic.cpp
dom_simplify_tactic.cpp
elim_term_ite_tactic.cpp elim_term_ite_tactic.cpp
elim_uncnstr_tactic.cpp elim_uncnstr_tactic.cpp
euf_completion_tactic.cpp euf_completion_tactic.cpp

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

@ -1,613 +0,0 @@
/*++
Copyright (c) 2017 Microsoft Corporation
Module Name:
dom_simplify_tactic.cpp
Abstract:
Dominator-based context simplifer.
Author:
Nikolaj and Nuno
Notes:
--*/
#include "ast/ast_util.h"
#include "ast/ast_pp.h"
#include "ast/ast_ll_pp.h"
#include "tactic/core/dom_simplify_tactic.h"
/**
\brief compute a post-order traversal for e.
Also populate the set of parents
*/
void expr_dominators::compute_post_order() {
unsigned post_num = 0;
SASSERT(m_post2expr.empty());
SASSERT(m_expr2post.empty());
ast_mark mark;
ptr_vector<expr> todo;
todo.push_back(m_root);
while (!todo.empty()) {
expr* e = todo.back();
if (mark.is_marked(e)) {
todo.pop_back();
continue;
}
if (is_app(e)) {
app* a = to_app(e);
bool done = true;
for (expr* arg : *a) {
if (!mark.is_marked(arg)) {
todo.push_back(arg);
done = false;
}
}
if (done) {
mark.mark(e, true);
m_expr2post.insert(e, post_num++);
m_post2expr.push_back(e);
todo.pop_back();
for (expr* arg : *a) {
add_edge(m_parents, arg, a);
}
}
}
else {
mark.mark(e, true);
todo.pop_back();
}
}
}
expr* expr_dominators::intersect(expr* x, expr * y) {
unsigned n1 = m_expr2post[x];
unsigned n2 = m_expr2post[y];
while (n1 != n2) {
if (n1 < n2) {
x = m_doms[x];
n1 = m_expr2post[x];
}
else if (n1 > n2) {
y = m_doms[y];
n2 = m_expr2post[y];
}
}
SASSERT(x == y);
return x;
}
bool expr_dominators::compute_dominators() {
expr * e = m_root;
SASSERT(m_doms.empty());
m_doms.insert(e, e);
bool change = true;
unsigned iterations = 1;
while (change) {
change = false;
TRACE("simplify",
for (auto & kv : m_doms) {
tout << mk_bounded_pp(kv.m_key, m) << " |-> " << mk_bounded_pp(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];
expr * new_idom = nullptr, *idom2 = nullptr;
for (expr * pred : p) {
if (m_doms.contains(pred)) {
new_idom = !new_idom ? pred : intersect(new_idom, pred);
}
}
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;
}
}
iterations *= 2;
if (change && iterations > m_post2expr.size()) {
return false;
}
}
return true;
}
void expr_dominators::extract_tree() {
for (auto const& kv : m_doms) {
add_edge(m_tree, kv.m_value, kv.m_key);
}
}
bool expr_dominators::compile(expr * e) {
reset();
m_root = e;
compute_post_order();
if (!compute_dominators()) return false;
extract_tree();
TRACE("simplify", display(tout););
return true;
}
bool expr_dominators::compile(unsigned sz, expr * const* es) {
expr_ref e(m.mk_and(sz, es), m);
return compile(e);
}
void expr_dominators::reset() {
m_expr2post.reset();
m_post2expr.reset();
m_parents.reset();
m_doms.reset();
m_tree.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 << r->get_id() << ": " << mk_bounded_pp(r, m, 1) << "\n";
if (m_tree.contains(r)) {
for (expr* child : m_tree[r]) {
if (child != r)
display(out, indent + 1, child);
}
}
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);
}
void dom_simplify_tactic::operator()(goal_ref const & in, goal_ref_buffer & result) {
tactic_report report("dom-simplify", *in.get());
simplify_goal(*(in.get()));
in->inc_depth();
result.push_back(in.get());
}
void dom_simplify_tactic::cleanup() {
m_trail.reset();
m_args.reset();
m_result.reset();
m_dominators.reset();
}
expr_ref dom_simplify_tactic::simplify_ite(app * ite) {
expr_ref r(m);
expr * c = nullptr, *t = nullptr, *e = nullptr;
VERIFY(m.is_ite(ite, c, t, e));
unsigned old_lvl = scope_level();
expr_ref new_c = simplify_arg(c);
if (m.is_true(new_c)) {
r = simplify_arg(t);
}
else if (!assert_expr(new_c, false)) {
r = simplify_arg(e);
}
else {
for (expr * child : tree(ite))
if (is_subexpr(child, t) && !is_subexpr(child, e))
simplify_rec(child);
pop(scope_level() - old_lvl);
expr_ref new_t = simplify_arg(t);
reset_cache();
if (!assert_expr(new_c, true)) {
return new_t;
}
for (expr * child : tree(ite))
if (is_subexpr(child, e) && !is_subexpr(child, t))
simplify_rec(child);
pop(scope_level() - old_lvl);
expr_ref new_e = simplify_arg(e);
if (c == new_c && t == new_t && e == new_e) {
r = ite;
}
else if (new_t == new_e) {
r = new_t;
}
else {
TRACE("simplify", tout << new_c << "\n" << new_t << "\n" << new_e << "\n";);
r = m.mk_ite(new_c, new_t, new_e);
}
}
reset_cache();
return r;
}
expr_ref dom_simplify_tactic::simplify_arg(expr * e) {
expr_ref r(m);
r = get_cached(e);
(*m_simplifier)(r);
CTRACE("simplify", e != r, 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 = nullptr;
if (!m_result.find(e0, e)) {
e = e0;
}
++m_depth;
if (m_depth > m_max_depth) {
r = e;
}
else if (m.is_ite(e)) {
r = simplify_ite(to_app(e));
}
else if (m.is_and(e)) {
r = simplify_and(to_app(e));
}
else if (m.is_or(e)) {
r = simplify_or(to_app(e));
}
else if (m.is_not(e)) {
r = simplify_not(to_app(e));
}
else {
for (expr * child : tree(e)) {
if (child != e)
simplify_rec(child);
}
if (is_app(e)) {
m_args.reset();
for (expr* arg : *to_app(e)) {
// we don't have a way to distinguish between e.g.
// ite(c, f(c), foo) (which should go to ite(c, f(true), foo))
// from and(or(x, y), f(x)), where we do a "trial" with x=false
// Trials are good for boolean formula simplification but not sound
// for fn applications.
m_args.push_back(m.is_bool(arg) ? arg : simplify_arg(arg));
}
r = m.mk_app(to_app(e)->get_decl(), m_args.size(), m_args.data());
}
else {
r = e;
}
}
CTRACE("simplify", e0 != r, tout << "depth before: " << m_depth << " " << mk_pp(e0, m) << " -> " << r << "\n";);
(*m_simplifier)(r);
cache(e0, r);
CTRACE("simplify", e0 != r, tout << "depth: " << m_depth << " " << mk_pp(e0, m) << " -> " << r << "\n";);
--m_depth;
m_subexpr_cache.reset();
return r;
}
expr_ref dom_simplify_tactic::simplify_and_or(bool is_and, app * e) {
expr_ref r(m);
unsigned old_lvl = scope_level();
auto is_subexpr_arg = [&](expr * child, expr * except) {
if (!is_subexpr(child, except))
return false;
for (expr * arg : *e) {
if (arg != except && is_subexpr(child, arg))
return false;
}
return true;
};
expr_ref_vector args(m);
auto simp_arg = [&](expr* 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)) {
pop(scope_level() - old_lvl);
r = is_and ? m.mk_false() : m.mk_true();
reset_cache();
return true;
}
return false;
};
if (m_forward) {
for (expr * arg : *e) {
if (simp_arg(arg))
return r;
}
}
else {
for (unsigned i = e->get_num_args(); i-- > 0; ) {
if (simp_arg(e->get_arg(i)))
return r;
}
args.reverse();
}
pop(scope_level() - old_lvl);
reset_cache();
return { is_and ? mk_and(args) : mk_or(args), m };
}
expr_ref dom_simplify_tactic::simplify_not(app * e) {
expr *ee;
ENSURE(m.is_not(e, ee));
unsigned old_lvl = scope_level();
expr_ref t = simplify_rec(ee);
pop(scope_level() - old_lvl);
reset_cache();
return mk_not(t);
}
bool dom_simplify_tactic::init(goal& g) {
expr_ref_vector args(m);
unsigned sz = g.size();
for (unsigned i = 0; i < sz; ++i) args.push_back(g.form(i));
expr_ref fml = mk_and(args);
m_result.reset();
m_trail.reset();
return m_dominators.compile(fml);
}
void dom_simplify_tactic::simplify_goal(goal& g) {
SASSERT(scope_level() == 0);
bool change = true;
unsigned n = 0;
m_depth = 0;
while (change && n < 10) {
change = false;
++n;
// 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_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_ref new_pr(m);
if (g.proofs_enabled() && g.pr(i)) {
new_pr = m.mk_modus_ponens(g.pr(i), m.mk_rewrite(g.form(i), r));
}
g.update(i, r, new_pr, g.dep(i));
}
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_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_ref new_pr(m);
if (g.proofs_enabled() && g.pr(i)) {
new_pr = m.mk_rewrite(g.form(i), r);
new_pr = m.mk_modus_ponens(g.pr(i), new_pr);
}
g.update(i, r, new_pr, g.dep(i));
}
pop(scope_level());
}
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;
bool r;
if (m_subexpr_cache.find(a, b, r))
return r;
if (get_depth(a) >= get_depth(b)) {
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) {
if (auto p = m_dominators.get_tree().find_core(e))
return p->get_data().get_value();
return m_empty;
}
// ---------------------
// expr_substitution_simplifier
namespace {
class expr_substitution_simplifier : public dom_simplifier {
ast_manager& m;
expr_substitution m_subst;
scoped_expr_substitution m_scoped_substitution;
obj_map<expr, unsigned> m_expr2depth;
expr_ref_vector m_trail;
// move from asserted_formulas to here..
void compute_depth(expr* e) {
ptr_vector<expr> todo;
todo.push_back(e);
while (!todo.empty()) {
e = todo.back();
unsigned d = 0;
if (m_expr2depth.contains(e)) {
todo.pop_back();
continue;
}
if (is_app(e)) {
app* a = to_app(e);
bool visited = true;
for (expr* arg : *a) {
unsigned d1 = 0;
if (m_expr2depth.find(arg, d1)) {
d = std::max(d, d1);
}
else {
visited = false;
todo.push_back(arg);
}
}
if (!visited) {
continue;
}
}
todo.pop_back();
m_expr2depth.insert(e, d + 1);
}
}
bool is_gt(expr* lhs, expr* rhs) {
if (lhs == rhs) {
return false;
}
if (m.is_value(rhs)) {
return true;
}
SASSERT(is_ground(lhs) && is_ground(rhs));
if (depth(lhs) > depth(rhs)) {
return true;
}
if (depth(lhs) == depth(rhs) && is_app(lhs) && is_app(rhs)) {
app* l = to_app(lhs);
app* r = to_app(rhs);
if (l->get_decl()->get_id() != r->get_decl()->get_id()) {
return l->get_decl()->get_id() > r->get_decl()->get_id();
}
if (l->get_num_args() != r->get_num_args()) {
return l->get_num_args() > r->get_num_args();
}
for (unsigned i = 0; i < l->get_num_args(); ++i) {
if (l->get_arg(i) != r->get_arg(i)) {
return is_gt(l->get_arg(i), r->get_arg(i));
}
}
UNREACHABLE();
}
return false;
}
unsigned depth(expr* e) { return m_expr2depth[e]; }
public:
expr_substitution_simplifier(ast_manager& m): m(m), m_subst(m), m_scoped_substitution(m_subst), m_trail(m) {}
void updt_params(params_ref const & p) override {}
void collect_param_descrs(param_descrs& r) override {}
bool assert_expr(expr * t, bool sign) override {
expr* tt;
if (m.is_not(t, tt))
return assert_expr(tt, !sign);
if (m.is_false(t))
return sign;
if (m.is_true(t))
return !sign;
TRACE("simplify", tout << t->get_id() << ": " << mk_bounded_pp(t, m) << " " << (sign?" - neg":" - pos") << "\n";);
m_scoped_substitution.push();
if (!sign) {
update_substitution(t, nullptr);
}
else {
expr_ref nt(m.mk_not(t), m);
update_substitution(nt, nullptr);
}
return true;
}
void update_substitution(expr* n, proof* pr) {
expr* lhs, *rhs, *n1;
if (is_ground(n) && m.is_eq(n, lhs, rhs)) {
compute_depth(lhs);
compute_depth(rhs);
m_trail.push_back(lhs);
m_trail.push_back(rhs);
if (is_gt(lhs, rhs)) {
TRACE("propagate_values", tout << "insert " << mk_pp(lhs, m) << " -> " << mk_pp(rhs, m) << "\n";);
m_scoped_substitution.insert(lhs, rhs, pr);
return;
}
if (is_gt(rhs, lhs)) {
TRACE("propagate_values", tout << "insert " << mk_pp(rhs, m) << " -> " << mk_pp(lhs, m) << "\n";);
m_scoped_substitution.insert(rhs, lhs, m.mk_symmetry(pr));
return;
}
TRACE("propagate_values", tout << "incompatible " << mk_pp(n, m) << "\n";);
}
if (m.is_not(n, n1)) {
m_scoped_substitution.insert(n1, m.mk_false(), m.mk_iff_false(pr));
}
else {
m_scoped_substitution.insert(n, m.mk_true(), m.mk_iff_true(pr));
}
}
void operator()(expr_ref& r) override { r = m_scoped_substitution.find(r); }
void pop(unsigned num_scopes) override { m_scoped_substitution.pop(num_scopes); }
unsigned scope_level() const override { return m_scoped_substitution.scope_level(); }
dom_simplifier * translate(ast_manager & m) override {
SASSERT(m_subst.empty());
return alloc(expr_substitution_simplifier, m);
}
};
}
tactic * mk_dom_simplify_tactic(ast_manager & m, params_ref const & p) {
return clean(alloc(dom_simplify_tactic, m, alloc(expr_substitution_simplifier, m), p));
}

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

@ -44,130 +44,15 @@ tree are visited. Since the paths selected by the dominator trees are limited, t
#include "ast/ast.h" #include "ast/ast.h"
#include "ast/expr_substitution.h" #include "ast/expr_substitution.h"
#include "ast/rewriter/dom_simplifier.h"
#include "tactic/tactic.h" #include "tactic/tactic.h"
#include "tactic/tactical.h" #include "tactic/dependent_expr_state_tactic.h"
#include "util/obj_pair_hashtable.h" #include "ast/simplifiers/dominator_simplifier.h"
inline tactic* mk_dom_simplify_tactic(ast_manager& m, params_ref const& p) {
class expr_dominators { return alloc(dependent_expr_state_tactic, m, p,
public: [](auto& m, auto& p, auto& s) -> dependent_expr_simplifier* { return alloc(dominator_simplifier, m, s, mk_expr_substitution_simplifier(m), p); });
typedef obj_map<expr, ptr_vector<expr>> tree_t; }
private:
ast_manager& m;
expr_ref m_root;
obj_map<expr, unsigned> m_expr2post; // reverse post-order number
ptr_vector<expr> m_post2expr;
tree_t m_parents;
obj_map<expr, expr*> m_doms;
tree_t m_tree;
void add_edge(tree_t& tree, expr * src, expr* dst) {
tree.insert_if_not_there(src, ptr_vector<expr>()).push_back(dst);
}
void compute_post_order();
expr* intersect(expr* x, expr * y);
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) {}
bool compile(expr * e);
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 {
public:
virtual ~dom_simplifier() = default;
/**
\brief assert_expr performs an implicit push
*/
virtual bool assert_expr(expr * t, bool sign) = 0;
/**
\brief apply simplification.
*/
virtual void operator()(expr_ref& r) = 0;
/**
\brief pop scopes accumulated from assertions.
*/
virtual void pop(unsigned num_scopes) = 0;
virtual dom_simplifier * translate(ast_manager & m) = 0;
virtual unsigned scope_level() const = 0;
virtual void updt_params(params_ref const & p) = 0;
virtual void collect_param_descrs(param_descrs& r) = 0;
};
class dom_simplify_tactic : public tactic {
ast_manager& m;
dom_simplifier* m_simplifier;
params_ref m_params;
expr_ref_vector m_trail, m_args;
obj_map<expr, expr*> m_result;
expr_dominators m_dominators;
unsigned m_depth;
unsigned m_max_depth;
ptr_vector<expr> m_empty;
obj_pair_map<expr, expr, bool> m_subexpr_cache;
bool m_forward;
expr_ref simplify_rec(expr* t);
expr_ref simplify_arg(expr* t);
expr_ref simplify_ite(app * ite);
expr_ref simplify_and(app * e) { return simplify_and_or(true, e); }
expr_ref simplify_or(app * e) { return simplify_and_or(false, e); }
expr_ref simplify_and_or(bool is_and, app * e);
expr_ref simplify_not(app * e);
void simplify_goal(goal& g);
bool is_subexpr(expr * a, expr * b);
expr_ref get_cached(expr* t) { expr* r = nullptr; if (!m_result.find(t, r)) r = t; return expr_ref(r, m); }
void cache(expr *t, expr* r) { m_result.insert(t, r); m_trail.push_back(r); }
void reset_cache() { m_result.reset(); }
ptr_vector<expr> const & tree(expr * e);
expr* idom(expr *e) const { return m_dominators.idom(e); }
unsigned scope_level() { return m_simplifier->scope_level(); }
void pop(unsigned n) { SASSERT(n <= m_simplifier->scope_level()); m_simplifier->pop(n); }
bool assert_expr(expr* f, bool sign) { return m_simplifier->assert_expr(f, sign); }
bool init(goal& g);
public:
dom_simplify_tactic(ast_manager & m, dom_simplifier* s, params_ref const & p = params_ref()):
m(m), m_simplifier(s), m_params(p),
m_trail(m), m_args(m),
m_dominators(m), m_depth(0), m_max_depth(1024), m_forward(true) {}
~dom_simplify_tactic() override;
char const* name() const override { return "dom_simplify"; }
tactic * translate(ast_manager & m) override;
void updt_params(params_ref const & p) override { m_simplifier->updt_params(p); }
void collect_param_descrs(param_descrs & r) override { m_simplifier->collect_param_descrs(r); }
void operator()(goal_ref const & in, goal_ref_buffer & result) override;
void cleanup() override;
};
tactic * mk_dom_simplify_tactic(ast_manager & m, params_ref const & p = params_ref());
/* /*
ADD_TACTIC("dom-simplify", "apply dominator simplification rules.", "mk_dom_simplify_tactic(m, p)") ADD_TACTIC("dom-simplify", "apply dominator simplification rules.", "mk_dom_simplify_tactic(m, p)")