Extra BVXOR simplification rules.

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

diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
index a4cbc2d9ddf2a8e1fbd68b0629eb68a50d39e931..944518fa46d436420b041d8425af188a108cea0b 100644 (file)
--- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
+++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
@@ -407,6 +407,28 @@ ASTNode SimplifyingNodeFactory::CreateSimpleEQ(const ASTVec& children)
                    }
              }
          }
+
+       if (k1 == BEEV::BVCONST && k2 == BEEV::BVXOR && in2.Degree() == 2 &&  in2[0].GetKind() == BEEV::BVCONST )
+         {
+              return NodeFactory::CreateNode(BEEV::EQ,NodeFactory::CreateTerm(BEEV::BVXOR,width,in1,in2[0] ), in2[1]);
+         }
+
+       if (k2 == BEEV::BVCONST && k1 == BEEV::BVXOR && in1.Degree() == 2 && in1[0].GetKind() == BEEV::BVCONST )
+        {
+             return NodeFactory::CreateNode(BEEV::EQ,NodeFactory::CreateTerm(BEEV::BVXOR,width,in2,in1[0] ), in1[1]);
+        }
+
+       if (k2 == BEEV::BVXOR && in2.Degree() == 2 && in1 == in2[0])
+        {
+           return NodeFactory::CreateNode(BEEV::EQ, bm.CreateZeroConst(width), in2[1]);
+        }
+
+        if (k1 == BEEV::BVXOR && in1.Degree() == 2 && in2 == in1[0])
+        {
+            return NodeFactory::CreateNode(BEEV::EQ, bm.CreateZeroConst(width), in1[1]);
+        }
+
+
        //last resort is to CreateNode
        return hashing.CreateNode(BEEV::EQ, children);
 }