From 226d721aba84a7164d68255bdb338f75b9133943 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 13 Apr 2011 01:43:16 +0000 Subject: [PATCH] Extra simplification rule. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1267 e59a4935-1847-0410-ae03-e826735625c1 --- src/AST/NodeFactory/SimplifyingNodeFactory.cpp | 17 +++++++++++++++-- 1 file changed, 15 insertions(+), 2 deletions(-) diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp index 85ec1d1..a4cbc2d 100644 --- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp +++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp @@ -358,6 +358,21 @@ ASTNode SimplifyingNodeFactory::CreateSimpleEQ(const ASTVec& children) return NodeFactory::CreateNode(BEEV::AND, a, b); } + + if (k1 == BEEV::BVCONST && k2 == BEEV::ITE && in2[1].GetKind() == BEEV::BVCONST && in2[2].GetKind() == BEEV::BVCONST) + { + + ASTNode result = + NodeFactory::CreateNode(BEEV::ITE, + in2[0], + NodeFactory::CreateNode(BEEV::EQ,in1,in2[1]), + NodeFactory::CreateNode(BEEV::EQ,in1,in2[2])); + + return result; + } + + + // Don't create a PLUS with the same operand on both sides. // We don't do big pluses, because 1) this algorithm isn't good enough // 2) it might split nodes (a lot). @@ -392,8 +407,6 @@ ASTNode SimplifyingNodeFactory::CreateSimpleEQ(const ASTVec& children) } } } - - //last resort is to CreateNode return hashing.CreateNode(BEEV::EQ, children); } -- 2.47.3