From 265f526c4bf192dde2a7c1ebe42a62dc75a486ba Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Mon, 5 Apr 2010 12:32:50 +0000 Subject: [PATCH] Disable expensive "and"/"or" simplifications in the simplifying node factory. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@665 e59a4935-1847-0410-ae03-e826735625c1 --- .../NodeFactory/SimplifyingNodeFactory.cpp | 68 +++++++++---------- 1 file changed, 33 insertions(+), 35 deletions(-) diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp index a967e6e..402295b 100644 --- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp +++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp @@ -1,4 +1,20 @@ -// nb. Some of the simplifications are duplicated with minor differences in the STPManager class. +/* A node factory that: + * * Sorts children to increases sharing, + * * Performs constant evaluation, + * * performs simplify boolean simplifications, + * * converts less thans to greater thans. + * + * NOTE: CreateNode doesn't necessary return a node with the same Kind as what it was called + * with. For example: (AND TRUE FALSE) will return FALSE. Which isn't an AND node. + * + * The intention is to never create nodes that will later be simplified by single level + * re-write rules. So we will never create the node (NOT(NOT x)). This is and example of + * a multi-level rule that never increases the global number of nodes. + * + * These rules never increase the total number of nodes. They are complimented by + * multi-level re-write rules that consider the global reference count when simplifying. + * + */ #include "../../AST/AST.h" #include @@ -10,6 +26,9 @@ static bool debug_simplifyingNodeFactory = false; ASTNode SimplifyingNodeFactory::CreateNode(Kind kind, const ASTVec & children) { + + assert(kind != BEEV::SYMBOL); // These are created specially. + // If all the parameters are constant, return the constant value. // The bitblaster calls CreateNode with a boolean vector. We don't try to simplify those. if (kind != BEEV::UNDEFINED) @@ -27,6 +46,7 @@ ASTNode SimplifyingNodeFactory::CreateNode(Kind kind, const ASTVec & children) { const ASTNode& hash = hashing.CreateNode(kind, children); const ASTNode& c = simplifier->BVConstEvaluator(hash); + assert(c.isConstant()); return c; } } @@ -146,24 +166,15 @@ ASTNode SimplifyingNodeFactory::CreateSimpleAndOr(bool IsAnd, return CreateSimpleAndOr(IsAnd, children); } -// FIXME: Could also handle (AND ... (NOT (OR ...) ...) ASTNode SimplifyingNodeFactory::CreateSimpleAndOr(bool IsAnd, const ASTVec &children) { const Kind k = IsAnd ? BEEV::AND : BEEV::OR; - // Copy so that it can be sorted. Sort so that identical nodes - // occur in sequential runs, followed by their negations. - - ASTVec children_copy = children; - SortByExprNum(children_copy); - - assert(children.size() == children_copy.size()); - if (debug_simplifyingNodeFactory) { cout << "========" << endl << "CreateSimpAndOr " << k << " "; - lpvec(children_copy); + lpvec(children); cout << endl; } @@ -171,10 +182,9 @@ ASTNode SimplifyingNodeFactory::CreateSimpleAndOr(bool IsAnd, const ASTNode& identity = (IsAnd ? ASTTrue : ASTFalse); ASTNode retval; - ASTVec new_children; - const ASTVec::const_iterator it_end = children_copy.end(); - for (ASTVec::const_iterator it = children_copy.begin(); it != it_end; it++) + const ASTVec::const_iterator it_end = children.end(); + for (ASTVec::const_iterator it = children.begin(); it != it_end; it++) { ASTVec::const_iterator next_it; @@ -197,43 +207,26 @@ ASTNode SimplifyingNodeFactory::CreateSimpleAndOr(bool IsAnd, { // just drop it } - else if (nextexists && (next_it->GetKind() == BEEV::NOT) - && ((*next_it)[0] == *it)) - { - // form and negation -- return FALSE for AND, TRUE for OR. - retval = annihilator; - // cout << "X and/or NOT X" << endl; - if (debug_simplifyingNodeFactory) - { - cout << "Annihilator. Not and Equals" << retval << endl; - } - return retval; - } - else - { - // add to children - new_children.push_back(*it); - } } // If we get here, we saw no annihilators, and children should // be only the non-True nodes. - if (new_children.size() < 2) + if (children.size() < 2) { - if (0 == new_children.size()) + if (0 == children.size()) { retval = identity; } else { // there is just one child - retval = new_children[0]; + retval = children[0]; } } else { // 2 or more children. Create a new node. - retval = hashing.CreateNode(IsAnd ? BEEV::AND : BEEV::OR, new_children); + retval = hashing.CreateNode(IsAnd ? BEEV::AND : BEEV::OR, children); } if (debug_simplifyingNodeFactory) { @@ -242,6 +235,7 @@ ASTNode SimplifyingNodeFactory::CreateSimpleAndOr(bool IsAnd, return retval; } + //Tries to simplify the input to TRUE/FALSE. if it fails, then //return the constructed equality ASTNode SimplifyingNodeFactory::CreateSimpleEQ(const ASTVec& children) @@ -447,6 +441,9 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, FatalError("CreateTerm: Illegal kind to CreateTerm:", ASTUndefined, kind); + assert(kind != BEEV::BVCONST); // These are created specially. + assert(kind != BEEV::SYMBOL); // so are these. + // If all the parameters are constant, return the constant value. bool allConstant = true; for (unsigned i = 0; i < children.size(); i++) @@ -462,6 +459,7 @@ ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, { const ASTNode& hash = hashing.CreateTerm(kind, width, children); const ASTNode& c = simplifier->BVConstEvaluator(hash); + assert(c.isConstant()); return c; } -- 2.47.3