Speed up VarSeenInTerm(..) slightly.

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

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index 4bdc3cda3d5b5085c27997764967c73998d61894..aa5a08a9690956dae1eef0ea4e722177f85aa647 100644 (file)
--- a/src/simplifier/bvsolver.cpp
+++ b/src/simplifier/bvsolver.cpp
@@ -932,36 +932,6 @@ namespace BEEV
 
   bool BVSolver::VarSeenInTerm(const ASTNode& var, const ASTNode& term)
   {
-    if (READ == term.GetKind() 
-        && WRITE == term[0].GetKind() 
-        && !_bm->GetRemoveWritesFlag())
-      {
-       /*
-               Trevor: This used to return false. But fails on the below input.
-               I don't know why the case of read-over-write was handled specially.
-
-
-               Printing: after simplification:
-               30:(EQ
-                 12:b3
-                 26:(READ
-                       22:(WRITE
-                         14:a3
-                         18:0b0000000000
-                         18:0b0000000000)
-                       12:b3))
-        */
-
-       //return false;
-      }
-
-    if (READ == term.GetKind() 
-        && WRITE == term[0].GetKind() 
-        && _bm->GetRemoveWritesFlag())
-      {
-        //return true;
-      }
-
     ASTNodeMap::iterator it;
     if ((it = TermsAlreadySeenMap.find(term)) != TermsAlreadySeenMap.end())
       {
@@ -976,6 +946,9 @@ namespace BEEV
         return true;
       }
 
+    if (term.isConstant())
+       return false;
+
     for (ASTVec::const_iterator 
            it = term.begin(), itend = term.end();
          it != itend; it++)
@@ -984,10 +957,6 @@ namespace BEEV
           {
             return true;
           }
-        else
-          {
-            TermsAlreadySeenMap[*it] = var;
-          }
       }
 
     TermsAlreadySeenMap[term] = var;