Improvement. Remove the do-not-solve-for set. I suspect this is no longer needed...

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

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index fcfe5ed1a91386b5c543d07464233641f0ce0cf6..37c037d86cb8fe370bdab15bd6d6741466de66aa 100644 (file)
--- a/src/simplifier/bvsolver.cpp
+++ b/src/simplifier/bvsolver.cpp
@@ -91,11 +91,6 @@ namespace BEEV
        assert(number_shifts >0); // shouldn't be odd.
   }
 
-  bool BVSolver::DoNotSolveThis(const ASTNode& var)
-  {
-    return (DoNotSolve_TheseVars.find(var) != DoNotSolve_TheseVars.end());
-  }
-
   //chooses a variable in the lhs and returns the chosen variable
   ASTNode BVSolver::ChooseMonom(const ASTNode& eq, ASTNode& modifiedlhs, ASTNodeSet& checked)
   {
@@ -129,7 +124,6 @@ namespace BEEV
                (
                SYMBOL == monom.GetKind()
             && !chosen_symbol
-                       && !DoNotSolveThis(monom)
                        && checked.find(monom)==checked.end()
             && !vars.VarSeenInTerm(monom,rhs)
             )
@@ -138,7 +132,6 @@ namespace BEEV
              BVUMINUS == monom.GetKind()
              && SYMBOL == monom[0].GetKind()
              && !chosen_symbol
-             && !DoNotSolveThis(monom[0])
              && checked.find(monom[0])==checked.end()
              && !vars.VarSeenInTerm(monom[0],rhs)
             )
@@ -191,7 +184,6 @@ namespace BEEV
                 && BVCONST == monom[0].GetKind() 
                 && _simp->BVConstIsOdd(monom[0]) 
                 && !chosen_symbol
-                && !DoNotSolveThis(var)
                 && checked.find(var)==checked.end()
                 && ((SYMBOL == var.GetKind() 
                      && !vars.VarSeenInTerm(var,rhs)
@@ -200,7 +192,6 @@ namespace BEEV
                         && SYMBOL == var[0].GetKind() 
                         && BVCONST == var[1].GetKind() 
                         && zero == var[2]
-                        && !DoNotSolveThis(var[0])
                         && !vars.VarSeenInTerm(var[0],rhs)
                         ))
                 )
@@ -216,7 +207,6 @@ namespace BEEV
                 && SYMBOL == monom[0].GetKind()
                 && BVCONST == monom[1].GetKind()
                 && zero == monom[2]
-                && !DoNotSolveThis(monom[0])
                 && checked.find(monom[0])==checked.end()
                 && !vars.VarSeenInTerm(monom[0],rhs)
             )
@@ -232,7 +222,6 @@ namespace BEEV
                        && SYMBOL == monom[0][0].GetKind()
                        && BVCONST == monom[0][1].GetKind()
                        && zero == monom[0][2]
-                       && !DoNotSolveThis(monom[0][0])
                        && checked.find(monom[0][0])==checked.end()
                        && !vars.VarSeenInTerm(monom[0][0],rhs)
                    )
@@ -279,8 +268,6 @@ 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
@@ -307,18 +294,16 @@ namespace BEEV
               && BVCONST == lhs[1].GetKind()
               && zero == lhs[2]
               && !vars.VarSeenInTerm(lhs[0], rhs)
-              && !DoNotSolveThis(lhs[0])))
+              ))
           {
             return eq;
           }
 
         if (vars.VarSeenInTerm(lhs[0], rhs))
           {
-            DoNotSolve_TheseVars.insert(lhs[0]);
             return eq;
           }
 
-        DoNotSolve_TheseVars.insert(lhs[0]);
         if (!_simp->UpdateSolverMap(lhs, rhs))
           {
             return eq;
@@ -380,7 +365,6 @@ namespace BEEV
         if (vars.VarSeenInTerm(chosenvar, chosenvar_value))
           {
             //abort solving
-            DoNotSolve_TheseVars.insert(lhs);
             return eq;
           }
 
@@ -390,7 +374,6 @@ namespace BEEV
                 return eq;
 
         //found a variable to solve
-        DoNotSolve_TheseVars.insert(chosenvar);
         chosenvar = lhs[1];
         if (!_simp->UpdateSolverMap(chosenvar, chosenvar_value))
           {

diff --git a/src/simplifier/bvsolver.h b/src/simplifier/bvsolver.h
index 24a6b215cfd1527d919e20ce1cf7471553e9d779..c547a400295bda48485202b8a8c06c91ad6753d7 100644 (file)
--- a/src/simplifier/bvsolver.h
+++ b/src/simplifier/bvsolver.h
@@ -54,14 +54,6 @@ namespace BEEV
     //
     ASTNode ASTTrue, ASTFalse, ASTUndefined;
 
-    //solved variables list: If a variable has been solved for then do
-    //not solve for it again
-    ASTNodeSet DoNotSolve_TheseVars;
-
-    //checks if var has been solved for or not. if yes, then return
-    //true else return false
-    bool DoNotSolveThis(const ASTNode& var);
-
     //choose a suitable var from the term
     ASTNode ChooseMonom(const ASTNode& eq, ASTNode& modifiedterm, ASTNodeSet& checked);
     //accepts an equation and solves for a variable or a monom in it
@@ -141,7 +133,6 @@ namespace BEEV
 
     void ClearAllTables(void)
     {
-         DoNotSolve_TheseVars.clear();
          FormulasAlreadySolvedMap.clear();
     } //End of ClearAllTables()