From 0a5f89863a92306c1a3eb75e6e12dd47498509ca Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 10 Jul 2010 09:43:33 +0000
Subject: [PATCH] Extra code (that's not currently enabled), so reduce the
 unncessary clearing of the simplification map during bit-vector solving. 
 This patch causes some instances to fail.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@945 e59a4935-1847-0410-ae03-e826735625c1
---
 src/simplifier/bvsolver.cpp | 72 ++++++++++++++++++++++++++++++++++---
 1 file changed, 67 insertions(+), 5 deletions(-)

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index abb1857..0b74b81 100644
--- a/src/simplifier/bvsolver.cpp
+++ b/src/simplifier/bvsolver.cpp
@@ -742,11 +742,49 @@ namespace BEEV
     	 don't have time. Trev.
 		  */
 
-    	ASTNode aaa =
-          (any_solved
-           && EQ == it->GetKind()) ?
-          _simp->SimplifyFormula_TopLevel(*it, false) :
-          *it;
+#if 1
+      ASTNode aaa =
+              (any_solved
+               && EQ == it->GetKind()) ?
+              _simp->SimplifyFormula_TopLevel(*it, false) :
+              *it;
+
+#else
+
+
+    	ASTNode aaa = *it;
+
+    	if (any_solved && EQ == aaa.GetKind())
+          {
+            bool done = false;
+            {
+                ASTNodeSet lhs;
+                SetofVarsSeenInTerm(aaa[0], lhs);
+
+                for (ASTNodeSet::const_iterator it = lhs.begin(); it != lhs.end(); it++)
+                  if (_simp->CheckSubstitutionMap(*it))
+                    {
+                      aaa = _simp->applySubstitutionMap(aaa);
+                      done = true;
+                      break;
+                    }
+              }
+            if (!done)
+              {
+                ASTNodeSet rhs;
+                SetofVarsSeenInTerm(aaa[1], rhs);
+
+                for (ASTNodeSet::const_iterator it = rhs.begin(); it != rhs.end(); it++)
+                  if (_simp->CheckSubstitutionMap(*it))
+                    {
+                      aaa = _simp->applySubstitutionMap(aaa);
+                      done = true;
+                      break;
+                    }
+              }
+          }
+#endif
+
         //_bm->ASTNodeStats("Printing after calling simplifyformula
         //inside the solver:", aaa);
         aaa = BVSolve_Odd(aaa);
@@ -1131,6 +1169,30 @@ namespace BEEV
 	    return;
 	  }//End of VarSeenInTerm
 
+	  void BVSolver::SetofVarsSeenInTerm(const ASTNode& term, ASTNodeSet& symbols)
+	  {
+            assert(symbols.size() ==0);
+
+            BuildSymbolGraph(term);
+
+            SymbolPtrSet visited;
+
+            vector<Symbols*> av;
+            VarSeenInTerm(symbol_graph[term],visited,symbols,av);
+
+            for (int i =0 ; i < av.size();i++)
+            {
+                    const ASTNodeSet& sym = TermsAlreadySeenMap.find(av[i])->second;
+                    symbols.insert(sym.begin(), sym.end());
+            }
+
+
+            if (visited.size() > 50) // No use caching it, unless we've done some work.
+            {
+                    TermsAlreadySeenMap.insert(make_pair(symbol_graph[term],symbols));
+            }
+          }
+
 	  bool BVSolver::VarSeenInTerm(const ASTNode& var, const ASTNode& term)
 	  {
 		  // This only returns true if we are searching for variables that aren't arrays.
-- 
2.47.3