From 13883de389d818122c71f4a9699fd7a107fa068e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 10 Mar 2020 20:13:25 -0700
Subject: [PATCH] fix #3177

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/tactic/core/reduce_invertible_tactic.cpp | 88 +++++++++++---------
 src/tactic/tactic.cpp                        |  2 +
 2 files changed, 51 insertions(+), 39 deletions(-)

diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp
index 697a67250..d7160e166 100644
--- a/src/tactic/core/reduce_invertible_tactic.cpp
+++ b/src/tactic/core/reduce_invertible_tactic.cpp
@@ -51,43 +51,49 @@ public:
     }
     
     void operator()(goal_ref const & g, goal_ref_buffer & result) override {
-        TRACE("reduce_invertible", g->display(tout););
         tactic_report report("reduce-invertible", *g);
-        m_inverted.reset();
-        m_parents.reset();
-        collect_parents(g);
-        collect_occs occs;
-        obj_hashtable<expr> vars;
-        generic_model_converter_ref mc;
-        occs(*g, vars);
-        expr_safe_replace sub(m);
-        expr_ref new_v(m);
-        expr * p;
-        for (expr* v : vars) {
-            if (is_invertible(v, p, new_v, &mc)) {
-                mark_inverted(p);
-                sub.insert(p, new_v);
+        bool change = true;
+        while (change) {
+            change = false;
+            m_inverted.reset();
+            m_parents.reset();
+            collect_parents(g);
+            collect_occs occs;
+            obj_hashtable<expr> vars;
+            generic_model_converter_ref mc;
+            occs(*g, vars);
+            expr_safe_replace sub(m);
+            expr_ref new_v(m);
+            expr * p;
+            for (expr* v : vars) {
+                if (is_invertible(v, p, new_v, &mc)) {
+                    mark_inverted(p);
+                    sub.insert(p, new_v);
+                    TRACE("invertible_tactic", tout << mk_pp(p, m) << " " << new_v << "\n";);
+                    change = true;
+                    break;
+                }
             }
-        }
-        reduce_q_rw rw(*this);
-        unsigned sz = g->size();
-        for (unsigned idx = 0; idx < sz; idx++) {
-            checkpoint();
-            expr* f = g->form(idx);
-            expr_ref f_new(m);
-            sub(f, f_new);
-            rw(f_new, f_new);
-            if (f == f_new) continue;
-            proof_ref new_pr(m);
-            if (g->proofs_enabled()) {
-                proof * pr = g->pr(idx);
-                new_pr     = m.mk_modus_ponens(pr, new_pr);
-            }
-            g->update(idx, f_new, new_pr, g->dep(idx));
-        }  
-        if (mc) g->add(mc.get());
-        result.push_back(g.get());
-        g->inc_depth();        
+            reduce_q_rw rw(*this);
+            unsigned sz = g->size();
+            for (unsigned idx = 0; idx < sz; idx++) {
+                checkpoint();
+                expr* f = g->form(idx);
+                expr_ref f_new(m);
+                sub(f, f_new);
+                rw(f_new, f_new);
+                if (f == f_new) continue;
+                proof_ref new_pr(m);
+                if (g->proofs_enabled()) {
+                    proof * pr = g->pr(idx);
+                    new_pr     = m.mk_modus_ponens(pr, new_pr);
+                }
+                g->update(idx, f_new, new_pr, g->dep(idx));
+            }  
+            if (mc) g->add(mc.get());
+            result.push_back(g.get());
+            g->inc_depth();
+        }        
     }
 
     void cleanup() override {}
@@ -239,11 +245,13 @@ private:
     // TBD: could be made to be recursive, by walking multiple layers of parents.
     
     bool is_invertible(expr* v, expr*& p, expr_ref& new_v, generic_model_converter_ref* mc, unsigned max_var = 0) {
-        if (m_parents.size() <= v->get_id()) return false;
+        if (m_parents.size() <= v->get_id()) {
+            return false;
+        }
         p = m_parents[v->get_id()].get();
-        if (!p) return false;
-        if (m_inverted.is_marked(p)) return false;
-        if (mc && !is_ground(p)) return false;
+        if (!p || m_inverted.is_marked(p) || (mc && !is_ground(p))) {
+            return false;
+        }
 
         if (m_bv.is_bv_xor(p) ||
             m_bv.is_bv_not(p) ||
@@ -380,6 +388,7 @@ private:
         }
        
         if (m.is_eq(p, e1, e2)) {
+            TRACE("invertible_tactic", tout << mk_pp(v, m) << "\n";);
             if (mc && has_diagonal(e1)) {
                 ensure_mc(mc);
                 new_v = m.mk_fresh_const("eq", m.mk_bool_sort());
@@ -465,6 +474,7 @@ private:
             for (unsigned i = 0; i < vars.size(); ++i) {
                 var* v = vars[i];
                 if (!occurs_under_nested_q(v, new_body) && t.is_invertible(v, p, new_v, nullptr, vars.size())) {
+                    TRACE("invertible_tactic", tout << mk_pp(v, m) << " " << mk_pp(p, m) << "\n";);
                     t.mark_inverted(p);
                     sub.insert(p, new_v);
                     new_sorts[i] = m.get_sort(new_v);
diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp
index ca4ca9dcf..6833f991d 100644
--- a/src/tactic/tactic.cpp
+++ b/src/tactic/tactic.cpp
@@ -34,11 +34,13 @@ struct tactic_report::imp {
         m_goal(g),
         m_start_memory(static_cast<double>(memory::get_allocation_size())/static_cast<double>(1024*1024)) {
         m_watch.start();
+        TRACE("tactic", g.display(tout << id << "\n"););
     }
         
     ~imp() {
         m_watch.stop();
         double end_memory = static_cast<double>(memory::get_allocation_size())/static_cast<double>(1024*1024);
+        TRACE("tactic", m_goal.display(tout););
         IF_VERBOSE(0, 
                    verbose_stream() << "(" << m_id
                    << " :num-exprs " << m_goal.num_exprs()