From d777600a5a1284e6296b4d5955d9558b227b449d Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Fri, 30 Dec 2011 04:09:42 +0000 Subject: [PATCH] Refactor. Automatically layout. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1456 e59a4935-1847-0410-ae03-e826735625c1 --- .../NodeFactory/SimplifyingNodeFactory.cpp | 2423 +++++++++-------- 1 file changed, 1219 insertions(+), 1204 deletions(-) diff --git a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp index f29b123..82ce399 100644 --- a/src/AST/NodeFactory/SimplifyingNodeFactory.cpp +++ b/src/AST/NodeFactory/SimplifyingNodeFactory.cpp @@ -50,750 +50,752 @@ static bool debug_simplifyingNodeFactory = false; static const bool translate_signed = true; -ASTNode SimplifyingNodeFactory::CreateNode(Kind kind, const ASTVec & children) +ASTNode +SimplifyingNodeFactory::CreateNode(Kind kind, const ASTVec & children) { - assert(kind != 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 && kind != BEEV::BOOLEAN && kind != BEEV::BITVECTOR && kind != BEEV::ARRAY) - { - bool allConstant = true; - - for (unsigned i = 0; i < children.size(); i++) - if (!children[i].isConstant()) - { - allConstant = false; - break; - } - - if (allConstant) - { - const ASTNode& hash = hashing.CreateNode(kind, children); - const ASTNode& c = NonMemberBVConstEvaluator(hash); - assert(c.isConstant()); - return c; - } - } - ASTNode result; - - switch (kind) - { - // convert the Less thans to greater thans. - case BEEV::BVLT: - assert(children.size() ==2); - result = NodeFactory::CreateNode(BEEV::BVGT, children[1], children[0]); - break; - - case BEEV::BVLE: - assert(children.size() ==2); - result = NodeFactory::CreateNode(BEEV::BVGE, children[1], children[0]); - break; - - case BEEV::BVSLT: - assert(children.size() ==2); - result = NodeFactory::CreateNode(BEEV::BVSGT, children[1], children[0]); - break; - - case BEEV::BVSLE: - assert(children.size() ==2); - result = NodeFactory::CreateNode(BEEV::BVSGE, children[1], children[0]); - break; - - - case BEEV::BVSGT: - assert(children.size() ==2); - if (children[0] == children[1]) - result = ASTFalse; - if (children[1].GetKind() == BEEV::BVCONST) - { - // 011111111 (most positive number.) - unsigned width = children[0].GetValueWidth(); - BEEV::CBV max = CONSTANTBV::BitVector_Create(width, false); - CONSTANTBV::BitVector_Fill(max); - CONSTANTBV::BitVector_Bit_Off(max, width - 1); - ASTNode biggestNumber = bm.CreateBVConst(max, width); - if (children[1] == biggestNumber) - result = ASTFalse; - } - if (children[0].GetKind() == BEEV::BVCONST) - { - unsigned width = children[0].GetValueWidth(); - // 1000000000 (most negative number.) - BEEV::CBV max = CONSTANTBV::BitVector_Create(width, true); - CONSTANTBV::BitVector_Bit_On(max, width - 1); - ASTNode smallestNumber = bm.CreateBVConst(max, width); - if (children[0] == smallestNumber) - result = ASTFalse; - } - - if (children[0].GetKind() ==BVCONCAT && children[1].GetKind() == BVCONCAT && children[0][1] == children[1][1]) - result = NodeFactory::CreateNode(BEEV::BVSGT, children[0][0], children[1][0]); - - - break; - - case BEEV::BVGT: - assert(children.size() ==2); - if (children[0] == children[1]) - result = ASTFalse; - if (children[0].isConstant() && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst())) - result = ASTFalse; - if (children[1].isConstant() && CONSTANTBV::BitVector_is_full(children[1].GetBVConst())) - result = ASTFalse; - if (children[0].GetKind() == BVRIGHTSHIFT && children[0][0] == children[1]) - result = ASTFalse; - if (children[0].GetKind() ==BVCONCAT && children[1].GetKind() == BVCONCAT && children[0][1] == children[1][1]) - result = NodeFactory::CreateNode(BEEV::BVGT, children[0][0], children[1][0]); - if (children[0].GetKind() ==BVCONCAT && children[1].GetKind() == BVCONCAT && children[0][0] == children[1][0]) - result = NodeFactory::CreateNode(BEEV::BVGT, children[0][1], children[1][1]); - if (children[1].isConstant() && CONSTANTBV::BitVector_is_empty(children[1].GetBVConst())) - result = NodeFactory::CreateNode(BEEV::NOT, NodeFactory::CreateNode(EQ, children[0], children[1])); - if (children[0].isConstant() && CONSTANTBV::BitVector_is_full(children[0].GetBVConst())) - result = NodeFactory::CreateNode(BEEV::NOT, NodeFactory::CreateNode(EQ, children[0], children[1])); - if (children[0].GetKind() ==BEEV::BVAND && children[0].Degree() > 1 && ((children[0][0] == children[1]) || children[0][1] == children[1])) - result = ASTFalse; - break; - - case BEEV::BVGE: - assert(children.size() ==2); - { - ASTNode a = NodeFactory::CreateNode(BEEV::BVGT, children[1], children[0]); - result = NodeFactory::CreateNode(BEEV::NOT, a); - } + assert(kind != 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 && kind != BEEV::BOOLEAN && kind != BEEV::BITVECTOR && kind != BEEV::ARRAY) + { + bool allConstant = true; + + for (unsigned i = 0; i < children.size(); i++) + if (!children[i].isConstant()) + { + allConstant = false; break; + } - case BEEV::BVSGE: - assert(children.size() ==2); - { - ASTNode a = NodeFactory::CreateNode(BEEV::BVSGT, children[1], children[0]); - result = NodeFactory::CreateNode(BEEV::NOT, a); - } - break; - - case BEEV::NOT: - result = CreateSimpleNot(children); - break; - case BEEV::AND: - result = CreateSimpleAndOr(1, children); - break; - case BEEV::OR: - result = CreateSimpleAndOr(0, children); - break; - case BEEV::NAND: - result = CreateSimpleNot(CreateSimpleAndOr(1, children)); - break; - case BEEV::NOR: - result = CreateSimpleNot(CreateSimpleAndOr(0, children)); - break; - case BEEV::XOR: - result = CreateSimpleXor(children); - break; - case ITE: - result = CreateSimpleFormITE(children); - break; - case EQ: - result = CreateSimpleEQ(children); - break; - case BEEV::IFF: - { - assert(children.size() ==2); - ASTVec newCh; - newCh.reserve(2); - newCh.push_back(CreateSimpleNot(children[0])); - newCh.push_back(children[1]); - result = CreateSimpleXor(newCh); - break; - } - case BEEV::IMPLIES: - { - assert(children.size() ==2); - if (children[0] == children[1]) - result = bm.ASTTrue; - else - { - ASTVec newCh; - newCh.reserve(2); - newCh.push_back(CreateSimpleNot(children[0])); - newCh.push_back(children[1]); - result = CreateSimpleAndOr(0, newCh); - } - break; - } - - - default: - result = hashing.CreateNode(kind, children); - } - - if (result.IsNull()) - result = hashing.CreateNode(kind, children); - - return result; + if (allConstant) + { + const ASTNode& hash = hashing.CreateNode(kind, children); + const ASTNode& c = NonMemberBVConstEvaluator(hash); + assert(c.isConstant()); + return c; + } + } + ASTNode result; + + switch (kind) + { + // convert the Less thans to greater thans. + case BEEV::BVLT: + assert(children.size() ==2); + result = NodeFactory::CreateNode(BEEV::BVGT, children[1], children[0]); + break; + + case BEEV::BVLE: + assert(children.size() ==2); + result = NodeFactory::CreateNode(BEEV::BVGE, children[1], children[0]); + break; + + case BEEV::BVSLT: + assert(children.size() ==2); + result = NodeFactory::CreateNode(BEEV::BVSGT, children[1], children[0]); + break; + + case BEEV::BVSLE: + assert(children.size() ==2); + result = NodeFactory::CreateNode(BEEV::BVSGE, children[1], children[0]); + break; + + case BEEV::BVSGT: + assert(children.size() ==2); + if (children[0] == children[1]) + result = ASTFalse; + if (children[1].GetKind() == BEEV::BVCONST) + { + // 011111111 (most positive number.) + unsigned width = children[0].GetValueWidth(); + BEEV::CBV max = CONSTANTBV::BitVector_Create(width, false); + CONSTANTBV::BitVector_Fill(max); + CONSTANTBV::BitVector_Bit_Off(max, width - 1); + ASTNode biggestNumber = bm.CreateBVConst(max, width); + if (children[1] == biggestNumber) + result = ASTFalse; + } + if (children[0].GetKind() == BEEV::BVCONST) + { + unsigned width = children[0].GetValueWidth(); + // 1000000000 (most negative number.) + BEEV::CBV max = CONSTANTBV::BitVector_Create(width, true); + CONSTANTBV::BitVector_Bit_On(max, width - 1); + ASTNode smallestNumber = bm.CreateBVConst(max, width); + if (children[0] == smallestNumber) + result = ASTFalse; + } + + if (children[0].GetKind() == BVCONCAT && children[1].GetKind() == BVCONCAT && children[0][1] == children[1][1]) + result = NodeFactory::CreateNode(BEEV::BVSGT, children[0][0], children[1][0]); + + break; + + case BEEV::BVGT: + assert(children.size() ==2); + if (children[0] == children[1]) + result = ASTFalse; + if (children[0].isConstant() && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst())) + result = ASTFalse; + if (children[1].isConstant() && CONSTANTBV::BitVector_is_full(children[1].GetBVConst())) + result = ASTFalse; + if (children[0].GetKind() == BVRIGHTSHIFT && children[0][0] == children[1]) + result = ASTFalse; + if (children[0].GetKind() == BVCONCAT && children[1].GetKind() == BVCONCAT && children[0][1] == children[1][1]) + result = NodeFactory::CreateNode(BEEV::BVGT, children[0][0], children[1][0]); + if (children[0].GetKind() == BVCONCAT && children[1].GetKind() == BVCONCAT && children[0][0] == children[1][0]) + result = NodeFactory::CreateNode(BEEV::BVGT, children[0][1], children[1][1]); + if (children[1].isConstant() && CONSTANTBV::BitVector_is_empty(children[1].GetBVConst())) + result = NodeFactory::CreateNode(BEEV::NOT, NodeFactory::CreateNode(EQ, children[0], children[1])); + if (children[0].isConstant() && CONSTANTBV::BitVector_is_full(children[0].GetBVConst())) + result = NodeFactory::CreateNode(BEEV::NOT, NodeFactory::CreateNode(EQ, children[0], children[1])); + if (children[0].GetKind() == BEEV::BVAND && children[0].Degree() > 1 + && ((children[0][0] == children[1]) || children[0][1] == children[1])) + result = ASTFalse; + break; + + case BEEV::BVGE: + assert(children.size() ==2); + { + ASTNode a = NodeFactory::CreateNode(BEEV::BVGT, children[1], children[0]); + result = NodeFactory::CreateNode(BEEV::NOT, a); + } + break; + + case BEEV::BVSGE: + assert(children.size() ==2); + { + ASTNode a = NodeFactory::CreateNode(BEEV::BVSGT, children[1], children[0]); + result = NodeFactory::CreateNode(BEEV::NOT, a); + } + break; + + case BEEV::NOT: + result = CreateSimpleNot(children); + break; + case BEEV::AND: + result = CreateSimpleAndOr(1, children); + break; + case BEEV::OR: + result = CreateSimpleAndOr(0, children); + break; + case BEEV::NAND: + result = CreateSimpleNot(CreateSimpleAndOr(1, children)); + break; + case BEEV::NOR: + result = CreateSimpleNot(CreateSimpleAndOr(0, children)); + break; + case BEEV::XOR: + result = CreateSimpleXor(children); + break; + case ITE: + result = CreateSimpleFormITE(children); + break; + case EQ: + result = CreateSimpleEQ(children); + break; + case BEEV::IFF: + { + assert(children.size() ==2); + ASTVec newCh; + newCh.reserve(2); + newCh.push_back(CreateSimpleNot(children[0])); + newCh.push_back(children[1]); + result = CreateSimpleXor(newCh); + break; + } + case BEEV::IMPLIES: + { + assert(children.size() ==2); + if (children[0] == children[1]) + result = bm.ASTTrue; + else + { + ASTVec newCh; + newCh.reserve(2); + newCh.push_back(CreateSimpleNot(children[0])); + newCh.push_back(children[1]); + result = CreateSimpleAndOr(0, newCh); + } + break; + } + + default: + result = hashing.CreateNode(kind, children); + } + + if (result.IsNull()) + result = hashing.CreateNode(kind, children); + + return result; } -ASTNode SimplifyingNodeFactory::CreateSimpleNot(const ASTNode& form) +ASTNode +SimplifyingNodeFactory::CreateSimpleNot(const ASTNode& form) { - const Kind k = form.GetKind(); - switch (k) - { - case BEEV::FALSE: - { - return form.GetSTPMgr()->ASTTrue; - } - case BEEV::TRUE: - { - return form.GetSTPMgr()->ASTFalse; - } - case BEEV::NOT: - { - return form[0]; - } // NOT NOT cancellation - default: - { - ASTVec children; - children.push_back(form); - return hashing.CreateNode(BEEV::NOT, children); - } - } + const Kind k = form.GetKind(); + switch (k) + { + case BEEV::FALSE: + { + return form.GetSTPMgr()->ASTTrue; + } + case BEEV::TRUE: + { + return form.GetSTPMgr()->ASTFalse; + } + case BEEV::NOT: + { + return form[0]; + } // NOT NOT cancellation + default: + { + ASTVec children; + children.push_back(form); + return hashing.CreateNode(BEEV::NOT, children); + } + } } -ASTNode SimplifyingNodeFactory::CreateSimpleNot(const ASTVec& children) +ASTNode +SimplifyingNodeFactory::CreateSimpleNot(const ASTVec& children) { - const Kind k = children[0].GetKind(); - switch (k) - { - case BEEV::FALSE: - { - return children[0].GetSTPMgr()->ASTTrue; - } - case BEEV::TRUE: - { - return children[0].GetSTPMgr()->ASTFalse; - } - case BEEV::NOT: - { - return children[0][0]; - } // NOT NOT cancellation - default: - { - return hashing.CreateNode(BEEV::NOT, children); - } - } + const Kind k = children[0].GetKind(); + switch (k) + { + case BEEV::FALSE: + { + return children[0].GetSTPMgr()->ASTTrue; + } + case BEEV::TRUE: + { + return children[0].GetSTPMgr()->ASTFalse; + } + case BEEV::NOT: + { + return children[0][0]; + } // NOT NOT cancellation + default: + { + return hashing.CreateNode(BEEV::NOT, children); + } + } } -ASTNode SimplifyingNodeFactory::CreateSimpleAndOr(bool IsAnd, - const ASTNode& form1, const ASTNode& form2) +ASTNode +SimplifyingNodeFactory::CreateSimpleAndOr(bool IsAnd, const ASTNode& form1, const ASTNode& form2) { - ASTVec children; - children.push_back(form1); - children.push_back(form2); - return CreateSimpleAndOr(IsAnd, children); + ASTVec children; + children.push_back(form1); + children.push_back(form2); + return CreateSimpleAndOr(IsAnd, children); } -ASTNode SimplifyingNodeFactory::CreateSimpleAndOr(bool IsAnd, - const ASTVec &children) +ASTNode +SimplifyingNodeFactory::CreateSimpleAndOr(bool IsAnd, const ASTVec &children) { - 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 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); - - ASTNode retval; - ASTVec new_children; - new_children.reserve(children.size()); - - const ASTVec::const_iterator it_end = children.end(); - for (ASTVec::const_iterator it = children.begin(); it != it_end; it++) - { - ASTVec::const_iterator next_it; - - bool nextexists = (it + 1 < it_end); - if (nextexists) - next_it = it + 1; - else - next_it = it_end; - - if (*it == annihilator) - { - return annihilator; - } - else if (*it == identity || (nextexists && (*next_it == *it))) - { - // just drop it - }else - new_children.push_back(*it); - } - - // If we get here, we saw no annihilators, and children should - // be only the non-True nodes. - - - if (0 == new_children.size()) - { - retval = identity; - } - else if (1==new_children.size()) - { - // there is just one child - retval = new_children[0]; - } - else - { - // 2 or more children. Create a new node. - retval = hashing.CreateNode(IsAnd ? BEEV::AND : BEEV::OR, new_children); - } - return retval; -} + const ASTNode& annihilator = (IsAnd ? ASTFalse : ASTTrue); + const ASTNode& identity = (IsAnd ? ASTTrue : ASTFalse); + + ASTNode retval; + ASTVec new_children; + new_children.reserve(children.size()); + + const ASTVec::const_iterator it_end = children.end(); + for (ASTVec::const_iterator it = children.begin(); it != it_end; it++) + { + ASTVec::const_iterator next_it; + + bool nextexists = (it + 1 < it_end); + if (nextexists) + next_it = it + 1; + else + next_it = it_end; + + if (*it == annihilator) + { + return annihilator; + } + else if (*it == identity || (nextexists && (*next_it == *it))) + { + // just drop it + } + else + new_children.push_back(*it); + } + + // If we get here, we saw no annihilators, and children should + // be only the non-True nodes. + if (0 == new_children.size()) + { + retval = identity; + } + else if (1 == new_children.size()) + { + // there is just one child + retval = new_children[0]; + } + else + { + // 2 or more children. Create a new node. + retval = hashing.CreateNode(IsAnd ? BEEV::AND : BEEV::OR, new_children); + } + return retval; +} //Tries to simplify the input to TRUE/FALSE. if it fails, then //return the constructed equality -ASTNode SimplifyingNodeFactory::CreateSimpleEQ(const ASTVec& children) +ASTNode +SimplifyingNodeFactory::CreateSimpleEQ(const ASTVec& children) { - assert(children.size() == 2); + assert(children.size() == 2); - // SYMBOL = something, if not that, then CONSTANT = - const bool swap = (children[1].GetKind() == BEEV::SYMBOL || ((children[0].GetKind() != BEEV::SYMBOL) && children[1].GetKind() == BEEV::BVCONST)); - const ASTNode& in1 = swap? children[1] : children[0]; - const ASTNode& in2 = swap ? children[0] : children[1]; - const Kind k1 = in1.GetKind(); - const Kind k2 = in2.GetKind(); - const int width = in1.GetValueWidth(); + // SYMBOL = something, if not that, then CONSTANT = + const bool swap = (children[1].GetKind() == BEEV::SYMBOL + || ((children[0].GetKind() != BEEV::SYMBOL) && children[1].GetKind() == BEEV::BVCONST)); + const ASTNode& in1 = swap ? children[1] : children[0]; + const ASTNode& in2 = swap ? children[0] : 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; + 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 == BVNEG && k2 == BVNEG) || (k1 == BVUMINUS && k2 == BVUMINUS)) - return NodeFactory::CreateNode(EQ, in1[0], in2[0]); + if ((k1 == BVNEG && k2 == BVNEG) || (k1 == BVUMINUS && k2 == BVUMINUS)) + return NodeFactory::CreateNode(EQ, in1[0], in2[0]); - if ((k1 == BVUMINUS && k2 == BEEV::BVCONST) || (k1 == BVNEG && k2 == BEEV::BVCONST)) - return NodeFactory::CreateNode(EQ, in1[0], NodeFactory::CreateTerm(k1,width, in2 )); + if ((k1 == BVUMINUS && k2 == BEEV::BVCONST) || (k1 == BVNEG && k2 == BEEV::BVCONST)) + return NodeFactory::CreateNode(EQ, in1[0], NodeFactory::CreateTerm(k1, width, in2)); - if (k2 == BVUMINUS && k1 == BEEV::BVCONST || (k2 == BVNEG && k1 == BEEV::BVCONST)) - return NodeFactory::CreateNode(EQ, in2[0], NodeFactory::CreateTerm(k2,width, in1 )); + if (k2 == BVUMINUS && k1 == BEEV::BVCONST || (k2 == BVNEG && k1 == BEEV::BVCONST)) + return NodeFactory::CreateNode(EQ, in2[0], NodeFactory::CreateTerm(k2, width, in1)); - if ((k1 == BVNEG && in1[0] == in2) || (k2 == BVNEG && in2[0] == in1)) - return in1.GetSTPMgr()->ASTFalse; + if ((k1 == BVNEG && in1[0] == in2) || (k2 == BVNEG && in2[0] == in1)) + return in1.GetSTPMgr()->ASTFalse; - if (k2 == BEEV::BVDIV && k1 == BEEV::BVCONST && (in1 == bm.CreateZeroConst(width))) - return NodeFactory::CreateNode(BEEV::BVGT, in2[1], in2[0]); + if (k2 == BEEV::BVDIV && k1 == BEEV::BVCONST && (in1 == bm.CreateZeroConst(width))) + return NodeFactory::CreateNode(BEEV::BVGT, in2[1], in2[0]); - if (k1 == BEEV::BVDIV && k2 == BEEV::BVCONST && (in2 == bm.CreateZeroConst(width))) - return NodeFactory::CreateNode(BEEV::BVGT, in1[1], in1[0]); + if (k1 == BEEV::BVDIV && k2 == BEEV::BVCONST && (in2 == bm.CreateZeroConst(width))) + return NodeFactory::CreateNode(BEEV::BVGT, in1[1], in1[0]); - // split the constant to equal each part of the concat. - if (BVCONCAT == k2 && BEEV::BVCONST == k1) - { - int low_b = 0; - int high_b = in2[1].GetValueWidth() -1; - int low_t = in2[1].GetValueWidth(); - int high_t = width-1; + // split the constant to equal each part of the concat. + if (BVCONCAT == k2 && BEEV::BVCONST == k1) + { + int low_b = 0; + int high_b = in2[1].GetValueWidth() - 1; + int low_t = in2[1].GetValueWidth(); + int high_t = width - 1; + + ASTNode c0 = NodeFactory::CreateTerm(BVEXTRACT, in2[1].GetValueWidth(), in1, bm.CreateBVConst(32, high_b), + bm.CreateBVConst(32, low_b)); + ASTNode c1 = NodeFactory::CreateTerm(BVEXTRACT, in2[0].GetValueWidth(), in1, bm.CreateBVConst(32, high_t), + bm.CreateBVConst(32, low_t)); + + ASTNode a = NodeFactory::CreateNode(EQ, in2[1], c0); + ASTNode b = NodeFactory::CreateNode(EQ, in2[0], c1); + return NodeFactory::CreateNode(BEEV::AND, a, b); + } - ASTNode c0 = NodeFactory::CreateTerm(BVEXTRACT, in2[1].GetValueWidth(), in1, bm.CreateBVConst(32, high_b), bm.CreateBVConst(32, low_b)); - ASTNode c1 = NodeFactory::CreateTerm(BVEXTRACT, in2[0].GetValueWidth(), in1, bm.CreateBVConst(32, high_t), bm.CreateBVConst(32, low_t)); + // This increases the number of nodes. So disable for now. + if (false && BVCONCAT == k1 && BVCONCAT == k2 && in1[0].GetValueWidth() == in2[0].GetValueWidth()) + { + ASTNode a = NodeFactory::CreateNode(EQ, in1[0], in2[0]); + ASTNode b = NodeFactory::CreateNode(EQ, in1[1], in2[1]); + return NodeFactory::CreateNode(BEEV::AND, a, b); + } - ASTNode a = NodeFactory::CreateNode(EQ, in2[1],c0); - ASTNode b = NodeFactory::CreateNode(EQ, in2[0],c1); - return NodeFactory::CreateNode(BEEV::AND, a, b); - } + if (k1 == BEEV::BVCONST && k2 == ITE && in2[1].GetKind() == BEEV::BVCONST && in2[2].GetKind() == BEEV::BVCONST) + { - // This increases the number of nodes. So disable for now. - if (false && BVCONCAT == k1 && BVCONCAT == k2 && in1[0].GetValueWidth() == in2[0].GetValueWidth()) - { - ASTNode a = NodeFactory::CreateNode(EQ, in1[0],in2[0]); - ASTNode b = NodeFactory::CreateNode(EQ, in1[1],in2[1]); - return NodeFactory::CreateNode(BEEV::AND, a, b); - } - - - if (k1 == BEEV::BVCONST && k2 == ITE && in2[1].GetKind() == BEEV::BVCONST && in2[2].GetKind() == BEEV::BVCONST) - { - - ASTNode result = - NodeFactory::CreateNode(ITE, - in2[0], - NodeFactory::CreateNode(EQ,in1,in2[1]), - NodeFactory::CreateNode(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). - if ((k1 == BVPLUS && in1.Degree() <=2) || (k2 == BVPLUS && in2.Degree() <=2)) - { - const ASTVec& c1 = (k1 == BVPLUS)? in1.GetChildren() : ASTVec(1,in1) ; - const ASTVec& c2 = (k2 == BVPLUS)? in2.GetChildren() : ASTVec(1,in2) ; - - if (c1.size() <=2 && c2.size() <=2) - { - int match1 =-1, match2=-1; - - for (int i =0; i < c1.size();i++) - for (int j =0; j < c2.size();j++) - { - if (c1[i] == c2[j]) - { - match1 = i; - match2 = j; - } - } - - if (match1 != -1) - { - assert(match2 !=-1); - assert(match1 == 0 || match1 == 1); - assert(match2 == 0 || match2 == 1); - // If it was 1 element before, it's zero now. - ASTNode n1 = c1.size() == 1 ? bm.CreateZeroConst(width) : c1[match1==0?1:0]; - ASTNode n2 = c2.size() == 1 ? bm.CreateZeroConst(width) : c2[match2==0?1:0]; - return NodeFactory::CreateNode(EQ, n1, n2); - } - } - } - - if (k2 == BVPLUS && in2.Degree() ==2 && (in2[1] == in1 || in2[0] == in1)) - { - return NodeFactory::CreateNode(EQ,bm.CreateZeroConst(width),in2[1] == in1 ? in2[0]: in2[1]); - } - - if (k1 == BVPLUS && in1.Degree() ==2 && (in1[1] == in2 || in1[0] == in2)) - { - return NodeFactory::CreateNode(EQ,bm.CreateZeroConst(width),in1[1] == in2 ? in1[0]: in1[1]); - } + ASTNode result = NodeFactory::CreateNode(ITE, in2[0], NodeFactory::CreateNode(EQ, in1, in2[1]), + NodeFactory::CreateNode(EQ, in1, in2[2])); + return result; + } - if (k1 == BEEV::BVCONST && k2 == BEEV::BVXOR && in2.Degree() == 2 && in2[0].GetKind() == BEEV::BVCONST ) - { - return NodeFactory::CreateNode(EQ,NodeFactory::CreateTerm(BEEV::BVXOR,width,in1,in2[0] ), in2[1]); - } + // 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). + if ((k1 == BVPLUS && in1.Degree() <= 2) || (k2 == BVPLUS && in2.Degree() <= 2)) + { + const ASTVec& c1 = (k1 == BVPLUS) ? in1.GetChildren() : ASTVec(1, in1); + const ASTVec& c2 = (k2 == BVPLUS) ? in2.GetChildren() : ASTVec(1, in2); - if (k2 == BEEV::BVCONST && k1 == BEEV::BVXOR && in1.Degree() == 2 && in1[0].GetKind() == BEEV::BVCONST ) + if (c1.size() <= 2 && c2.size() <= 2) { - return NodeFactory::CreateNode(EQ,NodeFactory::CreateTerm(BEEV::BVXOR,width,in2,in1[0] ), in1[1]); - } + int match1 = -1, match2 = -1; - if (k2 == BEEV::BVXOR && in2.Degree() == 2 && in1 == in2[0]) - { - return NodeFactory::CreateNode(EQ, bm.CreateZeroConst(width), in2[1]); - } + for (int i = 0; i < c1.size(); i++) + for (int j = 0; j < c2.size(); j++) + { + if (c1[i] == c2[j]) + { + match1 = i; + match2 = j; + } + } - if (k1 == BEEV::BVXOR && in1.Degree() == 2 && in2 == in1[0]) - { - return NodeFactory::CreateNode(EQ, bm.CreateZeroConst(width), in1[1]); + if (match1 != -1) + { + assert(match2 !=-1); + assert(match1 == 0 || match1 == 1); + assert(match2 == 0 || match2 == 1); + // If it was 1 element before, it's zero now. + ASTNode n1 = c1.size() == 1 ? bm.CreateZeroConst(width) : c1[match1 == 0 ? 1 : 0]; + ASTNode n2 = c2.size() == 1 ? bm.CreateZeroConst(width) : c2[match2 == 0 ? 1 : 0]; + return NodeFactory::CreateNode(EQ, n1, n2); + } } + } + if (k2 == BVPLUS && in2.Degree() == 2 && (in2[1] == in1 || in2[0] == in1)) + { + return NodeFactory::CreateNode(EQ, bm.CreateZeroConst(width), in2[1] == in1 ? in2[0] : in2[1]); + } - if (k1 == BEEV::BVCONST && k2 == BEEV::BVSX && (in2[0].GetValueWidth() != width)) - { - // Each of the bits in the extended part, and one into the un-extended part must be the same. - bool foundZero=false, foundOne=false; - const unsigned original_width = in2[0].GetValueWidth(); - const unsigned new_width = in2.GetValueWidth(); - for (int i = original_width-1; i < new_width;i++) - if (CONSTANTBV::BitVector_bit_test(in1.GetBVConst(),i)) - foundOne=true; - else - foundZero=true; - if (foundZero && foundOne) - return ASTFalse; - ASTNode lhs = NodeFactory::CreateTerm(BVEXTRACT, original_width, in1, bm.CreateBVConst(32,original_width-1), bm.CreateZeroConst(32)); - ASTNode rhs = NodeFactory::CreateTerm(BVEXTRACT, original_width, in2, bm.CreateBVConst(32,original_width-1), bm.CreateZeroConst(32)); - return NodeFactory::CreateNode(EQ, lhs,rhs); - } + if (k1 == BVPLUS && in1.Degree() == 2 && (in1[1] == in2 || in1[0] == in2)) + { + return NodeFactory::CreateNode(EQ, bm.CreateZeroConst(width), in1[1] == in2 ? in1[0] : in1[1]); + } - // Simplifiy (5 = 4/x) to FALSE. - if (bm.UserFlags.division_by_zero_returns_one_flag && k1 == BEEV::BVCONST && k2 == BEEV::BVDIV && in2[0].GetKind() == BEEV::BVCONST) - { - ASTNode oneV = bm.CreateOneConst(width); - if ( CONSTANTBV::BitVector_Lexicompare(in1.GetBVConst(), oneV.GetBVConst()) > 0 && - in1 != oneV && - CONSTANTBV::BitVector_Lexicompare(in1.GetBVConst(), in2[0].GetBVConst()) > 0) - { return ASTFalse; - } - } + if (k1 == BEEV::BVCONST && k2 == BEEV::BVXOR && in2.Degree() == 2 && in2[0].GetKind() == BEEV::BVCONST) + { + return NodeFactory::CreateNode(EQ, NodeFactory::CreateTerm(BEEV::BVXOR, width, in1, in2[0]), in2[1]); + } - if (k1 == BVNEG && k2 == BVUMINUS && in1[0] == in2[0]) - return ASTFalse; + if (k2 == BEEV::BVCONST && k1 == BEEV::BVXOR && in1.Degree() == 2 && in1[0].GetKind() == BEEV::BVCONST) + { + return NodeFactory::CreateNode(EQ, NodeFactory::CreateTerm(BEEV::BVXOR, width, in2, in1[0]), in1[1]); + } + + if (k2 == BEEV::BVXOR && in2.Degree() == 2 && in1 == in2[0]) + { + return NodeFactory::CreateNode(EQ, bm.CreateZeroConst(width), in2[1]); + } + + if (k1 == BEEV::BVXOR && in1.Degree() == 2 && in2 == in1[0]) + { + return NodeFactory::CreateNode(EQ, bm.CreateZeroConst(width), in1[1]); + } + + if (k1 == BEEV::BVCONST && k2 == BEEV::BVSX && (in2[0].GetValueWidth() != width)) + { + // Each of the bits in the extended part, and one into the un-extended part must be the same. + bool foundZero = false, foundOne = false; + const unsigned original_width = in2[0].GetValueWidth(); + const unsigned new_width = in2.GetValueWidth(); + for (int i = original_width - 1; i < new_width; i++) + if (CONSTANTBV::BitVector_bit_test(in1.GetBVConst(), i)) + foundOne = true; + else + foundZero = true; + if (foundZero && foundOne) + return ASTFalse; + ASTNode lhs = NodeFactory::CreateTerm(BVEXTRACT, original_width, in1, bm.CreateBVConst(32, original_width - 1), + bm.CreateZeroConst(32)); + ASTNode rhs = NodeFactory::CreateTerm(BVEXTRACT, original_width, in2, bm.CreateBVConst(32, original_width - 1), + bm.CreateZeroConst(32)); + return NodeFactory::CreateNode(EQ, lhs, rhs); + } - if (k1 == BVUMINUS && k2 == BVNEG && in1[0] == in2[0]) + // Simplifiy (5 = 4/x) to FALSE. + if (bm.UserFlags.division_by_zero_returns_one_flag && k1 == BEEV::BVCONST && k2 == BEEV::BVDIV + && in2[0].GetKind() == BEEV::BVCONST) + { + ASTNode oneV = bm.CreateOneConst(width); + if (CONSTANTBV::BitVector_Lexicompare(in1.GetBVConst(), oneV.GetBVConst()) > 0 && in1 != oneV + && CONSTANTBV::BitVector_Lexicompare(in1.GetBVConst(), in2[0].GetBVConst()) > 0) + { return ASTFalse; + } + } + + if (k1 == BVNEG && k2 == BVUMINUS && in1[0] == in2[0]) + return ASTFalse; - //last resort is to CreateNode - return hashing.CreateNode(EQ, children); + if (k1 == BVUMINUS && k2 == BVNEG && in1[0] == in2[0]) + return ASTFalse; + + //last resort is to CreateNode + return hashing.CreateNode(EQ, children); } // Constant children are accumulated in "accumconst". -ASTNode SimplifyingNodeFactory::CreateSimpleXor(const ASTVec &children) +ASTNode +SimplifyingNodeFactory::CreateSimpleXor(const ASTVec &children) { - if (debug_simplifyingNodeFactory) - { - cout << "========" << endl << "CreateSimpXor "; - lpvec(children); - cout << endl; - } - - ASTVec flat_children; // empty vector - flat_children = children; - - // sort so that identical nodes occur in sequential runs, followed by - // their negations. - SortByExprNum(flat_children); - - // This is the C Boolean value of all constant args seen. It is initially - // 0. TRUE children cause it to change value. - bool accumconst = 0; - - ASTVec new_children; - new_children.reserve(children.size()); - - const ASTVec::const_iterator it_end = flat_children.end(); - ASTVec::iterator next_it; - for (ASTVec::iterator it = flat_children.begin(); it != it_end; it++) - { - next_it = it + 1; - bool nextexists = (next_it < it_end); - - if (ASTTrue == *it) - { - accumconst = !accumconst; - } - else if (ASTFalse == *it) - { - // Ignore it - } - else if (nextexists && (*next_it == *it)) - { - // x XOR x = FALSE. Skip current, write "false" into next_it - // so that it gets tossed, too. - *next_it = ASTFalse; - } - else if (nextexists && (next_it->GetKind() == BEEV::NOT) - && ((*next_it)[0] == *it)) - { - // x XOR NOT x = TRUE. Skip current, write "true" into next_it - // so that it gets tossed, too. - *next_it = ASTTrue; - } - else if (BEEV::NOT == it->GetKind()) - { - // If child is (NOT alpha), we can flip accumconst and use alpha. - // This is ok because (NOT alpha) == TRUE XOR alpha - accumconst = !accumconst; - // CreateSimpNot just takes child of not. - new_children.push_back(CreateSimpleNot(*it)); - } - else - { - new_children.push_back(*it); - } - } - - ASTNode retval; - - // Children should be non-constant. - if (new_children.size() < 2) - { - if (0 == new_children.size()) - { - // XOR(TRUE, FALSE) -- accumconst will be 1. - if (accumconst) - { - retval = ASTTrue; - } - else - { - retval = ASTFalse; - } - } - else - { - // there is just one child - // XOR(x, TRUE) -- accumconst will be 1. - if (accumconst) - { - retval = CreateSimpleNot(new_children[0]); - } - else - { - retval = new_children[0]; - } - } - } - else - { - // negate first child if accumconst == 1 - if (accumconst) - { - new_children[0] = CreateSimpleNot(new_children[0]); - } - retval = hashing.CreateNode(BEEV::XOR, new_children); - } - - if (debug_simplifyingNodeFactory) - { - cout << "returns " << retval << endl; - } - return retval; + if (debug_simplifyingNodeFactory) + { + cout << "========" << endl << "CreateSimpXor "; + lpvec(children); + cout << endl; + } + + ASTVec flat_children; // empty vector + flat_children = children; + + // sort so that identical nodes occur in sequential runs, followed by + // their negations. + SortByExprNum(flat_children); + + // This is the C Boolean value of all constant args seen. It is initially + // 0. TRUE children cause it to change value. + bool accumconst = 0; + + ASTVec new_children; + new_children.reserve(children.size()); + + const ASTVec::const_iterator it_end = flat_children.end(); + ASTVec::iterator next_it; + for (ASTVec::iterator it = flat_children.begin(); it != it_end; it++) + { + next_it = it + 1; + bool nextexists = (next_it < it_end); + + if (ASTTrue == *it) + { + accumconst = !accumconst; + } + else if (ASTFalse == *it) + { + // Ignore it + } + else if (nextexists && (*next_it == *it)) + { + // x XOR x = FALSE. Skip current, write "false" into next_it + // so that it gets tossed, too. + *next_it = ASTFalse; + } + else if (nextexists && (next_it->GetKind() == BEEV::NOT) && ((*next_it)[0] == *it)) + { + // x XOR NOT x = TRUE. Skip current, write "true" into next_it + // so that it gets tossed, too. + *next_it = ASTTrue; + } + else if (BEEV::NOT == it->GetKind()) + { + // If child is (NOT alpha), we can flip accumconst and use alpha. + // This is ok because (NOT alpha) == TRUE XOR alpha + accumconst = !accumconst; + // CreateSimpNot just takes child of not. + new_children.push_back(CreateSimpleNot(*it)); + } + else + { + new_children.push_back(*it); + } + } + + ASTNode retval; + + // Children should be non-constant. + if (new_children.size() < 2) + { + if (0 == new_children.size()) + { + // XOR(TRUE, FALSE) -- accumconst will be 1. + if (accumconst) + { + retval = ASTTrue; + } + else + { + retval = ASTFalse; + } + } + else + { + // there is just one child + // XOR(x, TRUE) -- accumconst will be 1. + if (accumconst) + { + retval = CreateSimpleNot(new_children[0]); + } + else + { + retval = new_children[0]; + } + } + } + else + { + // negate first child if accumconst == 1 + if (accumconst) + { + new_children[0] = CreateSimpleNot(new_children[0]); + } + retval = hashing.CreateNode(BEEV::XOR, new_children); + } + + if (debug_simplifyingNodeFactory) + { + cout << "returns " << retval << endl; + } + return retval; } -ASTNode SimplifyingNodeFactory::CreateSimpleFormITE(const ASTVec& children) +ASTNode +SimplifyingNodeFactory::CreateSimpleFormITE(const ASTVec& children) { - const ASTNode& child0 = children[0]; - const ASTNode& child1 = children[1]; - const ASTNode& child2 = children[2]; - - ASTNode retval; - - if (debug_simplifyingNodeFactory) - { - cout << "========" << endl << "CreateSimpleFormITE " << child0 - << child1 << child2 << endl; - } - - if (ASTTrue == child0) - { - retval = child1; - } - else if (ASTFalse == child0) - { - retval = child2; - } - else if (child1 == child2) - { - retval = child1; - } - // ITE(x, TRUE, y ) == x OR y - else if (ASTTrue == child1) - { - retval = CreateSimpleAndOr(0, child0, child2); - } - // ITE(x, FALSE, y ) == (!x AND y) - else if (ASTFalse == child1) - { - retval = CreateSimpleAndOr(1, CreateSimpleNot(child0), child2); - } - // ITE(x, y, TRUE ) == (!x OR y) - else if (ASTTrue == child2) - { - retval = CreateSimpleAndOr(0, CreateSimpleNot(child0), child1); - } - // ITE(x, y, FALSE ) == (x AND y) - else if (ASTFalse == child2) - { - 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(ITE, children); - } - - if (debug_simplifyingNodeFactory) - { - cout << "returns " << retval << endl; - } - - return retval; + const ASTNode& child0 = children[0]; + const ASTNode& child1 = children[1]; + const ASTNode& child2 = children[2]; + + ASTNode retval; + + if (debug_simplifyingNodeFactory) + { + cout << "========" << endl << "CreateSimpleFormITE " << child0 << child1 << child2 << endl; + } + + if (ASTTrue == child0) + { + retval = child1; + } + else if (ASTFalse == child0) + { + retval = child2; + } + else if (child1 == child2) + { + retval = child1; + } + // ITE(x, TRUE, y ) == x OR y + else if (ASTTrue == child1) + { + retval = CreateSimpleAndOr(0, child0, child2); + } + // ITE(x, FALSE, y ) == (!x AND y) + else if (ASTFalse == child1) + { + retval = CreateSimpleAndOr(1, CreateSimpleNot(child0), child2); + } + // ITE(x, y, TRUE ) == (!x OR y) + else if (ASTTrue == child2) + { + retval = CreateSimpleAndOr(0, CreateSimpleNot(child0), child1); + } + // ITE(x, y, FALSE ) == (x AND y) + else if (ASTFalse == child2) + { + 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(ITE, children); + } + + if (debug_simplifyingNodeFactory) + { + cout << "returns " << retval << endl; + } + + return retval; } // Move reads down through writes until, either we hit a write to an identical (syntactically) index, // or we hit a write to an index that might be the same. This is intended to simplify things like: // read(write(write(A,1,2),2,3),4) cheaply. // The "children" that are passed should be the children of a READ. -ASTNode SimplifyingNodeFactory::chaseRead(const ASTVec& children, unsigned int width) +ASTNode +SimplifyingNodeFactory::chaseRead(const ASTVec& children, unsigned int width) { - assert(children[0].GetKind() == BEEV::WRITE); - const ASTNode& readIndex = children[1]; - ASTNode write = children[0]; - - const bool read_is_const = (BEEV::BVCONST == readIndex.GetKind()); - ASTVec c(2); - - while (write.GetKind() == BEEV::WRITE) - { - const ASTNode& write_index = write[1]; - - if (readIndex == write_index) - { - // The are definately the same. - //cerr << "-"; - return write[2]; - } - else if (read_is_const && BEEV::BVCONST == write_index.GetKind()) - { - // They are definately different. Ignore this. - //cerr << "+"; - }else - { - // They may be the same. Exit. - // We've finished the cheap tests, now do the expensive one. - // I don't know if the cost of this justifies the benefit. - //cerr << "#"; - c[0] =write_index; - c[1] = readIndex; - ASTNode n = CreateSimpleEQ(c); - if (n == ASTTrue) - { - //cerr << "#"; - return write[2]; - } - else if (n == ASTFalse) - { - //cerr << "!"; - } - else - { - //cerr << "." - //Perhaps they are the same, perhaps not. - break; - } - } - write = write[0]; - } - return hashing.CreateTerm(BEEV::READ, width, write,readIndex); + assert(children[0].GetKind() == BEEV::WRITE); + const ASTNode& readIndex = children[1]; + ASTNode write = children[0]; + + const bool read_is_const = (BEEV::BVCONST == readIndex.GetKind()); + ASTVec c(2); + + while (write.GetKind() == BEEV::WRITE) + { + const ASTNode& write_index = write[1]; + + if (readIndex == write_index) + { + // The are definately the same. + //cerr << "-"; + return write[2]; + } + else if (read_is_const && BEEV::BVCONST == write_index.GetKind()) + { + // They are definately different. Ignore this. + //cerr << "+"; + } + else + { + // They may be the same. Exit. + // We've finished the cheap tests, now do the expensive one. + // I don't know if the cost of this justifies the benefit. + //cerr << "#"; + c[0] = write_index; + c[1] = readIndex; + ASTNode n = CreateSimpleEQ(c); + if (n == ASTTrue) + { + //cerr << "#"; + return write[2]; + } + else if (n == ASTFalse) + { + //cerr << "!"; + } + else + { + //cerr << "." + //Perhaps they are the same, perhaps not. + break; + } + } + write = write[0]; + } + return hashing.CreateTerm(BEEV::READ, width, write, readIndex); } // This gets called with the arguments swapped as well. So the rules don't need to know about commutivity. -ASTNode SimplifyingNodeFactory::plusRules(const ASTNode& n0, const ASTNode& n1) +ASTNode +SimplifyingNodeFactory::plusRules(const ASTNode& n0, const ASTNode& n1) { ASTNode result; const int width = n0.GetValueWidth(); @@ -804,597 +806,610 @@ ASTNode SimplifyingNodeFactory::plusRules(const ASTNode& n0, const ASTNode& n1) result = bm.CreateZeroConst(1); else if (n0 == n1) result = NodeFactory::CreateTerm(BEEV::BVMULT, width, bm.CreateBVConst(string("2"), 10, width), n0); - else if (n0.GetKind() == BVUMINUS && n1 == n0[0]) + else if (n0.GetKind() == BVUMINUS && n1 == n0[0]) result = bm.CreateZeroConst(width); - else if (n1.GetKind() == BVPLUS && n1[1].GetKind() == BVUMINUS && n0 == n1[1][0] && n1.Degree() ==2 ) + else if (n1.GetKind() == BVPLUS && n1[1].GetKind() == BVUMINUS && n0 == n1[1][0] && n1.Degree() == 2) result = n1[0]; - else if (n1.GetKind() == BVPLUS && n1[0].GetKind() == BVUMINUS && n0 == n1[0][0] && n1.Degree() ==2 ) + else if (n1.GetKind() == BVPLUS && n1[0].GetKind() == BVUMINUS && n0 == n1[0][0] && n1.Degree() == 2) result = n1[1]; - else if (n1.GetKind() == BVUMINUS && n0.GetKind() == BVPLUS && n0.Degree() ==2 && n1[0] == n0[1]) + else if (n1.GetKind() == BVUMINUS && n0.GetKind() == BVPLUS && n0.Degree() == 2 && n1[0] == n0[1]) result = n0[0]; - else if (n1.GetKind() == BVUMINUS && n0.GetKind() == BVPLUS && n0.Degree() ==2 && n1[0] == n0[0]) + else if (n1.GetKind() == BVUMINUS && n0.GetKind() == BVPLUS && n0.Degree() == 2 && n1[0] == n0[0]) result = n0[1]; else if (n1.GetKind() == BVNEG && n1[0] == n0) result = bm.CreateMaxConst(width); - else if (n0.GetKind() == BEEV::BVCONST && n1.GetKind() == BVPLUS && n1.Degree() ==2 && n1[0].GetKind() == BEEV::BVCONST) + else if (n0.GetKind() == BEEV::BVCONST && n1.GetKind() == BVPLUS && n1.Degree() == 2 + && n1[0].GetKind() == BEEV::BVCONST) { ASTVec ch; ch.push_back(n0); ch.push_back(n1[0]); - ASTNode constant = NonMemberBVConstEvaluator(&bm , BVPLUS, ch, width); + ASTNode constant = NonMemberBVConstEvaluator(&bm, BVPLUS, ch, width); result = NodeFactory::CreateTerm(BVPLUS, width, constant, n1[1]); } - else if (n1.GetKind() == BVUMINUS && (n0.isConstant() && CONSTANTBV::BitVector_is_full(n0.GetBVConst()))) + else if (n1.GetKind() == BVUMINUS && (n0.isConstant() && CONSTANTBV::BitVector_is_full(n0.GetBVConst()))) { result = NodeFactory::CreateTerm(BVNEG, width, n1[0]); } - else if (n1.GetKind() == BVUMINUS && n0.GetKind() == BVUMINUS ) - { - ASTNode r = NodeFactory::CreateTerm(BVPLUS, width, n0[0],n1[0]); - result = NodeFactory::CreateTerm(BVUMINUS, width, r); - } + else if (n1.GetKind() == BVUMINUS && n0.GetKind() == BVUMINUS) + { + ASTNode r = NodeFactory::CreateTerm(BVPLUS, width, n0[0], n1[0]); + result = NodeFactory::CreateTerm(BVUMINUS, width, r); + } return result; } - -ASTNode SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, - const ASTVec &children) +ASTNode +SimplifyingNodeFactory::CreateTerm(Kind kind, unsigned int width, const ASTVec &children) { - if (!is_Term_kind(kind)) - 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++) - if (!children[i].isConstant()) - { - allConstant = false; - break; - } - - assert(bm.hashingNodeFactory == &hashing); - - if (allConstant) - { - const ASTNode& hash = hashing.CreateTerm(kind, width, children); - const ASTNode& c = NonMemberBVConstEvaluator(hash); - assert(c.isConstant()); - return c; - } - - ASTNode result; - - switch (kind) - { - - case ITE: - { - if (children[0]== ASTTrue) - result = children[1]; - else if (children[0]== ASTFalse) - result = children[2]; - else if (children[1] == children[2]) - result = children[1]; - else if (children[2].GetKind() == ITE && (children[2][0] == children[0])) - result = NodeFactory::CreateTerm(ITE, width, children[0], children[1], children[2][2]); - else if (children[1].GetKind() == ITE && (children[1][0] == children[0])) - result = NodeFactory::CreateTerm(ITE, width, children[0], children[1][1], children[2]); - else if (children[0].GetKind() == BEEV::NOT) - result = NodeFactory::CreateTerm(ITE, width, children[0][0], children[2], children[1]); - else if (children[0].GetKind() ==EQ && children[0][1] == children[1] && children[0][0].GetKind() == BEEV::BVCONST && children[0][1].GetKind() != BEEV::BVCONST) - result = NodeFactory::CreateTerm(ITE, width, children[0], children[0][0], children[2]); - else if (children[0].GetKind() == EQ && children[0][0] == children[1] && children[0][1].GetKind() == BEEV::BVCONST && children[0][0].GetKind() != BEEV::BVCONST) - result = NodeFactory::CreateTerm(ITE, width, children[0], children[0][1], children[2]); - break; - } - - case BEEV::BVMULT: - { - if (children.size() ==2) - { - if (children[0].isConstant() && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst())) - result = bm.CreateZeroConst(width); - - else if (children[1].isConstant() && CONSTANTBV::BitVector_is_empty(children[1].GetBVConst())) - result = bm.CreateZeroConst(width); - - else if (children[1].isConstant() && children[1] == bm.CreateOneConst(width)) - result = children[0]; - - else if (children[0].isConstant() && children[0] == bm.CreateOneConst(width)) - result = children[1]; - - else if (width == 1 && children[0] == children[1]) - result = children[0]; - - else if (children[0].GetKind() == BVUMINUS && children[1].GetKind() == BVUMINUS) - result = NodeFactory::CreateTerm(BEEV::BVMULT, width, children[0][0],children[1][0]); - else if (children[0].GetKind() == BVUMINUS) - { - result = NodeFactory::CreateTerm(BEEV::BVMULT, width, children[0][0], children[1]); - result = NodeFactory::CreateTerm(BVUMINUS, width, result); - } - else if (children[1].GetKind() == BVUMINUS) - { - result = NodeFactory::CreateTerm(BEEV::BVMULT, width, children[1][0], children[0]); - result = NodeFactory::CreateTerm(BVUMINUS, width, result); - } - } - else if (children.size() > 2) - { - //Never create multiplications with arity > 2. - - deque names; - - for (unsigned i = 0; i < children.size(); i++) - names.push_back(children[i]); - - while (names.size() > 1) - { - ASTNode a = names.front(); - names.pop_front(); - - ASTNode b = names.front(); - names.pop_front(); - - ASTNode n = NodeFactory::CreateTerm(BVMULT, a.GetValueWidth(), a, b); - names.push_back(n); - } - result = names.front(); - } - } - break; - - case BEEV::BVLEFTSHIFT: - { + if (!is_Term_kind(kind)) + 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++) + if (!children[i].isConstant()) + { + allConstant = false; + break; + } + + assert(bm.hashingNodeFactory == &hashing); + + if (allConstant) + { + const ASTNode& hash = hashing.CreateTerm(kind, width, children); + const ASTNode& c = NonMemberBVConstEvaluator(hash); + assert(c.isConstant()); + return c; + } + + ASTNode result; + + switch (kind) + { + + case ITE: + { + if (children[0] == ASTTrue) + result = children[1]; + else if (children[0] == ASTFalse) + result = children[2]; + else if (children[1] == children[2]) + result = children[1]; + else if (children[2].GetKind() == ITE && (children[2][0] == children[0])) + result = NodeFactory::CreateTerm(ITE, width, children[0], children[1], children[2][2]); + else if (children[1].GetKind() == ITE && (children[1][0] == children[0])) + result = NodeFactory::CreateTerm(ITE, width, children[0], children[1][1], children[2]); + else if (children[0].GetKind() == BEEV::NOT) + result = NodeFactory::CreateTerm(ITE, width, children[0][0], children[2], children[1]); + else if (children[0].GetKind() == EQ && children[0][1] == children[1] && children[0][0].GetKind() == BEEV::BVCONST + && children[0][1].GetKind() != BEEV::BVCONST) + result = NodeFactory::CreateTerm(ITE, width, children[0], children[0][0], children[2]); + else if (children[0].GetKind() == EQ && children[0][0] == children[1] && children[0][1].GetKind() == BEEV::BVCONST + && children[0][0].GetKind() != BEEV::BVCONST) + result = NodeFactory::CreateTerm(ITE, width, children[0], children[0][1], children[2]); + break; + } + + case BEEV::BVMULT: + { + if (children.size() == 2) + { if (children[0].isConstant() && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst())) result = bm.CreateZeroConst(width); - else if (children[1].isConstant()) - result = BEEV::Simplifier::convertKnownShiftAmount(kind, children, bm, &hashing); + + else if (children[1].isConstant() && CONSTANTBV::BitVector_is_empty(children[1].GetBVConst())) + result = bm.CreateZeroConst(width); + + else if (children[1].isConstant() && children[1] == bm.CreateOneConst(width)) + result = children[0]; + + else if (children[0].isConstant() && children[0] == bm.CreateOneConst(width)) + result = children[1]; + else if (width == 1 && children[0] == children[1]) - result = bm.CreateZeroConst(1); + result = children[0]; + + else if (children[0].GetKind() == BVUMINUS && children[1].GetKind() == BVUMINUS) + result = NodeFactory::CreateTerm(BEEV::BVMULT, width, children[0][0], children[1][0]); else if (children[0].GetKind() == BVUMINUS) - result = NodeFactory::CreateTerm(BVUMINUS, width, NodeFactory::CreateTerm(BEEV::BVLEFTSHIFT, width, children[0][0],children[1])); - } - break; + { + result = NodeFactory::CreateTerm(BEEV::BVMULT, width, children[0][0], children[1]); + result = NodeFactory::CreateTerm(BVUMINUS, width, result); + } + else if (children[1].GetKind() == BVUMINUS) + { + result = NodeFactory::CreateTerm(BEEV::BVMULT, width, children[1][0], children[0]); + result = NodeFactory::CreateTerm(BVUMINUS, width, result); + } + } + else if (children.size() > 2) + { + //Never create multiplications with arity > 2. + + deque names; + + for (unsigned i = 0; i < children.size(); i++) + names.push_back(children[i]); + + while (names.size() > 1) + { + ASTNode a = names.front(); + names.pop_front(); + + ASTNode b = names.front(); + names.pop_front(); + + ASTNode n = NodeFactory::CreateTerm(BVMULT, a.GetValueWidth(), a, b); + names.push_back(n); + } + result = names.front(); + } + } + break; + + case BEEV::BVLEFTSHIFT: + { + if (children[0].isConstant() && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst())) + result = bm.CreateZeroConst(width); + else if (children[1].isConstant()) + result = BEEV::Simplifier::convertKnownShiftAmount(kind, children, bm, &hashing); + else if (width == 1 && children[0] == children[1]) + result = bm.CreateZeroConst(1); + else if (children[0].GetKind() == BVUMINUS) + result = NodeFactory::CreateTerm(BVUMINUS, width, + NodeFactory::CreateTerm(BEEV::BVLEFTSHIFT, width, children[0][0], children[1])); + } + break; + + case BVRIGHTSHIFT: + { + if (children[0] == children[1]) + result = bm.CreateZeroConst(width); + if (children[0].isConstant() && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst())) + result = bm.CreateZeroConst(width); + else if (children[1].isConstant()) + result = BEEV::Simplifier::convertKnownShiftAmount(kind, children, bm, &hashing); + else if (children[0].isConstant() && children[0] == bm.CreateOneConst(width)) + result = NodeFactory::CreateTerm(ITE, width, + NodeFactory::CreateNode(EQ, children[1], bm.CreateZeroConst(width)), children[0], + bm.CreateZeroConst(width)); + } + break; + + case BEEV::BVSRSHIFT: + { + if (children[0].isConstant() && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst())) + result = bm.CreateZeroConst(width); + else if (width > 1 && children[0].isConstant() && children[0] == bm.CreateOneConst(width)) + result = NodeFactory::CreateTerm(ITE, width, + NodeFactory::CreateNode(EQ, children[1], bm.CreateZeroConst(width)), children[0], + bm.CreateZeroConst(width)); + else if (children[0].isConstant() && CONSTANTBV::BitVector_is_full(children[0].GetBVConst())) + result = bm.CreateMaxConst(width); + else if (children[1].isConstant() && CONSTANTBV::BitVector_is_empty(children[1].GetBVConst())) + result = children[0]; + else if (width == 1 && children[0] == children[1]) + result = children[0]; + else if ((children[0] == children[1]) || (children[0].GetKind() == BVUMINUS && children[0][0] == children[1])) + { + assert(width >1); + ASTNode extract = NodeFactory::CreateTerm(BVEXTRACT, 1, children[0], bm.CreateBVConst(32, width - 1), + bm.CreateBVConst(32, width - 1)); + result = NodeFactory::CreateTerm(BEEV::BVSX, width, extract, bm.CreateBVConst(32, width)); + } + else if (width == 1 && children[1].isConstant() && children[1] == bm.CreateOneConst(1)) + result = children[0]; + else if (children[1].isConstant()) + result = BEEV::Simplifier::convertArithmeticKnownShiftAmount(kind, children, bm, &hashing); + else if (children[1].GetKind() == BVUMINUS && children[0] == children[1][0]) + result = NodeFactory::CreateTerm(BEEV::BVSRSHIFT, width, children[0], children[1][0]); + else if (children[0].isConstant() && !CONSTANTBV::BitVector_bit_test(children[0].GetBVConst(), width - 1)) + result = NodeFactory::CreateTerm(BVRIGHTSHIFT, width, children[0], children[1]); + } + break; - case BVRIGHTSHIFT: + case BEEV::BVSUB: + if (children.size() == 2) + { + if (children.size() == 2 && children[0] == children[1]) + result = bm.CreateZeroConst(width); + else if (children.size() == 2 && children[1] == bm.CreateZeroConst(width)) + result = children[0]; + else + result = NodeFactory::CreateTerm(BVPLUS, width, children[0], + NodeFactory::CreateTerm(BVUMINUS, width, children[1])); + } + break; + + case BEEV::BVOR: + { + if (children.size() == 2) { if (children[0] == children[1]) - result= bm.CreateZeroConst(width); + result = children[0]; + + if (children[0].isConstant() && CONSTANTBV::BitVector_is_full(children[0].GetBVConst())) + result = bm.CreateMaxConst(width); + + if (children[1].isConstant() && CONSTANTBV::BitVector_is_full(children[1].GetBVConst())) + result = bm.CreateMaxConst(width); + + if (children[1].isConstant() && CONSTANTBV::BitVector_is_empty(children[1].GetBVConst())) + result = children[0]; + if (children[0].isConstant() && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst())) - result = bm.CreateZeroConst(width); - else if (children[1].isConstant()) - result = BEEV::Simplifier::convertKnownShiftAmount(kind, children, bm, &hashing); - else if(children[0].isConstant() && children[0] == bm.CreateOneConst(width)) - result = NodeFactory::CreateTerm(ITE,width, NodeFactory::CreateNode(EQ, children[1], bm.CreateZeroConst(width)), children[0], bm.CreateZeroConst(width)); + result = children[1]; + + if (children[1].GetKind() == BVNEG && children[0] == children[1][0]) + result = bm.CreateMaxConst(width); + if (children[0].GetKind() == BVNEG && children[1] == children[0][0]) + result = bm.CreateMaxConst(width); } - break; - - case BEEV::BVSRSHIFT: - { - if (children[0].isConstant() && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst())) - result = bm.CreateZeroConst(width); - else if (width > 1 && children[0].isConstant() && children[0] == bm.CreateOneConst(width)) - result = NodeFactory::CreateTerm(ITE,width, NodeFactory::CreateNode(EQ, children[1], bm.CreateZeroConst(width)), children[0], bm.CreateZeroConst(width)); - else if (children[0].isConstant() && CONSTANTBV::BitVector_is_full(children[0].GetBVConst())) - result = bm.CreateMaxConst(width); - else if (children[1].isConstant() && CONSTANTBV::BitVector_is_empty(children[1].GetBVConst())) - result = children[0]; - else if (width == 1 && children[0] == children[1]) - result = children[0]; - else if ((children[0] == children[1]) || (children[0].GetKind() == BVUMINUS && children[0][0] == children[1])) - { - assert(width >1); - ASTNode extract = NodeFactory::CreateTerm(BVEXTRACT,1, children[0], bm.CreateBVConst(32,width-1), bm.CreateBVConst(32,width-1)); - result = NodeFactory::CreateTerm(BEEV::BVSX, width, extract, bm.CreateBVConst(32,width)); - } - else if (width == 1 && children[1].isConstant() && children[1] == bm.CreateOneConst(1)) - result = children[0]; - else if (children[1].isConstant()) - result = BEEV::Simplifier::convertArithmeticKnownShiftAmount(kind, children, bm, &hashing); - else if (children[1].GetKind() == BVUMINUS && children[0] == children[1][0]) - result = NodeFactory::CreateTerm(BEEV::BVSRSHIFT,width, children[0], children[1][0]); - else if(children[0].isConstant() && !CONSTANTBV::BitVector_bit_test(children[0].GetBVConst(), width-1)) - result = NodeFactory::CreateTerm(BVRIGHTSHIFT,width, children[0], children[1]); - } - break; - - case BEEV::BVSUB: - if (children.size() == 2) - { - if (children.size() == 2 && children[0] == children[1]) - result = bm.CreateZeroConst(width); - else if (children.size() == 2 && children[1] == bm.CreateZeroConst(width)) - result = children[0]; - else - result = NodeFactory::CreateTerm(BVPLUS,width,children[0], NodeFactory::CreateTerm(BVUMINUS,width, children[1])); - } - break; - - case BEEV::BVOR: - { - if (children.size() ==2) - { - if (children[0] == children[1]) - result = children[0]; - - if (children[0].isConstant() && CONSTANTBV::BitVector_is_full(children[0].GetBVConst())) - result = bm.CreateMaxConst(width); - - if (children[1].isConstant() && CONSTANTBV::BitVector_is_full(children[1].GetBVConst())) - result = bm.CreateMaxConst(width); - - if (children[1].isConstant() && CONSTANTBV::BitVector_is_empty(children[1].GetBVConst())) - result = children[0]; - - if (children[0].isConstant() && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst())) - result = children[1]; - - if (children[1].GetKind() == BVNEG && children[0] == children[1][0]) - result = bm.CreateMaxConst(width); - if (children[0].GetKind() == BVNEG && children[1] == children[0][0]) - result = bm.CreateMaxConst(width); - } - } - break; - - case BEEV::BVXOR: - if (children.size() ==2) - { - if (children[0] == children[1]) - result = bm.CreateZeroConst(width); + } + break; - if (children[1].isConstant() && CONSTANTBV::BitVector_is_empty(children[1].GetBVConst())) - result = children[0]; + case BEEV::BVXOR: + if (children.size() == 2) + { + if (children[0] == children[1]) + result = bm.CreateZeroConst(width); - if (children[0].isConstant() && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst())) - result = children[1]; + if (children[1].isConstant() && CONSTANTBV::BitVector_is_empty(children[1].GetBVConst())) + result = children[0]; - if (children[1].isConstant() && CONSTANTBV::BitVector_is_full(children[1].GetBVConst())) - result = NodeFactory::CreateTerm(BVNEG, width, children[0]); + if (children[0].isConstant() && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst())) + result = children[1]; - if (children[0].isConstant() && CONSTANTBV::BitVector_is_full(children[0].GetBVConst())) - result = NodeFactory::CreateTerm(BVNEG, width, children[1]); + if (children[1].isConstant() && CONSTANTBV::BitVector_is_full(children[1].GetBVConst())) + result = NodeFactory::CreateTerm(BVNEG, width, children[0]); - if ( children[1].GetKind() == BVNEG && children[1][0] == children[0]) - result = bm.CreateMaxConst(width); - if ( children[0].GetKind() == BVNEG && children[0][0] == children[1]) - result = bm.CreateMaxConst(width); - } - break; + if (children[0].isConstant() && CONSTANTBV::BitVector_is_full(children[0].GetBVConst())) + result = NodeFactory::CreateTerm(BVNEG, width, children[1]); + if (children[1].GetKind() == BVNEG && children[1][0] == children[0]) + result = bm.CreateMaxConst(width); + if (children[0].GetKind() == BVNEG && children[0][0] == children[1]) + result = bm.CreateMaxConst(width); + } + break; - case BEEV::BVAND: - { + case BEEV::BVAND: + { - bool oneFound=false; - bool zeroFound=false; + bool oneFound = false; + bool zeroFound = false; - for (int i = 0; i < children.size(); i++) + for (int i = 0; i < children.size(); i++) + { + if (children[i].GetKind() == BEEV::BVCONST) { - if (children[i].GetKind() == BEEV::BVCONST) - { - if (CONSTANTBV::BitVector_is_full(children[i].GetBVConst())) - oneFound = true; - else if (CONSTANTBV::BitVector_is_empty(children[i].GetBVConst())) - zeroFound = true; - - } + if (CONSTANTBV::BitVector_is_full(children[i].GetBVConst())) + oneFound = true; + else if (CONSTANTBV::BitVector_is_empty(children[i].GetBVConst())) + zeroFound = true; + } + } - if (zeroFound) - { - result = bm.CreateZeroConst(width); - } - else if (oneFound) - { - ASTVec new_children; - for (int i = 0; i < children.size(); i++) - { - if (children[i].GetKind() != BEEV::BVCONST || !CONSTANTBV::BitVector_is_full(children[i].GetBVConst())) - new_children.push_back(children[i]); - } - - assert(new_children.size() != 0); // constant. Should have been handled earlier. - if (new_children.size() == 1) - { - result = new_children[0]; - } - else - result = hashing.CreateTerm(kind, width, new_children); - } - } + if (zeroFound) + { + result = bm.CreateZeroConst(width); + } + else if (oneFound) + { + ASTVec new_children; + for (int i = 0; i < children.size(); i++) + { + if (children[i].GetKind() != BEEV::BVCONST || !CONSTANTBV::BitVector_is_full(children[i].GetBVConst())) + new_children.push_back(children[i]); + } + assert(new_children.size() != 0); + // constant. Should have been handled earlier. + if (new_children.size() == 1) + { + result = new_children[0]; + } + else + result = hashing.CreateTerm(kind, width, new_children); + } + } - if (children.size() ==2 && children[0] == children[1]) + if (children.size() == 2 && children[0] == children[1]) + { + result = children[0]; + } + + // If there is just one run of 1 bits, replace by an extract and a concat. + // i.e. 00011111111000000 & x , will be replaced by an extract of x just where + // there are one bits. This should + if (children.size() == 2 && (children[0].isConstant() || children[1].isConstant())) + { + ASTNode c0 = children[0]; + ASTNode c1 = children[1]; + if (c1.isConstant()) { - result = children[0]; + ASTNode t = c0; + c0 = c1; + c1 = t; } - // If there is just one run of 1 bits, replace by an extract and a concat. - // i.e. 00011111111000000 & x , will be replaced by an extract of x just where - // there are one bits. This should - if (children.size() ==2 && (children[0].isConstant() || children[1].isConstant())) - { - ASTNode c0 = children[0]; - ASTNode c1 = children[1]; - if (c1.isConstant()) - { - ASTNode t = c0; - c0 = c1; - c1 = t; - } - - int start=-1; - int end=-1; - BEEV::CBV c = c0.GetBVConst(); - bool bad= false; - for (int i =0; i < width; i++) - { - if (CONSTANTBV::BitVector_bit_test(c,i)) - if (start == -1) - start = i; // first one bit. - else if (end != -1) - bad = true; - - if (!CONSTANTBV::BitVector_bit_test(c,i)) - if (start != -1 && end==-1) - end = i-1; // end of run. - } - if (start != -1 && end == -1) - end = width-1; - - if (!bad && start !=-1) - { - assert(end != -1); - - result = NodeFactory::CreateTerm(BVEXTRACT, end-start+1, c1, bm.CreateBVConst(32,end) , bm.CreateBVConst(32,start)); - - if (start > 0) - { - ASTNode z = bm.CreateZeroConst(start); - result = NodeFactory::CreateTerm(BVCONCAT, end+1, result,z); - } - if (end < width-1) - { - ASTNode z = bm.CreateZeroConst(width-end-1); - result = NodeFactory::CreateTerm(BVCONCAT, width, z,result); - } - } - } - - if (children.size() == 2) - { - if ( children[1].GetKind() == BVNEG && children[1][0] == children[0]) - result = bm.CreateZeroConst(width); - if ( children[0].GetKind() == BVNEG && children[0][0] == children[1]) - result = bm.CreateZeroConst(width); - } - break; - - case BEEV::BVSX: - { - if (width == children[0].GetValueWidth()) - result = children[0]; - break; - } - - case BVNEG: - if (children[0].GetKind() == BVNEG) - result = children[0][0]; - if (children[0].GetKind() == BVPLUS && children[0].Degree() == 2 && children[0][0].GetKind() == BEEV::BVCONST - && children[0][0] == bm.CreateMaxConst(width)) - result = NodeFactory::CreateTerm(BVUMINUS, width, children[0][1]); - if (children[0].GetKind() == BVUMINUS) - result = NodeFactory::CreateTerm(BVPLUS, width, children[0][0], bm.CreateMaxConst(width)); - if (children[0].GetKind() == BVMOD && children[0][0].GetKind() == BVNEG && children[0][1].GetKind() == BVUMINUS && children[0][1][0] == children[0][0][0]) - result = children[0][0][0]; - - break; - - case BVUMINUS: - if (children[0].GetKind() == BVUMINUS) - result = children[0][0]; - else if (width == 1) - result = children[0]; - else if (children[0].GetKind() == BVPLUS && children[0].Degree() == 2 && children[0][0].GetKind() == BEEV::BVCONST && children[0][0] == bm.CreateOneConst(width)) - result = NodeFactory::CreateTerm(BVNEG, width, children[0][1]); - else if (children[0].GetKind() == BVNEG) - result = NodeFactory::CreateTerm(BVPLUS, width, children[0][0], bm.CreateOneConst(width)); - else if (children[0].GetKind() == BEEV::BVSX && children[0][0].GetValueWidth() ==1) - result = NodeFactory::CreateTerm(BVCONCAT, width, bm.CreateZeroConst(width-1), children[0][0]); - else if ( children[0].GetKind() == BVMULT && children[0].Degree()==2 && children[0][0] == bm.CreateMaxConst(width)) - result = children[0][1]; - break; - - case BVEXTRACT: - if (width == children[0].GetValueWidth()) - result = children[0]; - else if (BVEXTRACT == children[0].GetKind()) // reduce an extract over an extract. - { - const unsigned outerLow = children[2].GetUnsignedConst(); - const unsigned outerHigh = children[1].GetUnsignedConst(); + int start = -1; + int end = -1; + BEEV::CBV c = c0.GetBVConst(); + bool bad = false; + for (int i = 0; i < width; i++) + { + if (CONSTANTBV::BitVector_bit_test(c, i)) + if (start == -1) + start = i; // first one bit. + else if (end != -1) + bad = true; + + if (!CONSTANTBV::BitVector_bit_test(c, i)) + if (start != -1 && end == -1) + end = i - 1; // end of run. + } + if (start != -1 && end == -1) + end = width - 1; - const unsigned innerLow = children[0][2].GetUnsignedConst(); - const unsigned innerHigh = children[0][1].GetUnsignedConst(); - result = NodeFactory::CreateTerm(BVEXTRACT, width, children[0][0], bm.CreateBVConst(32, outerHigh - + innerLow), bm.CreateBVConst(32, outerLow + innerLow)); - } - else if (BVCONCAT == children[0].GetKind()) - { - // If the extract doesn't cross the concat, then remove the concat. - const ASTNode& a = children[0][0]; - const ASTNode& b = children[0][1]; + if (!bad && start != -1) + { + assert(end != -1); - const unsigned low = children[2].GetUnsignedConst(); - const unsigned high = children[1].GetUnsignedConst(); + result = NodeFactory::CreateTerm(BVEXTRACT, end - start + 1, c1, bm.CreateBVConst(32, end), + bm.CreateBVConst(32, start)); - if (high < b.GetValueWidth()) // Extract entirely from the lower value (b). - { - result = NodeFactory::CreateTerm(BVEXTRACT, width, b, children[1], children[2]); - } - if (low >= b.GetValueWidth()) // Extract entirely from the upper value (a). - { - ASTNode i = bm.CreateBVConst(32, high - b.GetValueWidth()); - ASTNode j = bm.CreateBVConst(32, low - b.GetValueWidth()); - result = NodeFactory::CreateTerm(BVEXTRACT, width, a, i, j); - } + if (start > 0) + { + ASTNode z = bm.CreateZeroConst(start); + result = NodeFactory::CreateTerm(BVCONCAT, end + 1, result, z); + } + if (end < width - 1) + { + ASTNode z = bm.CreateZeroConst(width - end - 1); + result = NodeFactory::CreateTerm(BVCONCAT, width, z, result); } - else if (BVUMINUS == children[0].GetKind() && children[1] ==bm.CreateZeroConst(children[1].GetValueWidth()) && children[2] == bm.CreateZeroConst(children[2].GetValueWidth())) - { - result = NodeFactory::CreateTerm(BVEXTRACT, width, children[0][0],children[1],children[2]); - } - break; - - case BVPLUS: - if (children.size() == 2) - { - result = plusRules(children[0],children[1]); - if (result.IsNull()) - result = plusRules(children[1],children[0]); } - break; + } - case SBVMOD: - if (children[1].isConstant() && CONSTANTBV::BitVector_is_empty( - children[1].GetBVConst())) - result = children[0]; - else if (children[0] == children[1]) - result = bm.CreateZeroConst(width); - else if (children[1].isConstant() && children[1] == bm.CreateOneConst(width)) - result = bm.CreateZeroConst(width); - else if (children[1].isConstant() && children[1] == bm.CreateMaxConst(width)) - result = bm.CreateZeroConst(width); - else if (children[0].isConstant() && children[0] == bm.CreateZeroConst(width)) - result = bm.CreateZeroConst(width); - else if (children[0].GetKind() == BVUMINUS && children[0][0] == children[1]) - result = bm.CreateZeroConst(width); - else if (children[1].GetKind() == BVUMINUS && children[1][0] == children[0]) - result = bm.CreateZeroConst(width); - else if (translate_signed) - result = BEEV::ArrayTransformer::TranslateSignedDivModRem(hashing.CreateTerm(kind, width, children),this,&bm); - break; - - case BEEV::BVDIV: - if (children[1].isConstant() && children[1] == bm.CreateOneConst(width)) - result = children[0]; - if (children[1].isConstant() && CONSTANTBV::BitVector_bit_test(children[1].GetBVConst(),width-1)) - { - // We are dividing by something that has a one in the MSB. It's either 1 or zero. - result = NodeFactory::CreateTerm(ITE,width, NodeFactory::CreateNode(BEEV::BVGE, children[0], children[1]), bm.CreateOneConst(width), bm.CreateZeroConst(width)); - } - else if (children[1].isConstant() && children[1] == bm.CreateZeroConst(width) && bm.UserFlags.division_by_zero_returns_one_flag) - result = bm.CreateOneConst(width); - else if (bm.UserFlags.division_by_zero_returns_one_flag && children[0] == children[1]) - result = bm.CreateOneConst(width); - //else if (bm.UserFlags.division_by_zero_returns_one_flag && children[0].isConstant() && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst())) - // result = NodeFactory::CreateTerm(ITE,width, NodeFactory::CreateNode(EQ, children[1], bm.CreateZeroConst(width)), children[0], bm.CreateZeroConst(width)); - // else if (bm.UserFlags.division_by_zero_returns_one_flag && width >= 2 && children[0].GetKind() == BVNEG && children[1].GetKind() == BVUMINUS && children[1][0] == children[0][0]) - // result = NodeFactory::CreateTerm(ITE,width,NodeFactory::CreateNode(EQ,bm.CreateZeroConst(width),children[0][0]),bm.CreateOneConst(width),bm.CreateZeroConst(width)); + if (children.size() == 2) + { + if (children[1].GetKind() == BVNEG && children[1][0] == children[0]) + result = bm.CreateZeroConst(width); + if (children[0].GetKind() == BVNEG && children[0][0] == children[1]) + result = bm.CreateZeroConst(width); + } + break; + case BEEV::BVSX: + { + if (width == children[0].GetValueWidth()) + result = children[0]; + break; + } - break; + case BVNEG: + if (children[0].GetKind() == BVNEG) + result = children[0][0]; + if (children[0].GetKind() == BVPLUS && children[0].Degree() == 2 && children[0][0].GetKind() == BEEV::BVCONST + && children[0][0] == bm.CreateMaxConst(width)) + result = NodeFactory::CreateTerm(BVUMINUS, width, children[0][1]); + if (children[0].GetKind() == BVUMINUS) + result = NodeFactory::CreateTerm(BVPLUS, width, children[0][0], bm.CreateMaxConst(width)); + if (children[0].GetKind() == BVMOD && children[0][0].GetKind() == BVNEG && children[0][1].GetKind() == BVUMINUS + && children[0][1][0] == children[0][0][0]) + result = children[0][0][0]; + + break; + + case BVUMINUS: + if (children[0].GetKind() == BVUMINUS) + result = children[0][0]; + else if (width == 1) + result = children[0]; + else if (children[0].GetKind() == BVPLUS && children[0].Degree() == 2 && children[0][0].GetKind() == BEEV::BVCONST + && children[0][0] == bm.CreateOneConst(width)) + result = NodeFactory::CreateTerm(BVNEG, width, children[0][1]); + else if (children[0].GetKind() == BVNEG) + result = NodeFactory::CreateTerm(BVPLUS, width, children[0][0], bm.CreateOneConst(width)); + else if (children[0].GetKind() == BEEV::BVSX && children[0][0].GetValueWidth() == 1) + result = NodeFactory::CreateTerm(BVCONCAT, width, bm.CreateZeroConst(width - 1), children[0][0]); + else if (children[0].GetKind() == BVMULT && children[0].Degree() == 2 && children[0][0] == bm.CreateMaxConst(width)) + result = children[0][1]; + break; + + case BVEXTRACT: + if (width == children[0].GetValueWidth()) + result = children[0]; + else if (BVEXTRACT == children[0].GetKind()) // reduce an extract over an extract. + { + const unsigned outerLow = children[2].GetUnsignedConst(); + const unsigned outerHigh = children[1].GetUnsignedConst(); - case SBVDIV: - if (children[1].isConstant() && children[1] == bm.CreateOneConst(width)) - result = children[0]; - else if (children[0] == children[1] && bm.UserFlags.division_by_zero_returns_one_flag) - result = bm.CreateOneConst(width); - else if (children[1].GetKind() == BVUMINUS && children[0] == children[1][0] && bm.UserFlags.division_by_zero_returns_one_flag) - result = NodeFactory::CreateTerm(SBVDIV,width, children[1], children[0]); - else if (bm.UserFlags.division_by_zero_returns_one_flag && children[0].isConstant() && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst())) - result = NodeFactory::CreateTerm(ITE,width, NodeFactory::CreateNode(EQ, children[1], bm.CreateZeroConst(width)), bm.CreateOneConst(width), bm.CreateZeroConst(width)); - if (children[1].isConstant() && CONSTANTBV::BitVector_is_full(children[1].GetBVConst())) - result = NodeFactory::CreateTerm(BVUMINUS,width, children[1]); - else if (translate_signed) - result = BEEV::ArrayTransformer::TranslateSignedDivModRem(hashing.CreateTerm(kind, width, children),this,&bm); - break; - - - case SBVREM: - if (children[0] == children[1]) - result = bm.CreateZeroConst(width); - else if (children[0].isConstant() && CONSTANTBV::BitVector_is_empty( - children[0].GetBVConst())) - result = bm.CreateZeroConst(width); - else if (children[1].isConstant() && CONSTANTBV::BitVector_is_full( - children[1].GetBVConst())) - result = bm.CreateZeroConst(width); - else if (children[1].isConstant() && CONSTANTBV::BitVector_is_empty( - children[1].GetBVConst())) - result = children[0]; - else if (children[1].isConstant() && bm.CreateOneConst(width) == children[1]) - result = bm.CreateZeroConst(width); - else if (children[1].GetKind() == BVUMINUS) - result = NodeFactory::CreateTerm(SBVREM, width, children[0], children[1][0]); - else if (children[0].GetKind() == BVUMINUS && children[0][0] == children[1]) - result = bm.CreateZeroConst(width); - else if (translate_signed) - result = BEEV::ArrayTransformer::TranslateSignedDivModRem(hashing.CreateTerm(kind, width, children),this,&bm); - break; - - case BEEV::BVMOD: - { - if (children[0] == children[1]) - result = bm.CreateZeroConst(width); - - if (children[0].isConstant() && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst())) - result = bm.CreateZeroConst(width); - - if (children[1].isConstant() && CONSTANTBV::BitVector_is_empty(children[1].GetBVConst())) - result = children[0]; - - if (children[0].GetKind() == BVPLUS && children[0][0] == bm.CreateMaxConst(width) && children[1] == children[0][1] ) - result = children[0]; - - const ASTNode one = bm.CreateOneConst(width); - - if (children[0].GetKind() == BVNEG && children[1].GetKind() == BVUMINUS && children[1][0] == children[0][0]) - result = children[0]; - - if (children[1].isConstant() && children[1] == one) - result = bm.CreateZeroConst(width); - - if (children[0].isConstant() && children[0] == one) - result = NodeFactory::CreateTerm(ITE,width, NodeFactory::CreateNode(EQ, children[1], one), bm.CreateZeroConst(width), one); - } - - break; - - case BEEV::WRITE: - if (children[0].GetKind() == BEEV::WRITE && children[1] == children[0][1]) + const unsigned innerLow = children[0][2].GetUnsignedConst(); + const unsigned innerHigh = children[0][1].GetUnsignedConst(); + result = NodeFactory::CreateTerm(BVEXTRACT, width, children[0][0], bm.CreateBVConst(32, outerHigh + innerLow), + bm.CreateBVConst(32, outerLow + innerLow)); + } + else if (BVCONCAT == children[0].GetKind()) + { + // If the extract doesn't cross the concat, then remove the concat. + const ASTNode& a = children[0][0]; + const ASTNode& b = children[0][1]; + + const unsigned low = children[2].GetUnsignedConst(); + const unsigned high = children[1].GetUnsignedConst(); + + if (high < b.GetValueWidth()) // Extract entirely from the lower value (b). { - // If the indexes of two writes are the same, then discard the inner write. - result = NodeFactory::CreateArrayTerm(BEEV::WRITE, children[0].GetIndexWidth(), children[0].GetValueWidth(), children[0][0], children[1], children[2]); + result = NodeFactory::CreateTerm(BVEXTRACT, width, b, children[1], children[2]); } - else if (children[2].GetKind() == BEEV::READ && children[0] == children[2][0] && children[1] == children[2][1]) + if (low >= b.GetValueWidth()) // Extract entirely from the upper value (a). { - // Its writing into the array what's already there. i.e. a[i] = a[i] - result = children[0]; + ASTNode i = bm.CreateBVConst(32, high - b.GetValueWidth()); + ASTNode j = bm.CreateBVConst(32, low - b.GetValueWidth()); + result = NodeFactory::CreateTerm(BVEXTRACT, width, a, i, j); } - break; + } + else if (BVUMINUS == children[0].GetKind() && children[1] == bm.CreateZeroConst(children[1].GetValueWidth()) + && children[2] == bm.CreateZeroConst(children[2].GetValueWidth())) + { + result = NodeFactory::CreateTerm(BVEXTRACT, width, children[0][0], children[1], children[2]); + } + break; + + case BVPLUS: + if (children.size() == 2) + { + result = plusRules(children[0], children[1]); + if (result.IsNull()) + result = plusRules(children[1], children[0]); + } + break; + + case SBVMOD: + if (children[1].isConstant() && CONSTANTBV::BitVector_is_empty(children[1].GetBVConst())) + result = children[0]; + else if (children[0] == children[1]) + result = bm.CreateZeroConst(width); + else if (children[1].isConstant() && children[1] == bm.CreateOneConst(width)) + result = bm.CreateZeroConst(width); + else if (children[1].isConstant() && children[1] == bm.CreateMaxConst(width)) + result = bm.CreateZeroConst(width); + else if (children[0].isConstant() && children[0] == bm.CreateZeroConst(width)) + result = bm.CreateZeroConst(width); + else if (children[0].GetKind() == BVUMINUS && children[0][0] == children[1]) + result = bm.CreateZeroConst(width); + else if (children[1].GetKind() == BVUMINUS && children[1][0] == children[0]) + result = bm.CreateZeroConst(width); + else if (translate_signed) + result = BEEV::ArrayTransformer::TranslateSignedDivModRem(hashing.CreateTerm(kind, width, children), this, &bm); + break; + + case BEEV::BVDIV: + if (children[1].isConstant() && children[1] == bm.CreateOneConst(width)) + result = children[0]; + if (children[1].isConstant() && CONSTANTBV::BitVector_bit_test(children[1].GetBVConst(), width - 1)) + { + // We are dividing by something that has a one in the MSB. It's either 1 or zero. + result = NodeFactory::CreateTerm(ITE, width, NodeFactory::CreateNode(BEEV::BVGE, children[0], children[1]), + bm.CreateOneConst(width), bm.CreateZeroConst(width)); + } + else if (children[1].isConstant() && children[1] == bm.CreateZeroConst(width) + && bm.UserFlags.division_by_zero_returns_one_flag) + result = bm.CreateOneConst(width); + else if (bm.UserFlags.division_by_zero_returns_one_flag && children[0] == children[1]) + result = bm.CreateOneConst(width); + //else if (bm.UserFlags.division_by_zero_returns_one_flag && children[0].isConstant() && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst())) + // result = NodeFactory::CreateTerm(ITE,width, NodeFactory::CreateNode(EQ, children[1], bm.CreateZeroConst(width)), children[0], bm.CreateZeroConst(width)); + // else if (bm.UserFlags.division_by_zero_returns_one_flag && width >= 2 && children[0].GetKind() == BVNEG && children[1].GetKind() == BVUMINUS && children[1][0] == children[0][0]) + // result = NodeFactory::CreateTerm(ITE,width,NodeFactory::CreateNode(EQ,bm.CreateZeroConst(width),children[0][0]),bm.CreateOneConst(width),bm.CreateZeroConst(width)); + + break; + + case SBVDIV: + if (children[1].isConstant() && children[1] == bm.CreateOneConst(width)) + result = children[0]; + else if (children[0] == children[1] && bm.UserFlags.division_by_zero_returns_one_flag) + result = bm.CreateOneConst(width); + else if (children[1].GetKind() == BVUMINUS && children[0] == children[1][0] + && bm.UserFlags.division_by_zero_returns_one_flag) + result = NodeFactory::CreateTerm(SBVDIV, width, children[1], children[0]); + else if (bm.UserFlags.division_by_zero_returns_one_flag && children[0].isConstant() + && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst())) + result = NodeFactory::CreateTerm(ITE, width, NodeFactory::CreateNode(EQ, children[1], bm.CreateZeroConst(width)), + bm.CreateOneConst(width), bm.CreateZeroConst(width)); + if (children[1].isConstant() && CONSTANTBV::BitVector_is_full(children[1].GetBVConst())) + result = NodeFactory::CreateTerm(BVUMINUS, width, children[1]); + else if (translate_signed) + result = BEEV::ArrayTransformer::TranslateSignedDivModRem(hashing.CreateTerm(kind, width, children), this, &bm); + break; + + case SBVREM: + if (children[0] == children[1]) + result = bm.CreateZeroConst(width); + else if (children[0].isConstant() && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst())) + result = bm.CreateZeroConst(width); + else if (children[1].isConstant() && CONSTANTBV::BitVector_is_full(children[1].GetBVConst())) + result = bm.CreateZeroConst(width); + else if (children[1].isConstant() && CONSTANTBV::BitVector_is_empty(children[1].GetBVConst())) + result = children[0]; + else if (children[1].isConstant() && bm.CreateOneConst(width) == children[1]) + result = bm.CreateZeroConst(width); + else if (children[1].GetKind() == BVUMINUS) + result = NodeFactory::CreateTerm(SBVREM, width, children[0], children[1][0]); + else if (children[0].GetKind() == BVUMINUS && children[0][0] == children[1]) + result = bm.CreateZeroConst(width); + else if (translate_signed) + result = BEEV::ArrayTransformer::TranslateSignedDivModRem(hashing.CreateTerm(kind, width, children), this, &bm); + break; + + case BEEV::BVMOD: + { + if (children[0] == children[1]) + result = bm.CreateZeroConst(width); + + if (children[0].isConstant() && CONSTANTBV::BitVector_is_empty(children[0].GetBVConst())) + result = bm.CreateZeroConst(width); + + if (children[1].isConstant() && CONSTANTBV::BitVector_is_empty(children[1].GetBVConst())) + result = children[0]; + if (children[0].GetKind() == BVPLUS && children[0][0] == bm.CreateMaxConst(width) + && children[1] == children[0][1]) + result = children[0]; - case BEEV::READ: - if (children[0].GetKind() == BEEV::WRITE) - { - result = chaseRead(children,width); - } - break; + const ASTNode one = bm.CreateOneConst(width); - default: // quieten compiler. - break; - } + if (children[0].GetKind() == BVNEG && children[1].GetKind() == BVUMINUS && children[1][0] == children[0][0]) + result = children[0]; + if (children[1].isConstant() && children[1] == one) + result = bm.CreateZeroConst(width); - if (result.IsNull()) - result = hashing.CreateTerm(kind, width, children); + if (children[0].isConstant() && children[0] == one) + result = NodeFactory::CreateTerm(ITE, width, NodeFactory::CreateNode(EQ, children[1], one), + bm.CreateZeroConst(width), one); + } + + break; - return result; + case BEEV::WRITE: + if (children[0].GetKind() == BEEV::WRITE && children[1] == children[0][1]) + { + // If the indexes of two writes are the same, then discard the inner write. + result = NodeFactory::CreateArrayTerm(BEEV::WRITE, children[0].GetIndexWidth(), children[0].GetValueWidth(), + children[0][0], children[1], children[2]); + } + else if (children[2].GetKind() == BEEV::READ && children[0] == children[2][0] && children[1] == children[2][1]) + { + // Its writing into the array what's already there. i.e. a[i] = a[i] + result = children[0]; + } + break; + + case BEEV::READ: + if (children[0].GetKind() == BEEV::WRITE) + { + result = chaseRead(children, width); + } + break; + + default: // quieten compiler. + break; + } + + if (result.IsNull()) + result = hashing.CreateTerm(kind, width, children); + + return result; } -- 2.47.3