From c94a9e8dddb9b6ec2b9ab772a6ade28264c12023 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 1 May 2020 13:17:37 -0700
Subject: [PATCH] na

---
 src/smt/smt_induction.cpp | 53 ++++++++++++++++++++++++++-------------
 src/smt/smt_induction.h   |  6 ++++-
 2 files changed, 40 insertions(+), 19 deletions(-)

diff --git a/src/smt/smt_induction.cpp b/src/smt/smt_induction.cpp
index e6ee18c4f..6a98520bd 100644
--- a/src/smt/smt_induction.cpp
+++ b/src/smt/smt_induction.cpp
@@ -105,33 +105,49 @@ literal_vector collect_induction_literals::operator()() {
 // --------------------------------------
 // create_induction_lemmas
 
-bool create_induction_lemmas::is_induction_candidate(enode* n) {
-    app* e = n->get_owner();
-    if (m.is_value(e))
-        return false;
+bool create_induction_lemmas::viable_induction_sort(sort* s) {
+    // potentially also induction on integers, sequences
+    return m_dt.is_datatype(s) && m_dt.is_recursive(s);
+}
+
+bool create_induction_lemmas::viable_induction_parent(enode* n) {
     bool in_good_context = false;
     for (enode* p : n->get_parents()) {
         app* o = p->get_owner();
-        if (o->get_family_id() != m.get_basic_family_id())
-            in_good_context = true;
+        if (o->get_family_id() == m.get_basic_family_id())
+            continue;
+        if (o->get_family_id() == m_rec.get_family_id()) {
+            in_good_context |= m_rec.is_defined(o);
+            continue;
+        }
+        if (o->get_family_id() == m_dt.get_family_id()) {
+            in_good_context |= m_dt.is_constructor(o);
+            continue;
+        }
     }
-    if (!in_good_context)
-        return false;
+    return in_good_context;
+}
 
-    // avoid recursively unfolding skolem terms.
-    if (e->get_num_args() > 0 && e->get_family_id() == null_family_id) {
+bool create_induction_lemmas::viable_induction_term(enode* n) {
+    app* e = n->get_owner();
+    if (m.is_value(e))
         return false;
-    }
-    sort* s = m.get_sort(e);
-    if (m_dt.is_datatype(s) && m_dt.is_recursive(s))
+    if (n->get_num_args() == 0)
         return true;
-    
-    // potentially also induction on integers, sequences
-    // m_arith.is_int(s)
-    //  return true;
+    if (e->get_family_id() == m_rec.get_family_id()) 
+        return m_rec.is_defined(e);
+    if (e->get_family_id() == m_dt.get_family_id()) 
+        return m_dt.is_constructor(e);
     return false;
 }
 
+bool create_induction_lemmas::viable_induction_position(enode* n) {
+    return 
+        viable_induction_sort(m.get_sort(n->get_owner())) &&
+        viable_induction_parent(n) &&
+        viable_induction_term(n);
+}
+
 /**
  * positions in n that can be used for induction
  * the positions are distinct roots
@@ -152,7 +168,7 @@ enode_vector create_induction_lemmas::induction_positions(enode* n) {
         n = todo[i];
         for (enode* a : smt::enode::args(n)) 
             add_todo(a);        
-        if (is_induction_candidate(n)) 
+        if (viable_induction_position(n)) 
             result.push_back(n);
     }
     for (enode* n : todo)
@@ -365,6 +381,7 @@ create_induction_lemmas::create_induction_lemmas(context& ctx, ast_manager& m, v
     vs(vs),
     m_dt(m),
     m_a(m),
+    m_rec(m),
     m_num_lemmas(0)
 {}
 
diff --git a/src/smt/smt_induction.h b/src/smt/smt_induction.h
index 2a2e317f9..93f209107 100644
--- a/src/smt/smt_induction.h
+++ b/src/smt/smt_induction.h
@@ -54,6 +54,7 @@ namespace smt {
         value_sweep&   vs;
         datatype::util m_dt;
         arith_util     m_a;
+        recfun::util   m_rec;
         unsigned       m_num_lemmas;
 
         typedef svector<std::pair<expr*,expr*>> expr_pair_vector;
@@ -82,7 +83,10 @@ namespace smt {
         };
         typedef vector<abstraction_arg> abstraction_args;
 
-        bool is_induction_candidate(enode* n);
+        bool viable_induction_sort(sort* s);
+        bool viable_induction_parent(enode* n);
+        bool viable_induction_term(enode* n);
+        bool viable_induction_position(enode* n);
         enode_vector induction_positions(enode* n);
         void abstract(enode* n, enode* t, expr* x, abstractions& result);
         void abstract1(enode* n, enode* t, expr* x, abstractions& result);