From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 1 Feb 2011 12:40:57 +0000 (+0000)
Subject: Speedup. Track which sets have already being added to a cache, and don't add them... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=4476961e7aef0f1e3fb9e642c1b53f00465c3c13;p=francis%2Fstp.git

Speedup. Track which sets have already being added to a cache, and don't add them again.

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

diff --git a/src/simplifier/SubstitutionMap.cpp b/src/simplifier/SubstitutionMap.cpp
index fca5a83..f311282 100644
--- a/src/simplifier/SubstitutionMap.cpp
+++ b/src/simplifier/SubstitutionMap.cpp
@@ -319,8 +319,18 @@ void SubstitutionMap::buildDepends(const ASTNode& n0, const ASTNode& n1)
 	{
 		if (i!=0 && av[i] == av[i-1])
 			continue; // Treat it like a set of Symbol* in effect.
-		const ASTNodeSet& sym = *(vars.TermsAlreadySeenMap.find(av[i])->second);
-		rhs.insert(sym.begin(), sym.end());
+
+		ASTNodeSet* sym = (vars.TermsAlreadySeenMap.find(av[i])->second);
+		if(rhsAlreadyAdded.find(sym) != rhsAlreadyAdded.end())
+			continue;
+		rhsAlreadyAdded.insert(sym);
+
+		//cout << loopCount++ << " ";
+		//cout << "initial" << rhs.size() << " Adding: " <<sym->size();
+		rhs.insert(sym->begin(), sym->end());
+		//cout << "final:" << rhs.size();
+		//cout << "added:" << sym << endl;
+
 	}
 
 	assert (dependsOn.find(n0) == dependsOn.end());
diff --git a/src/simplifier/SubstitutionMap.h b/src/simplifier/SubstitutionMap.h
index b07a67c..014bec5 100644
--- a/src/simplifier/SubstitutionMap.h
+++ b/src/simplifier/SubstitutionMap.h
@@ -29,6 +29,7 @@ class SubstitutionMap {
 	typedef hash_map<ASTNode, Symbols*,ASTNode::ASTNodeHasher> DependsType;
 	DependsType dependsOn; // The lhs depends on the variables in the rhs.
 	ASTNodeSet rhs; // All the rhs that have been seeen.
+	set<ASTNodeSet*> rhsAlreadyAdded;
 	VariablesInExpression::SymbolPtrSet rhs_visited; // the rhs contains all the variables in here already.
 
 	int loopCount;
@@ -46,6 +47,7 @@ public:
 		dependsOn.clear();
 		rhs.clear();
 		rhs_visited.clear();
+		rhsAlreadyAdded.clear();
 	}
 
 	VariablesInExpression vars;