From 0f3c56213ebffedd5cf52bc6099c14a3cd9d9039 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 27 Jan 2023 17:11:48 -0800
Subject: [PATCH] move dominator simplifier functionality to rewriter and
simplifier, move bv_bounds simplifier functionality to simplifier
---
src/ast/rewriter/CMakeLists.txt | 1 +
src/ast/rewriter/bv_bounds_base.h | 566 +++++++++++++++++
src/ast/rewriter/dom_simplifier.cpp | 325 ++++++++++
src/ast/rewriter/dom_simplifier.h | 86 +++
src/ast/simplifiers/CMakeLists.txt | 2 +
src/ast/simplifiers/bv_bounds_simplifier.cpp | 65 ++
src/ast/simplifiers/bv_bounds_simplifier.h | 18 +
src/ast/simplifiers/dominator_simplifier.cpp | 303 +++++++++
src/ast/simplifiers/dominator_simplifier.h | 71 +++
src/tactic/bv/bv_bounds_tactic.cpp | 606 +-----------------
src/tactic/core/CMakeLists.txt | 1 -
src/tactic/core/dom_simplify_tactic.cpp | 613 -------------------
src/tactic/core/dom_simplify_tactic.h | 129 +---
13 files changed, 1456 insertions(+), 1330 deletions(-)
create mode 100644 src/ast/rewriter/bv_bounds_base.h
create mode 100644 src/ast/rewriter/dom_simplifier.cpp
create mode 100644 src/ast/rewriter/dom_simplifier.h
create mode 100644 src/ast/simplifiers/bv_bounds_simplifier.cpp
create mode 100644 src/ast/simplifiers/bv_bounds_simplifier.h
create mode 100644 src/ast/simplifiers/dominator_simplifier.cpp
create mode 100644 src/ast/simplifiers/dominator_simplifier.h
delete mode 100644 src/tactic/core/dom_simplify_tactic.cpp
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<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);
+ }
+
+ };
+
+}
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<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);
+}
+
+
+
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<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);
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<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;
+}
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<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); }
+};
+
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 <climits>
-static uint64_t uMaxInt(unsigned sz) {
- SASSERT(sz <= 64);
- return ULLONG_MAX >> (64u - sz);
-}
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) {}
- 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 {
+ 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<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));
-}
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<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());
+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)")