Speedup. Use the better caching for the bit-vector solver.

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

diff --git a/src/absrefine_counterexample/AbstractionRefinement.cpp b/src/absrefine_counterexample/AbstractionRefinement.cpp
index ea24277575613e4d1b6fb179f5b3e83a80368945..9cc8437464edd2178ab1d58f5559fc057aaf1daf 100644 (file)
--- a/src/absrefine_counterexample/AbstractionRefinement.cpp
+++ b/src/absrefine_counterexample/AbstractionRefinement.cpp
@@ -91,7 +91,10 @@ namespace BEEV
                // We assume there are no duplicate constant indexes in the list of readindexes,
                // so "i" and "j" will never be equal.
                if (BVCONST == index_i.GetKind() && index_j.GetKind() == BVCONST)
+               {
+                       assert(index_i != index_j);
                        continue;
+               }
 
                 //prepare for SAT LOOP
                 //first construct the antecedent for the LA axiom

diff --git a/src/simplifier/CountOfSymbols.h b/src/simplifier/CountOfSymbols.h
deleted file mode 100644 (file)
index c7f489d..0000000
--- a/src/simplifier/CountOfSymbols.h
+++ /dev/null
@@ -1,66 +0,0 @@
-#ifndef COUNTOFSYMBOLS_H_
-#define COUNTOFSYMBOLS_H_
-
-#include "../AST/AST.h"
-#include <cassert>
-#include "Symbols.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 {
-
-       typedef hash_map<ASTNode, int, ASTNode::ASTNodeHasher,
-                       ASTNode::ASTNodeEqual> ASTNodeToIntMap;
-
-       ASTNodeToIntMap Vars;
-       const Symbols* top;
-       bool loaded;
-
-       // If no variables are found in "term", then it's cached---we don't need to visit there
-       // again. However, if it's true, we need to revisit (and hence recount), the next time it's
-       // encountered.
-
-       void VarsInTheTerm(const Symbols* term) {
-               assert(!term->empty());
-
-               if (!term->found.IsNull())
-               {
-                       Vars[term->found]++;
-               }
-               else
-               {
-                       const vector<Symbols*>& c = term->children;
-                       for (vector<Symbols*>::const_iterator it = c.begin(), itend = c.end(); it
-                                       != itend; it++)
-                       {
-                               VarsInTheTerm(*it);
-                       }
-               }
-       } //end of VarsInTheTerm()
-
-public:
-
-       CountOfSymbols(const Symbols* top_v) :
-               top(top_v) {
-               loaded = false;
-       }
-
-       bool single(const ASTNode &m) {
-               if (!loaded)
-               {
-                       VarsInTheTerm(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/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index 51325ff9157a60ad2f0c85ba280792c546c85ef1..c98e2983b6db407b9ccef99c287f61cb3f8f007b 100644 (file)
--- a/src/simplifier/bvsolver.cpp
+++ b/src/simplifier/bvsolver.cpp
@@ -11,7 +11,6 @@
 #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
@@ -99,7 +98,6 @@ namespace BEEV
 
     //collect all the vars in the lhs and rhs
     BuildSymbolGraph(eq);
-    CountOfSymbols count(symbol_graph[eq]);
 
     //handle BVPLUS case
     ASTVec c = FlattenKind(BVPLUS, lhs.GetChildren());
@@ -176,14 +174,14 @@ namespace BEEV
                 && !chosen_symbol
                 && !DoNotSolveThis(var)
                 && ((SYMBOL == var.GetKind() 
-                     && count.single(var)
+                     && !VarSeenInTerm(var,rhs)
                     )
                     || (BVEXTRACT == var.GetKind() 
                         && SYMBOL == var[0].GetKind() 
                         && BVCONST == var[1].GetKind() 
                         && zero == var[2]
                         && !DoNotSolveThis(var[0])
-                        && count.single(var[0])
+                        && !VarSeenInTerm(var[0],rhs)
                         ))
                 )
               {
@@ -198,7 +196,7 @@ namespace BEEV
                 && BVCONST == monom[1].GetKind()
                 && zero == monom[2]
                 && !DoNotSolveThis(monom[0])
-                && count.single(monom[0])
+                && !VarSeenInTerm(monom[0],rhs)
             )
               {
               outmonom = monom;
@@ -212,7 +210,7 @@ namespace BEEV
                        && BVCONST == monom[0][1].GetKind()
                        && zero == monom[0][2]
                        && !DoNotSolveThis(monom[0][0])
-                       && count.single(monom[0][0])
+                       && !VarSeenInTerm(monom[0][0],rhs)
                    )
                      {
                      outmonom = monom;