Speedup. Reduce the amount of checking that the bvsolver performs.

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

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index aa5a08a9690956dae1eef0ea4e722177f85aa647..4e9883a15003c293e37cd698b96d1747d5dc0a5f 100644 (file)
--- a/src/simplifier/bvsolver.cpp
+++ b/src/simplifier/bvsolver.cpp
@@ -309,6 +309,9 @@ namespace BEEV
         return output;
       }
 
+    // ChooseMonom makes sure that the the LHS is not contained on the RHS, so we
+    // set this "single" to true in the branch that runs checkMonomial.
+    bool single = false;
 
     if (BVPLUS == lhs.GetKind())
       {
@@ -334,6 +337,7 @@ namespace BEEV
         rhs =
           _simp->SimplifyTerm(_bm->CreateTerm(BVPLUS, len, rhs, leftover_lhs));
         lhs = chosen_monom;
+        single = true;
       } //end of if(BVPLUS ...)
 
     if (BVUMINUS == lhs.GetKind())
@@ -349,13 +353,14 @@ namespace BEEV
       {
       case SYMBOL:
         {
+            DoNotSolve_TheseVars.insert(lhs);
+
           //input is of the form x = rhs first make sure that the lhs
           //symbol does not occur on the rhs or that it has not been
           //solved for
-          if (VarSeenInTerm(lhs, rhs))
+          if (!single && VarSeenInTerm(lhs, rhs))
             {
               //found the lhs in the rhs. Abort!
-              DoNotSolve_TheseVars.insert(lhs);
               return eq;
             }
 
@@ -365,7 +370,6 @@ namespace BEEV
           //            return eq;
           //       }
 
-          DoNotSolve_TheseVars.insert(lhs);
           if (!_simp->UpdateSolverMap(lhs, rhs))
             {
               return eq;

diff --git a/src/simplifier/bvsolver.h b/src/simplifier/bvsolver.h
index 310b8d62da071f69379bc5bf2c98da9ce8e292be..3dad93a9620aaad6932afb331ae6f7affa37b4f6 100644 (file)
--- a/src/simplifier/bvsolver.h
+++ b/src/simplifier/bvsolver.h
@@ -61,7 +61,7 @@ namespace BEEV
     //identifying variables in the those terms. Prevents double
     //counting.
     ASTNodeMap TermsAlreadySeenMap;
-    ASTNodeMap TermsAlreadySeenMap_ForArrays;
+    //ASTNodeMap TermsAlreadySeenMap_ForArrays;
 
     //solved variables list: If a variable has been solved for then do
     //not solve for it again
@@ -88,8 +88,8 @@ namespace BEEV
 
     //Checks for arrayreads in a term. if yes then returns true, else
     //return false
-    bool CheckForArrayReads(const ASTNode& term);
-    bool CheckForArrayReads_TopLevel(const ASTNode& term);
+    //bool CheckForArrayReads(const ASTNode& term);
+    //bool CheckForArrayReads_TopLevel(const ASTNode& term);
 
     //Creates new variables used in solving
     ASTNode NewVar(unsigned int n);
@@ -146,7 +146,7 @@ namespace BEEV
         TermsAlreadySeenMap.clear();
         DoNotSolve_TheseVars.clear();
         FormulasAlreadySolvedMap.clear();
-        TermsAlreadySeenMap_ForArrays.clear();
+        //TermsAlreadySeenMap_ForArrays.clear();
       }
 
     //Top Level Solver: Goes over the input DAG, identifies the
@@ -157,7 +157,7 @@ namespace BEEV
     {
       DoNotSolve_TheseVars.clear();
       FormulasAlreadySolvedMap.clear();
-      TermsAlreadySeenMap_ForArrays.clear();
+      //TermsAlreadySeenMap_ForArrays.clear();
     } //End of ClearAllTables()
 
   }; //end of class bvsolver