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 833571a32786cb4708a91f4843106a5bc5e5b41b..94f95a9e75597d1553f4499b8d5505d122b6df2c 100644 (file)
--- 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 3ca6d83033b62dfc76ffe6789509651d53f07152..de4bdbc2e80c6261050a30ad59344a83751027ac 100644 (file)
--- 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.
                   */