Enable upfront simplifications of terms.

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

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index 09978c69ce917125626ba50580b5e1383b496d00..5ee80adca65981da10825b7f04ebd63e00c47588 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -17,7 +17,15 @@ namespace BEEV
  // If enabled, simplifyTerm will simplify all the arguments to a function before attempting
  // the simplification of that function. Without this option the case will be selected for
  // each kind, and that case needs to simplify the arguments.
- const bool simplify_upfront = false;
+
+ // Longer term, this means that each function doesn't need to worry about calling simplify
+// on it's arguments (I suspect some paths don't call simplify on their arguments). But it
+// does mean that we can't short cut, for example, if the first argument to a BVOR is all trues,
+// then all the other arguments have already been simplified, so won't be short-cutted.
+
+// I tried enabling it on the formulae, but it interferred with the bvsolver (sometime),
+// so that's disabled.
+  const bool simplify_upfront = true;
 
   ASTNode Simplifier::Flatten(const ASTNode& a)
   {
@@ -275,6 +283,34 @@ namespace BEEV
     if (CheckSimplifyMap(a, output, pushNeg, VarConstMap))
       return output;
 
+    kind = a.GetKind();
+
+    if (false && simplify_upfront)
+    {
+               if (!a.isConstant() && kind != SYMBOL) // const and symbols need to be created specially.
+               {
+                       assert(a.Degree() > 0);
+                       ASTVec v;
+                       v.reserve(a.Degree());
+                       for (unsigned i = 0; i < a.Degree(); i++)
+                               if (a[i].GetType() == BITVECTOR_TYPE)
+                                       v.push_back(SimplifyTerm(a[i], VarConstMap));
+                               else if (a[i].GetType() == BOOLEAN_TYPE)
+                                       v.push_back(SimplifyFormula(a[i], VarConstMap));
+                               else
+                                       v.push_back(a[i]);
+
+                       // TODO: Should check if the children arrays are different and only
+                       // create then.
+                       ASTNode output = nf->CreateNode(kind, v);
+
+                       if (a != output) {
+                               UpdateSimplifyMap(a, output, false, VarConstMap);
+                               a = output;
+                       }
+               }
+    }
+
     a = PullUpITE(a);
     kind = a.GetKind(); // pullUpITE can change the Kind of the node.
 
@@ -1655,6 +1691,7 @@ namespace BEEV
                        output = n;
                        break;
                 }
+               assert(n.GetKind() == BVPLUS || n.GetKind() == BVMULT);
                ASTVec c = n.GetChildren();
           SortByArith(c);
           ASTVec constkids, nonconstkids;