Add some extra simplifications to the simplifying node factory.

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

diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
index 7c009c92e8ff99c8af64a8c287e95e38f80f3ff7..47f2e16883935736f739c4d14e9e809c2cf665cd 100644 (file)
--- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
+++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
@@ -76,6 +76,27 @@ ASTNode SimplifyingNodeFactory::CreateNode(Kind kind, const ASTVec & children)
                result = NodeFactory::CreateNode(BEEV::BVSGE, children[1], children[0]);
                break;
 
+
+       case BEEV::BVSGT:
+       case BEEV::BVGT:
+               assert(children.size() ==2);
+               if (children[0] == children[1])
+                       result = ASTFalse;
+               else
+                       result = hashing.CreateNode(kind, children);
+               break;
+
+       case BEEV::BVSGE:
+       case BEEV::BVGE:
+               assert(children.size() ==2);
+               if (children[0] == children[1])
+                       result = ASTTrue;
+               else
+                       result = hashing.CreateNode(kind, children);
+               break;
+
+
+
        case BEEV::NOT:
                result = CreateSimpleNot(children);
                break;
@@ -110,6 +131,17 @@ ASTNode SimplifyingNodeFactory::CreateNode(Kind kind, const ASTVec & children)
            result = CreateSimpleXor(newCh);
            break;
        }
+       case BEEV::IMPLIES:
+       {
+               assert(children.size() ==2);
+               ASTVec newCh;
+               newCh.reserve(2);
+               newCh.push_back(CreateSimpleNot(children[0]));
+               newCh.push_back(children[1]);
+           result = CreateSimpleAndOr(0,newCh);
+           break;
+       }
+
 
        default:
                result = hashing.CreateNode(kind, children);
@@ -512,6 +544,15 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width,
                break;
        }
 
+
+       case BEEV::BVSX:
+       {
+               if (width == children[0].GetValueWidth())
+                       result = children[0];
+               break;
+       }
+
+
        case BEEV::BVNEG:
        {
                switch (children[0].GetKind())
@@ -526,6 +567,17 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width,
        }
        break;
 
+
+       case BEEV::BVMOD:
+               if (children[1].isConstant())
+               {
+                       ASTNode one = bm.CreateOneConst(width);
+                       if (children[1] == one)
+                               result = bm.CreateZeroConst(width);
+               }
+               break;
+
+
        case BEEV::READ:
        if (children[0].GetKind() == BEEV::WRITE)
        {