Adds a Userflag to control whether the xor solver is enabled.

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

diff --git a/src/STPManager/UserDefinedFlags.h b/src/STPManager/UserDefinedFlags.h
index 1efeb89c17a705c7083307c6fb470d64a38d62a5..99c235e8c37d47fffc26ff43a10d62c108d5c8c5 100644 (file)
--- a/src/STPManager/UserDefinedFlags.h
+++ b/src/STPManager/UserDefinedFlags.h
@@ -121,6 +121,8 @@ namespace BEEV
 
     bool simplify_during_BB_flag;
 
+    bool solve_for_XORS_flag;
+
     // Available back-end SAT solvers.
     enum SATSolvers
       {
@@ -240,6 +242,8 @@ namespace BEEV
       // If the bit-blaster discovers new constants, should the term simplifier be re-run.
       simplify_during_BB_flag=false;
 
+      solve_for_XORS_flag = true;
+
     } //End of constructor for UserDefinedFlags
 
   }; //End of struct UserDefinedFlags

diff --git a/src/simplifier/bvsolver.cpp b/src/simplifier/bvsolver.cpp
index 173dc8d63c3f3bb8b2b0c81defb9929a16bdfe73..bcd4783decbc3ab97f2fc06c9ddde03819bc1825 100644 (file)
--- a/src/simplifier/bvsolver.cpp
+++ b/src/simplifier/bvsolver.cpp
@@ -603,7 +603,9 @@ namespace BEEV
   // to do. Flatten the XOR.
   ASTNode BVSolver::solveForXOR(const ASTNode& xorNode)
   {
-     if (xorNode.GetKind() != XOR)
+    assert(_bm->UserFlags.solve_for_XORS_flag);
+
+    if (xorNode.GetKind() != XOR)
       {
        return xorNode;
       }
@@ -688,6 +690,8 @@ namespace BEEV
    ASTNode
   BVSolver::solveForAndOfXOR(const ASTNode& n)
   {
+    assert(_bm->UserFlags.solve_for_XORS_flag);
+
     if (n.GetKind() != AND)
       return n;
 
@@ -733,7 +737,7 @@ namespace BEEV
       }
 
     Kind k = input.GetKind();
-    if (XOR ==k)
+    if (XOR ==k && _bm->UserFlags.solve_for_XORS_flag)
     {
        ASTNode output = solveForXOR(_input);
        UpdateAlreadySolvedMap(_input, output);
@@ -748,29 +752,19 @@ namespace BEEV
 
     if (flatten_ands && AND == k)
     {
-               ASTNode n = input;
-               while (true) {
-                       ASTNode nold = n;
-                       n = _simp->FlattenOneLevel(n);
-                       if ((n == nold))
-                               break;
-               }
-
-               input = n;
-
-               // When flattening simplifications will be applied to the node, potentially changing it's type:
-               // (AND x (ANY (not x) y)) gives us FALSE.
-               if (!(EQ == n.GetKind() || AND == n.GetKind())) {
-                       {
-                               return n;
-                       }
+        ASTVec c = FlattenKind(AND,input.GetChildren());
+        input = _bm->CreateNode(AND,c);
 
-           if (CheckAlreadySolvedMap(input, output))
-             {
-               //output is TRUE. The formula is thus dropped
-               return output;
-             }
-               }
+        // When flattening simplifications will be applied to the node, potentially changing it's type:
+        // (AND x (ANY (not x) y)) gives us FALSE.
+       if (!(EQ == input.GetKind() || AND == input.GetKind()))
+           return input;
+
+          if (CheckAlreadySolvedMap(input, output))
+            {
+              //output is TRUE. The formula is thus dropped
+              return output;
+            }
     }
 
     _bm->GetRunTimes()->start(RunTimes::BVSolver);
@@ -895,7 +889,8 @@ namespace BEEV
     if (evens != ASTTrue)
       output = _bm->CreateNode(AND, output, evens);
 
-    output = solveForAndOfXOR(output);
+    if (_bm->UserFlags.solve_for_XORS_flag)
+      output = solveForAndOfXOR(output);
 
     // 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.