From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sun, 27 Jun 2010 01:50:22 +0000 (+0000)
Subject: Speedup. Flatten ands at the start of the bvsolver.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=e9523ca472b8b070fdfc1f6b6f0480e8afaa41fb;p=francis%2Fstp.git

Speedup. Flatten ands at the start of the bvsolver.

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

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index 5e3a687..ca53ebc 100644
--- a/src/simplifier/bvsolver.cpp
+++ b/src/simplifier/bvsolver.cpp
@@ -38,8 +38,7 @@
 //4. Outside the solver, Substitute and Re-normalize the input DAG
 namespace BEEV
 {
-	//experimental options. Don't curerntly work.
-	const bool flatten_ands = false;
+	const bool flatten_ands = true;
 	const bool sort_extracts_last = false;
 
   //check the solver map for 'key'. If key is present, then return the
@@ -601,6 +600,12 @@ namespace BEEV
 			{
 				return n;
 			}
+
+	    if (CheckAlreadySolvedMap(input, output))
+	      {
+	        //output is TRUE. The formula is thus dropped
+	        return output;
+	      }
 		}
     }
 
@@ -619,7 +624,6 @@ namespace BEEV
     bool any_solved = false;
     for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++)
       {
-
 		 /*
     	 Calling simplifyFormula makes the required substitutions. For instance, if
     	 first was : v = x,