From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 30 May 2010 13:02:47 +0000 (+0000)
Subject: Split out the class which lazily builds the variables in terms.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=e93ea4a7024cb927c94f60335d98410f2325e334;p=francis%2Fstp.git

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
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 735a1c5..cc1f6a1 100644
--- 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())) {