From 6ed8b46207e93dbb72a0b260402e67a45c86f31c Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Thu, 14 Apr 2011 06:34:08 +0000 Subject: [PATCH] Add some missing simplification rules for AND/OR/ propositional ITE. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1277 e59a4935-1847-0410-ae03-e826735625c1 --- .../NodeFactory/SimplifyingNodeFactory.cpp | 30 +++++++++++++++++-- 1 file changed, 28 insertions(+), 2 deletions(-) diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp index 944518f..a40c98d 100644 --- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp +++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp @@ -261,6 +261,26 @@ ASTNode SimplifyingNodeFactory::CreateSimpleAndOr(bool IsAnd, { const Kind k = IsAnd ? BEEV::AND : BEEV::OR; + if (k == BEEV::OR && children.size() ==2) + { + const ASTNode& c0 = children[0]; + const ASTNode& c1 = children[1]; + if (c0.GetKind() == BEEV::NOT && c0[0] == c1) + return ASTTrue; + if (c1.GetKind() == BEEV::NOT && c1[0] == c0) + return ASTTrue; + } + if (k == BEEV::AND && children.size() ==2) + { + const ASTNode& c0 = children[0]; + const ASTNode& c1 = children[1]; + if (c0.GetKind() == BEEV::NOT && c0[0] == c1) + return ASTFalse; + if (c1.GetKind() == BEEV::NOT && c1[0] == c0) + return ASTFalse; + } + + const ASTNode& annihilator = (IsAnd ? ASTFalse : ASTTrue); const ASTNode& identity = (IsAnd ? ASTTrue : ASTFalse); @@ -547,10 +567,8 @@ ASTNode SimplifyingNodeFactory::CreateSimpleXor(const ASTVec &children) return retval; } -// FIXME: How do I know whether ITE is a formula or not? ASTNode SimplifyingNodeFactory::CreateSimpleFormITE(const ASTVec& children) { - const ASTNode& child0 = children[0]; const ASTNode& child1 = children[1]; const ASTNode& child2 = children[2]; @@ -595,6 +613,14 @@ ASTNode SimplifyingNodeFactory::CreateSimpleFormITE(const ASTVec& children) { retval = CreateSimpleAndOr(1, child0, child1); } + else if (child0 == child1) + { + retval = CreateSimpleAndOr(0, child0, child2); + } + else if (child0 == child2) + { + retval = CreateSimpleAndOr(1, child0, child1); + } else { retval = hashing.CreateNode(BEEV::ITE, children); -- 2.47.3