From e459cf4cc1a3a03e0cf3c64184d59bb2ee5ecfef Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 7 May 2020 11:04:24 -0700
Subject: [PATCH] na

---
 src/smt/smt_induction.cpp | 26 ++++++++++++++++++++++++++
 src/smt/smt_induction.h   |  3 +++
 2 files changed, 29 insertions(+)

diff --git a/src/smt/smt_induction.cpp b/src/smt/smt_induction.cpp
index 5497c3fb0..ac629781e 100644
--- a/src/smt/smt_induction.cpp
+++ b/src/smt/smt_induction.cpp
@@ -171,6 +171,32 @@ enode_vector induction_lemmas::induction_positions(enode* n) {
         n->unset_mark2();
     return result;
 }
+
+
+// Collecting induction positions relative to parent.
+induction_lemmas::induction_positions_t induction_lemmas::induction_positions2(enode* n) {
+    induction_positions_t result;
+    enode_vector todo;
+    todo.push_back(n);
+    n->set_mark();
+    for (unsigned i = 0; i < todo.size(); ++i) {
+        enode* n = todo[i];
+        unsigned idx = 0;
+        for (enode* a : smt::enode::args(n)) {
+            if (viable_induction_term(n, a)) {
+                result.push_back(induction_position_t(n, idx));
+            }
+            if (!a->is_marked()) {
+                a->set_mark();
+                todo.push_back(a);
+            }
+            ++idx;
+        }
+    }
+    for (enode* n : todo) 
+        n->unset_mark();
+    return result;
+}
     
 /**
    extract substitutions for x into accessor values of the same sort.
diff --git a/src/smt/smt_induction.h b/src/smt/smt_induction.h
index 27931ab7c..17a5478ba 100644
--- a/src/smt/smt_induction.h
+++ b/src/smt/smt_induction.h
@@ -60,12 +60,15 @@ namespace smt {
         typedef svector<std::pair<expr*,expr*>> expr_pair_vector;
         typedef std::pair<expr_ref_vector, expr_ref> cond_subst_t;
         typedef vector<cond_subst_t> cond_substs_t;
+        typedef std::pair<enode*, unsigned> induction_position_t;
+        typedef svector<induction_position_t> induction_positions_t;
 
         bool viable_induction_sort(sort* s);
         bool viable_induction_parent(enode* p, enode* n);
         bool viable_induction_children(enode* n);
         bool viable_induction_term(enode* p , enode* n);
         enode_vector induction_positions(enode* n);
+        induction_positions_t induction_positions2(enode* n);
         void mk_hypothesis_substs(unsigned depth, expr* x, cond_substs_t& subst);
         void mk_hypothesis_substs_rec(unsigned depth, sort* s, expr* y, expr_ref_vector& conds, cond_substs_t& subst);
         void mk_hypothesis_lemma(expr_ref_vector const& conds, expr_pair_vector const& subst, literal alpha);