Remove the full bvsolve option. I'm soon to commit a much better replacement of...

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

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index ec6c7c51e2a5f461c9ed83ad23f92ac72519f1d7..8602a7c46c665cf35836c11b955682b46d24d8b7 100644 (file)
--- a/src/simplifier/bvsolver.cpp
+++ b/src/simplifier/bvsolver.cpp
@@ -643,8 +643,7 @@ namespace BEEV
         != and_end; and_child++)
       {
 
-      ASTNode r = solveForXOR(!changed?*and_child:_simp->SimplifyFormula(completelySubstitute? _simp->applySubstitutionMap(*and_child)
-                 : _simp->applySubstitutionMapUntilArrays(*and_child),false,NULL));
+      ASTNode r = solveForXOR(!changed?*and_child:_simp->SimplifyFormula(_simp->applySubstitutionMapUntilArrays(*and_child),false,NULL));
       if (r!=*and_child)
         changed=true;
       output_children.push_back(r);
@@ -660,7 +659,6 @@ namespace BEEV
   //the formula
   ASTNode BVSolver::TopLevelBVSolve(const ASTNode& _input)
   {
-      completelySubstitute = _bm->UserFlags.isSet("full_bvsolve","0");
       assert (_bm->UserFlags.wordlevel_solve_flag);
          ASTNode input = _input;
 
@@ -671,10 +669,6 @@ namespace BEEV
         return output;
       }
 
-    if (completelySubstitute)
-       input = _simp->applySubstitutionMap(input);
-
-
     Kind k = input.GetKind();
     if (XOR ==k && _bm->UserFlags.solve_for_XORS_flag)
     {
@@ -740,8 +734,7 @@ namespace BEEV
           */
 
        ASTNode aaa = (any_solved && EQ == it->GetKind()) ? _simp->SimplifyFormula
-                       (completelySubstitute ? _simp->applySubstitutionMap(*it):
-                       _simp->applySubstitutionMapUntilArrays(*it),false,NULL) : *it;
+                       (_simp->applySubstitutionMapUntilArrays(*it),false,NULL) : *it;
 
         if (ASTFalse == aaa)
         {
@@ -799,10 +792,7 @@ namespace BEEV
 
     // Imagine in the last conjunct A is replaced by B. But there could
     // be variable A's in the first conjunct. This gets rid of 'em.
-    if (completelySubstitute)
-       output = _simp->applySubstitutionMap(output);
-    else
-       output = _simp->applySubstitutionMapUntilArrays(output);
+       output = _simp->applySubstitutionMapUntilArrays(output);
 
 
     UpdateAlreadySolvedMap(_input, output);

diff --git a/src/simplifier/bvsolver.h b/src/simplifier/bvsolver.h
index 8aba0329135c0dc28019cde3fc7602bf716b58eb..3c0989607182d66106edec005c1ca27a27bb45a5 100644 (file)
--- a/src/simplifier/bvsolver.h
+++ b/src/simplifier/bvsolver.h
@@ -1,5 +1,5 @@
 /********************************************************************
- * AUTHORS: Vijay Ganesh
+ * AUTHORS: Vijay Ganesh, Trevor Hansen
  *
  * BEGIN DATE: November, 2005
  *
@@ -113,11 +113,6 @@ namespace BEEV
     //else returns FALSE
     bool CheckAlreadySolvedMap(const ASTNode& key, ASTNode& output);
 
-    // If array terms contain variables that have been substituted for, then , it breaks.
-    // However, completely substituting is extremely expensive to do. And only rarely necessary.
-    // With this option enabled, it will do it properly. And slowly!!
-    bool completelySubstitute;
-
     VariablesInExpression vars;
 
   public: