From d3e7cd8c52465f6b8b6d7710d8ae3111734a854d Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 17 Jan 2011 11:21:46 +0000
Subject: [PATCH] Speedup. Use the better caching for the bit-vector solver.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1065 e59a4935-1847-0410-ae03-e826735625c1
---
 .../AbstractionRefinement.cpp                 |  3 +
 src/simplifier/CountOfSymbols.h               | 66 -------------------
 src/simplifier/bvsolver.cpp                   | 10 ++-
 3 files changed, 7 insertions(+), 72 deletions(-)
 delete mode 100644 src/simplifier/CountOfSymbols.h

diff --git a/src/absrefine_counterexample/AbstractionRefinement.cpp b/src/absrefine_counterexample/AbstractionRefinement.cpp
index ea24277..9cc8437 100644
--- a/src/absrefine_counterexample/AbstractionRefinement.cpp
+++ b/src/absrefine_counterexample/AbstractionRefinement.cpp
@@ -91,7 +91,10 @@ namespace BEEV
             	// We assume there are no duplicate constant indexes in the list of readindexes,
             	// so "i" and "j" will never be equal.
             	if (BVCONST == index_i.GetKind() && index_j.GetKind() == BVCONST)
+            	{
+            		assert(index_i != index_j);
             		continue;
+            	}
 
                 //prepare for SAT LOOP
                 //first construct the antecedent for the LA axiom
diff --git a/src/simplifier/CountOfSymbols.h b/src/simplifier/CountOfSymbols.h
deleted file mode 100644
index c7f489d..0000000
--- a/src/simplifier/CountOfSymbols.h
+++ /dev/null
@@ -1,66 +0,0 @@
-#ifndef COUNTOFSYMBOLS_H_
-#define COUNTOFSYMBOLS_H_
-
-#include "../AST/AST.h"
-#include <cassert>
-#include "Symbols.h"
-
-// Count the number of times each symbol appears in the input term.
-// This can be expensive to build for large terms, so it's built lazily.
-
-namespace BEEV
-{
-class CountOfSymbols {
-
-	typedef hash_map<ASTNode, int, ASTNode::ASTNodeHasher,
-			ASTNode::ASTNodeEqual> ASTNodeToIntMap;
-
-	ASTNodeToIntMap Vars;
-	const Symbols* top;
-	bool loaded;
-
-	// If no variables are found in "term", then it's cached---we don't need to visit there
-	// again. However, if it's true, we need to revisit (and hence recount), the next time it's
-	// encountered.
-
-	void VarsInTheTerm(const Symbols* term) {
-		assert(!term->empty());
-
-		if (!term->found.IsNull())
-		{
-			Vars[term->found]++;
-		}
-		else
-		{
-			const vector<Symbols*>& c = term->children;
-			for (vector<Symbols*>::const_iterator it = c.begin(), itend = c.end(); it
-					!= itend; it++)
-			{
-				VarsInTheTerm(*it);
-			}
-		}
-	} //end of VarsInTheTerm()
-
-public:
-
-	CountOfSymbols(const Symbols* top_v) :
-		top(top_v) {
-		loaded = false;
-	}
-
-	bool single(const ASTNode &m) {
-		if (!loaded)
-		{
-			VarsInTheTerm(top);
-			loaded = true;
-		}
-
-		ASTNodeToIntMap::const_iterator it = Vars.find(m);
-		if (it == Vars.end())
-			return false;
-		else
-			return (it->second == 1);
-	}
-};
-}
-#endif /* COUNTOFSYMBOLS_H_ */
diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index 51325ff..c98e298 100644
--- a/src/simplifier/bvsolver.cpp
+++ b/src/simplifier/bvsolver.cpp
@@ -11,7 +11,6 @@
 #include "../AST/AST.h"
 #include "../STPManager/STPManager.h"
 #include "bvsolver.h"
-#include "CountOfSymbols.h"
 
 //This file contains the implementation of member functions of
 //bvsolver class, which represents the bitvector arithmetic linear
@@ -99,7 +98,6 @@ namespace BEEV
 
     //collect all the vars in the lhs and rhs
     BuildSymbolGraph(eq);
-    CountOfSymbols count(symbol_graph[eq]);
 
     //handle BVPLUS case
     ASTVec c = FlattenKind(BVPLUS, lhs.GetChildren());
@@ -176,14 +174,14 @@ namespace BEEV
                 && !chosen_symbol
                 && !DoNotSolveThis(var)
                 && ((SYMBOL == var.GetKind() 
-                     && count.single(var)
+                     && !VarSeenInTerm(var,rhs)
                     )
                     || (BVEXTRACT == var.GetKind() 
                         && SYMBOL == var[0].GetKind() 
                         && BVCONST == var[1].GetKind() 
                         && zero == var[2]
                         && !DoNotSolveThis(var[0])
-                        && count.single(var[0])
+                        && !VarSeenInTerm(var[0],rhs)
                         ))
                 )
               {
@@ -198,7 +196,7 @@ namespace BEEV
                 && BVCONST == monom[1].GetKind()
                 && zero == monom[2]
                 && !DoNotSolveThis(monom[0])
-                && count.single(monom[0])
+                && !VarSeenInTerm(monom[0],rhs)
             )
               {
               outmonom = monom;
@@ -212,7 +210,7 @@ namespace BEEV
                        && BVCONST == monom[0][1].GetKind()
                        && zero == monom[0][2]
                        && !DoNotSolveThis(monom[0][0])
-                       && count.single(monom[0][0])
+                       && !VarSeenInTerm(monom[0][0],rhs)
                    )
                      {
                      outmonom = monom;
-- 
2.47.3