remove dependencies on stale component

Z3Prover · Aug 17, 2021 · 749d1ab · 749d1ab
1 parent 3516c52
commit 749d1ab
Show file tree

Hide file tree

Showing 6 changed files with 1 addition and 14 deletions.
diff --git 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
@@ -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
@@ -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 → src/smt/smt_induction.cpp.disabled b/src/smt/smt_induction.cpp → src/smt/smt_induction.cpp.disabled
diff --git a/src/smt/smt_induction.h → src/smt/smt_induction.h.disabled b/src/smt/smt_induction.h → src/smt/smt_induction.h.disabled
diff --git 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"