Remove unused code.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1587 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/simplifier/constantBitP/ConstantBitPropagation.cpp b/src/simplifier/constantBitP/ConstantBitPropagation.cpp
index 0190a567ce29f3687d29da2f622c719eb410ed88..423867b2aafa8579653273cf62dbaf6f142b2edc 100644 (file)
--- a/src/simplifier/constantBitP/ConstantBitPropagation.cpp
+++ b/src/simplifier/constantBitP/ConstantBitPropagation.cpp
@@ -7,11 +7,7 @@
 #include "ConstantBitP_Utility.h"
 #include <iostream>
 #include <fstream>
-
-  #include "ConstantBitP_TransferFunctions.h"
-#ifdef WITHCBITP
-  #include "ConstantBitP_MaxPrecision.h"
-#endif
+#include "ConstantBitP_TransferFunctions.h"
 
 using std::endl;
 using std::cout;
@@ -763,47 +759,6 @@ namespace simplifier
       return result;
 
     }
-
-
-  Result dispatchToMaximallyPrecise(const Kind k, vector<FixedBits*>& children,
-      FixedBits& output, const ASTNode n)
-    {
-  #if WITHCBITP
-
-      Signature signature;
-      signature.kind = k;
-
-      vector<FixedBits> childrenCopy;
-
-      for (int i = 0; i < (int) children.size(); i++)
-      childrenCopy.push_back(*(children[i]));
-      FixedBits outputCopy(output);
-
-      if (k == BVMULT)
-        {
-          // We've got some of multiply already implemented. So help it out by getting some done first.
-          Result r = bvMultiplyBothWays(children, output, n.GetSTPMgr());
-          if (CONFLICT == r)
-          return CONFLICT;
-        }
-
-      bool bad = maxPrecision(children, output, k, n.GetSTPMgr());
-
-      if (bad)
-      return CONFLICT;
-
-      if (!FixedBits::equals(outputCopy, output))
-      return CHANGED;
-
-      for (int i = 0; i < (int) children.size(); i++)
-        {
-          if (!FixedBits::equals(*(children[i]), childrenCopy[i]))
-          return CHANGED;
-        }
-
-  #endif
-      return NOT_IMPLEMENTED;
-    }
   }
 }