From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 26 Feb 2011 05:06:58 +0000 (+0000)
Subject: Fix.  XORs with >2 children sometimes reached the simplifier. This patch adds simplif... 
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=ae62317e51ae443a7427301e0027bda787daad79;p=francis%2Fstp.git

Fix.  XORs with >2 children sometimes reached the simplifier. This patch adds simplification for those, rather than generating an assertion error.

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 bfa21cd..5e5f46b 100644
--- 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);