From 749d1ab3052e61ba6ad8bd1414e05c1f6ebb55b1 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 16 Aug 2021 17:51:59 -0700
Subject: [PATCH] remove dependencies on stale component

---
 src/smt/CMakeLists.txt                                 |  1 -
 src/smt/smt_context.cpp                                | 10 ----------
 src/smt/smt_context.h                                  |  3 ---
 .../{smt_induction.cpp => smt_induction.cpp.disabled}  |  0
 src/smt/{smt_induction.h => smt_induction.h.disabled}  |  0
 src/smt/theory_recfun.h                                |  1 +
 6 files changed, 1 insertion(+), 14 deletions(-)
 rename src/smt/{smt_induction.cpp => smt_induction.cpp.disabled} (100%)
 rename src/smt/{smt_induction.h => smt_induction.h.disabled} (100%)

diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt
index 77757b5e60f..9d2a2b40683 100644
--- a/src/smt/CMakeLists.txt
+++ b/src/smt/CMakeLists.txt
@@ -30,7 +30,6 @@ z3_add_component(smt
     smt_farkas_util.cpp
     smt_for_each_relevant_expr.cpp
     smt_implied_equalities.cpp
-    smt_induction.cpp
     smt_internalizer.cpp
     smt_justification.cpp
     smt_kernel.cpp
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index ad1dda4b28b..8ebbe506a3e 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -1667,16 +1667,6 @@ namespace smt {
             !m_th_diseq_propagation_queue.empty();
     }
 
-    /**
-       \brief retrieve facilities for creating induction lemmas.
-     */
-    induction& context::get_induction() {
-        if (!m_induction) {
-            m_induction = alloc(induction, *this, get_manager());
-        }
-        return *m_induction;
-    }
-
     /**
        \brief unit propagation.
        Cancelation is not safe during propagation at base level because
diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 20d17795588..a607deab3a1 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -33,7 +33,6 @@ Revision History:
 #include "smt/smt_statistics.h"
 #include "smt/smt_conflict_resolution.h"
 #include "smt/smt_relevancy.h"
-#include "smt/smt_induction.h"
 #include "smt/smt_case_split_queue.h"
 #include "smt/smt_almost_cg_table.h"
 #include "smt/smt_failure.h"
@@ -184,7 +183,6 @@ namespace smt {
         unsigned                    m_simp_qhead { 0 };
         int                         m_simp_counter { 0 }; //!< can become negative
         scoped_ptr<case_split_queue> m_case_split_queue;
-        scoped_ptr<induction>       m_induction;
         double                      m_bvar_inc { 1.0 };
         bool                        m_phase_cache_on { true };
         unsigned                    m_phase_counter { 0 }; //!< auxiliary variable used to decide when to turn on/off phase caching
@@ -1323,7 +1321,6 @@ namespace smt {
     public:
         bool can_propagate() const;
 
-        induction& get_induction(); 
 
         // Retrieve arithmetic values. 
         bool get_arith_lo(expr* e, rational& lo, bool& strict);
diff --git a/src/smt/smt_induction.cpp b/src/smt/smt_induction.cpp.disabled
similarity index 100%
rename from src/smt/smt_induction.cpp
rename to src/smt/smt_induction.cpp.disabled
diff --git a/src/smt/smt_induction.h b/src/smt/smt_induction.h.disabled
similarity index 100%
rename from src/smt/smt_induction.h
rename to src/smt/smt_induction.h.disabled
diff --git a/src/smt/theory_recfun.h b/src/smt/theory_recfun.h
index c6dead6c497..097181d2206 100644
--- a/src/smt/theory_recfun.h
+++ b/src/smt/theory_recfun.h
@@ -18,6 +18,7 @@ Revision History:
 --*/
 #pragma once
 
+#include "util/scoped_ptr_vector.h"
 #include "smt/smt_theory.h"
 #include "smt/smt_context.h"
 #include "ast/ast_pp.h"