Convert subtraction to addition in the simplifying node factory.

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

diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
index e0a7e8d2006f73803ad6d23d91a7679943b42d7e..ae33358540404fd329b9a3b0162aa53df0410c61 100644 (file)
--- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
+++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
@@ -838,11 +838,16 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width,
         break;
 
        case BEEV::BVSUB:
-            if (children.size() == 2 && children[0] == children[1])
-              result = bm.CreateZeroConst(width);
-            if (children.size() == 2 && children[1] == bm.CreateZeroConst(width))
-              result = children[0];
-            break;
+         if (children.size() == 2)
+           {
+             if (children.size() == 2 && children[0] == children[1])
+                result = bm.CreateZeroConst(width);
+              else if (children.size() == 2 && children[1] == bm.CreateZeroConst(width))
+                result = children[0];
+              else
+                  result = NodeFactory::CreateTerm(BEEV::BVPLUS,width,children[0], NodeFactory::CreateTerm(BEEV::BVUMINUS,width, children[1]));
+           }
+         break;
 
        case BEEV::BVOR:
                  {
@@ -1010,6 +1015,17 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width,
               result = bm.CreateZeroConst(width);
             else if (children[0].GetKind() == BEEV::BVUMINUS  && children[1] == children[0][0])
               result = bm.CreateZeroConst(width);
+            /* This is ridiculously complicated, it should be cleaner.
+            else if (children[1].GetKind() == BEEV::BVPLUS && children[1][1].GetKind() == BEEV::BVUMINUS && children[0] == children[1][1][0])
+              result = children[1][0];
+            else if (children[1].GetKind() == BEEV::BVPLUS && children[1][0].GetKind() == BEEV::BVUMINUS && children[0] == children[1][0][0])
+              result = children[1][1];
+            else if (children[0].GetKind() == BEEV::BVPLUS && children[0][0].GetKind() == BEEV::BVUMINUS && children[1] == children[0][0][0])
+              result = children[0][1];
+            else if (children[0].GetKind() == BEEV::BVPLUS && children[0][1].GetKind() == BEEV::BVUMINUS && children[1] == children[0][1][0])
+                result = children[0][0];
+                */
+
           }
         break;