From e795fbe7527e8808c0f65f2af93a1583ab61b1ad Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 16 Mar 2011 13:58:56 +0000
Subject: [PATCH] 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
---
 .../NodeFactory/SimplifyingNodeFactory.cpp    | 52 +++++++++++++++++++
 1 file changed, 52 insertions(+)

diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp
index 7c009c9..47f2e16 100644
--- 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)
 	{
-- 
2.47.3