From 5ad4a9972a7007902a73b141e3bf58ed896e1297 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sat, 30 Apr 2011 02:07:39 +0000 Subject: [PATCH] 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 --- .../NodeFactory/SimplifyingNodeFactory.cpp | 26 +++++++++++++++---- 1 file changed, 21 insertions(+), 5 deletions(-) diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp index e0a7e8d..ae33358 100644 --- 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; -- 2.47.3