From 35a987a8cc60e003a1a351e91db4ed8b86838001 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Sun, 3 Apr 2011 14:14:56 +0000 Subject: [PATCH] Improvement. Some extra simplifications for the simplifyingNF. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1250 e59a4935-1847-0410-ae03-e826735625c1 --- .../NodeFactory/SimplifyingNodeFactory.cpp | 19 ++++++++++++++----- 1 file changed, 14 insertions(+), 5 deletions(-) diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp index 03cda2d..1cd2d52 100644 --- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp +++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp @@ -320,15 +320,25 @@ ASTNode SimplifyingNodeFactory::CreateSimpleEQ(const ASTVec& children) const ASTNode& in2 = children[1]; const Kind k1 = in1.GetKind(); const Kind k2 = in2.GetKind(); + const int width = in1.GetValueWidth(); if (in1 == in2) //terms are syntactically the same return in1.GetSTPMgr()->ASTTrue; - //here the terms are definitely not syntactically equal but may be - //semantically equal. - if (BEEV::BVCONST == k1 && BEEV::BVCONST == k2) - return in1.GetSTPMgr()->ASTFalse; + //here the terms are definitely not syntactically equal but may be + //semantically equal. + if (BEEV::BVCONST == k1 && BEEV::BVCONST == k2) + return in1.GetSTPMgr()->ASTFalse; + + if ((k1 == BEEV::BVNEG && k2 == BEEV::BVNEG) || (k1 == BEEV::BVUMINUS && k2 == BEEV::BVUMINUS)) + return NodeFactory::CreateNode(BEEV::EQ, in1[0], in2[0]); + + if ((k1 == BEEV::BVUMINUS && k2 == BEEV::BVCONST) || (k1 == BEEV::BVNEG && k2 == BEEV::BVCONST)) + return NodeFactory::CreateNode(BEEV::EQ, in1[0], NodeFactory::CreateTerm(k1,width, in2 )); + + if (k2 == BEEV::BVUMINUS && k1 == BEEV::BVCONST || (k2 == BEEV::BVNEG && k1 == BEEV::BVCONST)) + return NodeFactory::CreateNode(BEEV::EQ, in2[0], NodeFactory::CreateTerm(k2,width, in1 )); // This increases the number of nodes. So disable for now. if (false && BEEV::BVCONCAT == k1 && BEEV::BVCONCAT == k2 && in1[0].GetValueWidth() == in2[0].GetValueWidth()) @@ -363,7 +373,6 @@ ASTNode SimplifyingNodeFactory::CreateSimpleEQ(const ASTVec& children) if (match1 != -1) { assert(match2 !=-1); - const int width = in1.GetValueWidth(); assert(match1 == 0 || match1 == 1); assert(match2 == 0 || match2 == 1); // If it was 1 element before, it's zero now. -- 2.47.3