Refactor. Remove code that's not used.

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

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 7819e77c08e03c23f92cc4b575e16107a4e331fc..eac0d75387521607c918f53dce4421ba4f68f3d3 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -770,30 +770,6 @@ namespace BEEV
     return output;
   }
 
-  //Look through the AND Node for terms that contradict.
-  //Should be made significantly more general..
-  ASTNode Simplifier::RemoveContradictionsFromAND(const ASTNode& in)
-  {
-    assert(AND == in.GetKind());
-    const int childrenSize = in.GetChildren().size();
-
-    for (int i = 0; i < childrenSize; i++)
-      {
-        if (BVLT != in[i].GetKind())
-          continue;
-
-        for (int j = i + 1; j < childrenSize; j++)
-          {
-            if (BVLT != in[j].GetKind())
-              continue;
-            // parameters are swapped.
-            if (in[i][0] == in[j][1] && in[i][1] == in[j][0])
-              return ASTFalse;
-          }
-      }
-    return in;
-  }
-
   // turns say (bvslt (ite a b c) (ite a d e)) INTO (ite a (bvslt b d)
   // (bvslt c e)) Expensive. But makes some other simplifications
   // possible.
@@ -3032,7 +3008,6 @@ namespace BEEV
     UpdateSimplifyMap(actualInputterm, output, false, VarConstMap);
 
     //cerr << "SimplifyTerm: output" << output << endl;
-    // CheckSimplifyInvariant(inputterm,output);
 
     assert(!output.IsNull());
     assert(inputterm.GetValueWidth() == output.GetValueWidth());
@@ -3041,27 +3016,6 @@ namespace BEEV
     return output;
   } //end of SimplifyTerm()
 
-  //At the end of each simplification call, we want the output to be
-  //always smaller or equal to the input in size.
-  void Simplifier::CheckSimplifyInvariant(const ASTNode& a, 
-                                          const ASTNode& output)
-  {
-
-    if (_bm->NodeSize(a, true) + 1 < _bm->NodeSize(output, true))
-      {
-        cerr << "lhs := " << a << endl;
-        cerr << "NodeSize of lhs is: " 
-             << _bm->NodeSize(a, true) << endl;
-        cerr << endl;
-        cerr << "rhs := " << output << endl;
-        cerr << "NodeSize of rhs is: " 
-             << _bm->NodeSize(output, true) << endl;
-        //  FatalError("SimplifyFormula: The nodesize shoudl decrease
-        //  from lhs to rhs: ",ASTUndefined);
-      }
-  }
-
-
   //this function assumes that the input is a vector of childnodes of
   //a BVPLUS term. it combines like terms and returns a bvplus
   //term. e.g. 1.x + 2.x is converted to 3.x

diff --git a/src/simplifier/simplifier.h b/src/simplifier/simplifier.h
index 02bc83bc10f66498c26ee18143375b1a10a9e45c..a53837d518f450ef8e2e5a1c9b9df37ea661f279 100644 (file)
--- a/src/simplifier/simplifier.h
+++ b/src/simplifier/simplifier.h
@@ -148,10 +148,6 @@ namespace BEEV
                                            bool pushNeg, 
                                            ASTNodeMap* VarConstMap=NULL);
 
-    void CheckSimplifyInvariant(const ASTNode& a, 
-                                const ASTNode& output);
-
-
     ASTNode SimplifyAtomicFormula(const ASTNode& a, 
                                   bool pushNeg, 
                                   ASTNodeMap* VarConstMap=NULL);
@@ -164,8 +160,6 @@ namespace BEEV
 
     ASTNode PullUpITE(const ASTNode& in);
 
-    ASTNode RemoveContradictionsFromAND(const ASTNode& in);
-      
     ASTNode CreateSimplifiedTermITE(const ASTNode& t1, 
                                     const ASTNode& t2, 
                                     const ASTNode& t3);