From a9ad4493293959a6b463a7935bc99be573a35991 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Thu, 31 Mar 2011 13:02:27 +0000 Subject: [PATCH] Tiny improvement. Add the one-bit operations that evaluate to a child or a constant. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1248 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/NodeFactory/SimplifyingNodeFactory.cpp | 17 ++++++++++++++++- 1 file changed, 16 insertions(+), 1 deletion(-) diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp index ebd16ac..cf1229d 100644 --- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp +++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp @@ -616,6 +616,8 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, if (children[0].isConstant() && children[0] == bm.CreateOneConst(width)) result = children[1]; + if (width == 1 && children[0] == children[1]) + result = children[0]; } } break; @@ -626,6 +628,9 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, result = bm.CreateZeroConst(width); else if (children[1].isConstant()) result = BEEV::Simplifier::convertKnownShiftAmount(kind, children, bm, &hashing); + else if (width == 1 && children[0] == children[1]) + result = bm.CreateZeroConst(1); + } break; @@ -649,6 +654,11 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, result = bm.CreateMaxConst(width); else if (children[1].isConstant() && CONSTANTBV::BitVector_is_empty(children[1].GetBVConst())) result = children[0]; + else if (width == 1 && children[0] == children[1]) + result = children[0]; + else if (width == 1 && children[1].isConstant() && children[1] == bm.CreateOneConst(1)) + result = children[0]; + } break; @@ -767,6 +777,9 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, case BEEV::BVUMINUS: if (children[0].GetKind() == BEEV::BVUMINUS) result = children[0][0]; + else if (width == 1) + result = children[0]; + break; case BEEV::BVEXTRACT: @@ -809,8 +822,10 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, { if (children[1].isConstant() && CONSTANTBV::BitVector_is_empty(children[1].GetBVConst())) result = children[0]; - if (children[0].isConstant() && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst())) + else if (children[0].isConstant() && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst())) result = children[1]; + else if (width == 1 && children[0] == children[1]) + result = bm.CreateZeroConst(1); } break; -- 2.47.3