Fix. XORs with >2 children sometimes reached the simplifier. This patch adds simplif...

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

diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index bfa21cdf9b34c4ed852fce0decab2b0ce4dec9e3..5e5f46b69e42f42084b99aa0bc4a54ce3d0a2fe0 100644 (file)
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -1249,30 +1249,37 @@ namespace BEEV
     if (CheckSimplifyMap(a, output, pushNeg, VarConstMap))
       return output;
 
-    if (a.GetChildren().size() > 2)
+    assert(a.GetChildren().size() > 0);
+
+    if (a.GetChildren().size()==1)
       {
-        FatalError("Simplify got an XOR with more than two children.");
+        output = a[0];
       }
-
-    ASTNode a0 = SimplifyFormula(a[0], false, VarConstMap);
-    ASTNode a1 = SimplifyFormula(a[1], false, VarConstMap);
-    output = 
-      pushNeg ? 
-      nf->CreateNode(IFF, a0, a1) :
-      nf->CreateNode(XOR, a0, a1);
-
-    if (XOR == output.GetKind())
+    else  if (a.GetChildren().size()==2)
       {
-        a0 = output[0];
-        a1 = output[1];
+        ASTNode a0 = SimplifyFormula(a[0], false, VarConstMap);
+        ASTNode a1 = SimplifyFormula(a[1], false, VarConstMap);
+        if (pushNeg)
+          a0 = nf->CreateNode(NOT, a0);
+        output = nf->CreateNode(XOR, a0, a1);
+
         if (a0 == a1)
           output = ASTFalse;
-        else if ((a0 == ASTTrue 
-                  && a1 == ASTFalse) 
-                 || (a0 == ASTFalse 
-                     && a1 == ASTTrue))
+        else if ((a0 == ASTTrue && a1 == ASTFalse) || (a0 == ASTFalse && a1 == ASTTrue))
           output = ASTTrue;
       }
+    else
+      {
+       ASTVec newC;
+       for (int i = 0;i < a.GetChildren().size(); i++)
+         {
+             newC.push_back(SimplifyFormula(a[i], false, VarConstMap));
+         }
+       if (pushNeg)
+         newC[0] = nf->CreateNode(NOT,newC[0]);
+
+       output = nf->CreateNode(XOR, newC);
+      }
 
     //memoize
     UpdateSimplifyMap(a, output, pushNeg, VarConstMap);