* In the bvsolver perform cheap tests which maybe short-cut before expensive tests.

* Lazily count the number of symbols in the bvsolver.

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

diff --git a/src/simplifier/CountOfSymbols.h b/src/simplifier/CountOfSymbols.h
index 3c10ab0332763140de1bf14476c2be7c6732cf3d..1fee0f166170e2c5a19109a80f7e000672cf0704 100644 (file)
--- a/src/simplifier/CountOfSymbols.h
+++ b/src/simplifier/CountOfSymbols.h
@@ -3,16 +3,14 @@
 
 #include "../AST/AST.h"
 #include <cassert>
-#include "simplifier.h"
+
+// Count the number of times each symbol appears in the input term.
+// This can be expensive to build for large terms, so it's built lazily.
 
 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;
 
@@ -20,20 +18,11 @@ class CountOfSymbols {
        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);
-       }
+       ASTNodeSet visited;
 
-       //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)
+               if (visited.find(term) != visited.end())
                        return;
 
                switch (term.GetKind()) {
@@ -63,8 +52,7 @@ class CountOfSymbols {
                }
                }
 
-               //ensures that you don't double count. if you have seen the term
-               //once, then memoize
+               visited.insert(term);
                return;
        } //end of VarsInTheTerm()
 
@@ -78,8 +66,9 @@ public:
        bool single(const ASTNode &m) {
                if (!loaded)
                {
-                       VarsInTheTerm_TopLevel(top);
+                       VarsInTheTerm(top);
                        loaded = true;
+                       visited.clear();
                }
 
                ASTNodeToIntMap::const_iterator it = Vars.find(m);

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index e1d9edd264dcf2d3485a392a0c23f8a67a875947..bca6fdd63796ea7636e0e1b330811e33630a1e0a 100644 (file)
--- a/src/simplifier/bvsolver.cpp
+++ b/src/simplifier/bvsolver.cpp
@@ -11,6 +11,7 @@
 #include "../AST/AST.h"
 #include "../STPManager/STPManager.h"
 #include "bvsolver.h"
+#include "CountOfSymbols.h"
 
 //This file contains the implementation of member functions of
 //bvsolver class, which represents the bitvector arithmetic linear
@@ -196,63 +197,6 @@ namespace BEEV
     return false;
   } //end of UpdateSolverMap()
 
-  //collects the vars in the term 'lhs' into the multiset Vars
-  void BVSolver::VarsInTheTerm_TopLevel(const ASTNode& lhs, 
-                                        ASTNodeMultiSet& Vars)
-  {
-    TermsAlreadySeenMap.clear();
-    VarsInTheTerm(lhs, Vars);
-  }
-
-  //collects the vars in the term 'lhs' into the multiset Vars
-  void BVSolver::VarsInTheTerm(const ASTNode& term, ASTNodeMultiSet& Vars)
-  {
-    ASTNode a = term;
-    ASTNodeMap::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.insert(term);
-        return;
-      case READ:
-        //skip the arrayname, provided the arrayname is a SYMBOL
-        if (SYMBOL == term[0].GetKind())
-          {
-            VarsInTheTerm(term[1], Vars);
-          }
-        else
-          {
-            VarsInTheTerm(term[0], Vars);
-            VarsInTheTerm(term[1], Vars);
-          }
-        break;
-      default:
-        {
-          ASTVec c = term.GetChildren();
-          for (ASTVec::iterator
-                 it = c.begin(), itend = c.end(); it != itend; it++)
-            {
-              VarsInTheTerm(*it, Vars);
-            }
-          break;
-        }
-      }
-
-    //ensures that you don't double count. if you have seen the term
-    //once, then memoize
-    TermsAlreadySeenMap[term] = ASTTrue;
-    return;
-  } //end of VarsInTheTerm()
-
   bool BVSolver::DoNotSolveThis(const ASTNode& var)
   {
     if (DoNotSolve_TheseVars.find(var) != DoNotSolve_TheseVars.end())
@@ -275,8 +219,7 @@ namespace BEEV
     ASTNode zero = _bm->CreateZeroConst(32);
 
     //collect all the vars in the lhs and rhs
-    ASTNodeMultiSet Vars;
-    VarsInTheTerm_TopLevel(lhs, Vars);
+    CountOfSymbols count(lhs);
 
     //handle BVPLUS case
     ASTVec c = lhs.GetChildren();
@@ -290,19 +233,22 @@ namespace BEEV
       {
         ASTNode monom = *it;
         if (SYMBOL == monom.GetKind() 
-            && Vars.count(monom) == 1 
-            && !VarSeenInTerm(monom, rhs) 
-            && !DoNotSolveThis(monom) && !chosen_symbol)
+            && !chosen_symbol
+                       && !DoNotSolveThis(monom)
+            && count.single(monom)
+            && !VarSeenInTerm(monom, rhs)
+        )
           {
             outmonom = monom;
             chosen_symbol = true;
           }
         else if (BVUMINUS == monom.GetKind() 
-                 && SYMBOL == monom[0].GetKind() 
-                 && Vars.count(monom[0]) == 1 
-                 && !DoNotSolveThis(monom[0])
-                 && !VarSeenInTerm(monom[0], rhs) 
-                 && !chosen_symbol)
+                       && SYMBOL == monom[0].GetKind()
+                       && !chosen_symbol
+                       && !DoNotSolveThis(monom[0])
+                && count.single(monom[0])
+                && !VarSeenInTerm(monom[0], rhs)
+                 )
           {
             //cerr << "Chosen Monom: " << monom << endl;
             outmonom = monom;
@@ -330,17 +276,18 @@ namespace BEEV
             if (BVMULT == monom.GetKind() 
                 && BVCONST == monom[0].GetKind() 
                 && _simp->BVConstIsOdd(monom[0]) 
+                && !chosen_odd
+                && !DoNotSolveThis(var)
                 && ((SYMBOL == var.GetKind() 
-                     && Vars.count(var) == 1) 
+                     && count.single(var))
                     || (BVEXTRACT == var.GetKind() 
                         && SYMBOL == var[0].GetKind() 
                         && BVCONST == var[1].GetKind() 
                         && zero == var[2]
-                        && !VarSeenInTerm(var[0], rhs) 
-                        && !DoNotSolveThis(var[0]))) 
-                && !DoNotSolveThis(var) 
+                        && !DoNotSolveThis(var[0])
+                        && !VarSeenInTerm(var[0], rhs)))
                 && !VarSeenInTerm(var, rhs)
-                && !chosen_odd)
+                )
               {
                 //monom[0] is odd.
                 outmonom = monom;