From c9cb824f9a10b492db064fb3ff2adc89cfff5d1f Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Mon, 30 Apr 2012 14:32:57 +0000 Subject: [PATCH] Improvement. Nicer handling of bit-vector not in bvxors. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1658 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/NodeFactory/SimplifyingNodeFactory.cpp | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp index 647e64c..f688209 100644 --- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp +++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp @@ -1089,13 +1089,14 @@ SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, const ASTVec & if (children[0].isConstant() && CONSTANTBV::BitVector_is_full(children[0].GetBVConst())) result = NodeFactory::CreateTerm(BVNEG, width, children[1]); - if (children[1].GetKind() == BVNEG && children[1][0] == children[0]) - result = bm.CreateMaxConst(width); - - if (children[0].GetKind() == BVNEG && children[0][0] == children[1]) - result = bm.CreateMaxConst(width); - if ( width >= 3 && children.size() ==2 && children[0].GetKind() == BVNEG && children[1].GetKind() == BVNEG ) - result = NodeFactory::CreateTerm(BVXOR,width,children[1][0],children[0][0]);//133 -> 133 + if (children[1].GetKind() == BVNEG) + { + result = NodeFactory::CreateTerm(BVNEG, width, NodeFactory::CreateTerm(BVXOR, width, children[0], children[1][0])); + } + else if (children[0].GetKind() == BVNEG) + { + result = NodeFactory::CreateTerm(BVNEG, width, NodeFactory::CreateTerm(BVXOR, width, children[1], children[0][0])); + } } break; -- 2.47.3