From 76b9ee9ffcb3b24d9fd5f97b740c51563527eb74 Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 19 Jan 2011 00:32:46 +0000
Subject: [PATCH] Add the --config_full_bvsolve=1 option. With this option
 enabled, I know of no other segfaults/crashes in STP. However, for now,
 enabling it causes STP to run very slowly when processing problems with
 arrays.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1071 e59a4935-1847-0410-ae03-e826735625c1
---
 src/STPManager/UserDefinedFlags.h |  6 ++++++
 src/simplifier/bvsolver.cpp       | 26 +++++++++++++++++---------
 src/simplifier/bvsolver.h         |  4 ++++
 3 files changed, 27 insertions(+), 9 deletions(-)

diff --git a/src/STPManager/UserDefinedFlags.h b/src/STPManager/UserDefinedFlags.h
index db38a4a..7350eec 100644
--- a/src/STPManager/UserDefinedFlags.h
+++ b/src/STPManager/UserDefinedFlags.h
@@ -153,6 +153,12 @@ namespace BEEV
     	return get(n,"");
     }
 
+    // "1" is set.
+    bool isSet(string n, string def)
+    {
+    	return (get(n,def) == string("1"));
+    }
+
     string get(string n, string def)
     {
     	if (config_options.empty())
diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index c98e298..a5509bd 100644
--- a/src/simplifier/bvsolver.cpp
+++ b/src/simplifier/bvsolver.cpp
@@ -643,7 +643,8 @@ namespace BEEV
         != and_end; and_child++)
       {
 
-      ASTNode r = solveForXOR(!changed?*and_child:_simp->SimplifyFormula(_simp->applySubstitutionMapUntilArrays(*and_child),false,NULL));
+      ASTNode r = solveForXOR(!changed?*and_child:_simp->SimplifyFormula(completelySubstitute? _simp->applySubstitutionMap(*and_child)
+    		  : _simp->applySubstitutionMapUntilArrays(*and_child),false,NULL));
       if (r!=*and_child)
         changed=true;
       output_children.push_back(r);
@@ -659,14 +660,10 @@ namespace BEEV
   //the formula
   ASTNode BVSolver::TopLevelBVSolve(const ASTNode& _input)
   {
-    //    if (!wordlevel_solve_flag)
-    //       {
-    //         return input;
-    //       }
+      completelySubstitute = _bm->UserFlags.isSet("full_bvsolve","0");
+      assert (_bm->UserFlags.wordlevel_solve_flag);
 	  ASTNode input = _input;
 
-
-
     ASTNode output = input;
     if (CheckAlreadySolvedMap(input, output))
       {
@@ -674,6 +671,10 @@ namespace BEEV
         return output;
       }
 
+    if (completelySubstitute)
+    	input = _simp->applySubstitutionMap(input);
+
+
     Kind k = input.GetKind();
     if (XOR ==k && _bm->UserFlags.solve_for_XORS_flag)
     {
@@ -737,7 +738,10 @@ namespace BEEV
     	 b = write(A,b,b),
     	 which shouldn't be simplified.
   	   */
-        ASTNode aaa = (any_solved && EQ == it->GetKind()) ? _simp->SimplifyFormula(_simp->applySubstitutionMapUntilArrays(*it),false,NULL) : *it;
+
+    	ASTNode aaa = (any_solved && EQ == it->GetKind()) ? _simp->SimplifyFormula
+    			(completelySubstitute ? _simp->applySubstitutionMap(*it):
+    			_simp->applySubstitutionMapUntilArrays(*it),false,NULL) : *it;
 
         if (ASTFalse == aaa)
         {
@@ -795,7 +799,11 @@ 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.
-    output = _simp->applySubstitutionMapUntilArrays(output);
+    if (completelySubstitute)
+    	output = _simp->applySubstitutionMap(output);
+    else
+    	output = _simp->applySubstitutionMapUntilArrays(output);
+
 
     UpdateAlreadySolvedMap(_input, output);
     _bm->GetRunTimes()->stop(RunTimes::BVSolver);
diff --git a/src/simplifier/bvsolver.h b/src/simplifier/bvsolver.h
index 7e65615..981126f 100644
--- a/src/simplifier/bvsolver.h
+++ b/src/simplifier/bvsolver.h
@@ -144,6 +144,10 @@ 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;
 
   public:
     //constructor
-- 
2.47.3