From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 12 Sep 2011 14:58:35 +0000 (+0000)
Subject: Improvement. speed up checking for array terms.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=46a4d46cbc08c2e543fb8a086820c0b2dcce0513;p=francis%2Fstp.git

Improvement. speed up checking for array terms.

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

diff --git a/src/AST/ASTmisc.cpp b/src/AST/ASTmisc.cpp
index 833571a..94f95a9 100644
--- a/src/AST/ASTmisc.cpp
+++ b/src/AST/ASTmisc.cpp
@@ -63,26 +63,32 @@ namespace BEEV
   } //end of arithless
 
 
-bool containsArrayOps(const ASTNode& n, ASTNodeSet& visited)
+bool containsArrayOps(const ASTNode& n, hash_set<int> & visited)
 {
-	if (visited.find(n) != visited.end())
-		return false;
-	if (n.GetType() == ARRAY_TYPE)
-		return true;
+        if (n.GetIndexWidth() > 0)
+            return true;
+
+        if (n.Degree() ==0)
+            return false;
+
+        if (visited.find(n.GetNodeNum()) != visited.end())
+            return false;
+
+        visited.insert(n.GetNodeNum());
 
 	for (int i =0; i < n.Degree();i++)
 		if (containsArrayOps(n[i],visited))
 			return true;
 
-	visited.insert(n);
 	return false;
 }
 
-bool containsArrayOps(const ASTNode&n)
-{
-	ASTNodeSet visited;
-	return containsArrayOps(n, visited);
-}
+    bool
+    containsArrayOps(const ASTNode&n)
+    {
+        hash_set<int> visited;
+        return containsArrayOps(n, visited);
+    }
 
 	bool isCommutative(const Kind k) {
 	switch (k) {
diff --git a/src/AST/ArrayTransformer.cpp b/src/AST/ArrayTransformer.cpp
index 3ca6d83..de4bdbc 100644
--- a/src/AST/ArrayTransformer.cpp
+++ b/src/AST/ArrayTransformer.cpp
@@ -746,7 +746,7 @@ namespace BEEV
 		  ASTNode elsRead = nf->CreateTerm(READ, width, els, readIndex);
 		  assert(BVTypeCheck(elsRead));
 
-		  /* We try to call TransformArrayRead only if necessary, because it
+		  /* We try to call TransformTerm only if necessary, because it
 		   * introduces a new symbol for each read. The amount of work we
 		   * need to do later is based on the square of the number of symbols.
 		   */