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

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 fca5a8320bb3189e4e4f741dddcc947de79d026b..f31128226b26207666a6168fab35c649675ec829 100644 (file)
--- 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 b07a67c35221044d4bd0cb6346c791af32dab168..014bec502abb2066437cf66ae2ab2d954d2309f0 100644 (file)
--- 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;