1 files changed, 0 insertions, 41 deletions
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 2f63f1a52..7475feccc 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -33,11 +33,7 @@
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
-
 namespace theory {
-
-class ExtTheory;
-
 namespace bv {
 
 class CoreSolver;
@@ -101,12 +97,6 @@ class TheoryBV : public Theory {
 
   std::string identify() const override { return std::string("TheoryBV"); }
 
-  bool getCurrentSubstitution(int effort,
-                              std::vector<Node>& vars,
-                              std::vector<Node>& subs,
-                              std::map<Node, std::vector<Node>>& exp) override;
-  int getReduction(int effort, Node n, Node& nr) override;
-
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions) override;
 
   TrustNode ppRewrite(TNode t) override;
@@ -177,9 +167,6 @@ class TheoryBV : public Theory {
   /** Index of the next literal to propagate */
   context::CDO<unsigned> d_literalsToPropagateIndex;
 
-  /** Extended theory module, for context-dependent simplification. */
-  std::unique_ptr<ExtTheory> d_extTheory;
-
   /**
    * Keeps a map from nodes to the subtheory that propagated it so that we can explain it
    * properly.
@@ -191,34 +178,6 @@ class TheoryBV : public Theory {
   std::unique_ptr<AbstractionModule> d_abstractionModule;
   bool d_calledPreregister;
 
-  //for extended functions
-  bool d_needsLastCallCheck;
-  context::CDHashSet<Node, NodeHashFunction> d_extf_range_infer;
-  context::CDHashSet<Node, NodeHashFunction> d_extf_collapse_infer;
-  /** do extended function inferences
-   *
-   * This method adds lemmas on the output channel of TheoryBV based on
-   * reasoning about extended functions, such as bv2nat and int2bv. Examples
-   * of lemmas added by this method include:
-   *   0 <= ((_ int2bv w) x) < 2^w
-   *   ((_ int2bv w) (bv2nat x)) = x
-   *   (bv2nat ((_ int2bv w) x)) == x + k*2^w
-   * The purpose of these lemmas is to recognize easy conflicts before fully
-   * reducing extended functions based on their full semantics.
-   */
-  bool doExtfInferences( std::vector< Node >& terms );
-  /** do extended function reductions
-   *
-   * This method adds lemmas on the output channel of TheoryBV based on
-   * reducing all extended function applications that are preregistered to
-   * this theory and have not already been reduced by context-dependent
-   * simplification (see theory/ext_theory.h). Examples of lemmas added by
-   * this method include:
-   *   (bv2nat x) = (ite ((_ extract w w-1) x) 2^{w-1} 0) + ... +
-   *                (ite ((_ extract 1 0) x) 1 0)
-   */
-  bool doExtfReductions( std::vector< Node >& terms );
-
   bool wasPropagatedBySubtheory(TNode literal) const {
     return d_propagatedBy.find(literal) != d_propagatedBy.end();
   }