From b3809a21ff2f0d754fce0f81ec55e8ae4926b9cc Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 30 Jan 2011 02:26:28 +0000
Subject: [PATCH]  Remove the full bvsolve option. I'm soon to commit a much
 better replacement of this.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1097 e59a4935-1847-0410-ae03-e826735625c1
---
 src/simplifier/bvsolver.cpp | 16 +++-------------
 src/simplifier/bvsolver.h   |  7 +------
 2 files changed, 4 insertions(+), 19 deletions(-)

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index ec6c7c5..8602a7c 100644
--- 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 8aba032..3c09896 100644
--- 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:
-- 
2.47.3