From 75aae8bc61cbf98714554392cbbb4de0b1ca8fa9 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 16 Jun 2010 03:22:39 +0000
Subject: [PATCH] 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
---
 src/simplifier/bvsolver.cpp | 37 +++----------------------------------
 1 file changed, 3 insertions(+), 34 deletions(-)

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index 4bdc3cd..aa5a08a 100644
--- 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;
-- 
2.47.3