Bugfix. Variables were reported as only occuring a single time, when they actually...

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

diff --git a/src/simplifier/CountOfSymbols.h b/src/simplifier/CountOfSymbols.h
index 1fee0f166170e2c5a19109a80f7e000672cf0704..4041f56e5a28285b6dc5e645b6bcda6bc40a32c1 100644 (file)
--- a/src/simplifier/CountOfSymbols.h
+++ b/src/simplifier/CountOfSymbols.h
@@ -20,40 +20,47 @@ class CountOfSymbols {
 
        ASTNodeSet visited;
 
-       void VarsInTheTerm(const ASTNode& term) {
+       // 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.
+
+       bool VarsInTheTerm(const ASTNode& term) {
 
                if (visited.find(term) != visited.end())
-                       return;
+                       return false;
+
+               bool found = false;
 
                switch (term.GetKind()) {
                case BVCONST:
-                       return;
+                       return false;
                case SYMBOL:
                        //cerr << "debugging: symbol added: " << term << endl;
                        Vars[term]++;
-                       return;
+                       return true;
                case READ:
                        //skip the arrayname, provided the arrayname is a SYMBOL
                        //But we don't skip it if it's a WRITE function??
                        if (SYMBOL == term[0].GetKind()) {
-                               VarsInTheTerm(term[1]);
+                               found |= VarsInTheTerm(term[1]);
                        } else {
-                               VarsInTheTerm(term[0]);
-                               VarsInTheTerm(term[1]);
+                               found |= VarsInTheTerm(term[0]);
+                               found |= VarsInTheTerm(term[1]);
                        }
                        break;
                default: {
                        const ASTVec& c = term.GetChildren();
                        for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it
                                        != itend; it++) {
-                               VarsInTheTerm(*it);
+                               found |= VarsInTheTerm(*it);
                        }
                        break;
                }
                }
 
-               visited.insert(term);
-               return;
+               if (!found)
+                       visited.insert(term);
+               return found;
        } //end of VarsInTheTerm()
 
 public: