From df947fd311ee4e1df060338968ede7328affa530 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 13 Mar 2011 04:09:22 +0000
Subject: [PATCH] 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
---
 src/simplifier/simplifier.cpp | 46 -----------------------------------
 src/simplifier/simplifier.h   |  6 -----
 2 files changed, 52 deletions(-)

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 7819e77..eac0d75 100644
--- 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 02bc83b..a53837d 100644
--- 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);
-- 
2.47.3