Split out the class which lazily builds the variables in terms.

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

diff --git a/src/simplifier/CountOfSymbols.h b/src/simplifier/CountOfSymbols.h
new file mode 100644 (file)
index 0000000..244e44a
--- /dev/null
+++ b/src/simplifier/CountOfSymbols.h
@@ -0,0 +1,93 @@
+#ifndef COUNTOFSYMBOLS_H_
+#define COUNTOFSYMBOLS_H_
+
+#include "../AST/AST.h"
+#include <cassert>
+#include "simplifier.h"
+
+namespace BEEV
+{
+class CountOfSymbols {
+
+
+       //collect all the vars in the lhs and rhs
+       //Build this only if it's needed.
+
+       typedef hash_map<ASTNode, int, ASTNode::ASTNodeHasher,
+                       ASTNode::ASTNodeEqual> ASTNodeToIntMap;
+
+       ASTNodeToIntMap Vars;
+       const ASTNode& top;
+       bool loaded;
+
+       ASTNodeSet TermsAlreadySeenMap;
+
+       //collects the vars in the term 'lhs' into the multiset Vars
+       void VarsInTheTerm_TopLevel(const ASTNode& lhs) {
+               TermsAlreadySeenMap.clear();
+               VarsInTheTerm(lhs);
+       }
+
+       //collects the vars in the term 'lhs' into the multiset Vars
+       void VarsInTheTerm(const ASTNode& term) {
+               ASTNodeSet::const_iterator it;
+               bool inserted = (TermsAlreadySeenMap.insert(term).second);
+
+               if (!inserted)
+                       return;
+
+               switch (term.GetKind()) {
+               case BVCONST:
+                       return;
+               case SYMBOL:
+                       //cerr << "debugging: symbol added: " << term << endl;
+                       Vars[term]++;
+                       break;
+               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]);
+                       } else {
+                               VarsInTheTerm(term[0]);
+                               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);
+                       }
+                       break;
+               }
+               }
+
+               //ensures that you don't double count. if you have seen the term
+               //once, then memoize
+               return;
+       } //end of VarsInTheTerm()
+
+public:
+
+       CountOfSymbols(const ASTNode& top_v) :
+               top(top_v) {
+               loaded = false;
+       }
+
+       bool single(const ASTNode &m) {
+               if (!loaded)
+               {
+                       VarsInTheTerm_TopLevel(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/bvsolverExp.cpp b/src/simplifier/bvsolverExp.cpp
index 735a1c53fa77bf3416ec82c1e106fa2f127f9fe1..cc1f6a1092328e69eba58759e17ba0280e34195d 100644 (file)
--- a/src/simplifier/bvsolverExp.cpp
+++ b/src/simplifier/bvsolverExp.cpp
@@ -1,4 +1,4 @@
-// Experiment bvsolver.
+// Experimental bvsolver.
 
 
 /********************************************************************
@@ -14,6 +14,7 @@
 #include "bvsolverExp.h"
 #include <cassert>
 #include "simplifier.h"
+#include "CountOfSymbols.h"
 
 //This file contains the implementation of member functions of
 //bvsolver class, which represents the bitvector arithmetic linear
@@ -165,85 +166,6 @@ bool BVSolverExp::DoNotSolveThis(const ASTNode& var) {
        return false;
 }
 
-class CountOfSymbols {
-       //collect all the vars in the lhs and rhs
-       //Build this only if it's needed.
-
-       typedef hash_map<ASTNode, int, ASTNode::ASTNodeHasher,
-                       ASTNode::ASTNodeEqual> ASTNodeToIntMap;
-
-       ASTNodeToIntMap Vars;
-       const ASTNode& top;
-       bool loaded;
-
-       ASTNodeSet TermsAlreadySeenMap;
-
-       //collects the vars in the term 'lhs' into the multiset Vars
-       void VarsInTheTerm_TopLevel(const ASTNode& lhs) {
-               TermsAlreadySeenMap.clear();
-               VarsInTheTerm(lhs);
-       }
-
-       //collects the vars in the term 'lhs' into the multiset Vars
-       void VarsInTheTerm(const ASTNode& term) {
-               ASTNodeSet::const_iterator it;
-               if ((it = TermsAlreadySeenMap.find(term)) != TermsAlreadySeenMap.end()) {
-                       //if the term has been seen, then simply return
-                       return;
-               }
-
-               switch (term.GetKind()) {
-               case BVCONST:
-                       return;
-               case SYMBOL:
-                       //cerr << "debugging: symbol added: " << term << endl;
-                       Vars[term]++;
-                       break;
-               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]);
-                       } else {
-                               VarsInTheTerm(term[0]);
-                               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);
-                       }
-                       break;
-               }
-               }
-
-               //ensures that you don't double count. if you have seen the term
-               //once, then memoize
-               TermsAlreadySeenMap.insert(term);
-               return;
-       } //end of VarsInTheTerm()
-
-public:
-
-       CountOfSymbols(const ASTNode& top_v) :
-               top(top_v) {
-               loaded = false;
-       }
-
-       bool single(const ASTNode &m) {
-               if (!loaded)
-                       VarsInTheTerm_TopLevel(top);
-
-               ASTNodeToIntMap::const_iterator it = Vars.find(m);
-               if (it == Vars.end())
-                       return false;
-               else
-                       return (it->second == 1);
-       }
-};
-
 //chooses a variable in the lhs and returns the chosen variable
 ASTNode BVSolverExp::ChooseMonom(const ASTNode& eq, ASTNode& modifiedlhs) {
        if (!(EQ == eq.GetKind() && BVPLUS == eq[0].GetKind())) {