From deba7d4d6e74c2896b2f75aeeacc205618157f05 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 7 Oct 2017 14:35:44 +0100
Subject: [PATCH] use idom for checking dominator relationships

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/tactic/core/dom_simplify_tactic.cpp | 24 ++++++++++++++++--------
 src/tactic/core/dom_simplify_tactic.h   |  2 ++
 2 files changed, 18 insertions(+), 8 deletions(-)

diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp
index 366e1edb0..3a6d55569 100644
--- a/src/tactic/core/dom_simplify_tactic.cpp
+++ b/src/tactic/core/dom_simplify_tactic.cpp
@@ -257,11 +257,14 @@ expr_ref dom_simplify_tactic::simplify_arg(expr * e) {
     return r;
 }
 
+/**
+   \brief simplify e recursively.
+*/
 expr_ref dom_simplify_tactic::simplify_rec(expr * e0) {
     expr_ref r(m);
     expr* e = 0;
 
-    TRACE("simplify", tout << "depth: " << m_depth << " " << mk_pp(e0, m) << " -> " << r << "\n";);
+    TRACE("simplify", tout << "depth: " << m_depth << " " << mk_pp(e0, m) << "\n";);
     if (!m_result.find(e0, e)) {
         e = e0;
     }
@@ -408,6 +411,12 @@ void dom_simplify_tactic::simplify_goal(goal& g) {
     SASSERT(scope_level() == 0);
 }
 
+/**
+   \brief determine if a is dominated by b. 
+   Walk the immediate dominators of a upwards until hitting b or a term that is deeper than b.
+   Save intermediary results in a cache to avoid recomputations.
+*/
+
 bool dom_simplify_tactic::is_subexpr(expr * a, expr * b) {
     if (a == b)
         return true;
@@ -416,14 +425,13 @@ bool dom_simplify_tactic::is_subexpr(expr * a, expr * b) {
     if (m_subexpr_cache.find(a, b, r))
         return r;
 
-    for (expr * e : tree(b)) {
-        if (is_subexpr(a, e)) {
-            m_subexpr_cache.insert(a, b, true);
-            return true;
-        }
+    if (get_depth(a) >= get_depth(b)) {
+        return false;
     }
-    m_subexpr_cache.insert(a, b, false);   
-    return false;
+    SASSERT(a != idom(a) && get_depth(idom(a)) > get_depth(a));
+    r = is_subexpr(idom(a), b);
+    m_subexpr_cache.insert(a, b, r);   
+    return r;
 }
 
 ptr_vector<expr> const & dom_simplify_tactic::tree(expr * e) {
diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h
index 4f9851514..79bc9728c 100644
--- a/src/tactic/core/dom_simplify_tactic.h
+++ b/src/tactic/core/dom_simplify_tactic.h
@@ -57,6 +57,7 @@ public:
     bool compile(unsigned sz, expr * const* es);
     tree_t const& get_tree() { return m_tree; }
     void reset();
+    expr* idom(expr *e) const { return m_doms[e]; }
 
     std::ostream& display(std::ostream& out);
 };
@@ -113,6 +114,7 @@ class dom_simplify_tactic : public tactic {
     void cache(expr *t, expr* r) { m_result.insert(t, r); m_trail.push_back(r); }
 
     ptr_vector<expr> const & tree(expr * e);
+    expr* idom(expr *e) const { return m_dominators.idom(e); }
 
     unsigned scope_level() { return m_scope_level; }
     void pop(unsigned n) { SASSERT(n <= m_scope_level); m_scope_level -= n; m_simplifier->pop(n); }