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 5e3a68700c58d5746c128322aa04f82428c508a7..ca53ebcaa78ccf5324bd8f9c41ebac6ba1c04c3b 100644 (file)
--- 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,