From b1c8325421c94d6bb539697ffac837b5b80ae350 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Mon, 28 Mar 2011 00:34:44 +0000 Subject: [PATCH] Extra simplification rule for BVXOR. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1241 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/NodeFactory/SimplifyingNodeFactory.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp index 6f24778..d638808 100644 --- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp +++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp @@ -694,6 +694,13 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, if (children[0].isConstant() && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst())) result = children[1]; + + if (children[1].isConstant() && CONSTANTBV::BitVector_is_full(children[1].GetBVConst())) + result = NodeFactory::CreateTerm(BEEV::BVNEG, width, children[0]); + + if (children[0].isConstant() && CONSTANTBV::BitVector_is_full(children[0].GetBVConst())) + result = NodeFactory::CreateTerm(BEEV::BVNEG, width, children[1]); + } break; -- 2.47.3