From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 8 Sep 2010 02:46:59 +0000 (+0000)
Subject: Adds a Userflag to control whether the xor solver is enabled.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=7304c2c33f38ec6a5487a5d83de2793456d59ac1;p=francis%2Fstp.git

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 1efeb89..99c235e 100644
--- 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 173dc8d..bcd4783 100644
--- 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.