diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt index c785804c1..17410807a 100644 --- a/src/ast/rewriter/CMakeLists.txt +++ b/src/ast/rewriter/CMakeLists.txt @@ -14,6 +14,7 @@ z3_add_component(rewriter der.cpp distribute_forall.cpp dl_rewriter.cpp + dom_simplifier.cpp elim_bounds.cpp enum2bv_rewriter.cpp expr_replacer.cpp diff --git a/src/ast/rewriter/bv_bounds_base.h b/src/ast/rewriter/bv_bounds_base.h new file mode 100644 index 000000000..8ddb429e9 --- /dev/null +++ b/src/ast/rewriter/bv_bounds_base.h @@ -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 + 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& 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& 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& 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& 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 { + 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 { + 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 map; + typedef obj_map expr_set; + typedef obj_map expr_cnt; + + ast_manager& m; + bv_util m_bv; + vector m_scopes; + svector m_expr_vars; + svector m_bound_exprs; + map m_bound; + bool m_propagate_eq = false; + ptr_vector 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 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); + } + + }; + +} diff --git a/src/ast/rewriter/dom_simplifier.cpp b/src/ast/rewriter/dom_simplifier.cpp new file mode 100644 index 000000000..205c81dbb --- /dev/null +++ b/src/ast/rewriter/dom_simplifier.cpp @@ -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 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 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 m_expr2depth; + expr_ref_vector m_trail; + + // move from asserted_formulas to here.. + void compute_depth(expr* e) { + ptr_vector 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); +} + + + diff --git a/src/ast/rewriter/dom_simplifier.h b/src/ast/rewriter/dom_simplifier.h new file mode 100644 index 000000000..4d9c63c1e --- /dev/null +++ b/src/ast/rewriter/dom_simplifier.h @@ -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> tree_t; +private: + ast_manager& m; + expr_ref m_root; + obj_map m_expr2post; // reverse post-order number + ptr_vector m_post2expr; + tree_t m_parents; + obj_map m_doms; + tree_t m_tree; + + void add_edge(tree_t& tree, expr * src, expr* dst) { + tree.insert_if_not_there(src, ptr_vector()).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); diff --git a/src/ast/simplifiers/CMakeLists.txt b/src/ast/simplifiers/CMakeLists.txt index cd1b34f8c..826717c5a 100644 --- a/src/ast/simplifiers/CMakeLists.txt +++ b/src/ast/simplifiers/CMakeLists.txt @@ -4,10 +4,12 @@ z3_add_component(simplifiers bound_manager.cpp bound_propagator.cpp bound_simplifier.cpp + bv_bounds_simplifier.cpp bv_slice.cpp card2bv.cpp demodulator_simplifier.cpp dependent_expr_state.cpp + dominator_simplifier.cpp distribute_forall.cpp elim_unconstrained.cpp eliminate_predicates.cpp diff --git a/src/ast/simplifiers/bv_bounds_simplifier.cpp b/src/ast/simplifiers/bv_bounds_simplifier.cpp new file mode 100644 index 000000000..72010c507 --- /dev/null +++ b/src/ast/simplifiers/bv_bounds_simplifier.cpp @@ -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); +} diff --git a/src/ast/simplifiers/bv_bounds_simplifier.h b/src/ast/simplifiers/bv_bounds_simplifier.h new file mode 100644 index 000000000..ed2955bba --- /dev/null +++ b/src/ast/simplifiers/bv_bounds_simplifier.h @@ -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); diff --git a/src/ast/simplifiers/dominator_simplifier.cpp b/src/ast/simplifiers/dominator_simplifier.cpp new file mode 100644 index 000000000..12f2e2941 --- /dev/null +++ b/src/ast/simplifiers/dominator_simplifier.cpp @@ -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 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; +} diff --git a/src/ast/simplifiers/dominator_simplifier.h b/src/ast/simplifiers/dominator_simplifier.h new file mode 100644 index 000000000..562aeace1 --- /dev/null +++ b/src/ast/simplifiers/dominator_simplifier.h @@ -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 m_result; + expr_dominators m_dominators; + unsigned m_depth; + unsigned m_max_depth; + ptr_vector m_empty; + obj_pair_map 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 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); } +}; + diff --git a/src/tactic/bv/bv_bounds_tactic.cpp b/src/tactic/bv/bv_bounds_tactic.cpp index 2e0ce0391..45ff60ec0 100644 --- a/src/tactic/bv/bv_bounds_tactic.cpp +++ b/src/tactic/bv/bv_bounds_tactic.cpp @@ -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/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 -static uint64_t uMaxInt(unsigned sz) { - SASSERT(sz <= 64); - return ULLONG_MAX >> (64u - sz); -} namespace { - template - 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& 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& 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& 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& 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 { - 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 { - 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 map; - typedef obj_map expr_set; - typedef obj_map expr_cnt; - - ast_manager& m; - bv_util m_bv; - vector m_scopes; - svector m_expr_vars; - svector m_bound_exprs; - map m_bound; - bool m_propagate_eq = false; - ptr_vector 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 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 { + class bv_bounds_simplifier : public ctx_simplify_tactic::simplifier, public bv::bv_bounds_base { params_ref m_params; 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); } @@ -608,7 +70,7 @@ namespace { return true; expr* t1; - interval b; + bv::interval b; // skip common case: single bound constraint without any context for simplification if (is_bound(t, t1, b)) 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) { 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) { - return clean(alloc(dom_simplify_tactic, m, alloc(dom_bv_bounds_simplifier, m, p), p)); +tactic* mk_dom_bv_bounds_tactic(ast_manager& m, params_ref const& p) { + return alloc(dependent_expr_state_tactic, m, p, mk_bv_bounds_simplifier); } diff --git a/src/tactic/core/CMakeLists.txt b/src/tactic/core/CMakeLists.txt index d4a115dcc..0827c12fb 100644 --- a/src/tactic/core/CMakeLists.txt +++ b/src/tactic/core/CMakeLists.txt @@ -6,7 +6,6 @@ z3_add_component(core_tactics collect_statistics_tactic.cpp ctx_simplify_tactic.cpp der_tactic.cpp - dom_simplify_tactic.cpp elim_term_ite_tactic.cpp elim_uncnstr_tactic.cpp euf_completion_tactic.cpp diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp deleted file mode 100644 index 82fb7ec44..000000000 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ /dev/null @@ -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 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 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 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 m_expr2depth; - expr_ref_vector m_trail; - - // move from asserted_formulas to here.. - void compute_depth(expr* e) { - ptr_vector 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)); -} diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h index 771c8c654..2dba378b7 100644 --- a/src/tactic/core/dom_simplify_tactic.h +++ b/src/tactic/core/dom_simplify_tactic.h @@ -44,130 +44,15 @@ tree are visited. Since the paths selected by the dominator trees are limited, t #include "ast/ast.h" #include "ast/expr_substitution.h" +#include "ast/rewriter/dom_simplifier.h" #include "tactic/tactic.h" -#include "tactic/tactical.h" -#include "util/obj_pair_hashtable.h" +#include "tactic/dependent_expr_state_tactic.h" +#include "ast/simplifiers/dominator_simplifier.h" - -class expr_dominators { -public: - typedef obj_map> tree_t; -private: - ast_manager& m; - expr_ref m_root; - obj_map m_expr2post; // reverse post-order number - ptr_vector m_post2expr; - tree_t m_parents; - obj_map m_doms; - tree_t m_tree; - - void add_edge(tree_t& tree, expr * src, expr* dst) { - tree.insert_if_not_there(src, ptr_vector()).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 m_result; - expr_dominators m_dominators; - unsigned m_depth; - unsigned m_max_depth; - ptr_vector m_empty; - obj_pair_map 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 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()); +inline tactic* mk_dom_simplify_tactic(ast_manager& m, params_ref const& p) { + return alloc(dependent_expr_state_tactic, m, p, + [](auto& m, auto& p, auto& s) -> dependent_expr_simplifier* { return alloc(dominator_simplifier, m, s, mk_expr_substitution_simplifier(m), p); }); +} /* ADD_TACTIC("dom-simplify", "apply dominator simplification rules.", "mk_dom_simplify_tactic(m, p)")