From 692f1582c956a660d303673f5ab7db0d54d58bf9 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Fri, 18 Nov 2011 11:12:27 +0000 Subject: [PATCH] Refactor. Automatically layout the code. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1422 e59a4935-1847-0410-ae03-e826735625c1 --- src/simplifier/simplifier.cpp | 3733 ++++++++++++++++----------------- 1 file changed, 1779 insertions(+), 1954 deletions(-) diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index 8d518a9..f7e97c8 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -15,37 +15,38 @@ namespace BEEV { - // If enabled, simplifyTerm will simplify all the arguments to a function before attempting - // the simplification of that function. Without this option the case will be selected for - // each kind, and that case needs to simplify the arguments. + // If enabled, simplifyTerm will simplify all the arguments to a function before attempting + // the simplification of that function. Without this option the case will be selected for + // each kind, and that case needs to simplify the arguments. - // Longer term, this means that each function doesn't need to worry about calling simplify + // Longer term, this means that each function doesn't need to worry about calling simplify // on it's arguments (I suspect some paths don't call simplify on their arguments). But it // does mean that we can't short cut, for example, if the first argument to a BVOR is all trues, // then all the other arguments have already been simplified, so won't be short-cutted. // is it ITE(p,bv0[1], bv1[1]) OR ITE(p,bv0[0], bv1[0]) - bool isPropositionToTerm(const ASTNode& n) - { - if (n.GetType() != BITVECTOR_TYPE) - return false; - if (n.GetValueWidth() != 1) - return false; - if (n.GetKind() != ITE) - return false; - if (!n[1].isConstant()) - return false; - if (!n[2].isConstant()) - return false; - if (n[1] == n[0]) - return false; - return true; + bool + isPropositionToTerm(const ASTNode& n) + { + if (n.GetType() != BITVECTOR_TYPE) + return false; + if (n.GetValueWidth() != 1) + return false; + if (n.GetKind() != ITE) + return false; + if (!n[1].isConstant()) + return false; + if (!n[2].isConstant()) + return false; + if (n[1] == n[0]) + return false; + return true; } - bool Simplifier::CheckMap(ASTNodeMap* VarConstMap, - const ASTNode& key, ASTNode& output) + bool + Simplifier::CheckMap(ASTNodeMap* VarConstMap, const ASTNode& key, ASTNode& output) { - if(NULL == VarConstMap) + if (NULL == VarConstMap) { return false; } @@ -58,12 +59,10 @@ namespace BEEV return false; } - - bool Simplifier::CheckSimplifyMap(const ASTNode& key, - ASTNode& output, - bool pushNeg, ASTNodeMap* VarConstMap) + bool + Simplifier::CheckSimplifyMap(const ASTNode& key, ASTNode& output, bool pushNeg, ASTNodeMap* VarConstMap) { - if(NULL != VarConstMap) + if (NULL != VarConstMap) { return false; } @@ -74,7 +73,6 @@ namespace BEEV return true; } - ASTNodeMap::iterator it, itend; it = pushNeg ? SimplifyNegMap->find(key) : SimplifyMap->find(key); itend = pushNeg ? SimplifyNegMap->end() : SimplifyMap->end(); @@ -88,11 +86,8 @@ namespace BEEV if (pushNeg && (it = SimplifyMap->find(key)) != SimplifyMap->end()) { - output = - (ASTFalse == it->second) ? - ASTTrue : - (ASTTrue == it->second) ? - ASTFalse : nf->CreateNode(NOT, it->second); + output = (ASTFalse == it->second) ? ASTTrue : + (ASTTrue == it->second) ? ASTFalse : nf->CreateNode(NOT, it->second); CountersAndStats("2nd_Successful_CheckSimplifyMap", _bm); return true; } @@ -100,15 +95,13 @@ namespace BEEV return false; } - void Simplifier::UpdateSimplifyMap(const ASTNode& key, - const ASTNode& value, - bool pushNeg, ASTNodeMap* VarConstMap) + void + Simplifier::UpdateSimplifyMap(const ASTNode& key, const ASTNode& value, bool pushNeg, ASTNodeMap* VarConstMap) { - if(NULL != VarConstMap) + if (NULL != VarConstMap) { return; - } - assert(!value.IsNull()); + }assert(!value.IsNull()); // Don't add leaves. Leaves are easy to recalculate, no need // to cache. @@ -128,52 +121,59 @@ namespace BEEV // Substitution Map methods.... - ASTNode Simplifier::CreateSubstitutionMap(const ASTNode& a, - ArrayTransformer* at) { - _bm->GetRunTimes()->start(RunTimes::CreateSubstitutionMap); - ASTNode result = substitutionMap.CreateSubstitutionMap(a, at); - _bm->GetRunTimes()->stop(RunTimes::CreateSubstitutionMap); - return result; - } - - bool Simplifier::UpdateSolverMap(const ASTNode& key, const ASTNode& value) + ASTNode + Simplifier::CreateSubstitutionMap(const ASTNode& a, ArrayTransformer* at) { - return substitutionMap.UpdateSolverMap(key,value); + _bm->GetRunTimes()->start(RunTimes::CreateSubstitutionMap); + ASTNode result = substitutionMap.CreateSubstitutionMap(a, at); + _bm->GetRunTimes()->stop(RunTimes::CreateSubstitutionMap); + return result; } - bool Simplifier::CheckSubstitutionMap(const ASTNode& key, ASTNode& output) + bool + Simplifier::UpdateSolverMap(const ASTNode& key, const ASTNode& value) { - return substitutionMap.CheckSubstitutionMap(key,output); + return substitutionMap.UpdateSolverMap(key, value); } - ASTNode Simplifier::applySubstitutionMap(const ASTNode& n) + bool + Simplifier::CheckSubstitutionMap(const ASTNode& key, ASTNode& output) { - return substitutionMap.applySubstitutionMap(n); + return substitutionMap.CheckSubstitutionMap(key, output); } - ASTNode Simplifier::applySubstitutionMapUntilArrays(const ASTNode& n) + ASTNode + Simplifier::applySubstitutionMap(const ASTNode& n) { - return substitutionMap.applySubstitutionMapUntilArrays(n); + return substitutionMap.applySubstitutionMap(n); } + ASTNode + Simplifier::applySubstitutionMapUntilArrays(const ASTNode& n) + { + return substitutionMap.applySubstitutionMapUntilArrays(n); + } - bool Simplifier::CheckSubstitutionMap(const ASTNode& key) + bool + Simplifier::CheckSubstitutionMap(const ASTNode& key) { - return substitutionMap.CheckSubstitutionMap(key); + return substitutionMap.CheckSubstitutionMap(key); } - bool Simplifier::UpdateSubstitutionMapFewChecks(const ASTNode& e0, const ASTNode& e1) + bool + Simplifier::UpdateSubstitutionMapFewChecks(const ASTNode& e0, const ASTNode& e1) { - return substitutionMap.UpdateSubstitutionMapFewChecks(e0,e1); + return substitutionMap.UpdateSubstitutionMapFewChecks(e0, e1); } - bool Simplifier::UpdateSubstitutionMap(const ASTNode& e0, const ASTNode& e1) + bool + Simplifier::UpdateSubstitutionMap(const ASTNode& e0, const ASTNode& e1) { - return substitutionMap.UpdateSubstitutionMap(e0,e1); + return substitutionMap.UpdateSubstitutionMap(e0, e1); } // --- Substitution Map methods.... - - bool Simplifier::CheckMultInverseMap(const ASTNode& key, ASTNode& output) + bool + Simplifier::CheckMultInverseMap(const ASTNode& key, ASTNode& output) { ASTNodeMap::iterator it; if ((it = MultInverseMap.find(key)) != MultInverseMap.end()) @@ -184,49 +184,49 @@ namespace BEEV return false; } - void Simplifier::UpdateMultInverseMap(const ASTNode& key, - const ASTNode& value) + void + Simplifier::UpdateMultInverseMap(const ASTNode& key, const ASTNode& value) { MultInverseMap[key] = value; } // Check if key, or NOT(key) is found in the alwaysTrueSet. - bool Simplifier::CheckAlwaysTrueFormSet(const ASTNode& key, bool& result) + bool + Simplifier::CheckAlwaysTrueFormSet(const ASTNode& key, bool& result) { HASHSET::const_iterator it_end_2 = AlwaysTrueHashSet.end(); HASHSET::const_iterator it2 = AlwaysTrueHashSet.find(key.GetNodeNum()); - if(it2 != it_end_2) - { - result = true; // The key should be replaced by TRUE. - return true; - } + if (it2 != it_end_2) + { + result = true; // The key should be replaced by TRUE. + return true; + } int toSearch; if (key.GetKind() == NOT) - toSearch = key.GetNodeNum()-1; + toSearch = key.GetNodeNum() - 1; else - toSearch = key.GetNodeNum()+1; + toSearch = key.GetNodeNum() + 1; it2 = AlwaysTrueHashSet.find(toSearch); - if(it2 != it_end_2) - { - result = false; - return true; - } + if (it2 != it_end_2) + { + result = false; + return true; + } return false; } - void Simplifier::UpdateAlwaysTrueFormSet(const ASTNode& key) + void + Simplifier::UpdateAlwaysTrueFormSet(const ASTNode& key) { AlwaysTrueHashSet.insert(key.GetNodeNum()); } - ASTNode - Simplifier::SimplifyFormula_NoRemoveWrites(const ASTNode& b, - bool pushNeg, - ASTNodeMap* VarConstMap) + ASTNode + Simplifier::SimplifyFormula_NoRemoveWrites(const ASTNode& b, bool pushNeg, ASTNodeMap* VarConstMap) { _bm->Begin_RemoveWrites = false; ASTNode out = SimplifyFormula(b, pushNeg, VarConstMap); @@ -234,38 +234,37 @@ namespace BEEV } // I like simplify to have been run on all the nodes. - void Simplifier::checkIfInSimplifyMap(const ASTNode& n, ASTNodeSet visited) + void + Simplifier::checkIfInSimplifyMap(const ASTNode& n, ASTNodeSet visited) { - if (n.isConstant() || (n.GetKind() == SYMBOL)) - return; + if (n.isConstant() || (n.GetKind() == SYMBOL)) + return; - if (visited.find(n) != visited.end()) - return; + if (visited.find(n) != visited.end()) + return; - if (SimplifyMap->find(n) == SimplifyMap->end()) - { - cerr << "not found"; - cerr << n; - assert(false); - } + if (SimplifyMap->find(n) == SimplifyMap->end()) + { + cerr << "not found"; + cerr << n; + assert(false); + } - for(int i =0; i < n.Degree();i++) - { - checkIfInSimplifyMap(n[i],visited); - } + for (int i = 0; i < n.Degree(); i++) + { + checkIfInSimplifyMap(n[i], visited); + } - visited.insert(n); + visited.insert(n); } - // The SimplifyMaps on entry to the topLevel functions may contain // useful entries. E.g. The BVSolver calls SimplifyTerm() - ASTNode Simplifier::SimplifyFormula_TopLevel(const ASTNode& b, - bool pushNeg, - ASTNodeMap* VarConstMap) + ASTNode + Simplifier::SimplifyFormula_TopLevel(const ASTNode& b, bool pushNeg, ASTNodeMap* VarConstMap) { - assert(_bm->UserFlags.optimize_flag); - _bm->GetRunTimes()->start(RunTimes::SimplifyTopLevel); + assert(_bm->UserFlags.optimize_flag); + _bm->GetRunTimes()->start(RunTimes::SimplifyTopLevel); ASTNode out = SimplifyFormula(b, pushNeg, VarConstMap); ASTNodeSet visited; //checkIfInSimplifyMap(out,visited); @@ -274,9 +273,10 @@ namespace BEEV return out; } - ASTNode Simplifier::SimplifyTerm_TopLevel(const ASTNode& b) + ASTNode + Simplifier::SimplifyTerm_TopLevel(const ASTNode& b) { - assert(_bm->UserFlags.optimize_flag); + assert(_bm->UserFlags.optimize_flag); _bm->GetRunTimes()->start(RunTimes::SimplifyTopLevel); ASTNode out = SimplifyTerm(b); ResetSimplifyMaps(); @@ -284,26 +284,24 @@ namespace BEEV return out; } - - ASTNode - Simplifier::SimplifyFormula(const ASTNode& b, - bool pushNeg, ASTNodeMap* VarConstMap) + ASTNode + Simplifier::SimplifyFormula(const ASTNode& b, bool pushNeg, ASTNodeMap* VarConstMap) { - assert(_bm->UserFlags.optimize_flag); - assert (BOOLEAN_TYPE == b.GetType()); + assert(_bm->UserFlags.optimize_flag); + assert(BOOLEAN_TYPE == b.GetType()); - if (b.isConstant()) - { - if (!pushNeg) - return b; - else - { - if (ASTTrue==b) - return ASTFalse; - else - return ASTTrue; - } - } + if (b.isConstant()) + { + if (!pushNeg) + return b; + else + { + if (ASTTrue == b) + return ASTFalse; + else + return ASTTrue; + } + } ASTNode output; if (CheckSimplifyMap(b, output, pushNeg, VarConstMap)) @@ -313,104 +311,99 @@ namespace BEEV ASTNode a = b; ASTVec ca = a.GetChildren(); - if (!(IMPLIES == kind || - ITE == kind || - PARAMBOOL==kind || - isAtomic(kind))) + if (!(IMPLIES == kind || ITE == kind || PARAMBOOL == kind || isAtomic(kind))) { - SortByArith(ca); - if (ca != a.GetChildren()) - a = nf->CreateNode(kind, ca); + SortByArith(ca); + if (ca != a.GetChildren()) + a = nf->CreateNode(kind, ca); } - kind = a.GetKind(); if (false) - { - if (!a.isConstant() && kind != SYMBOL) // const and symbols need to be created specially. - { - assert(a.Degree() > 0); - ASTVec v; - v.reserve(a.Degree()); - for (unsigned i = 0; i < a.Degree(); i++) - if (a[i].GetType() == BITVECTOR_TYPE) - v.push_back(SimplifyTerm(a[i], VarConstMap)); - else if (a[i].GetType() == BOOLEAN_TYPE) - v.push_back(SimplifyFormula(a[i], VarConstMap)); - else - v.push_back(a[i]); - - // TODO: Should check if the children arrays are different and only - // create then. - ASTNode output = nf->CreateNode(kind, v); - - if (a != output) { - UpdateSimplifyMap(a, output, false, VarConstMap); - a = output; - } - } - } + { + if (!a.isConstant() && kind != SYMBOL) // const and symbols need to be created specially. + { + assert(a.Degree() > 0); + ASTVec v; + v.reserve(a.Degree()); + for (unsigned i = 0; i < a.Degree(); i++) + if (a[i].GetType() == BITVECTOR_TYPE) + v.push_back(SimplifyTerm(a[i], VarConstMap)); + else if (a[i].GetType() == BOOLEAN_TYPE) + v.push_back(SimplifyFormula(a[i], VarConstMap)); + else + v.push_back(a[i]); + + // TODO: Should check if the children arrays are different and only + // create then. + ASTNode output = nf->CreateNode(kind, v); + + if (a != output) + { + UpdateSimplifyMap(a, output, false, VarConstMap); + a = output; + } + } + } a = PullUpITE(a); kind = a.GetKind(); // pullUpITE can change the Kind of the node. switch (kind) { - case AND: - case OR: - output = SimplifyAndOrFormula(a, pushNeg, VarConstMap); - break; - case NOT: - output = SimplifyNotFormula(a, pushNeg, VarConstMap); - break; - case XOR: - output = SimplifyXorFormula(a, pushNeg, VarConstMap); - break; - case NAND: - output = SimplifyNandFormula(a, pushNeg, VarConstMap); - break; - case NOR: - output = SimplifyNorFormula(a, pushNeg, VarConstMap); - break; - case IFF: - output = SimplifyIffFormula(a, pushNeg, VarConstMap); - break; - case IMPLIES: - output = SimplifyImpliesFormula(a, pushNeg, VarConstMap); - break; - case ITE: - output = SimplifyIteFormula(a, pushNeg, VarConstMap); - break; - default: - //kind can be EQ,NEQ,BVLT,BVLE,... or a propositional variable - output = SimplifyAtomicFormula(a, pushNeg, VarConstMap); - break; + case AND: + case OR: + output = SimplifyAndOrFormula(a, pushNeg, VarConstMap); + break; + case NOT: + output = SimplifyNotFormula(a, pushNeg, VarConstMap); + break; + case XOR: + output = SimplifyXorFormula(a, pushNeg, VarConstMap); + break; + case NAND: + output = SimplifyNandFormula(a, pushNeg, VarConstMap); + break; + case NOR: + output = SimplifyNorFormula(a, pushNeg, VarConstMap); + break; + case IFF: + output = SimplifyIffFormula(a, pushNeg, VarConstMap); + break; + case IMPLIES: + output = SimplifyImpliesFormula(a, pushNeg, VarConstMap); + break; + case ITE: + output = SimplifyIteFormula(a, pushNeg, VarConstMap); + break; + default: + //kind can be EQ,NEQ,BVLT,BVLE,... or a propositional variable + output = SimplifyAtomicFormula(a, pushNeg, VarConstMap); + break; } UpdateSimplifyMap(b, output, pushNeg, VarConstMap); UpdateSimplifyMap(a, output, pushNeg, VarConstMap); - ASTNode input_with_not = pushNeg? nf->CreateNode(NOT,a):a; + ASTNode input_with_not = pushNeg ? nf->CreateNode(NOT, a) : a; if (input_with_not != output) - { - return SimplifyFormula(output, false, VarConstMap); - } + { + return SimplifyFormula(output, false, VarConstMap); + } return output; } - ASTNode - Simplifier::SimplifyForFormula(const ASTNode& a, - bool pushNeg, ASTNodeMap* VarConstMap) + ASTNode + Simplifier::SimplifyForFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap) { //FIXME: Code this up properly later. Mainly pushing the negation //down return a; } - ASTNode - Simplifier::SimplifyAtomicFormula(const ASTNode& a, - bool pushNeg, ASTNodeMap* VarConstMap) + ASTNode + Simplifier::SimplifyAtomicFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap) { // if (!optimize_flag) // return a; @@ -435,216 +428,214 @@ namespace BEEV Kind kind = a.GetKind(); switch (kind) { - case TRUE: - output = pushNeg ? ASTFalse : ASTTrue; - break; - case FALSE: - output = pushNeg ? ASTTrue : ASTFalse; + case TRUE: + output = pushNeg ? ASTFalse : ASTTrue; + break; + case FALSE: + output = pushNeg ? ASTTrue : ASTFalse; + break; + case SYMBOL: + if (!CheckSubstitutionMap(a, output)) + { + output = a; + } + output = pushNeg ? nf->CreateNode(NOT, output) : output; + break; + case PARAMBOOL: + { + ASTNode term = SimplifyTerm(a[1], VarConstMap); + output = nf->CreateNode(PARAMBOOL, a[0], term); + output = pushNeg ? nf->CreateNode(NOT, output) : output; break; - case SYMBOL: - if (!CheckSubstitutionMap(a, output)) + } + case BVGETBIT: + { + ASTNode term = SimplifyTerm(a[0], VarConstMap); + ASTNode thebit = a[1]; + ASTNode zero = _bm->CreateZeroConst(1); + ASTNode one = _bm->CreateOneConst(1); + ASTNode getthebit = SimplifyTerm(nf->CreateTerm(BVEXTRACT, 1, term, thebit, thebit), VarConstMap); + if (getthebit == zero) + output = pushNeg ? ASTTrue : ASTFalse; + else if (getthebit == one) + output = pushNeg ? ASTFalse : ASTTrue; + else { - output = a; + output = nf->CreateNode(BVGETBIT, term, thebit); + output = pushNeg ? nf->CreateNode(NOT, output) : output; } - output = pushNeg ? nf->CreateNode(NOT, output) : output; break; - case PARAMBOOL: - { - ASTNode term = SimplifyTerm(a[1], VarConstMap); - output = nf->CreateNode(PARAMBOOL, a[0], term); + } + case EQ: + { + output = CreateSimplifiedEQ(left, right); + output = LhsMinusRhs(output); + output = ITEOpt_InEqs(output); + if (output == ASTTrue) + output = pushNeg ? ASTFalse : ASTTrue; + else if (output == ASTFalse) + output = pushNeg ? ASTTrue : ASTFalse; + else output = pushNeg ? nf->CreateNode(NOT, output) : output; - break; - } - case BVGETBIT: - { - ASTNode term = SimplifyTerm(a[0], VarConstMap); - ASTNode thebit = a[1]; - ASTNode zero = _bm->CreateZeroConst(1); - ASTNode one = _bm->CreateOneConst(1); - ASTNode getthebit = - SimplifyTerm(nf->CreateTerm(BVEXTRACT, 1, term, thebit, thebit), - VarConstMap); - if (getthebit == zero) - output = pushNeg ? ASTTrue : ASTFalse; - else if (getthebit == one) - output = pushNeg ? ASTFalse : ASTTrue; - else - { - output = nf->CreateNode(BVGETBIT, term, thebit); - output = pushNeg ? nf->CreateNode(NOT, output) : output; - } - break; - } - case EQ: - { - output = CreateSimplifiedEQ(left, right); - output = LhsMinusRhs(output); - output = ITEOpt_InEqs(output); - if (output == ASTTrue) - output = pushNeg ? ASTFalse : ASTTrue; - else if (output == ASTFalse) - output = pushNeg ? ASTTrue : ASTFalse; - else - output = pushNeg ? nf->CreateNode(NOT, output) : output; - break; - } - case BVLT: - case BVLE: - case BVGT: - case BVGE: - case BVSLT: - case BVSLE: - case BVSGT: - case BVSGE: - { - output = CreateSimplifiedINEQ(kind, left, right, pushNeg); - break; - } - default: - FatalError("SimplifyAtomicFormula: "\ - "NO atomic formula of the kind: ", ASTUndefined, kind); break; } + case BVLT: + case BVLE: + case BVGT: + case BVGE: + case BVSLT: + case BVSLE: + case BVSGT: + case BVSGE: + { + output = CreateSimplifiedINEQ(kind, left, right, pushNeg); + break; + } + default: + FatalError("SimplifyAtomicFormula: " + "NO atomic formula of the kind: ", ASTUndefined, kind); + break; + } //memoize UpdateSimplifyMap(a, output, pushNeg, VarConstMap); return output; } //end of SimplifyAtomicFormula() - // number of constant bits in the most significant places. - int mostSignificantConstants(const ASTNode& n) + int + mostSignificantConstants(const ASTNode& n) { - if (n.isConstant()) - return n.GetValueWidth(); - if (n.GetKind() == BVCONCAT) - return mostSignificantConstants(n[0]); - return 0; + if (n.isConstant()) + return n.GetValueWidth(); + if (n.GetKind() == BVCONCAT) + return mostSignificantConstants(n[0]); + return 0; + } + + int + getConstantBit(const ASTNode& n, const int i) + { + if (n.GetKind() == BVCONST) + { + assert(n.GetValueWidth()-1-i >=0); + return CONSTANTBV::BitVector_bit_test(n.GetBVConst(), n.GetValueWidth() - 1 - i) ? 1 : 0; + } + if (n.GetKind() == BVCONCAT) + return getConstantBit(n[0], i); + + assert(false); + } + + ASTNode + replaceIteConst(const ASTNode&n, const ASTNode& newVal, NodeFactory *nf) + { + assert(!n.IsNull()); + assert(!newVal.IsNull()); + if (n.GetKind() == BVCONST) + { + return nf->CreateNode(EQ, newVal, n); + } + else if (n.GetKind() == ITE) + { + return nf->CreateNode(ITE, n[0], replaceIteConst(n[1], newVal, nf), replaceIteConst(n[2], newVal, nf)); + } + FatalError("never here", n); + } + + bool + getPossibleValues(const ASTNode&n, ASTNodeSet& visited, vector& found, int maxCount = 45) + { + if (maxCount <= 0) + return false; + + ASTNodeSet::iterator it = visited.find(n); + if (it != visited.end()) + return true; + visited.insert(n); + + if (n.GetKind() == BVCONST) + { + found.push_back(n); + return true; + } + + if (n.GetKind() == ITE) + { + bool a = getPossibleValues(n[1], visited, found, maxCount - 1); + if (!a) + return a; + + bool b = getPossibleValues(n[2], visited, found, maxCount - 1); + if (!b) + return b; + return true; + } + + return false; + } + + int + numberOfLeadingZeroes(const ASTNode& n) + { + int c = mostSignificantConstants(n); + if (c <= 0) + return 0; + + for (int i = 0; i < c; i++) + if (getConstantBit(n, i) != 0) + return i; + return c; + } + + bool + unsignedGreaterThan(const ASTNode& n1, const ASTNode& n2) + { + assert(n1.isConstant()); + assert(n2.isConstant()); + assert(n1.GetValueWidth() == n2.GetValueWidth()); + + int comp = CONSTANTBV::BitVector_Lexicompare(n1.GetBVConst(), n2.GetBVConst()); + return comp == 1; + } + + bool + signedGreaterThan(const ASTNode& n1, const ASTNode& n2) + { + assert(n1.isConstant()); + assert(n2.isConstant()); + assert(n1.GetValueWidth() == n2.GetValueWidth()); + + int comp = CONSTANTBV::BitVector_Compare(n1.GetBVConst(), n2.GetBVConst()); + return comp == 1; } - int getConstantBit(const ASTNode& n, const int i) - { - if (n.GetKind() == BVCONST) - { - assert(n.GetValueWidth()-1-i >=0); - return CONSTANTBV::BitVector_bit_test(n.GetBVConst(), n.GetValueWidth()-1-i) ? 1:0; - } - if (n.GetKind() == BVCONCAT) - return getConstantBit(n[0],i); - - assert(false); - } - - ASTNode replaceIteConst(const ASTNode&n, const ASTNode& newVal, NodeFactory *nf) - { - assert(!n.IsNull()); - assert(!newVal.IsNull()); - if (n.GetKind() == BVCONST) - { - return nf->CreateNode(EQ, newVal, n); - } - else if (n.GetKind() == ITE) - { - return nf->CreateNode(ITE,n[0], replaceIteConst(n[1],newVal,nf), replaceIteConst(n[2],newVal,nf)); - } - FatalError("never here",n); - } - - bool getPossibleValues(const ASTNode&n, ASTNodeSet& visited, vector& found, int maxCount = 45) - { - if (maxCount <=0) - return false; - - ASTNodeSet::iterator it = visited.find(n); - if (it != visited.end()) - return true; - visited.insert(n); - - if (n.GetKind() == BVCONST) - { - found.push_back(n); - return true; - } - - if (n.GetKind() == ITE) - { - bool a = getPossibleValues(n[1],visited,found,maxCount-1); - if (!a) - return a; - - bool b = getPossibleValues(n[2],visited,found,maxCount-1); - if (!b) - return b; - return true; - } - - return false; - } - - int numberOfLeadingZeroes(const ASTNode& n) - { - int c = mostSignificantConstants( n); - if (c<=0) - return 0; - - for (int i =0; i < c;i++) - if (getConstantBit(n,i)!=0) - return i; - return c; - } - - - bool unsignedGreaterThan(const ASTNode& n1, const ASTNode& n2) - { - assert(n1.isConstant()); - assert(n2.isConstant()); - assert(n1.GetValueWidth() == n2.GetValueWidth()); - - int comp = CONSTANTBV::BitVector_Lexicompare(n1.GetBVConst(), - n2.GetBVConst()); - return comp == 1; - } - - bool signedGreaterThan(const ASTNode& n1, const ASTNode& n2) - { - assert(n1.isConstant()); - assert(n2.isConstant()); - assert(n1.GetValueWidth() == n2.GetValueWidth()); - - int comp = CONSTANTBV::BitVector_Compare(n1.GetBVConst(), - n2.GetBVConst()); - return comp == 1; - } - - - - ASTNode Simplifier::CreateSimplifiedINEQ(const Kind k_i, - const ASTNode& left_i, - const ASTNode& right_i, bool pushNeg) - { - - // We reduce down to four possible inequalities. - // NB. If the simplifying node factory is enabled, it will have done this already. - bool swap = false; - if (k_i == BVLT || k_i == BVLE || k_i == BVSLT || k_i == BVSLE) - swap = true; - - const ASTNode& left = (swap) ? right_i : left_i; - const ASTNode& right = (swap) ? left_i : right_i; - - Kind k = k_i; - if (k == BVLT) - k = BVGT; - else if (k == BVLE) - k = BVGE; - else if (k == BVSLT) - k = BVSGT; - else if (k == BVSLE) - k = BVSGE; - - assert (k == BVGT || k == BVGE || k== BVSGT || k == BVSGE); - - ASTNode output; + ASTNode + Simplifier::CreateSimplifiedINEQ(const Kind k_i, const ASTNode& left_i, const ASTNode& right_i, bool pushNeg) + { + + // We reduce down to four possible inequalities. + // NB. If the simplifying node factory is enabled, it will have done this already. + bool swap = false; + if (k_i == BVLT || k_i == BVLE || k_i == BVSLT || k_i == BVSLE) + swap = true; + + const ASTNode& left = (swap) ? right_i : left_i; + const ASTNode& right = (swap) ? left_i : right_i; + + Kind k = k_i; + if (k == BVLT) + k = BVGT; + else if (k == BVLE) + k = BVGE; + else if (k == BVSLT) + k = BVSGT; + else if (k == BVSLE) + k = BVSGE; + + assert(k == BVGT || k == BVGE || k== BVSGT || k == BVSGE); + + ASTNode output; if (BVCONST == left.GetKind() && BVCONST == right.GetKind()) { output = BVConstEvaluator(nf->CreateNode(k, left, right)); @@ -652,48 +643,52 @@ namespace BEEV return output; } - if (k == BVLT || k ==BVGT || k == BVSLT || k == BVSGT) - { - if (left == right) - return pushNeg ? ASTTrue : ASTFalse; - } + if (k == BVLT || k == BVGT || k == BVSLT || k == BVSGT) + { + if (left == right) + return pushNeg ? ASTTrue : ASTFalse; + } - if (k == BVLE || k ==BVGE || k == BVSLE || k == BVSGE) - { - if (left == right) - return pushNeg ? ASTFalse : ASTTrue; - } + if (k == BVLE || k == BVGE || k == BVSLE || k == BVSGE) + { + if (left == right) + return pushNeg ? ASTFalse : ASTTrue; + } const unsigned len = left.GetValueWidth(); - if(_bm->UserFlags.isSet("inequality-simplifications","1")) - { + if (_bm->UserFlags.isSet("inequality-simplifications", "1")) + { - const int constStart = std::min(mostSignificantConstants(left),mostSignificantConstants(right)); - int comparator =0; + const int constStart = std::min(mostSignificantConstants(left), mostSignificantConstants(right)); + int comparator = 0; - for (int i = 0; i < constStart; i++) { - const int a = getConstantBit(left, i); - const int b = getConstantBit(right, i); - assert(a==1 || a==0); - assert(b==1 || b==0); + for (int i = 0; i < constStart; i++) + { + const int a = getConstantBit(left, i); + const int b = getConstantBit(right, i); + assert(a==1 || a==0); + assert(b==1 || b==0); - if (a < b) { - comparator = -1; - break; - } else if (a > b) { - comparator = +1; - break; - } - } + if (a < b) + { + comparator = -1; + break; + } + else if (a > b) + { + comparator = +1; + break; + } + } - if (comparator!=0 && (k == BVGT || k == BVGE)) - { - ASTNode status = (comparator ==1)? ASTTrue: ASTFalse; - return pushNeg ? nf->CreateNode(NOT, status) : status; - } + if (comparator != 0 && (k == BVGT || k == BVGE)) + { + ASTNode status = (comparator == 1) ? ASTTrue : ASTFalse; + return pushNeg ? nf->CreateNode(NOT, status) : status; + } - if (comparator != 0 && (k == BVSGT || k == BVSGE)) + if (comparator != 0 && (k == BVSGT || k == BVSGE)) { // one is bigger than the other. int sign_a = getConstantBit(left, 0); @@ -746,67 +741,60 @@ namespace BEEV const ASTNode one = _bm->CreateOneConst(len); const ASTNode unsigned_max = _bm->CreateMaxConst(len); - switch (k) { - case BVGT: - if (left == unsigned_min) - { - output = pushNeg ? ASTTrue : ASTFalse; - } - else if (one == left) - { - output = CreateSimplifiedEQ(right, unsigned_min); - output = pushNeg ? nf->CreateNode(NOT, output) : output; - } - else if (right == unsigned_max) + case BVGT: + if (left == unsigned_min) { output = pushNeg ? ASTTrue : ASTFalse; } - else - { - output = - pushNeg ? - nf->CreateNode(BVLE, left, right) : - nf->CreateNode(BVLT, right, left); - } - break; - case BVGE: - if (right == unsigned_min) - { - output = pushNeg ? ASTFalse : ASTTrue; - } - else if (unsigned_max == left) - { - output = pushNeg ? ASTFalse : ASTTrue; - } - else if (unsigned_min == left) - { - output = CreateSimplifiedEQ(right, unsigned_min); - output = pushNeg ? nf->CreateNode(NOT, output) : output; - } - else - { - output = - pushNeg ? - nf->CreateNode(BVLT, left, right) : - nf->CreateNode(BVLE, right, left); - } - break; - case BVSGE: + else if (one == left) + { + output = CreateSimplifiedEQ(right, unsigned_min); + output = pushNeg ? nf->CreateNode(NOT, output) : output; + } + else if (right == unsigned_max) + { + output = pushNeg ? ASTTrue : ASTFalse; + } + else + { + output = pushNeg ? nf->CreateNode(BVLE, left, right) : nf->CreateNode(BVLT, right, left); + } + break; + case BVGE: + if (right == unsigned_min) + { + output = pushNeg ? ASTFalse : ASTTrue; + } + else if (unsigned_max == left) + { + output = pushNeg ? ASTFalse : ASTTrue; + } + else if (unsigned_min == left) + { + output = CreateSimplifiedEQ(right, unsigned_min); + output = pushNeg ? nf->CreateNode(NOT, output) : output; + } + else + { + output = pushNeg ? nf->CreateNode(BVLT, left, right) : nf->CreateNode(BVLE, right, left); + } + break; + case BVSGE: { output = nf->CreateNode(k, left, right); output = pushNeg ? nf->CreateNode(NOT, output) : output; } - break; - case BVSGT: - output = nf->CreateNode(k, left, right); - output = pushNeg ? nf->CreateNode(NOT, output) : output; - break; - default: - FatalError("Wrong Kind"); - break; + break; + case BVSGT: + output = nf->CreateNode(k, left, right); + output = pushNeg ? nf->CreateNode(NOT, output) : output; + break; + default: + FatalError("Wrong Kind"); + break; } assert(!output.IsNull()); @@ -816,7 +804,8 @@ namespace BEEV // turns say (bvslt (ite a b c) (ite a d e)) INTO (ite a (bvslt b d) // (bvslt c e)) Expensive. But makes some other simplifications // possible. - ASTNode Simplifier::PullUpITE(const ASTNode& in) + ASTNode + Simplifier::PullUpITE(const ASTNode& in) { if (2 != in.GetChildren().size()) return in; @@ -843,15 +832,9 @@ namespace BEEV } else { - l1 = - nf->CreateTerm(in.GetKind(), - in.GetValueWidth(), in[0][1], in[1][1]); - l2 = - nf->CreateTerm(in.GetKind(), - in.GetValueWidth(), in[0][2], in[1][2]); - result = - nf->CreateTerm(ITE, - in.GetValueWidth(), in[0][0], l1, l2); + l1 = nf->CreateTerm(in.GetKind(), in.GetValueWidth(), in[0][1], in[1][1]); + l2 = nf->CreateTerm(in.GetKind(), in.GetValueWidth(), in[0][2], in[1][2]); + result = nf->CreateTerm(ITE, in.GetValueWidth(), in[0][0], l1, l2); } assert(result.GetType() == in.GetType()); @@ -863,7 +846,8 @@ namespace BEEV } //takes care of some simple ITE Optimizations in the context of equations - ASTNode Simplifier::ITEOpt_InEqs(const ASTNode& in, ASTNodeMap* VarConstMap) + ASTNode + Simplifier::ITEOpt_InEqs(const ASTNode& in, ASTNodeMap* VarConstMap) { CountersAndStats("ITEOpts_InEqs", _bm); @@ -892,9 +876,7 @@ namespace BEEV assert(in1!=in2); output = ASTFalse; } - else if (ITE == k1 && - BVCONST == in1[1].GetKind() && - BVCONST == in1[2].GetKind() && BVCONST == k2) + else if (ITE == k1 && BVCONST == in1[1].GetKind() && BVCONST == in1[2].GetKind() && BVCONST == k2) { //if one side is a BVCONST and the other side is an ITE over //BVCONST then we can do the following optimization: @@ -923,9 +905,7 @@ namespace BEEV output = nf->CreateNode(EQ, in1, in2); } } - else if (ITE == k2 && - BVCONST == in2[1].GetKind() && - BVCONST == in2[2].GetKind() && BVCONST == k1) + else if (ITE == k2 && BVCONST == in2[1].GetKind() && BVCONST == in2[2].GetKind() && BVCONST == k1) { ASTNode cond = in2[0]; if (in2[1] == in1 && (in1 != in2[2])) @@ -956,9 +936,10 @@ namespace BEEV //Tries to simplify the input to TRUE/FALSE. if it fails, then //return the constructed equality - ASTNode Simplifier::CreateSimplifiedEQ(const ASTNode& in1, const ASTNode& in2) + ASTNode + Simplifier::CreateSimplifiedEQ(const ASTNode& in1, const ASTNode& in2) { - CountersAndStats("CreateSimplifiedEQ", _bm); + CountersAndStats("CreateSimplifiedEQ", _bm); const Kind k1 = in1.GetKind(); const Kind k2 = in2.GetKind(); @@ -971,19 +952,20 @@ namespace BEEV if (BVCONST == k1 && BVCONST == k2) return ASTFalse; - // Check if some of the leading constant bits are different. Fancier code would check + // Check if some of the leading constant bits are different. Fancier code would check // each bit, not just the leading bits. - const int constStart = std::min(mostSignificantConstants(in1),mostSignificantConstants(in2)); + const int constStart = std::min(mostSignificantConstants(in1), mostSignificantConstants(in2)); - for (int i = 0; i < constStart; i++) { - const int a = getConstantBit(in1, i); - const int b = getConstantBit(in2, i); - assert(a==1 || a==0); - assert(b==1 || b==0); + for (int i = 0; i < constStart; i++) + { + const int a = getConstantBit(in1, i); + const int b = getConstantBit(in2, i); + assert(a==1 || a==0); + assert(b==1 || b==0); - if (a != b) - return ASTFalse; - } + if (a != b) + return ASTFalse; + } // The above loop has determined that the leading bits are the same. if (constStart > 0) @@ -991,9 +973,9 @@ namespace BEEV int newWidth = in1.GetValueWidth() - constStart; ASTNode zero = _bm->CreateZeroConst(32); - ASTNode lhs = nf->CreateTerm(BVEXTRACT,newWidth, in1,_bm->CreateBVConst(32,newWidth-1) ,zero); - ASTNode rhs = nf->CreateTerm(BVEXTRACT,newWidth, in2,_bm->CreateBVConst(32,newWidth-1) ,zero); - ASTNode r= nf->CreateNode(EQ, lhs,rhs); + ASTNode lhs = nf->CreateTerm(BVEXTRACT, newWidth, in1, _bm->CreateBVConst(32, newWidth - 1), zero); + ASTNode rhs = nf->CreateTerm(BVEXTRACT, newWidth, in2, _bm->CreateBVConst(32, newWidth - 1), zero); + ASTNode r = nf->CreateNode(EQ, lhs, rhs); assert(BVTypeCheck(r)); return r; } @@ -1002,37 +984,38 @@ namespace BEEV // nb. This doesn't cover the case when the children are organised differently: // (concat (concat A B) C) == (concat A (concat B C)) if (k1 == BVCONCAT && k2 == BVCONCAT && in1[0].GetValueWidth() == in2[0].GetValueWidth()) - { - return nf->CreateNode(AND, nf->CreateNode(EQ, in1[0], in2[0]), nf->CreateNode(EQ, in1[1], in2[1])); - } + { + return nf->CreateNode(AND, nf->CreateNode(EQ, in1[0], in2[0]), nf->CreateNode(EQ, in1[1], in2[1])); + } // If the rhs is a concat, and the lhs is a constant. Split. - if (k1== BVCONST && k2 == BVCONCAT) - { + if (k1 == BVCONST && k2 == BVCONCAT) + { int width = in1.GetValueWidth(); int bottomW = in2[1].GetValueWidth(); ASTNode zero = _bm->CreateZeroConst(32); // split the constant. - ASTNode top = nf->CreateTerm(BVEXTRACT,width-bottomW, in1,_bm->CreateBVConst(32,width-1) ,_bm->CreateBVConst(32,bottomW)); - ASTNode bottom = nf->CreateTerm(BVEXTRACT,bottomW, in1,_bm->CreateBVConst(32,bottomW-1) ,zero); + ASTNode top = nf->CreateTerm(BVEXTRACT, width - bottomW, in1, _bm->CreateBVConst(32, width - 1), + _bm->CreateBVConst(32, bottomW)); + ASTNode bottom = nf->CreateTerm(BVEXTRACT, bottomW, in1, _bm->CreateBVConst(32, bottomW - 1), zero); assert(BVTypeCheck(top)); assert(BVTypeCheck(bottom)); - ASTNode r = nf->CreateNode(AND, nf->CreateNode(EQ, top, in2[0]), nf->CreateNode(EQ, bottom, in2[1])); + ASTNode r = nf->CreateNode(AND, nf->CreateNode(EQ, top, in2[0]), nf->CreateNode(EQ, bottom, in2[1])); return r; - } + } - if ((k1 == ITE || k1 == BVCONST) && (k2 == ITE || k2 == BVCONST)) - { - // If it can only evaluate to constants on the LHS and the RHS, and those constants are never equal, - // then it must be false. e.g. ite( f, 10 , 20 ) = ite (g, 30 ,12) - ASTNodeSet visited0, visited1; - vector l0, l1; + if ((k1 == ITE || k1 == BVCONST) && (k2 == ITE || k2 == BVCONST)) + { + // If it can only evaluate to constants on the LHS and the RHS, and those constants are never equal, + // then it must be false. e.g. ite( f, 10 , 20 ) = ite (g, 30 ,12) + ASTNodeSet visited0, visited1; + vector l0, l1; - if (getPossibleValues(in1, visited0, l0) && getPossibleValues(in2, visited1, l1)) - { + if (getPossibleValues(in1, visited0, l0) && getPossibleValues(in2, visited1, l1)) + { sort(l0.begin(), l0.end()); sort(l1.begin(), l1.end()); vector result(l0.size() + l1.size()); @@ -1040,18 +1023,17 @@ namespace BEEV if (it == result.begin()) return ASTFalse; - if (it == result.begin() +1 ) - { - // If there is just one value in common, then, set it to true whenever it equals that value. - ASTNode lhs= replaceIteConst(in1, *result.begin(),nf); - ASTNode rhs= replaceIteConst(in2, *result.begin(),nf); - - ASTNode result = nf->CreateNode(AND, lhs,rhs); - return result; - } - } - } + if (it == result.begin() + 1) + { + // If there is just one value in common, then, set it to true whenever it equals that value. + ASTNode lhs = replaceIteConst(in1, *result.begin(), nf); + ASTNode rhs = replaceIteConst(in2, *result.begin(), nf); + ASTNode result = nf->CreateNode(AND, lhs, rhs); + return result; + } + } + } //last resort is to CreateNode return nf->CreateNode(EQ, in1, in2); @@ -1059,9 +1041,8 @@ namespace BEEV // nb. this is sometimes used to build array terms. //accepts cond == t1, then part is t2, and else part is t3 - ASTNode Simplifier::CreateSimplifiedTermITE(const ASTNode& in0, - const ASTNode& in1, - const ASTNode& in2) + ASTNode + Simplifier::CreateSimplifiedTermITE(const ASTNode& in0, const ASTNode& in1, const ASTNode& in2) { const ASTNode& t0 = in0; const ASTNode& t1 = in1; @@ -1072,16 +1053,16 @@ namespace BEEV if (t1.GetValueWidth() != t2.GetValueWidth()) { cerr << "t2 is : = " << t2; - FatalError("CreateSimplifiedTermITE: "\ - "the lengths of the two branches don't match", t1); + FatalError("CreateSimplifiedTermITE: " + "the lengths of the two branches don't match", t1); } if (t1.GetIndexWidth() != t2.GetIndexWidth()) { cerr << "t2 is : = " << t2; - FatalError("CreateSimplifiedTermITE: "\ - "the lengths of the two branches don't match", t1); + FatalError("CreateSimplifiedTermITE: " + "the lengths of the two branches don't match", t1); } - return nf->CreateArrayTerm(ITE, t1.GetIndexWidth(),t1.GetValueWidth(), t0, t1, t2); + return nf->CreateArrayTerm(ITE, t1.GetIndexWidth(), t1.GetValueWidth(), t0, t1, t2); } if (t0 == ASTTrue) @@ -1092,7 +1073,7 @@ namespace BEEV return t1; bool result; - if (CheckAlwaysTrueFormSet(t0,result)) + if (CheckAlwaysTrueFormSet(t0, result)) { if (result) return t1; @@ -1100,13 +1081,11 @@ namespace BEEV return t2; } - return nf->CreateArrayTerm(ITE, t1.GetIndexWidth(),t1.GetValueWidth(), t0, t1, t2); + return nf->CreateArrayTerm(ITE, t1.GetIndexWidth(), t1.GetValueWidth(), t0, t1, t2); } - ASTNode - Simplifier:: - CreateSimplifiedFormulaITE(const ASTNode& in0, - const ASTNode& in1, const ASTNode& in2) + ASTNode + Simplifier::CreateSimplifiedFormulaITE(const ASTNode& in0, const ASTNode& in1, const ASTNode& in2) { const ASTNode& t0 = in0; const ASTNode& t1 = in1; @@ -1123,7 +1102,7 @@ namespace BEEV return t1; bool result; - if (CheckAlwaysTrueFormSet(t0,result)) + if (CheckAlwaysTrueFormSet(t0, result)) { if (result) return t1; @@ -1137,9 +1116,8 @@ namespace BEEV return result; } - ASTNode Simplifier::SimplifyAndOrFormula(const ASTNode& a, - bool pushNeg, - ASTNodeMap* VarConstMap) + ASTNode + Simplifier::SimplifyAndOrFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap) { ASTNode output; //cerr << "input:\n" << a << endl; @@ -1148,20 +1126,14 @@ namespace BEEV return output; const Kind k = a.GetKind(); - ASTVec c = FlattenKind(k,a.GetChildren()); + ASTVec c = FlattenKind(k, a.GetChildren()); SortByArith(c); const bool isAnd = (k == AND) ? true : false; - const ASTNode annihilator = - isAnd ? - (pushNeg ? ASTTrue : ASTFalse) : - (pushNeg ? ASTFalse : ASTTrue); + const ASTNode annihilator = isAnd ? (pushNeg ? ASTTrue : ASTFalse) : (pushNeg ? ASTFalse : ASTTrue); - const ASTNode identity = - isAnd ? - (pushNeg ? ASTFalse : ASTTrue) : - (pushNeg ? ASTTrue : ASTFalse); + const ASTNode identity = isAnd ? (pushNeg ? ASTFalse : ASTTrue) : (pushNeg ? ASTTrue : ASTFalse); ASTVec outvec; outvec.reserve(c.size()); @@ -1210,29 +1182,24 @@ namespace BEEV switch (outvec.size()) { - case 0: - { - //only identities were dropped - output = identity; - break; - } - case 1: - { - output = outvec[0]; - break; - } - default: - { - output = - (isAnd) ? - (pushNeg ? - nf->CreateNode(OR, outvec) : - nf->CreateNode(AND, outvec)) : - (pushNeg ? - nf->CreateNode(AND, outvec) : - nf->CreateNode(OR,outvec)); - break; - } + case 0: + { + //only identities were dropped + output = identity; + break; + } + case 1: + { + output = outvec[0]; + break; + } + default: + { + output = + (isAnd) ? (pushNeg ? nf->CreateNode(OR, outvec) : nf->CreateNode(AND, outvec)) : + (pushNeg ? nf->CreateNode(AND, outvec) : nf->CreateNode(OR, outvec)); + break; + } } //memoize @@ -1241,18 +1208,15 @@ namespace BEEV return output; } //end of SimplifyAndOrFormula - - ASTNode - Simplifier::SimplifyNotFormula(const ASTNode& a, - bool pushNeg, ASTNodeMap* VarConstMap) + ASTNode + Simplifier::SimplifyNotFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap) { ASTNode output; if (CheckSimplifyMap(a, output, pushNeg, VarConstMap)) return output; if (!(a.Degree() == 1 && NOT == a.GetKind())) - FatalError("SimplifyNotFormula: input vector with more than 1 node", - ASTUndefined); + FatalError("SimplifyNotFormula: input vector with more than 1 node", ASTUndefined); //if pushNeg is set then there is NOT on top unsigned int NotCount = pushNeg ? 1 : 0; @@ -1268,10 +1232,10 @@ namespace BEEV bool pn = (NotCount % 2 == 0) ? false : true; bool alwaysTrue; - if (CheckAlwaysTrueFormSet(o,alwaysTrue)) + if (CheckAlwaysTrueFormSet(o, alwaysTrue)) { if (alwaysTrue) - return ( pn ? ASTFalse : ASTTrue); + return (pn ? ASTFalse : ASTTrue); // We don't do the false case because it is sometimes // called at the top level. @@ -1300,9 +1264,8 @@ namespace BEEV return output; } - ASTNode Simplifier::SimplifyXorFormula(const ASTNode& a, - bool pushNeg, - ASTNodeMap* VarConstMap) + ASTNode + Simplifier::SimplifyXorFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap) { ASTNode output; if (CheckSimplifyMap(a, output, pushNeg, VarConstMap)) @@ -1310,11 +1273,11 @@ namespace BEEV assert(a.GetChildren().size() > 0); - if (a.GetChildren().size()==1) + if (a.GetChildren().size() == 1) { output = a[0]; } - else if (a.GetChildren().size()==2) + else if (a.GetChildren().size() == 2) { ASTNode a0 = SimplifyFormula(a[0], false, VarConstMap); ASTNode a1 = SimplifyFormula(a[1], false, VarConstMap); @@ -1329,15 +1292,15 @@ namespace BEEV } else { - ASTVec newC; - for (int i = 0;i < a.GetChildren().size(); i++) - { - newC.push_back(SimplifyFormula(a[i], false, VarConstMap)); - } - if (pushNeg) - newC[0] = nf->CreateNode(NOT,newC[0]); + ASTVec newC; + for (int i = 0; i < a.GetChildren().size(); i++) + { + newC.push_back(SimplifyFormula(a[i], false, VarConstMap)); + } + if (pushNeg) + newC[0] = nf->CreateNode(NOT, newC[0]); - output = nf->CreateNode(XOR, newC); + output = nf->CreateNode(XOR, newC); } //memoize @@ -1345,9 +1308,8 @@ namespace BEEV return output; } - ASTNode Simplifier::SimplifyNandFormula(const ASTNode& a, - bool pushNeg, - ASTNodeMap* VarConstMap) + ASTNode + Simplifier::SimplifyNandFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap) { ASTNode output, a0, a1; if (CheckSimplifyMap(a, output, pushNeg, VarConstMap)) @@ -1373,9 +1335,8 @@ namespace BEEV return output; } - ASTNode Simplifier::SimplifyNorFormula(const ASTNode& a, - bool pushNeg, - ASTNodeMap* VarConstMap) + ASTNode + Simplifier::SimplifyNorFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap) { ASTNode output, a0, a1; if (CheckSimplifyMap(a, output, pushNeg, VarConstMap)) @@ -1401,17 +1362,15 @@ namespace BEEV return output; } - ASTNode Simplifier::SimplifyImpliesFormula(const ASTNode& a, - bool pushNeg, - ASTNodeMap* VarConstMap) + ASTNode + Simplifier::SimplifyImpliesFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap) { ASTNode output; if (CheckSimplifyMap(a, output, pushNeg, VarConstMap)) return output; if (!(a.Degree() == 2 && IMPLIES == a.GetKind())) - FatalError("SimplifyImpliesFormula: vector with wrong num of nodes", - ASTUndefined); + FatalError("SimplifyImpliesFormula: vector with wrong num of nodes", ASTUndefined); ASTNode c0, c1; if (pushNeg) @@ -1475,17 +1434,15 @@ namespace BEEV return output; } - ASTNode Simplifier::SimplifyIffFormula(const ASTNode& a, - bool pushNeg, - ASTNodeMap* VarConstMap) + ASTNode + Simplifier::SimplifyIffFormula(const ASTNode& a, bool pushNeg, ASTNodeMap* VarConstMap) { ASTNode output; if (CheckSimplifyMap(a, output, pushNeg, VarConstMap)) return output; if (!(a.Degree() == 2 && IFF == a.GetKind())) - FatalError("SimplifyIffFormula: vector with wrong num of nodes", - ASTUndefined); + FatalError("SimplifyIffFormula: vector with wrong num of nodes", ASTUndefined); ASTNode c0 = a[0]; ASTNode c1 = SimplifyFormula(a[1], false, VarConstMap); @@ -1517,21 +1474,18 @@ namespace BEEV { output = ASTTrue; } - else if ((NOT == c0.GetKind() - && c0[0] == c1) - || (NOT == c1.GetKind() - && c0 == c1[0])) + else if ((NOT == c0.GetKind() && c0[0] == c1) || (NOT == c1.GetKind() && c0 == c1[0])) { output = ASTFalse; } - else if (CheckAlwaysTrueFormSet(c0,alwaysResult)) + else if (CheckAlwaysTrueFormSet(c0, alwaysResult)) { if (alwaysResult) output = c1; else output = nf->CreateNode(NOT, c1); } - else if (CheckAlwaysTrueFormSet(c1,alwaysResult)) + else if (CheckAlwaysTrueFormSet(c1, alwaysResult)) { if (alwaysResult) output = c0; @@ -1540,7 +1494,7 @@ namespace BEEV } else { - output = nf->CreateNode(XOR, nf->CreateNode(NOT,c0), c1); + output = nf->CreateNode(XOR, nf->CreateNode(NOT, c0), c1); } //memoize @@ -1548,9 +1502,8 @@ namespace BEEV return output; } - ASTNode Simplifier::SimplifyIteFormula(const ASTNode& b, - bool pushNeg, - ASTNodeMap* VarConstMap) + ASTNode + Simplifier::SimplifyIteFormula(const ASTNode& b, bool pushNeg, ASTNodeMap* VarConstMap) { // if (!optimize_flag) // return b; @@ -1560,8 +1513,7 @@ namespace BEEV return output; if (!(b.Degree() == 3 && ITE == b.GetKind())) - FatalError("SimplifyIteFormula: vector with wrong num of nodes", - ASTUndefined); + FatalError("SimplifyIteFormula: vector with wrong num of nodes", ASTUndefined); ASTNode a = b; ASTNode t0 = SimplifyFormula(a[0], false, VarConstMap); @@ -1615,7 +1567,7 @@ namespace BEEV { output = nf->CreateNode(AND, t0, t1); } - else if (CheckAlwaysTrueFormSet(t0,alwaysTrue)) + else if (CheckAlwaysTrueFormSet(t0, alwaysTrue)) { if (alwaysTrue) output = t1; @@ -1632,7 +1584,6 @@ namespace BEEV return output; } - ASTNode Simplifier::makeTower(const Kind k, const BEEV::ASTVec &children) { @@ -1682,7 +1633,7 @@ namespace BEEV return false; if (n.GetKind() == SYMBOL) - return true; + return true; ASTNodeMap::const_iterator it; //If it's in the simplification map, it has been simplified. @@ -1692,8 +1643,9 @@ namespace BEEV return (it->second == n); } - // If both of the children are sign extended. Makes this node sign extended too. - ASTNode Simplifier::pullUpBVSX(ASTNode output) + // If both of the children are sign extended. Makes this node sign extended too. + ASTNode + Simplifier::pullUpBVSX(ASTNode output) { assert(output.GetChildren().size() ==2); assert(output[0].GetKind() == BVSX); @@ -1709,27 +1661,30 @@ namespace BEEV if (BVMULT == output.GetKind()) maxLength = lengthA + lengthB; else if (BVPLUS == output.GetKind() || SBVDIV == output.GetKind()) - maxLength = std::max(lengthA,lengthB)+1; + maxLength = std::max(lengthA, lengthB) + 1; else FatalError("Unexpected."); if (maxLength < output.GetValueWidth()) { - ASTNode newA = nf->CreateTerm(BVEXTRACT, maxLength, output.GetChildren()[0], _bm->CreateBVConst(32,maxLength-1), _bm->CreateZeroConst(32)); + ASTNode newA = nf->CreateTerm(BVEXTRACT, maxLength, output.GetChildren()[0], + _bm->CreateBVConst(32, maxLength - 1), _bm->CreateZeroConst(32)); newA = SimplifyTerm(newA); - ASTNode newB = nf->CreateTerm(BVEXTRACT, maxLength, output.GetChildren()[1], _bm->CreateBVConst(32,maxLength-1), _bm->CreateZeroConst(32)); + ASTNode newB = nf->CreateTerm(BVEXTRACT, maxLength, output.GetChildren()[1], + _bm->CreateBVConst(32, maxLength - 1), _bm->CreateZeroConst(32)); newB = SimplifyTerm(newB); - ASTNode mult = nf->CreateTerm(output.GetKind(), maxLength, newA,newB); - output = nf->CreateTerm(BVSX, inputValueWidth, mult, _bm->CreateBVConst(32,inputValueWidth)); + ASTNode mult = nf->CreateTerm(output.GetKind(), maxLength, newA, newB); + output = nf->CreateTerm(BVSX, inputValueWidth, mult, _bm->CreateBVConst(32, inputValueWidth)); } return output; } // If the shift is bigger than the bitwidth, replace by an extract. - ASTNode Simplifier::convertArithmeticKnownShiftAmount(const Kind k, const ASTVec& children, STPMgr& bm, NodeFactory *nf) + ASTNode + Simplifier::convertArithmeticKnownShiftAmount(const Kind k, const ASTVec& children, STPMgr& bm, NodeFactory *nf) { - const ASTNode a =children[0]; - const ASTNode b =children[1]; + const ASTNode a = children[0]; + const ASTNode b = children[1]; const int width = children[0].GetValueWidth(); ASTNode output; @@ -1738,97 +1693,93 @@ namespace BEEV if (CONSTANTBV::Set_Max(b.GetBVConst()) > 1 + log2(width)) { - ASTNode top = bm.CreateBVConst(32,width-1); - return nf->CreateTerm(BVSX, width, nf->CreateTerm(BVEXTRACT,1, children[0], top,top ), bm.CreateBVConst(32,width)); + ASTNode top = bm.CreateBVConst(32, width - 1); + return nf->CreateTerm(BVSX, width, nf->CreateTerm(BVEXTRACT, 1, children[0], top, top), + bm.CreateBVConst(32, width)); } else - { - if (b.GetUnsignedConst() >= width) + { + if (b.GetUnsignedConst() >= width) { - ASTNode top = bm.CreateBVConst(32,width-1); - return nf->CreateTerm(BVSX, width, nf->CreateTerm(BVEXTRACT,1, children[0], top,top ), bm.CreateBVConst(32,width)); + ASTNode top = bm.CreateBVConst(32, width - 1); + return nf->CreateTerm(BVSX, width, nf->CreateTerm(BVEXTRACT, 1, children[0], top, top), + bm.CreateBVConst(32, width)); } - } + } return ASTNode(); } - // If the rhs of a left or right shift is known. - ASTNode Simplifier::convertKnownShiftAmount(const Kind k, const ASTVec& children, STPMgr& bm, NodeFactory *nf) + ASTNode + Simplifier::convertKnownShiftAmount(const Kind k, const ASTVec& children, STPMgr& bm, NodeFactory *nf) { - const ASTNode a =children[0]; - const ASTNode b =children[1]; + const ASTNode a = children[0]; + const ASTNode b = children[1]; const int width = children[0].GetValueWidth(); ASTNode output; assert(b.isConstant()); assert(k == BVLEFTSHIFT || BVRIGHTSHIFT ==k); - if (CONSTANTBV::Set_Max(b.GetBVConst()) > 1 + log2(width)) - { - // Intended to remove shifts by very large amounts - // that don't fit into the unsigned. at thhe start - // of the "else" branch. - output = bm.CreateZeroConst(width); - } - else - { - const unsigned int shift = b.GetUnsignedConst(); - if (shift >= width) - { - output = bm.CreateZeroConst(width); - } - else if (shift == 0) - { - output = a; // unchanged. - } - else - { - if (k == BVLEFTSHIFT) - { - CBV cbv = CONSTANTBV::BitVector_Create(width,true); - CONSTANTBV::BitVector_Bit_On(cbv,shift); - ASTNode c = bm.CreateBVConst(cbv,width); - - output = - nf->CreateTerm(BVMULT, width, - a, c); - BVTypeCheck(output); - //cout << output; - //cout << a << b << endl; - } - else if (k == BVRIGHTSHIFT) - { - ASTNode zero = bm.CreateZeroConst(shift); - ASTNode hi = bm.CreateBVConst(32, width -1); - ASTNode low = bm.CreateBVConst(32, shift); - ASTNode extract = - nf->CreateTerm(BVEXTRACT, width - shift, - a, hi, low); - BVTypeCheck(extract); - output = - nf->CreateTerm(BVCONCAT, width, zero, extract); - BVTypeCheck(output); - } - else - FatalError("herasdf"); - } - } - return output; -} + if (CONSTANTBV::Set_Max(b.GetBVConst()) > 1 + log2(width)) + { + // Intended to remove shifts by very large amounts + // that don't fit into the unsigned. at thhe start + // of the "else" branch. + output = bm.CreateZeroConst(width); + } + else + { + const unsigned int shift = b.GetUnsignedConst(); + if (shift >= width) + { + output = bm.CreateZeroConst(width); + } + else if (shift == 0) + { + output = a; // unchanged. + } + else + { + if (k == BVLEFTSHIFT) + { + CBV cbv = CONSTANTBV::BitVector_Create(width, true); + CONSTANTBV::BitVector_Bit_On(cbv, shift); + ASTNode c = bm.CreateBVConst(cbv, width); + + output = nf->CreateTerm(BVMULT, width, a, c); + BVTypeCheck(output); + //cout << output; + //cout << a << b << endl; + } + else if (k == BVRIGHTSHIFT) + { + ASTNode zero = bm.CreateZeroConst(shift); + ASTNode hi = bm.CreateBVConst(32, width - 1); + ASTNode low = bm.CreateBVConst(32, shift); + ASTNode extract = nf->CreateTerm(BVEXTRACT, width - shift, a, hi, low); + BVTypeCheck(extract); + output = nf->CreateTerm(BVCONCAT, width, zero, extract); + BVTypeCheck(output); + } + else + FatalError("herasdf"); + } + } + return output; + } //This function simplifies terms based on their kind - ASTNode - Simplifier::SimplifyTerm(const ASTNode& actualInputterm, - ASTNodeMap* VarConstMap) + ASTNode + Simplifier::SimplifyTerm(const ASTNode& actualInputterm, ASTNodeMap* VarConstMap) { - assert(_bm->UserFlags.optimize_flag); + assert(_bm->UserFlags.optimize_flag); - if (actualInputterm.isConstant()) - return actualInputterm; + if (actualInputterm.isConstant()) + return actualInputterm; - ASTNode inputterm(actualInputterm); // mutable local copy. + ASTNode inputterm(actualInputterm); // mutable local copy. //cout << "SimplifyTerm: input: " << actualInputterm << endl; // if (!optimize_flag) @@ -1838,7 +1789,7 @@ namespace BEEV ASTNode output = inputterm; assert(BVTypeCheck(inputterm)); - + //######################################## //######################################## @@ -1865,1192 +1816,1121 @@ namespace BEEV const unsigned int inputValueWidth = inputterm.GetValueWidth(); - { - assert(k != BVCONST); - if (k != SYMBOL) // const and symbols need to be created specially. - { - ASTVec v; - ASTVec toProcess = actualInputterm.GetChildren(); - if (actualInputterm.GetKind() == BVAND || actualInputterm.GetKind() == BVOR || actualInputterm.GetKind() == BVPLUS) - { - // If we didn't flatten these, then we'd start flattening each of these - // from the bottom up. Potentially creating tons of the nodes along the way. - toProcess = FlattenKind(actualInputterm.GetKind(), toProcess); - } - - v.reserve(toProcess.size()); - for (unsigned i = 0; i < toProcess.size(); i++) - { - if (toProcess[i].GetType() == BITVECTOR_TYPE) - v.push_back(SimplifyTerm(toProcess[i], VarConstMap)); - else if (toProcess[i].GetType() == BOOLEAN_TYPE) - v.push_back(SimplifyFormula(toProcess[i], VarConstMap)); - else - v.push_back(toProcess[i]); - } - - assert(v.size() > 0); - if (v != actualInputterm.GetChildren()) // short-cut. - { - output = nf->CreateArrayTerm(k,actualInputterm.GetIndexWidth(), inputValueWidth, v); - } - else - output = actualInputterm; - - if (inputterm != output) - { - UpdateSimplifyMap(inputterm,output,false); - inputterm = output; - } - } - - const ASTVec& children = inputterm.GetChildren(); - k = inputterm.GetKind(); - - // Perform constant propagation if possible. - // This should do nothing if the simplifyingnodefactory is used. - if (k != BEEV::UNDEFINED && k != BEEV::SYMBOL) { - bool allConstant = true; - - for (unsigned i = 0; i < children.size(); i++) - if (!children[i].isConstant()) { - allConstant = false; - break; - } - - if (allConstant) { - const ASTNode& c = BVConstEvaluator(inputterm); - assert(c.isConstant()); - UpdateSimplifyMap(inputterm, c, false, VarConstMap); - return c; - } - } - } - - - { - ASTNode pulledUp = PullUpITE(inputterm); - if (pulledUp != inputterm) - { - ASTNode r = SimplifyTerm(pulledUp); - UpdateSimplifyMap(actualInputterm,r,false,NULL); - UpdateSimplifyMap(inputterm,r,false,NULL); - return r; - } - } + { + assert(k != BVCONST); + if (k != SYMBOL) // const and symbols need to be created specially. + { + ASTVec v; + ASTVec toProcess = actualInputterm.GetChildren(); + if (actualInputterm.GetKind() == BVAND || actualInputterm.GetKind() == BVOR + || actualInputterm.GetKind() == BVPLUS) + { + // If we didn't flatten these, then we'd start flattening each of these + // from the bottom up. Potentially creating tons of the nodes along the way. + toProcess = FlattenKind(actualInputterm.GetKind(), toProcess); + } + v.reserve(toProcess.size()); + for (unsigned i = 0; i < toProcess.size(); i++) + { + if (toProcess[i].GetType() == BITVECTOR_TYPE) + v.push_back(SimplifyTerm(toProcess[i], VarConstMap)); + else if (toProcess[i].GetType() == BOOLEAN_TYPE) + v.push_back(SimplifyFormula(toProcess[i], VarConstMap)); + else + v.push_back(toProcess[i]); + } - //Check that each of the bit-vector operands is simplified. - //I haven't measured if this is worth the expense. - { - bool notSimplified= false; - for (int i =0; i < inputterm.Degree();i++) - if (inputterm[i].GetType() != ARRAY_TYPE) - if (!hasBeenSimplified(inputterm[i])) - { - notSimplified = true; - break; - } - if (notSimplified) - { - ASTNode r = SimplifyTerm(inputterm); - UpdateSimplifyMap(actualInputterm,r,false,NULL); - UpdateSimplifyMap(inputterm,r,false,NULL); - return r; - } - } + assert(v.size() > 0); + if (v != actualInputterm.GetChildren()) // short-cut. + { + output = nf->CreateArrayTerm(k, actualInputterm.GetIndexWidth(), inputValueWidth, v); + } + else + output = actualInputterm; + + if (inputterm != output) + { + UpdateSimplifyMap(inputterm, output, false); + inputterm = output; + } + } + + const ASTVec& children = inputterm.GetChildren(); + k = inputterm.GetKind(); + + // Perform constant propagation if possible. + // This should do nothing if the simplifyingnodefactory is used. + if (k != BEEV::UNDEFINED && k != BEEV::SYMBOL) + { + bool allConstant = true; + + for (unsigned i = 0; i < children.size(); i++) + if (!children[i].isConstant()) + { + allConstant = false; + break; + } + + if (allConstant) + { + const ASTNode& c = BVConstEvaluator(inputterm); + assert(c.isConstant()); + UpdateSimplifyMap(inputterm, c, false, VarConstMap); + return c; + } + } + } - switch (k) { - case BVCONST: - output = inputterm; - break; - case SYMBOL: - if(CheckMap(VarConstMap, inputterm, output)) + ASTNode pulledUp = PullUpITE(inputterm); + if (pulledUp != inputterm) { - return output; + ASTNode r = SimplifyTerm(pulledUp); + UpdateSimplifyMap(actualInputterm, r, false, NULL); + UpdateSimplifyMap(inputterm, r, false, NULL); + return r; } - if (CheckSubstitutionMap(inputterm, output)) + } + + //Check that each of the bit-vector operands is simplified. + //I haven't measured if this is worth the expense. + { + bool notSimplified = false; + for (int i = 0; i < inputterm.Degree(); i++) + if (inputterm[i].GetType() != ARRAY_TYPE) + if (!hasBeenSimplified(inputterm[i])) + { + notSimplified = true; + break; + } + if (notSimplified) { - return SimplifyTerm(output, VarConstMap); + ASTNode r = SimplifyTerm(inputterm); + UpdateSimplifyMap(actualInputterm, r, false, NULL); + UpdateSimplifyMap(inputterm, r, false, NULL); + return r; } - output = inputterm; - break; - case BVMULT: - // follow on. - case BVPLUS: - { - const ASTVec c = FlattenKind(k,inputterm.GetChildren()); - - ASTVec constkids, nonconstkids; - - //go through the childnodes, and separate constant and - //nonconstant nodes. combine the constant nodes using the - //constevaluator. if the resultant constant is zero and k == - //BVPLUS, then ignore it (similarily for 1 and BVMULT). else, - //add the computed constant to the nonconst vector, flatten, - //sort, and create BVPLUS/BVMULT and return - for (ASTVec::const_iterator - it = c.begin(), itend = c.end(); - it != itend; it++) - { - ASTNode aaa = *it; + } - assert(hasBeenSimplified(aaa)); + switch (k) + { + case BVCONST: + output = inputterm; + break; + case SYMBOL: + if (CheckMap(VarConstMap, inputterm, output)) + { + return output; + } + if (CheckSubstitutionMap(inputterm, output)) + { + return SimplifyTerm(output, VarConstMap); + } + output = inputterm; + break; + case BVMULT: + // follow on. + case BVPLUS: + { + const ASTVec c = FlattenKind(k, inputterm.GetChildren()); - if (BVCONST == aaa.GetKind()) - { - constkids.push_back(aaa); - } - else - { - nonconstkids.push_back(aaa); - } - } + ASTVec constkids, nonconstkids; - const ASTNode one = _bm->CreateOneConst(inputValueWidth); - const ASTNode max = _bm->CreateMaxConst(inputValueWidth); - const ASTNode zero = _bm->CreateZeroConst(inputValueWidth); + //go through the childnodes, and separate constant and + //nonconstant nodes. combine the constant nodes using the + //constevaluator. if the resultant constant is zero and k == + //BVPLUS, then ignore it (similarily for 1 and BVMULT). else, + //add the computed constant to the nonconst vector, flatten, + //sort, and create BVPLUS/BVMULT and return + for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++) + { + ASTNode aaa = *it; - //initialize constoutput to zero, in case there are no elements - //in constkids - ASTNode constoutput = (k == BVPLUS) ? zero : one; + assert(hasBeenSimplified(aaa)); - if (1 == constkids.size()) - { - //only one element in constkids - constoutput = constkids[0]; - } - else if (1 < constkids.size()) - { - //many elements in constkids. simplify it - constoutput = - nf->CreateTerm(k, inputterm.GetValueWidth(), constkids); - constoutput = BVConstEvaluator(constoutput); - } + if (BVCONST == aaa.GetKind()) + { + constkids.push_back(aaa); + } + else + { + nonconstkids.push_back(aaa); + } + } - if (BVMULT == k - && zero == constoutput) - { - output = zero; - } - else if (BVMULT == k - && 1 == nonconstkids.size() - && constoutput == max) - { - //useful special case opt: when input is BVMULT(max_const,t), - //then output = BVUMINUS(t). this is easier on the bitblaster - output = - nf->CreateTerm(BVUMINUS, inputValueWidth, nonconstkids); - } - else - { - if (0 < nonconstkids.size()) - { - // ignore identities. - if (BVPLUS == k && constoutput != zero) - { - nonconstkids.push_back(constoutput); - } - else if (BVMULT == k && constoutput != one) - { - nonconstkids.push_back(constoutput); - } - - if (1 == nonconstkids.size()) - { - //exactly one element in nonconstkids. output is exactly - //nonconstkids[0] - output = nonconstkids[0]; - } - else if (BVMULT == k) - { + const ASTNode one = _bm->CreateOneConst(inputValueWidth); + const ASTNode max = _bm->CreateMaxConst(inputValueWidth); + const ASTNode zero = _bm->CreateZeroConst(inputValueWidth); + + //initialize constoutput to zero, in case there are no elements + //in constkids + ASTNode constoutput = (k == BVPLUS) ? zero : one; + + if (1 == constkids.size()) + { + //only one element in constkids + constoutput = constkids[0]; + } + else if (1 < constkids.size()) + { + //many elements in constkids. simplify it + constoutput = nf->CreateTerm(k, inputterm.GetValueWidth(), constkids); + constoutput = BVConstEvaluator(constoutput); + } + + if (BVMULT == k && zero == constoutput) + { + output = zero; + } + else if (BVMULT == k && 1 == nonconstkids.size() && constoutput == max) + { + //useful special case opt: when input is BVMULT(max_const,t), + //then output = BVUMINUS(t). this is easier on the bitblaster + output = nf->CreateTerm(BVUMINUS, inputValueWidth, nonconstkids); + } + else + { + if (0 < nonconstkids.size()) + { + // ignore identities. + if (BVPLUS == k && constoutput != zero) + { + nonconstkids.push_back(constoutput); + } + else if (BVMULT == k && constoutput != one) + { + nonconstkids.push_back(constoutput); + } + + if (1 == nonconstkids.size()) + { + //exactly one element in nonconstkids. output is exactly + //nonconstkids[0] + output = nonconstkids[0]; + } + else if (BVMULT == k) + { SortByArith(nonconstkids); if (k == BVMULT && nonconstkids.size() > 2) output = makeTower(k, nonconstkids); else - output = nf->CreateTerm(k, inputValueWidth, nonconstkids); + output = nf->CreateTerm(k, inputValueWidth, nonconstkids); output = DistributeMultOverPlus(output, true); } - else // pluss. - { - assert(BVPLUS == k); - //SortByArith(nonconstkids); - //output = nf->CreateTerm(k, inputValueWidth, nonconstkids); - //output = Flatten(output); - //output = CombineLikeTerms(output); - output = CombineLikeTerms(nonconstkids); + else // pluss. + { + assert(BVPLUS == k); + //SortByArith(nonconstkids); + //output = nf->CreateTerm(k, inputValueWidth, nonconstkids); + //output = Flatten(output); + //output = CombineLikeTerms(output); + output = CombineLikeTerms(nonconstkids); } - } - else - { - //nonconstkids was empty, all childnodes were constant, hence - //constoutput is the output. - output = constoutput; - } - } + } + else + { + //nonconstkids was empty, all childnodes were constant, hence + //constoutput is the output. + output = constoutput; + } + } - // propagate bvuminus upwards through multiplies. - if (BVMULT == output.GetKind()) - { - ASTVec d = output.GetChildren(); - int uminus = 0; - for (unsigned i = 0; i < d.size(); i++) - { - if (d[i].GetKind() == BVUMINUS) - { - d[i] = d[i][0]; - uminus++; - } - } - if (uminus != 0) - { - SortByArith(d); - output = nf->CreateTerm(BVMULT, output.GetValueWidth(), d); - if ((uminus & 0x1) != 0) // odd, pull up the uminus. - { - output = - nf->CreateTerm(BVUMINUS, - output.GetValueWidth(), - output); - } - } - } + // propagate bvuminus upwards through multiplies. + if (BVMULT == output.GetKind()) + { + ASTVec d = output.GetChildren(); + int uminus = 0; + for (unsigned i = 0; i < d.size(); i++) + { + if (d[i].GetKind() == BVUMINUS) + { + d[i] = d[i][0]; + uminus++; + } + } + if (uminus != 0) + { + SortByArith(d); + output = nf->CreateTerm(BVMULT, output.GetValueWidth(), d); + if ((uminus & 0x1) != 0) // odd, pull up the uminus. + { + output = nf->CreateTerm(BVUMINUS, output.GetValueWidth(), output); + } + } + } - if ((BVMULT == output.GetKind() || BVPLUS == output.GetKind()) && output.GetChildren().size() == 2 && output.GetChildren()[0].GetKind() == BVSX && output.GetChildren()[1].GetKind() == BVSX ) - { - output = pullUpBVSX(output); - } - else if (BVMULT == output.GetKind()) - { - output = makeTower(BVMULT,output.GetChildren()); - } - else if ( BVPLUS == output.GetKind()) - { - ASTVec d = output.GetChildren(); - SortByArith(d); - output = - nf->CreateTerm(output.GetKind(), - output.GetValueWidth(), d); - } - break; - } - case BVSUB: - { - assert(inputterm.Degree() == 2); + if ((BVMULT == output.GetKind() || BVPLUS == output.GetKind()) && output.GetChildren().size() == 2 + && output.GetChildren()[0].GetKind() == BVSX && output.GetChildren()[1].GetKind() == BVSX) + { + output = pullUpBVSX(output); + } + else if (BVMULT == output.GetKind()) + { + output = makeTower(BVMULT, output.GetChildren()); + } + else if (BVPLUS == output.GetKind()) + { + ASTVec d = output.GetChildren(); + SortByArith(d); + output = nf->CreateTerm(output.GetKind(), output.GetValueWidth(), d); + } + break; + } + case BVSUB: + { + assert(inputterm.Degree() == 2); - const ASTNode& a0 =inputterm[0]; - const ASTNode& a1 =inputterm[1]; + const ASTNode& a0 = inputterm[0]; + const ASTNode& a1 = inputterm[1]; - if (a0 == a1) - output = _bm->CreateZeroConst(inputValueWidth); - else - { - //covert x-y into x+(-y) and simplify. this transformation - //triggers more simplifications - // - output = nf->CreateTerm(BVPLUS, inputValueWidth, a0, nf->CreateTerm(BVUMINUS, inputValueWidth, a1)); - } + if (a0 == a1) + output = _bm->CreateZeroConst(inputValueWidth); + else + { + //covert x-y into x+(-y) and simplify. this transformation + //triggers more simplifications + // + output = nf->CreateTerm(BVPLUS, inputValueWidth, a0, nf->CreateTerm(BVUMINUS, inputValueWidth, a1)); + } + break; + } + case BVUMINUS: + { + //important to treat BVUMINUS as a special case, because it + //helps in arithmetic transformations. e.g. x + BVUMINUS(x) is + //actually 0. One way to reveal this fact is to strip bvuminus + //out, and replace with something else so that combineliketerms + //can catch this fact. + + const ASTNode& a0 = inputterm[0]; + const Kind k1 = a0.GetKind(); + const ASTNode one = _bm->CreateOneConst(inputValueWidth); + assert(k1 != BVCONST); + switch (k1) + { + case BVUMINUS: + output = a0[0]; break; - } - case BVUMINUS: - { - //important to treat BVUMINUS as a special case, because it - //helps in arithmetic transformations. e.g. x + BVUMINUS(x) is - //actually 0. One way to reveal this fact is to strip bvuminus - //out, and replace with something else so that combineliketerms - //can catch this fact. - - const ASTNode& a0 =inputterm[0]; - const Kind k1 = a0.GetKind(); - const ASTNode one = _bm->CreateOneConst(inputValueWidth); - assert(k1 != BVCONST); - switch (k1) - { - case BVUMINUS: - output = a0[0]; - break; - case BVNEG: + case BVNEG: + { + output = nf->CreateTerm(BVPLUS, inputValueWidth, a0[0], one); + break; + } + case BVMULT: + { + if (BVUMINUS == a0[0].GetKind()) { - output = nf->CreateTerm(BVPLUS, inputValueWidth, a0[0], one); - break; + output = nf->CreateTerm(BVMULT, inputValueWidth, a0[0][0], a0[1]); } - case BVMULT: + else if (BVUMINUS == a0[1].GetKind()) { - if (BVUMINUS == a0[0].GetKind()) - { - output = nf->CreateTerm(BVMULT, inputValueWidth, a0[0][0], a0[1]); - } - else if (BVUMINUS == a0[1].GetKind()) + output = nf->CreateTerm(BVMULT, inputValueWidth, a0[0], a0[1][0]); + } + else + { + // If the first argument to the multiply is a + // constant, push it through. Without regard for + // the splitting of nodes (hmm.) This is + // necessary because the bitvector solver can + // process -3*x, but not -(3*x). + if (BVCONST == a0[0].GetKind()) { - output = nf->CreateTerm(BVMULT, inputValueWidth, a0[0], a0[1][0]); + ASTNode a00 = SimplifyTerm(nf->CreateTerm(BVUMINUS, inputValueWidth, a0[0]), VarConstMap); + output = nf->CreateTerm(BVMULT, inputValueWidth, a00, a0[1]); } else - { - // If the first argument to the multiply is a - // constant, push it through. Without regard for - // the splitting of nodes (hmm.) This is - // necessary because the bitvector solver can - // process -3*x, but not -(3*x). - if (BVCONST == a0[0].GetKind()) - { - ASTNode a00 = - SimplifyTerm(nf->CreateTerm(BVUMINUS, inputValueWidth, a0[0]), - VarConstMap); - output = nf->CreateTerm(BVMULT, inputValueWidth, a00, a0[1]); - } - else - output = inputterm; - } - break; + output = inputterm; } - case BVPLUS: + break; + } + case BVPLUS: + { + //push BVUMINUS over all the monomials of BVPLUS. Simplify + //along the way + // + //BVUMINUS(a1x1 + a2x2 + ...) <=> BVPLUS(BVUMINUS(a1x1) + + //BVUMINUS(a2x2) + ... + const ASTVec& c = a0.GetChildren(); + ASTVec o; + for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++) { - //push BVUMINUS over all the monomials of BVPLUS. Simplify - //along the way - // - //BVUMINUS(a1x1 + a2x2 + ...) <=> BVPLUS(BVUMINUS(a1x1) + - //BVUMINUS(a2x2) + ... - const ASTVec& c = a0.GetChildren(); - ASTVec o; - for (ASTVec::const_iterator - it = c.begin(), itend = c.end(); it != itend; it++) - { - //Simplify(BVUMINUS(a1x1)) - ASTNode aaa = - SimplifyTerm(nf->CreateTerm(BVUMINUS, inputValueWidth, *it), - VarConstMap); - o.push_back(aaa); - } - - output = nf->CreateTerm(BVPLUS, inputValueWidth, o); - break; + //Simplify(BVUMINUS(a1x1)) + ASTNode aaa = SimplifyTerm(nf->CreateTerm(BVUMINUS, inputValueWidth, *it), VarConstMap); + o.push_back(aaa); } - case BVSUB: + + output = nf->CreateTerm(BVPLUS, inputValueWidth, o); + break; + } + case BVSUB: + { + //BVUMINUS(BVSUB(x,y)) <=> BVSUB(y,x) + output = nf->CreateTerm(BVSUB, inputValueWidth, a0[1], a0[0]); + break; + } + case BVAND: + if (a0.Degree() == 2 && (a0[1].GetKind() == BVUMINUS) && a0[1][0] == a0[0]) + { + output = nf->CreateTerm(BVOR, inputValueWidth, a0[0], a0[1]); + } + break; + case BVOR: + if (a0.Degree() == 2 && (a0[1].GetKind() == BVUMINUS) && a0[1][0] == a0[0]) + { + output = nf->CreateTerm(BVAND, inputValueWidth, a0[0], a0[1]); + } + break; + case BVLEFTSHIFT: + if (a0[0].GetKind() == BVCONST) + output = nf->CreateTerm(BVLEFTSHIFT, inputValueWidth, nf->CreateTerm(BVUMINUS, inputValueWidth, a0[0]), + a0[1]); + break; + case ITE: + { + //BVUMINUS(ITE(c,t1,t2)) <==> ITE(c,BVUMINUS(t1),BVUMINUS(t2)) + ASTNode c = a0[0]; + ASTNode t1 = SimplifyTerm(nf->CreateTerm(BVUMINUS, inputValueWidth, a0[1]), VarConstMap); + ASTNode t2 = SimplifyTerm(nf->CreateTerm(BVUMINUS, inputValueWidth, a0[2]), VarConstMap); + output = CreateSimplifiedTermITE(c, t1, t2); + break; + } + default: + { + output = inputterm; + break; + } + } + break; + } + case BVEXTRACT: + { + //it is important to take care of wordlevel transformation in + //BVEXTRACT. it exposes oppurtunities for later simplification + //and solving (variable elimination) + const ASTNode& a0 = inputterm[0]; + + const Kind k1 = a0.GetKind(); + + //indices for BVEXTRACT + ASTNode i = inputterm[1]; + ASTNode j = inputterm[2]; + const ASTNode zero = _bm->CreateZeroConst(32); + + //recall that the indices of BVEXTRACT are always 32 bits + //long. therefore doing a GetBVUnsigned is ok. + unsigned int i_val = i.GetUnsignedConst(); + unsigned int j_val = j.GetUnsignedConst(); + + // a0[i:0] and len(a0)=i+1, then return a0 + if (inputValueWidth == a0.GetValueWidth()) + { + assert(0 == j_val); + output = a0; + break; + } + + assert(k1 != BVCONST); + + switch (k1) + { + case BVEXTRACT: + { + const unsigned innerLow = a0[2].GetUnsignedConst(); + const unsigned innerHigh = a0[1].GetUnsignedConst(); + + output = nf->CreateTerm(BVEXTRACT, inputValueWidth, a0[0], _bm->CreateBVConst(32, i_val + innerLow), + _bm->CreateBVConst(32, j_val + innerLow)); + assert(BVTypeCheck(output)); + break; + } + + case BVCONCAT: + { + //assumes concatenation is binary + // + //input is of the form a0[i:j] + // + //a0 is the conatentation t@u, and a0[0] is t, and a0[1] is u + ASTNode t = a0[0]; + ASTNode u = a0[1]; + const unsigned int len_a0 = a0.GetValueWidth(); + const unsigned int len_u = u.GetValueWidth(); + + if (len_u > i_val) { - //BVUMINUS(BVSUB(x,y)) <=> BVSUB(y,x) - output = nf->CreateTerm(BVSUB, inputValueWidth, a0[1], a0[0]); - break; + //Apply the following rule: + // (t@u)[i:j] <==> u[i:j], if len(u) > i + // + output = nf->CreateTerm(BVEXTRACT, inputValueWidth, u, i, j); } - case BVAND: - if (a0.Degree() == 2 && (a0[1].GetKind() == BVUMINUS) && a0[1][0] == a0[0]) + else if (len_a0 > i_val && j_val >= len_u) { - output = nf->CreateTerm(BVOR, inputValueWidth, a0[0], a0[1]); + //Apply the rule: (t@u)[i:j] <==> + // t[i-len_u:j-len_u], if len(t@u) > i >= j >= + // len(u) + i = _bm->CreateBVConst(32, i_val - len_u); + j = _bm->CreateBVConst(32, j_val - len_u); + output = nf->CreateTerm(BVEXTRACT, inputValueWidth, t, i, j); } - break; - case BVOR: - if (a0.Degree() == 2 && (a0[1].GetKind() == BVUMINUS) && a0[1][0] == a0[0]) + else { - output = nf->CreateTerm(BVAND, inputValueWidth, a0[0], a0[1]); + //Apply the rule: + // (t@u)[i:j] <==> t[i-len_u:0] @ u[len_u-1:j] + i = _bm->CreateBVConst(32, i_val - len_u); + ASTNode m = _bm->CreateBVConst(32, len_u - 1); + t = SimplifyTerm(nf->CreateTerm(BVEXTRACT, i_val - len_u + 1, t, i, zero), VarConstMap); + u = SimplifyTerm(nf->CreateTerm(BVEXTRACT, len_u - j_val, u, m, j), VarConstMap); + output = nf->CreateTerm(BVCONCAT, inputValueWidth, t, u); } break; - case BVLEFTSHIFT: - if (a0[0].GetKind() == BVCONST) - output = nf->CreateTerm(BVLEFTSHIFT, inputValueWidth, nf->CreateTerm(BVUMINUS, inputValueWidth, a0[0]), - a0[1]); - break; - case ITE: + } + case BVPLUS: + case BVMULT: + { + // (BVMULT(n,t,u))[i:j] <==> BVMULT(i+1,t[i:0],u[i:0])[i:j] + //similar rule for BVPLUS + ASTVec c = a0.GetChildren(); + ASTVec o; + for (ASTVec::iterator jt = c.begin(), jtend = c.end(); jt != jtend; jt++) { - //BVUMINUS(ITE(c,t1,t2)) <==> ITE(c,BVUMINUS(t1),BVUMINUS(t2)) - ASTNode c = a0[0]; - ASTNode t1 = - SimplifyTerm(nf->CreateTerm(BVUMINUS, inputValueWidth, a0[1]), - VarConstMap); - ASTNode t2 = - SimplifyTerm(nf->CreateTerm(BVUMINUS, inputValueWidth, a0[2]), - VarConstMap); - output = CreateSimplifiedTermITE(c, t1, t2); - break; + ASTNode aaa = *jt; + aaa = SimplifyTerm(nf->CreateTerm(BVEXTRACT, i_val + 1, aaa, i, zero), VarConstMap); + o.push_back(aaa); } - default: + output = nf->CreateTerm(a0.GetKind(), i_val + 1, o); + if (j_val != 0) { - output = inputterm; - break; + //add extraction only if j is not zero + output = nf->CreateTerm(BVEXTRACT, inputValueWidth, output, i, j); } - } - break; - } - case BVEXTRACT: - { - //it is important to take care of wordlevel transformation in - //BVEXTRACT. it exposes oppurtunities for later simplification - //and solving (variable elimination) - const ASTNode& a0 =inputterm[0]; + break; + } + + // This can increase the number of nodes exponentially. + // If turned on bitrev2048 will blow out main memory, with + // this disabled it takes 12MB. +#if 0 - const Kind k1 = a0.GetKind(); + case BVAND: + case BVOR: + case BVXOR: + { + assert(a0.Degree() == 2); - //indices for BVEXTRACT - ASTNode i = inputterm[1]; - ASTNode j = inputterm[2]; - const ASTNode zero = _bm->CreateZeroConst(32); + //assumes these operators are binary + // + // (t op u)[i:j] <==> t[i:j] op u[i:j] + ASTNode t = a0[0]; + ASTNode u = a0[1]; + t = + SimplifyTerm(nf->CreateTerm(BVEXTRACT, + a_len, t, i, j), + VarConstMap); + u = + SimplifyTerm(nf->CreateTerm(BVEXTRACT, + a_len, u, i, j), + VarConstMap); + BVTypeCheck(t); + BVTypeCheck(u); + //output = nf->CreateTerm(k1, a_len, t, u); + + output = inputterm; + break; + } +#endif + case BVNEG: + { + // (~t)[i:j] <==> ~(t[i:j]) + ASTNode t = a0[0]; + t = SimplifyTerm(nf->CreateTerm(BVEXTRACT, inputValueWidth, t, i, j), VarConstMap); + output = nf->CreateTerm(BVNEG, inputValueWidth, t); + break; + } + // case BVSX:{ //(BVSX(t,n)[i:j] <==> BVSX(t,i+1), if n + // >= i+1 and j=0 ASTNode t = a0[0]; unsigned int + // bvsx_len = a0.GetValueWidth(); if(bvsx_len < + // a_len) { FatalError("SimplifyTerm: BVEXTRACT + // over BVSX:" "the length of BVSX term must be + // greater than extract-len",inputterm); } if(j + // != zero) { output = + // nf->CreateTerm(BVEXTRACT,a_len,a0,i,j); } + // else { output = + // nf->CreateTerm(BVSX,a_len,t, + // _bm->CreateBVConst(32,a_len)); + // } break; } + + /* + * On deeply nested ITES, this can cause an exponential number + * of nodes to be produced. Especially if there are different + * extracts over the same node. + * + case ITE: + { + const ASTNode& t0 = a0[0]; + ASTNode t1 = + SimplifyTerm(nf->CreateTerm(BVEXTRACT, + a_len, a0[1], i, j), + VarConstMap); + ASTNode t2 = + SimplifyTerm(nf->CreateTerm(BVEXTRACT, + a_len, a0[2], i, j), + VarConstMap); + output = CreateSimplifiedTermITE(t0, t1, t2); + break; + } + */ + default: + { + output = inputterm; + break; + } + } + break; + } + case BVNEG: + { + const ASTNode& a0 = inputterm[0]; - //recall that the indices of BVEXTRACT are always 32 bits - //long. therefore doing a GetBVUnsigned is ok. - unsigned int i_val = i.GetUnsignedConst(); - unsigned int j_val = j.GetUnsignedConst(); + assert(a0.GetKind() != BVCONST); - // a0[i:0] and len(a0)=i+1, then return a0 - if (inputValueWidth == a0.GetValueWidth()) + switch (a0.GetKind()) + { + case BVNEG: + output = a0[0]; + break; + case ITE: + if (a0[1].isConstant() && a0[2].isConstant()) { - assert(0 == j_val); - output = a0; - break; + ASTNode t = SimplifyTerm(nf->CreateTerm(BVNEG, inputValueWidth, a0[1])); + ASTNode f = SimplifyTerm(nf->CreateTerm(BVNEG, inputValueWidth, a0[2])); + output = nf->CreateTerm(ITE, inputValueWidth, a0[0], BVConstEvaluator(t), BVConstEvaluator(f)); + break; } + //follow on + default: + output = inputterm; + break; + } + break; + } - assert(k1 != BVCONST); + case BVSX: + { + //a0 is the expr which is being sign extended + ASTNode a0 = inputterm[0]; - switch (k1) - { - case BVEXTRACT: - { - const unsigned innerLow = a0[2].GetUnsignedConst(); - const unsigned innerHigh = a0[1].GetUnsignedConst(); + //a1 represents the length of the term BVSX(a0) + const ASTNode& a1 = inputterm[1]; - output = nf->CreateTerm(BVEXTRACT, inputValueWidth,a0[0], _bm->CreateBVConst(32,i_val+innerLow),_bm->CreateBVConst(32, j_val+innerLow)); - assert(BVTypeCheck(output)); - break; - } + if (a0.GetValueWidth() == inputValueWidth) + { + //nothing to signextend + output = a0; + break; + } - case BVCONCAT: - { - //assumes concatenation is binary - // - //input is of the form a0[i:j] - // - //a0 is the conatentation t@u, and a0[0] is t, and a0[1] is u - ASTNode t = a0[0]; - ASTNode u = a0[1]; - const unsigned int len_a0 = a0.GetValueWidth(); - const unsigned int len_u = u.GetValueWidth(); + // If the msb is known. Then puts 0's or the 1's infront. + if (mostSignificantConstants(a0) > 0) + { + if (getConstantBit(a0, 0) == 0) + output = nf->CreateTerm(BVCONCAT, inputValueWidth, + _bm->CreateZeroConst(inputValueWidth - a0.GetValueWidth()), a0); + else + output = nf->CreateTerm(BVCONCAT, inputValueWidth, + _bm->CreateMaxConst(inputValueWidth - a0.GetValueWidth()), a0); + break; + } - if (len_u > i_val) - { - //Apply the following rule: - // (t@u)[i:j] <==> u[i:j], if len(u) > i - // - output = nf->CreateTerm(BVEXTRACT, inputValueWidth, u, i, j); - } - else if (len_a0 > i_val && j_val >= len_u) - { - //Apply the rule: (t@u)[i:j] <==> - // t[i-len_u:j-len_u], if len(t@u) > i >= j >= - // len(u) - i = _bm->CreateBVConst(32, i_val - len_u); - j = _bm->CreateBVConst(32, j_val - len_u); - output = nf->CreateTerm(BVEXTRACT, inputValueWidth, t, i, j); - } - else + assert(a0.GetKind() != BVCONST); + + switch (a0.GetKind()) + { + case BVNEG: + output = nf->CreateTerm(a0.GetKind(), inputValueWidth, nf->CreateTerm(BVSX, inputValueWidth, a0[0], a1)); + break; + case BVAND: + case BVOR: + { + const ASTVec& c = a0.GetChildren(); + ASTVec newChildren; + newChildren.reserve(c.size()); + for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++) + { + newChildren.push_back(nf->CreateTerm(BVSX, inputValueWidth, *it, a1)); + } + output = nf->CreateTerm(a0.GetKind(), inputValueWidth, newChildren); + } + break; + case BVPLUS: + { + //BVSX(m,BVPLUS(n,BVSX(t1),BVSX(t2))) <==> + //BVPLUS(m,BVSX(m,t1),BVSX(m,t2)) + const ASTVec& c = a0.GetChildren(); + bool returnflag = false; + for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++) + { + if (BVSX != it->GetKind()) { - //Apply the rule: - // (t@u)[i:j] <==> t[i-len_u:0] @ u[len_u-1:j] - i = _bm->CreateBVConst(32, i_val - len_u); - ASTNode m = _bm->CreateBVConst(32, len_u - 1); - t = - SimplifyTerm(nf->CreateTerm(BVEXTRACT, - i_val - len_u + 1, - t, i, zero), - VarConstMap); - u = - SimplifyTerm(nf->CreateTerm(BVEXTRACT, - len_u - j_val, - u, m, j), - VarConstMap); - output = nf->CreateTerm(BVCONCAT, inputValueWidth, t, u); + returnflag = true; + break; } - break; } - case BVPLUS: - case BVMULT: + if (!returnflag) { - // (BVMULT(n,t,u))[i:j] <==> BVMULT(i+1,t[i:0],u[i:0])[i:j] - //similar rule for BVPLUS - ASTVec c = a0.GetChildren(); ASTVec o; - for (ASTVec::iterator - jt = c.begin(), jtend = c.end(); - jt != jtend; jt++) + o.reserve(c.size()); + for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++) { - ASTNode aaa = *jt; - aaa = - SimplifyTerm(nf->CreateTerm(BVEXTRACT, - i_val + 1, - aaa, i, zero), - VarConstMap); + ASTNode aaa = SimplifyTerm(nf->CreateTerm(BVSX, inputValueWidth, *it, a1), VarConstMap); o.push_back(aaa); } - output = nf->CreateTerm(a0.GetKind(), i_val + 1, o); - if (j_val != 0) - { - //add extraction only if j is not zero - output = nf->CreateTerm(BVEXTRACT, inputValueWidth, output, i, j); - } - break; + output = nf->CreateTerm(a0.GetKind(), inputValueWidth, o); } + break; + } + case BVSX: + { + //if you have BVSX(m,BVSX(n,a)) then you can drop the inner + //BVSX provided m is greater than n. + a0 = a0[0]; + assert(hasBeenSimplified(a0)); - // This can increase the number of nodes exponentially. - // If turned on bitrev2048 will blow out main memory, with - // this disabled it takes 12MB. - #if 0 + output = nf->CreateTerm(BVSX, inputValueWidth, a0, a1); + break; + } + case ITE: + { + const ASTNode& cond = a0[0]; + ASTNode thenpart = SimplifyTerm(nf->CreateTerm(BVSX, inputValueWidth, a0[1], a1), VarConstMap); + ASTNode elsepart = SimplifyTerm(nf->CreateTerm(BVSX, inputValueWidth, a0[2], a1), VarConstMap); + output = CreateSimplifiedTermITE(cond, thenpart, elsepart); + break; + } + default: + output = inputterm; + break; + } + break; + } + case BVAND: + case BVOR: + { + // turn BVAND(CONCAT CONCAT) into concat(BVAND() BVAND()). i.e. push ops through concat. + if (inputterm.Degree() == 2 && inputterm[0].GetKind() == BVCONCAT && inputterm[1].GetKind() == BVCONCAT + && inputterm[0][0].GetValueWidth() == inputterm[1][0].GetValueWidth()) + { + output = nf->CreateTerm(BVCONCAT, inputterm.GetValueWidth(), + nf->CreateTerm(k, inputterm[0][0].GetValueWidth(), inputterm[0][0], inputterm[1][0]), + nf->CreateTerm(k, inputterm[0][1].GetValueWidth(), inputterm[0][1], inputterm[1][1])); + break; + } - case BVAND: - case BVOR: - case BVXOR: + const ASTNode max = _bm->CreateMaxConst(inputValueWidth); + const ASTNode zero = _bm->CreateZeroConst(inputValueWidth); + + const ASTNode identity = (BVAND == k) ? max : zero; + const ASTNode annihilator = (BVAND == k) ? zero : max; + ASTVec c = FlattenKind(inputterm.GetKind(), inputterm.GetChildren()); + SortByArith(c); + ASTVec constants; + ASTVec o; + for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++) + { + ASTNode aaa = *it; + assert(hasBeenSimplified(aaa)); + + if (aaa == annihilator) { - assert(a0.Degree() == 2); + output = annihilator; + //memoize + UpdateSimplifyMap(inputterm, output, false, VarConstMap); + UpdateSimplifyMap(actualInputterm, output, false, VarConstMap); + //cerr << "output of SimplifyTerm: " << output << endl; + return output; + } - //assumes these operators are binary - // - // (t op u)[i:j] <==> t[i:j] op u[i:j] - ASTNode t = a0[0]; - ASTNode u = a0[1]; - t = - SimplifyTerm(nf->CreateTerm(BVEXTRACT, - a_len, t, i, j), - VarConstMap); - u = - SimplifyTerm(nf->CreateTerm(BVEXTRACT, - a_len, u, i, j), - VarConstMap); - BVTypeCheck(t); - BVTypeCheck(u); - //output = nf->CreateTerm(k1, a_len, t, u); - - output = inputterm; - break; + if (o.size() > 0 && o.back() == aaa) + { + continue; // duplicate. } - #endif - case BVNEG: + + // nb: There's no guarantee that the bvneg will immediately follow + // the thing it's negating if the degree > 2. + if (o.size() > 0 && aaa.GetKind() == BVNEG && o.back() == aaa[0]) { - // (~t)[i:j] <==> ~(t[i:j]) - ASTNode t = a0[0]; - t = - SimplifyTerm(nf->CreateTerm(BVEXTRACT, inputValueWidth, t, i, j), - VarConstMap); - output = nf->CreateTerm(BVNEG, inputValueWidth, t); - break; + output = annihilator; + UpdateSimplifyMap(inputterm, output, false, VarConstMap); + UpdateSimplifyMap(actualInputterm, output, false, VarConstMap); + return output; } - // case BVSX:{ //(BVSX(t,n)[i:j] <==> BVSX(t,i+1), if n - // >= i+1 and j=0 ASTNode t = a0[0]; unsigned int - // bvsx_len = a0.GetValueWidth(); if(bvsx_len < - // a_len) { FatalError("SimplifyTerm: BVEXTRACT - // over BVSX:" "the length of BVSX term must be - // greater than extract-len",inputterm); } if(j - // != zero) { output = - // nf->CreateTerm(BVEXTRACT,a_len,a0,i,j); } - // else { output = - // nf->CreateTerm(BVSX,a_len,t, - // _bm->CreateBVConst(32,a_len)); - // } break; } - - /* - * On deeply nested ITES, this can cause an exponential number - * of nodes to be produced. Especially if there are different - * extracts over the same node. - * - case ITE: + + if (BVCONST == aaa.GetKind()) { - const ASTNode& t0 = a0[0]; - ASTNode t1 = - SimplifyTerm(nf->CreateTerm(BVEXTRACT, - a_len, a0[1], i, j), - VarConstMap); - ASTNode t2 = - SimplifyTerm(nf->CreateTerm(BVEXTRACT, - a_len, a0[2], i, j), - VarConstMap); - output = CreateSimplifiedTermITE(t0, t1, t2); - break; + constants.push_back(aaa); } - */ - default: + else { - output = inputterm; - break; + o.push_back(aaa); } - } - break; - } - case BVNEG: - { - const ASTNode& a0 =inputterm[0]; - - assert (a0.GetKind() != BVCONST); - - switch (a0.GetKind()) - { - case BVNEG: - output = a0[0]; - break; - case ITE: - if (a0[1].isConstant() && a0[2].isConstant()) { - ASTNode t = SimplifyTerm(nf->CreateTerm(BVNEG, inputValueWidth, - a0[1])); - ASTNode f = SimplifyTerm(nf->CreateTerm(BVNEG, inputValueWidth, - a0[2])); - output = nf->CreateTerm(ITE, inputValueWidth, a0[0], - BVConstEvaluator(t), BVConstEvaluator(f)); - break; - } - //follow on - default: - output = inputterm; - break; - } - break; - } + } - case BVSX: - { - //a0 is the expr which is being sign extended - ASTNode a0 =inputterm[0]; + while (constants.size() >= 2) + { + ASTNode a = constants.back(); + constants.pop_back(); + ASTNode b = constants.back(); + constants.pop_back(); - //a1 represents the length of the term BVSX(a0) - const ASTNode& a1 = inputterm[1]; + ASTNode c = BVConstEvaluator(nf->CreateTerm(inputterm.GetKind(), inputterm.GetValueWidth(), a, b)); + constants.push_back(c); - if (a0.GetValueWidth() == inputValueWidth) - { - //nothing to signextend - output = a0; - break; - } + } + if (constants.size() != 0 && constants.back() != identity) + o.push_back(constants.back()); - // If the msb is known. Then puts 0's or the 1's infront. - if (mostSignificantConstants(a0) > 0) + switch (o.size()) { - if (getConstantBit(a0,0) == 0) - output = nf->CreateTerm(BVCONCAT, inputValueWidth, _bm->CreateZeroConst(inputValueWidth-a0.GetValueWidth()), a0); - else - output = nf->CreateTerm(BVCONCAT, inputValueWidth, _bm->CreateMaxConst(inputValueWidth-a0.GetValueWidth()), a0); - break; + case 0: + output = identity; + break; + case 1: + output = o[0]; + break; + default: + SortByArith(o); + output = nf->CreateTerm(inputterm.GetKind(), inputterm.GetValueWidth(), o); + break; } - assert (a0.GetKind() != BVCONST); - - switch (a0.GetKind()) - { - case BVNEG: - output = - nf->CreateTerm(a0.GetKind(), inputValueWidth, - nf->CreateTerm(BVSX, inputValueWidth, a0[0], a1)); - break; - case BVAND: - case BVOR: - { - const ASTVec& c = a0.GetChildren(); - ASTVec newChildren; - newChildren.reserve(c.size()); - for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++) - { - newChildren.push_back(nf->CreateTerm(BVSX, inputValueWidth, *it, a1)); - } - output = nf->CreateTerm(a0.GetKind(), inputValueWidth, newChildren ); - } - break; - case BVPLUS: + // This don't make it faster, just makes the graphs easier to understand. + if (output.GetKind() == BVAND) + { + assert(output.Degree() != 0); + bool allconv = true; + for (ASTVec::const_iterator it = output.begin(), itend = output.end(); it != itend; it++) { - //BVSX(m,BVPLUS(n,BVSX(t1),BVSX(t2))) <==> - //BVPLUS(m,BVSX(m,t1),BVSX(m,t2)) - const ASTVec& c = a0.GetChildren(); - bool returnflag = false; - for (ASTVec::const_iterator - it = c.begin(), itend = c.end(); it != itend; it++) - { - if (BVSX != it->GetKind()) - { - returnflag = true; - break; - } - } - if (!returnflag) + if (!isPropositionToTerm(*it)) { - ASTVec o; - o.reserve(c.size()); - for (ASTVec::const_iterator - it = c.begin(), itend = c.end(); it != itend; it++) - { - ASTNode aaa = - SimplifyTerm(nf->CreateTerm(BVSX, inputValueWidth, *it, a1), - VarConstMap); - o.push_back(aaa); - } - output = nf->CreateTerm(a0.GetKind(), inputValueWidth, o); + allconv = false; + break; } - break; } - case BVSX: + if (allconv) { - //if you have BVSX(m,BVSX(n,a)) then you can drop the inner - //BVSX provided m is greater than n. - a0 =a0[0]; - assert(hasBeenSimplified(a0)); + const ASTNode zero = _bm->CreateZeroConst(1); + ASTVec children; + for (ASTVec::const_iterator it = output.begin(), itend = output.end(); it != itend; it++) + { + const ASTNode& n = *it; - output = nf->CreateTerm(BVSX, inputValueWidth, a0, a1); - break; + if (n[1] == zero) + children.push_back(nf->CreateNode(NOT, n[0])); + else + children.push_back(n[0]); + } + output = nf->CreateTerm(ITE, 1, nf->CreateNode(AND, children), _bm->CreateOneConst(1), zero); + assert(BVTypeCheck(output)); } - case ITE: + + assert(BVTypeCheck(output)); + + // If the leading bits are zero. Replace it by a concat with zero. + int i; + if (output.GetKind() == BVAND && output.Degree() == 2 && ((i = numberOfLeadingZeroes(output[0])) > 0)) { - const ASTNode& cond = a0[0]; - ASTNode thenpart = - SimplifyTerm(nf->CreateTerm(BVSX, inputValueWidth, a0[1], a1), - VarConstMap); - ASTNode elsepart = - SimplifyTerm(nf->CreateTerm(BVSX, inputValueWidth, a0[2], a1), - VarConstMap); - output = CreateSimplifiedTermITE(cond, thenpart, elsepart); - break; + // i contains the number of leading zeroes. + if (i < output.GetValueWidth()) + output = nf->CreateTerm( + BVCONCAT, + output.GetValueWidth(), + _bm->CreateZeroConst(i), + nf->CreateTerm( + BVAND, + output.GetValueWidth() - i, + nf->CreateTerm(BVEXTRACT, output.GetValueWidth() - i, output[0], + _bm->CreateBVConst(32, output.GetValueWidth() - i - 1), _bm->CreateBVConst(32, 0)), + nf->CreateTerm(BVEXTRACT, output.GetValueWidth() - i, output[1], + _bm->CreateBVConst(32, output.GetValueWidth() - i - 1), _bm->CreateBVConst(32, 0)))); + + assert(BVTypeCheck(output)); } - default: - output = inputterm; - break; - } - break; - } - case BVAND: - case BVOR: - { - // turn BVAND(CONCAT CONCAT) into concat(BVAND() BVAND()). i.e. push ops through concat. - if (inputterm.Degree() ==2 && inputterm[0].GetKind() == BVCONCAT && inputterm[1].GetKind() == BVCONCAT && inputterm[0][0].GetValueWidth() ==inputterm[1][0].GetValueWidth() ) + } + if (output.GetKind() == BVAND) { - output = nf->CreateTerm(BVCONCAT, inputterm.GetValueWidth(), - nf->CreateTerm(k,inputterm[0][0].GetValueWidth(), inputterm[0][0],inputterm[1][0]), - nf->CreateTerm(k,inputterm[0][1].GetValueWidth(),inputterm[0][1],inputterm[1][1])); - break; + int trailingZeroes = 0; + for (int i = 0; i < output.Degree(); i++) + { + const ASTNode& n = output[i]; + if (n.GetKind() != BVCONST) + continue; + int j; + for (j = 0; j < n.GetValueWidth(); j++) + if (CONSTANTBV::BitVector_bit_test(n.GetBVConst(), j)) + break; + + if (j > trailingZeroes) + trailingZeroes = j; + } + if (trailingZeroes > 0) + { + if (trailingZeroes == output.GetValueWidth()) + output = _bm->CreateZeroConst(trailingZeroes); + else + { + //cerr << "old" << output; + ASTNode zeroes = _bm->CreateZeroConst(trailingZeroes); + ASTVec newChildren; + for (int i = 0; i < output.Degree(); i++) + newChildren.push_back( + nf->CreateTerm(BVEXTRACT, output.GetValueWidth() - trailingZeroes, output[i], + _bm->CreateBVConst(32, output.GetValueWidth() - 1), + _bm->CreateBVConst(32, trailingZeroes))); + + ASTNode newAnd = nf->CreateTerm(BVAND, output.GetValueWidth() - trailingZeroes, newChildren); + output = nf->CreateTerm(BVCONCAT, output.GetValueWidth(), newAnd, zeroes); + assert(BVTypeCheck(output)); + //cerr << "new" << output; + } + } + } - const ASTNode max = _bm->CreateMaxConst(inputValueWidth); - const ASTNode zero = _bm->CreateZeroConst(inputValueWidth); + break; + } + case BVCONCAT: + { + const ASTNode& t = inputterm[0]; + const ASTNode& u = inputterm[1]; - const ASTNode identity = (BVAND == k) ? max : zero; - const ASTNode annihilator = (BVAND == k) ? zero : max; - ASTVec c = FlattenKind(inputterm.GetKind(), inputterm.GetChildren()); - SortByArith(c); - ASTVec constants; - ASTVec o; - for (ASTVec::iterator - it = c.begin(), itend = c.end(); it != itend; it++) - { - ASTNode aaa =*it; - assert(hasBeenSimplified(aaa)); + const Kind tkind = t.GetKind(); + const Kind ukind = u.GetKind(); - if (aaa == annihilator) - { - output = annihilator; - //memoize - UpdateSimplifyMap(inputterm, output, false, VarConstMap); - UpdateSimplifyMap(actualInputterm, output, false, VarConstMap); - //cerr << "output of SimplifyTerm: " << output << endl; - return output; - } + assert(BVCONST != tkind || BVCONST != ukind); - if (o.size() > 0 && o.back() == aaa) + if (BVEXTRACT == tkind && BVEXTRACT == ukind && t[0] == u[0]) + { + //to handle the case x[m:n]@x[n-1:k] <==> x[m:k] + const ASTNode& t_hi = t[1]; + const ASTNode& t_low = t[2]; + const ASTNode& u_hi = u[1]; + const ASTNode& u_low = u[2]; + ASTNode c = BVConstEvaluator(nf->CreateTerm(BVPLUS, 32, u_hi, _bm->CreateOneConst(32))); + if (t_low == c) { - continue; // duplicate. + output = nf->CreateTerm(BVEXTRACT, inputValueWidth, t[0], t_hi, u_low); } - - // nb: There's no guarantee that the bvneg will immediately follow - // the thing it's negating if the degree > 2. - if (o.size() > 0 && aaa.GetKind() == BVNEG && o.back() == aaa[0]) + else { - output = annihilator; - UpdateSimplifyMap(inputterm, output, false, VarConstMap); - UpdateSimplifyMap(actualInputterm, output, false, VarConstMap); - return output; + output = nf->CreateTerm(BVCONCAT, inputValueWidth, t, u); } - - if (BVCONST == aaa.GetKind()) - { - constants.push_back(aaa); - } - else - { - o.push_back(aaa); - } - } - - while(constants.size() >=2) + } + else if (t.GetKind() == BVCONCAT && t[0].GetKind() != BVCONCAT) { - ASTNode a = constants.back(); - constants.pop_back(); - ASTNode b = constants.back(); - constants.pop_back(); - - ASTNode c = BVConstEvaluator(nf->CreateTerm(inputterm.GetKind(),inputterm.GetValueWidth(), a,b)); - - constants.push_back(c); + /// This makes the left hand child of every concat not a concat. + const ASTNode& left = t[0]; + ASTNode bottom = nf->CreateTerm(BVCONCAT, t[1].GetValueWidth() + u.GetValueWidth(), t[1], u); + output = nf->CreateTerm(BVCONCAT, inputValueWidth, left, bottom); + assert(BVTypeCheck(output)); } - if (constants.size() != 0 && constants.back() != identity) - o.push_back(constants.back()); - - switch (o.size()) - { - case 0: - output = identity; - break; - case 1: - output = o[0]; - break; - default: - SortByArith(o); - output = nf->CreateTerm(inputterm.GetKind(),inputterm.GetValueWidth(), o ); - break; - } - - // This don't make it faster, just makes the graphs easier to understand. - if (output.GetKind() == BVAND) - { - assert(output.Degree() != 0); - bool allconv = true; - for (ASTVec::const_iterator it = output.begin(), itend = - output.end(); it != itend; it++) - { - if (!isPropositionToTerm(*it)) - { - allconv = false; - break; - } - } - if (allconv) - { - const ASTNode zero = _bm->CreateZeroConst(1); - ASTVec children; - for (ASTVec::const_iterator it = output.begin(), itend = - output.end(); it != itend; it++) - { - const ASTNode& n = *it; - - if (n[1] == zero) - children.push_back(nf->CreateNode(NOT, n[0])); - else - children.push_back(n[0]); - } - output = nf->CreateTerm(ITE, 1, - nf->CreateNode(AND, children), _bm->CreateOneConst(1), - zero); - assert(BVTypeCheck(output)); - } - - assert(BVTypeCheck(output)); - - // If the leading bits are zero. Replace it by a concat with zero. - int i; - if (output.GetKind() == BVAND && output.Degree() ==2 && ((i=numberOfLeadingZeroes(output[0])) > 0) ) - { - // i contains the number of leading zeroes. - if (i < output.GetValueWidth()) - output = nf->CreateTerm(BVCONCAT, - output.GetValueWidth(), - _bm->CreateZeroConst(i), - nf->CreateTerm(BVAND, output.GetValueWidth() - i, - nf->CreateTerm(BVEXTRACT, - output.GetValueWidth() - i, - output[0], - _bm->CreateBVConst(32,output.GetValueWidth() - i-1), - _bm->CreateBVConst(32,0) - ), - nf->CreateTerm(BVEXTRACT, - output.GetValueWidth() - i, - output[1], - _bm->CreateBVConst(32,output.GetValueWidth() - i-1), - _bm->CreateBVConst(32,0) - )) - ); - - assert(BVTypeCheck(output)); - } - } - if (output.GetKind() == BVAND) - { - int trailingZeroes = 0; - for (int i = 0; i < output.Degree(); i++) - { - const ASTNode& n = output[i]; - if (n.GetKind() != BVCONST) - continue; - int j; - for (j = 0; j < n.GetValueWidth(); j++) - if (CONSTANTBV::BitVector_bit_test(n.GetBVConst(), j)) - break; - - if (j > trailingZeroes) - trailingZeroes = j; - } - if (trailingZeroes > 0) { - if (trailingZeroes == output.GetValueWidth()) - output = _bm->CreateZeroConst(trailingZeroes); - else { - //cerr << "old" << output; - ASTNode zeroes = _bm->CreateZeroConst(trailingZeroes); - ASTVec newChildren; - for (int i = 0; i < output.Degree(); i++) - newChildren.push_back(nf->CreateTerm(BVEXTRACT, - output.GetValueWidth() - trailingZeroes, - output[i], _bm->CreateBVConst(32, - output.GetValueWidth() - 1), - _bm->CreateBVConst(32, trailingZeroes))); - - ASTNode newAnd = nf->CreateTerm(BVAND, - output.GetValueWidth() - trailingZeroes, - newChildren); - output = nf->CreateTerm(BVCONCAT, output.GetValueWidth(), - newAnd, zeroes); - assert(BVTypeCheck(output)); - //cerr << "new" << output; - } - } - - } - - break; - } - case BVCONCAT: - { - const ASTNode& t =inputterm[0]; - const ASTNode& u =inputterm[1]; - - const Kind tkind = t.GetKind(); - const Kind ukind = u.GetKind(); - - assert (BVCONST != tkind || BVCONST != ukind); - - if (BVEXTRACT == tkind - && BVEXTRACT == ukind - && t[0] == u[0]) - { - //to handle the case x[m:n]@x[n-1:k] <==> x[m:k] - const ASTNode& t_hi = t[1]; - const ASTNode& t_low = t[2]; - const ASTNode& u_hi = u[1]; - const ASTNode& u_low = u[2]; - ASTNode c = - BVConstEvaluator(nf->CreateTerm(BVPLUS, 32, - u_hi, - _bm->CreateOneConst(32))); - if (t_low == c) - { - output = - nf->CreateTerm(BVEXTRACT, - inputValueWidth, t[0], t_hi, u_low); - } - else - { - output = nf->CreateTerm(BVCONCAT, inputValueWidth, t, u); - } - } - else if (t.GetKind() == BVCONCAT && t[0].GetKind() != BVCONCAT) - { - - /// This makes the left hand child of every concat not a concat. - const ASTNode& left= t[0]; - ASTNode bottom = nf->CreateTerm(BVCONCAT, t[1].GetValueWidth() + u.GetValueWidth(), t[1], u); - output = nf->CreateTerm(BVCONCAT, inputValueWidth, left, bottom); - assert(BVTypeCheck(output)); - } - else - { - output = nf->CreateTerm(BVCONCAT, inputValueWidth, t, u); - } - break; - } - - case BVLEFTSHIFT: - case BVRIGHTSHIFT: + else + { + output = nf->CreateTerm(BVCONCAT, inputValueWidth, t, u); + } + break; + } - { // If the shift amount is known. Then replace it by an extract. - const ASTNode a =inputterm[0]; - const ASTNode b =inputterm[1]; + case BVLEFTSHIFT: + case BVRIGHTSHIFT: + { // If the shift amount is known. Then replace it by an extract. + const ASTNode a = inputterm[0]; + const ASTNode b = inputterm[1]; - const unsigned int width = a.GetValueWidth(); - if (BVCONST == b.GetKind()) // known shift amount. - { - output = convertKnownShiftAmount(k, inputterm.GetChildren(), *_bm, nf); - } - else if (a == _bm->CreateZeroConst(width)) + const unsigned int width = a.GetValueWidth(); + if (BVCONST == b.GetKind()) // known shift amount. { - output = _bm->CreateZeroConst(width); + output = convertKnownShiftAmount(k, inputterm.GetChildren(), *_bm, nf); } - else - output = inputterm; - } - break; + else if (a == _bm->CreateZeroConst(width)) + { + output = _bm->CreateZeroConst(width); + } + else + output = inputterm; + } + break; - case BVDIV: - { + case BVDIV: + { if (inputterm[0] == inputterm[1]) { output = _bm->CreateOneConst(inputValueWidth); break; } if (inputterm[1] == _bm->CreateOneConst(inputValueWidth)) - { + { output = inputterm[0]; break; - } - ASTNode lessThan = SimplifyFormula(nf->CreateNode(BVLT, inputterm[0], inputterm[1]),false, NULL); + } + ASTNode lessThan = SimplifyFormula(nf->CreateNode(BVLT, inputterm[0], inputterm[1]), false, NULL); if (lessThan == ASTTrue) - output = _bm->CreateZeroConst(inputValueWidth); + output = _bm->CreateZeroConst(inputValueWidth); else - output = inputterm; + output = inputterm; } - break; - case BVMOD: - { - if (inputterm[0] == inputterm[1]) + break; + case BVMOD: + { + if (inputterm[0] == inputterm[1]) { output = _bm->CreateZeroConst(inputValueWidth); break; } - ASTNode lessThan = SimplifyFormula(nf->CreateNode(BVLT, inputterm[0], inputterm[1]),false, NULL); + ASTNode lessThan = SimplifyFormula(nf->CreateNode(BVLT, inputterm[0], inputterm[1]), false, NULL); - if (lessThan == ASTTrue) - output= inputterm[0]; - else - output = inputterm; - } + if (lessThan == ASTTrue) + output = inputterm[0]; + else + output = inputterm; + } break; case BVXOR: - { - if (inputterm.Degree() ==2 && inputterm[0] == inputterm[1]) - { - output = _bm->CreateZeroConst(inputterm.GetValueWidth()); - break; - } - if (inputterm.Degree() ==2 && inputterm[0].GetKind() == BVCONCAT && inputterm[1].GetKind() == BVCONCAT && inputterm[0][0].GetValueWidth() ==inputterm[1][0].GetValueWidth() ) - { - output = nf->CreateTerm(BVCONCAT, inputterm.GetValueWidth(), - nf->CreateTerm(k,inputterm[0][0].GetValueWidth(), inputterm[0][0],inputterm[1][0]), - nf->CreateTerm(k,inputterm[0][1].GetValueWidth(),inputterm[0][1],inputterm[1][1])); - break; - } - if (inputterm.Degree() ==2 && inputterm[0] == _bm->CreateZeroConst(inputterm.GetValueWidth())) - { - output = inputterm[1]; - break; - } - } - - output = inputterm; - break; - case BVXNOR: - case BVNAND: - case BVNOR: - case BVVARSHIFT: - case BVSRSHIFT: - { - output = inputterm; + { + if (inputterm.Degree() == 2 && inputterm[0] == inputterm[1]) + { + output = _bm->CreateZeroConst(inputterm.GetValueWidth()); break; - } - case READ: - { - ASTNode out1; + } + if (inputterm.Degree() == 2 && inputterm[0].GetKind() == BVCONCAT && inputterm[1].GetKind() == BVCONCAT + && inputterm[0][0].GetValueWidth() == inputterm[1][0].GetValueWidth()) + { + output = nf->CreateTerm(BVCONCAT, inputterm.GetValueWidth(), + nf->CreateTerm(k, inputterm[0][0].GetValueWidth(), inputterm[0][0], inputterm[1][0]), + nf->CreateTerm(k, inputterm[0][1].GetValueWidth(), inputterm[0][1], inputterm[1][1])); + break; + } + if (inputterm.Degree() == 2 && inputterm[0] == _bm->CreateZeroConst(inputterm.GetValueWidth())) + { + output = inputterm[1]; + break; + } + } + + output = inputterm; + break; + case BVXNOR: + case BVNAND: + case BVNOR: + case BVVARSHIFT: + case BVSRSHIFT: + { + output = inputterm; + break; + } + case READ: + { + ASTNode out1; - ASTNode array_term = SimplifyArrayTerm(inputterm[0], VarConstMap); - ASTNode read_index = SimplifyTerm(inputterm[1], VarConstMap); + ASTNode array_term = SimplifyArrayTerm(inputterm[0], VarConstMap); + ASTNode read_index = SimplifyTerm(inputterm[1], VarConstMap); - if (SYMBOL == array_term.GetKind()) - { - out1 = nf->CreateTerm(READ, inputterm.GetValueWidth(), array_term, read_index); - } - else if (WRITE == array_term.GetKind()) - { - ASTNode eq = CreateSimplifiedEQ(read_index, array_term[1]); - if (eq == ASTTrue) - out1 = array_term[2]; - else if (eq == ASTFalse) - { - out1 = nf->CreateTerm(READ, inputterm.GetValueWidth(), array_term[0], read_index); - out1 = SimplifyTerm(out1, VarConstMap); - } - else - { - out1 = nf->CreateTerm(READ, inputterm.GetValueWidth(), array_term, read_index); - } - } - else if (ITE == array_term.GetKind()) - { - // Pushes the READ through ITES, which is potentially exponential. - // At present, because there's no write refinement or similar, the - // array transformer is going to do this later anyway. So, we do it - // here. But it's ugggglly. - - ASTNode cond = - SimplifyFormula(inputterm[0][0], false, VarConstMap); - ASTNode read1 = - nf->CreateTerm(READ, - inputValueWidth, - inputterm[0][1], read_index); - ASTNode read2 = - nf->CreateTerm(READ, - inputValueWidth, - inputterm[0][2], read_index); - read1 = SimplifyTerm(read1, VarConstMap); - read2 = SimplifyTerm(read2, VarConstMap); - out1 = CreateSimplifiedTermITE(cond, read1, read2); - } - else - { - FatalError("ffff"); - } + if (SYMBOL == array_term.GetKind()) + { + out1 = nf->CreateTerm(READ, inputterm.GetValueWidth(), array_term, read_index); + } + else if (WRITE == array_term.GetKind()) + { + ASTNode eq = CreateSimplifiedEQ(read_index, array_term[1]); + if (eq == ASTTrue) + out1 = array_term[2]; + else if (eq == ASTFalse) + { + out1 = nf->CreateTerm(READ, inputterm.GetValueWidth(), array_term[0], read_index); + out1 = SimplifyTerm(out1, VarConstMap); + } + else + { + out1 = nf->CreateTerm(READ, inputterm.GetValueWidth(), array_term, read_index); + } + } + else if (ITE == array_term.GetKind()) + { + // Pushes the READ through ITES, which is potentially exponential. + // At present, because there's no write refinement or similar, the + // array transformer is going to do this later anyway. So, we do it + // here. But it's ugggglly. - assert(!out1.IsNull()); + ASTNode cond = SimplifyFormula(inputterm[0][0], false, VarConstMap); + ASTNode read1 = nf->CreateTerm(READ, inputValueWidth, inputterm[0][1], read_index); + ASTNode read2 = nf->CreateTerm(READ, inputValueWidth, inputterm[0][2], read_index); + read1 = SimplifyTerm(read1, VarConstMap); + read2 = SimplifyTerm(read2, VarConstMap); + out1 = CreateSimplifiedTermITE(cond, read1, read2); + } + else + { + FatalError("ffff"); + } - //process only if not in the substitution map. simplifymap - //has been checked already - if (!CheckSubstitutionMap(out1, out1) && out1.GetKind() == READ && WRITE == out1[0].GetKind()) - out1 = RemoveWrites_TopLevel(out1); + assert(!out1.IsNull()); - //it is possible that after all the procesing the READ term - //reduces to READ(Symbol,const) and hence we should check the - //substitutionmap once again. - if (!CheckSubstitutionMap(out1, output)) - output = out1; - break; - } - case ITE: - { - output = CreateSimplifiedTermITE(inputterm[0], inputterm[1], inputterm[2]); - break; - } - case SBVREM: - case SBVMOD: - { - if (inputterm[0] == inputterm[1]) + //process only if not in the substitution map. simplifymap + //has been checked already + if (!CheckSubstitutionMap(out1, out1) && out1.GetKind() == READ && WRITE == out1[0].GetKind()) + out1 = RemoveWrites_TopLevel(out1); + + //it is possible that after all the procesing the READ term + //reduces to READ(Symbol,const) and hence we should check the + //substitutionmap once again. + if (!CheckSubstitutionMap(out1, output)) + output = out1; + break; + } + case ITE: + { + output = CreateSimplifiedTermITE(inputterm[0], inputterm[1], inputterm[2]); + break; + } + case SBVREM: + case SBVMOD: + { + if (inputterm[0] == inputterm[1]) { output = _bm->CreateZeroConst(inputValueWidth); break; } - output = inputterm; - break; - } - case SBVDIV: - { - output = inputterm; - if (inputterm[0] == inputterm[1]) + output = inputterm; + break; + } + case SBVDIV: + { + output = inputterm; + if (inputterm[0] == inputterm[1]) { output = _bm->CreateOneConst(inputValueWidth); break; } - if (SBVDIV == output.GetKind() && output.GetChildren().size() == 2 && output.GetChildren()[0].GetKind() == BVSX && output.GetChildren()[1].GetKind() == BVSX ) - output = pullUpBVSX(output); + if (SBVDIV == output.GetKind() && output.GetChildren().size() == 2 && output.GetChildren()[0].GetKind() == BVSX + && output.GetChildren()[1].GetKind() == BVSX) + output = pullUpBVSX(output); - break; - } - case WRITE: - default: - FatalError("SimplifyTerm: Control should never reach here:", - inputterm, k); - return inputterm; break; } - assert(!output.IsNull()); + case WRITE: + default: + FatalError("SimplifyTerm: Control should never reach here:", inputterm, k); + return inputterm; + break; + }assert(!output.IsNull()); if (inputterm != output) - output = SimplifyTerm(output); + output = SimplifyTerm(output); //memoize UpdateSimplifyMap(inputterm, output, false, VarConstMap); UpdateSimplifyMap(actualInputterm, output, false, VarConstMap); @@ -3062,18 +2942,18 @@ namespace BEEV assert(inputterm.GetIndexWidth() == output.GetIndexWidth()); assert(hasBeenSimplified(output)); - #ifndef NDEBUG - for (int i =0; i < output.Degree();i++) - { - if (output[i].GetType() != ARRAY_TYPE) - if (!hasBeenSimplified(output[i])) - { - cout << output; - cout << i; - assert(hasBeenSimplified(output[i])); - } - } - #endif +#ifndef NDEBUG + for (int i = 0; i < output.Degree(); i++) + { + if (output[i].GetType() != ARRAY_TYPE) + if (!hasBeenSimplified(output[i])) + { + cout << output; + cout << i; + assert(hasBeenSimplified(output[i])); + } + } +#endif return output; } //end of SimplifyTerm() @@ -3081,7 +2961,8 @@ namespace BEEV //this function assumes that the input is a vector of childnodes of //a BVPLUS term. it combines like terms and returns a bvplus //term. e.g. 1.x + 2.x is converted to 3.x - ASTNode Simplifier::CombineLikeTerms(const ASTNode& a) + ASTNode + Simplifier::CombineLikeTerms(const ASTNode& a) { if (BVPLUS != a.GetKind()) return a; @@ -3097,10 +2978,11 @@ namespace BEEV return CombineLikeTerms(a.GetChildren()); } - ASTNode Simplifier::CombineLikeTerms(const ASTVec& c) - { - ASTNode output; - //map from variables to vector of constants + ASTNode + Simplifier::CombineLikeTerms(const ASTVec& c) + { + ASTNode output; + //map from variables to vector of constants ASTNodeToVecMap vars_to_consts; //vector to hold constants ASTVec constkids; @@ -3115,29 +2997,23 @@ namespace BEEV //go over the childnodes of the input bvplus, and collect like //terms in a map. the key of the map are the variables, and the //values are stored in a ASTVec - for (ASTVec::const_iterator - it = c.begin(), itend = c.end(); it != itend; it++) + for (ASTVec::const_iterator it = c.begin(), itend = c.end(); it != itend; it++) { const ASTNode& aaa = *it; if (SYMBOL == aaa.GetKind()) { vars_to_consts[aaa].push_back(one); } - else if (BVMULT == aaa.GetKind() - && BVUMINUS == aaa[0].GetKind() - && BVCONST == aaa[0][0].GetKind()) + else if (BVMULT == aaa.GetKind() && BVUMINUS == aaa[0].GetKind() && BVCONST == aaa[0][0].GetKind()) { //(BVUMINUS(c))*(y) <==> compute(BVUMINUS(c))*y ASTNode compute_const = BVConstEvaluator(aaa[0]); vars_to_consts[aaa[1]].push_back(compute_const); } - else if (BVMULT == aaa.GetKind() - && BVUMINUS == aaa[1].GetKind() - && BVCONST == aaa[0].GetKind()) + else if (BVMULT == aaa.GetKind() && BVUMINUS == aaa[1].GetKind() && BVCONST == aaa[0].GetKind()) { //c*(BVUMINUS(y)) <==> compute(BVUMINUS(c))*y - ASTNode cccc = - BVConstEvaluator(nf->CreateTerm(BVUMINUS, len, aaa[0])); + ASTNode cccc = BVConstEvaluator(nf->CreateTerm(BVUMINUS, len, aaa[0])); vars_to_consts[aaa[1][0]].push_back(cccc); } else if (BVMULT == aaa.GetKind() && BVCONST == aaa[0].GetKind()) @@ -3179,9 +3055,7 @@ namespace BEEV //go over the map from variables to vector of values. combine the //vector of values, multiply to the variable, and put the //resultant monomial in the output BVPLUS. - for (ASTNodeToVecMap::iterator - it = vars_to_consts.begin(), itend = vars_to_consts.end(); - it != itend; it++) + for (ASTNodeToVecMap::iterator it = vars_to_consts.begin(), itend = vars_to_consts.end(); it != itend; it++) { const ASTVec& ccc = it->second; @@ -3202,10 +3076,7 @@ namespace BEEV monom = it->first; else { - monom = - SimplifyTerm(nf->CreateTerm(BVMULT, - constant.GetValueWidth(), - constant, it->first)); + monom = SimplifyTerm(nf->CreateTerm(BVMULT, constant.GetValueWidth(), constant, it->first)); } if (zero != monom) { @@ -3215,7 +3086,7 @@ namespace BEEV if (constkids.size() > 1) { - ASTNode output = NonMemberBVConstEvaluator(_bm , BVPLUS, constkids, constkids[0].GetValueWidth()); + ASTNode output = NonMemberBVConstEvaluator(_bm, BVPLUS, constkids, constkids[0].GetValueWidth()); if (output != zero) outputvec.push_back(output); } @@ -3227,7 +3098,7 @@ namespace BEEV if (outputvec.size() > 1) { - output = nf->CreateTerm(BVPLUS, len, outputvec); + output = nf->CreateTerm(BVPLUS, len, outputvec); } else if (outputvec.size() == 1) { @@ -3247,7 +3118,8 @@ namespace BEEV //assumes that lhs and rhs have already been simplified. although //this assumption is not needed for correctness, it is essential for //performance. The function also assumes that lhs is a BVPLUS - ASTNode Simplifier::LhsMinusRhs(const ASTNode& eq) + ASTNode + Simplifier::LhsMinusRhs(const ASTNode& eq) { //if input is not an equality, simply return it if (EQ != eq.GetKind()) @@ -3259,10 +3131,7 @@ namespace BEEV const Kind k_rhs = rhs.GetKind(); //either the lhs has to be a BVPLUS or the rhs has to be a //BVPLUS - if (!(BVPLUS == k_lhs - || BVPLUS == k_rhs - || (BVMULT == k_lhs - && BVMULT == k_rhs))) + if (!(BVPLUS == k_lhs || BVPLUS == k_rhs || (BVMULT == k_lhs && BVMULT == k_rhs))) { return eq; } @@ -3283,10 +3152,9 @@ namespace BEEV ASTNode swap = lhs; lhs = rhs; rhs = swap; - // swap_flag = true; + // swap_flag = true; } - unsigned int len = lhs.GetValueWidth(); ASTNode zero = _bm->CreateZeroConst(len); //right is -1*(rhs): Simplify(-1*rhs) @@ -3312,7 +3180,7 @@ namespace BEEV } else { - lhsplusrhs = nf->CreateTerm(BVPLUS, len, lhs, rhs); + lhsplusrhs = nf->CreateTerm(BVPLUS, len, lhs, rhs); } //combine like terms @@ -3342,8 +3210,8 @@ namespace BEEV // (y1 + y2 + ...+ yn)*x <==> x*y1 + x*y2 + ... + x*yn // // The function assumes that the BVPLUSes have been flattened - ASTNode Simplifier::DistributeMultOverPlus(const ASTNode& a, - bool startdistribution) + ASTNode + Simplifier::DistributeMultOverPlus(const ASTNode& a, bool startdistribution) { if (!startdistribution) return a; @@ -3367,14 +3235,9 @@ namespace BEEV } //special case optimization: c1*(c2*t1) <==> (c1*c2)*t1 - if (BVCONST == left_kind - && BVMULT == right_kind - && BVCONST == right[0].GetKind()) - { - ASTNode c = - BVConstEvaluator(nf->CreateTerm(BVMULT, - a.GetValueWidth(), - left, right[0])); + if (BVCONST == left_kind && BVMULT == right_kind && BVCONST == right[0].GetKind()) + { + ASTNode c = BVConstEvaluator(nf->CreateTerm(BVMULT, a.GetValueWidth(), left, right[0])); c = nf->CreateTerm(BVMULT, a.GetValueWidth(), c, right[1]); return c; left = c[0]; @@ -3384,14 +3247,9 @@ namespace BEEV } //special case optimization: c1*(t1*c2) <==> (c1*c2)*t1 - if (BVCONST == left_kind - && BVMULT == right_kind - && BVCONST == right[1].GetKind()) - { - ASTNode c = - BVConstEvaluator(nf->CreateTerm(BVMULT, - a.GetValueWidth(), - left, right[1])); + if (BVCONST == left_kind && BVMULT == right_kind && BVCONST == right[1].GetKind()) + { + ASTNode c = BVConstEvaluator(nf->CreateTerm(BVMULT, a.GetValueWidth(), left, right[1])); c = nf->CreateTerm(BVMULT, a.GetValueWidth(), c, right[0]); return c; left = c[0]; @@ -3439,12 +3297,9 @@ namespace BEEV } else { - for (ASTVec::iterator - j = rightnodes.begin(), jend = rightnodes.end(); - j != jend; j++) + for (ASTVec::iterator j = rightnodes.begin(), jend = rightnodes.end(); j != jend; j++) { - ASTNode out = - SimplifyTerm(nf->CreateTerm(BVMULT, len, left, *j)); + ASTNode out = SimplifyTerm(nf->CreateTerm(BVMULT, len, left, *j)); outputvec.push_back(out); } } @@ -3454,17 +3309,12 @@ namespace BEEV ASTVec leftnodes = left.GetChildren(); // (x1 + x2 + ... + xm)*(y1 + y2 + ...+ yn) <==> x1*y1 + x1*y2 + // ... + x2*y1 + ... + xm*yn - for (ASTVec::iterator - i = leftnodes.begin(), iend = leftnodes.end(); - i != iend; i++) + for (ASTVec::iterator i = leftnodes.begin(), iend = leftnodes.end(); i != iend; i++) { ASTNode multiplier = *i; - for (ASTVec::iterator - j = rightnodes.begin(), jend = rightnodes.end(); - j != jend; j++) + for (ASTVec::iterator j = rightnodes.begin(), jend = rightnodes.end(); j != jend; j++) { - ASTNode out = - SimplifyTerm(nf->CreateTerm(BVMULT, len, multiplier, *j)); + ASTNode out = SimplifyTerm(nf->CreateTerm(BVMULT, len, multiplier, *j)); outputvec.push_back(out); } } @@ -3486,7 +3336,8 @@ namespace BEEV //converts the BVSX(len, a0) operator into ITE( check top bit, //extend a0 by 1, extend a0 by 0) - ASTNode Simplifier::ConvertBVSXToITE(const ASTNode& a) + ASTNode + Simplifier::ConvertBVSXToITE(const ASTNode& a) { if (BVSX != a.GetKind()) return a; @@ -3530,11 +3381,9 @@ namespace BEEV BEEV::ASTNode BVZeros = _bm->CreateBVConst(zeros.c_str(), 2); //string of ones BVCONCAT a0 - BEEV::ASTNode concatOnes = - nf->CreateTerm(BEEV::BVCONCAT, a_len, BVOnes, a0); + BEEV::ASTNode concatOnes = nf->CreateTerm(BEEV::BVCONCAT, a_len, BVOnes, a0); //string of zeros BVCONCAT a0 - BEEV::ASTNode concatZeros = - nf->CreateTerm(BEEV::BVCONCAT, a_len, BVZeros, a0); + BEEV::ASTNode concatZeros = nf->CreateTerm(BEEV::BVCONCAT, a_len, BVZeros, a0); //extract top bit of a0 BEEV::ASTNode hi = _bm->CreateBVConst(32, a0_len - 1); @@ -3542,8 +3391,7 @@ namespace BEEV BEEV::ASTNode topBit = nf->CreateTerm(BEEV::BVEXTRACT, 1, a0, hi, low); //compare topBit of a0 with 0bin1 - BEEV::ASTNode condition = - CreateSimplifiedEQ(_bm->CreateBVConst(1, 1), topBit); + BEEV::ASTNode condition = CreateSimplifiedEQ(_bm->CreateBVConst(1, 1), topBit); //ITE(topbit = 0bin1, 0bin1111...a0, 0bin000...a0) output = CreateSimplifiedTermITE(condition, concatOnes, concatZeros); @@ -3551,23 +3399,19 @@ namespace BEEV return output; } //end of ConvertBVSXToITE() - - ASTNode Simplifier::RemoveWrites_TopLevel(const ASTNode& term) + ASTNode + Simplifier::RemoveWrites_TopLevel(const ASTNode& term) { if (READ != term.GetKind() || WRITE != term[0].GetKind()) { FatalError("RemovesWrites: Input must be a READ over a WRITE", term); } - if (!_bm->Begin_RemoveWrites - && !_bm->SimplifyWrites_InPlace_Flag - && !_bm->start_abstracting) + if (!_bm->Begin_RemoveWrites && !_bm->SimplifyWrites_InPlace_Flag && !_bm->start_abstracting) { return term; } - else if (!_bm->Begin_RemoveWrites - && _bm->SimplifyWrites_InPlace_Flag - && !_bm->start_abstracting) + else if (!_bm->Begin_RemoveWrites && _bm->SimplifyWrites_InPlace_Flag && !_bm->start_abstracting) { //return term; return SimplifyWrites_InPlace(term); @@ -3578,60 +3422,59 @@ namespace BEEV } } //end of RemoveWrites_TopLevel() - // recursively simplify things that are of type array. - ASTNode Simplifier::SimplifyArrayTerm(const ASTNode& term, - ASTNodeMap* VarConstMap) { - - const unsigned iw = term.GetIndexWidth(); - assert(iw > 0); - - ASTNode output; - if (CheckSimplifyMap(term, output, false)) { - return output; - } + ASTNode + Simplifier::SimplifyArrayTerm(const ASTNode& term, ASTNodeMap* VarConstMap) + { - switch (term.GetKind()) { - case SYMBOL: - return term; - case ITE: { - output = CreateSimplifiedTermITE( - SimplifyFormula(term[0],VarConstMap), - SimplifyArrayTerm(term[1], VarConstMap), - SimplifyArrayTerm(term[2], VarConstMap)); - assert(output.GetIndexWidth() == iw); - } - break; - case WRITE: { - ASTNode array = SimplifyArrayTerm(term[0], VarConstMap); - ASTNode idx = SimplifyTerm(term[1]); - ASTNode val = SimplifyTerm(term[2]); + const unsigned iw = term.GetIndexWidth(); + assert(iw > 0); - output = nf->CreateArrayTerm(WRITE,iw, term.GetValueWidth(), array, idx, val); - } + ASTNode output; + if (CheckSimplifyMap(term, output, false)) + { + return output; + } - break; - default: - FatalError("2313456331"); - } + switch (term.GetKind()) + { + case SYMBOL: + return term; + case ITE: + { + output = CreateSimplifiedTermITE(SimplifyFormula(term[0], VarConstMap), SimplifyArrayTerm(term[1], VarConstMap), + SimplifyArrayTerm(term[2], VarConstMap)); + assert(output.GetIndexWidth() == iw); + } + break; + case WRITE: + { + ASTNode array = SimplifyArrayTerm(term[0], VarConstMap); + ASTNode idx = SimplifyTerm(term[1]); + ASTNode val = SimplifyTerm(term[2]); - UpdateSimplifyMap(term, output, false); - assert(term.GetIndexWidth() == output.GetIndexWidth()); - assert(BVTypeCheck(output)); - return output; - } + output = nf->CreateArrayTerm(WRITE, iw, term.GetValueWidth(), array, idx, val); + } + break; + default: + FatalError("2313456331"); + } + UpdateSimplifyMap(term, output, false); + assert(term.GetIndexWidth() == output.GetIndexWidth()); + assert(BVTypeCheck(output)); + return output; + } - ASTNode Simplifier::SimplifyWrites_InPlace(const ASTNode& term, - ASTNodeMap* VarConstMap) + ASTNode + Simplifier::SimplifyWrites_InPlace(const ASTNode& term, ASTNodeMap* VarConstMap) { ASTNodeMultiSet WriteIndicesSeenSoFar; bool SeenNonConstWriteIndex = false; - if ((READ != term.GetKind()) - || (WRITE != term[0].GetKind())) + if ((READ != term.GetKind()) || (WRITE != term[0].GetKind())) { FatalError("RemovesWrites: Input must be a READ over a WRITE", term); } @@ -3640,7 +3483,7 @@ namespace BEEV if (CheckSimplifyMap(term, output, false)) { return output; - } + } ASTVec writeIndices, writeValues; unsigned int width = term.GetValueWidth(); @@ -3651,14 +3494,13 @@ namespace BEEV do { - ASTNode writeIndex = SimplifyTerm(write[1]); + ASTNode writeIndex = SimplifyTerm(write[1]); ASTNode writeVal = SimplifyTerm(write[2]); //compare the readIndex and the current writeIndex and see if they //simplify to TRUE or FALSE or UNDETERMINABLE at this stage - ASTNode compare_readwrite_indices = - SimplifyFormula(CreateSimplifiedEQ(writeIndex, readIndex), - false, VarConstMap); + ASTNode compare_readwrite_indices = SimplifyFormula(CreateSimplifiedEQ(writeIndex, readIndex), false, + VarConstMap); //if readIndex and writeIndex are equal if (ASTTrue == compare_readwrite_indices && !SeenNonConstWriteIndex) @@ -3667,16 +3509,14 @@ namespace BEEV return writeVal; } - if (!(ASTTrue == compare_readwrite_indices - || ASTFalse == compare_readwrite_indices)) + if (!(ASTTrue == compare_readwrite_indices || ASTFalse == compare_readwrite_indices)) { SeenNonConstWriteIndex = true; } //if (readIndex=writeIndex <=> FALSE) - if (ASTFalse == compare_readwrite_indices - || (WriteIndicesSeenSoFar.find(writeIndex) - != WriteIndicesSeenSoFar.end())) + if (ASTFalse == compare_readwrite_indices + || (WriteIndicesSeenSoFar.find(writeIndex) != WriteIndicesSeenSoFar.end())) { //drop the current level write //do nothing @@ -3694,17 +3534,16 @@ namespace BEEV //Setup the write for the new iteration, one level inner write write = write[0]; - } while (WRITE == write.GetKind()); - assert(BVTypeCheck(write)); + } + while (WRITE == write.GetKind());assert(BVTypeCheck(write)); assert(write.GetIndexWidth() >0); // todo write[1] and write[2] should be simplified too. - if(ITE == write.GetKind()) + if (ITE == write.GetKind()) { - write = SimplifyArrayTerm(write,VarConstMap); + write = SimplifyArrayTerm(write, VarConstMap); } - ASTVec::reverse_iterator it_index = writeIndices.rbegin(); ASTVec::reverse_iterator itend_index = writeIndices.rend(); ASTVec::reverse_iterator it_values = writeValues.rbegin(); @@ -3720,11 +3559,11 @@ namespace BEEV output = nf->CreateTerm(READ, width, write, readIndex); assert(BVTypeCheck(output)); - if (ITE == write.GetKind()) { - output = SimplifyTerm(output, VarConstMap); - assert(BVTypeCheck(output)); - } - + if (ITE == write.GetKind()) + { + output = SimplifyTerm(output, VarConstMap); + assert(BVTypeCheck(output)); + } //UpdateSimplifyMap(original_write, write, false); UpdateSimplifyMap(term, output, false); @@ -3734,7 +3573,8 @@ namespace BEEV //accepts a read over a write and returns a term without the write //READ(WRITE(A i val) j) <==> ITE(i=j,val,READ(A,j)). We use a memo //table for this function called RemoveWritesMemoMap - ASTNode Simplifier::RemoveWrites(const ASTNode& input) + ASTNode + Simplifier::RemoveWrites(const ASTNode& input) { //unsigned int width = input.GetValueWidth(); if (READ != input.GetKind() || WRITE != input[0].GetKind()) @@ -3749,8 +3589,7 @@ namespace BEEV return output; } - if (!_bm->start_abstracting - && _bm->Begin_RemoveWrites) + if (!_bm->start_abstracting && _bm->Begin_RemoveWrites) { output = ReadOverWrite_To_ITE(input); } @@ -3760,13 +3599,12 @@ namespace BEEV ASTNode newVar; if (!CheckSimplifyMap(input, newVar, false)) { - newVar = _bm->CreateFreshVariable(0,input.GetValueWidth(),"v_solver"); + newVar = _bm->CreateFreshVariable(0, input.GetValueWidth(), "v_solver"); (*ReadOverWrite_NewName_Map)[input] = newVar; NewName_ReadOverWrite_Map[newVar] = input; UpdateSimplifyMap(input, newVar, false); - _bm->ASTNodeStats("New Var Name which replace Read_Over_Write: ", - newVar); + _bm->ASTNodeStats("New Var Name which replace Read_Over_Write: ", newVar); } output = newVar; } //end of start_abstracting if condition @@ -3776,8 +3614,8 @@ namespace BEEV return output; } //end of RemoveWrites() - ASTNode Simplifier::ReadOverWrite_To_ITE(const ASTNode& term, - ASTNodeMap* VarConstMap) + ASTNode + Simplifier::ReadOverWrite_To_ITE(const ASTNode& term, ASTNodeMap* VarConstMap) { unsigned int width = term.GetValueWidth(); ASTNode input = term; @@ -3806,10 +3644,7 @@ namespace BEEV ASTNode writeIndex = SimplifyTerm(write[1]); ASTNode writeVal = SimplifyTerm(write[2]); - ASTNode cond = - SimplifyFormula(CreateSimplifiedEQ(writeIndex, readIndex), - false, - VarConstMap); + ASTNode cond = SimplifyFormula(CreateSimplifiedEQ(writeIndex, readIndex), false, VarConstMap); ASTNode newRead = nf->CreateTerm(READ, width, writeA, readIndex); ASTNode newRead_memoized = newRead; if (CheckSimplifyMap(newRead, newRead_memoized, false)) @@ -3817,8 +3652,7 @@ namespace BEEV newRead = newRead_memoized; } - if (ASTTrue == cond - && (term == partialITE)) + if (ASTTrue == cond && (term == partialITE)) { //found the write-value in the first iteration //itself. return it @@ -3827,19 +3661,16 @@ namespace BEEV return output; } - if (READ == partialITE.GetKind() - && WRITE == partialITE[0].GetKind()) + if (READ == partialITE.GetKind() && WRITE == partialITE[0].GetKind()) { //first iteration or (previous cond==ASTFALSE and //partialITE is a "READ over WRITE") - partialITE = - CreateSimplifiedTermITE(cond, writeVal, newRead); + partialITE = CreateSimplifiedTermITE(cond, writeVal, newRead); } else if (ITE == partialITE.GetKind()) { //ITE(i1 = j, v1, R(A,j)) - ASTNode ElseITE = - CreateSimplifiedTermITE(cond, writeVal, newRead); + ASTNode ElseITE = CreateSimplifiedTermITE(cond, writeVal, newRead); //R(W(A,i1,v1),j) <==> ITE(i1 = j, v1, R(A,j)) UpdateSimplifyMap(oldRead, ElseITE, false); //ITE(i2 = j, v2, R(W(A,i1,v1),j)) <==> ITE(i2 = j, v2, @@ -3861,7 +3692,8 @@ namespace BEEV input = newRead; oldRead = newRead; - } while (READ == input.GetKind() && WRITE == input[0].GetKind()); + } + while (READ == input.GetKind() && WRITE == input[0].GetKind()); output = partialITE; @@ -3871,7 +3703,8 @@ namespace BEEV } //ReadOverWrite_To_ITE() //compute the multiplicative inverse of the input - ASTNode Simplifier::MultiplicativeInverse(const ASTNode& d) + ASTNode + Simplifier::MultiplicativeInverse(const ASTNode& d) { ASTNode c = d; if (BVCONST != c.GetKind()) @@ -3902,9 +3735,7 @@ namespace BEEV //create a '0' which is 1 bit long ASTNode onebit_zero = _bm->CreateZeroConst(1); //zero pad t0, i.e. 0 @ t0 - c = - BVConstEvaluator(nf->CreateTerm(BVCONCAT, - inputwidth + 1, onebit_zero, c)); + c = BVConstEvaluator(nf->CreateTerm(BVCONCAT, inputwidth + 1, onebit_zero, c)); //construct 2^(inputwidth), i.e. a bitvector of length //'inputwidth+1', which is max(inputwidth)+1 @@ -3912,17 +3743,12 @@ namespace BEEV //all 1's ASTNode max = _bm->CreateMaxConst(inputwidth); //zero pad max - max = - BVConstEvaluator(nf->CreateTerm(BVCONCAT, - inputwidth + 1, onebit_zero, max)); + max = BVConstEvaluator(nf->CreateTerm(BVCONCAT, inputwidth + 1, onebit_zero, max)); //_bm->Create a '1' which has leading zeros of length 'inputwidth' - ASTNode inputwidthplusone_one = - _bm->CreateOneConst(inputwidth + 1); + ASTNode inputwidthplusone_one = _bm->CreateOneConst(inputwidth + 1); //add 1 to max - max = - nf->CreateTerm(BVPLUS, inputwidth + 1, max, inputwidthplusone_one); - max = - BVConstEvaluator(max); + max = nf->CreateTerm(BVPLUS, inputwidth + 1, max, inputwidthplusone_one); + max = BVConstEvaluator(max); ASTNode zero = _bm->CreateZeroConst(inputwidth + 1); ASTNode max_bvgt_0 = nf->CreateNode(BVGT, max, zero); ASTNode quotient, remainder; @@ -3935,22 +3761,13 @@ namespace BEEV while (ASTTrue == BVConstEvaluator(max_bvgt_0)) { //quotient = (c divided by max) - quotient = - BVConstEvaluator(nf->CreateTerm(BVDIV, - inputwidth + 1, c, max)); + quotient = BVConstEvaluator(nf->CreateTerm(BVDIV, inputwidth + 1, c, max)); //remainder of (c divided by max) - remainder = - BVConstEvaluator(nf->CreateTerm(BVMOD, - inputwidth + 1, c, max)); + remainder = BVConstEvaluator(nf->CreateTerm(BVMOD, inputwidth + 1, c, max)); //x = x2 - q*x1 - x = - nf->CreateTerm(BVSUB, - inputwidth + 1, x2, - nf->CreateTerm(BVMULT, - inputwidth + 1, - quotient, x1)); + x = nf->CreateTerm(BVSUB, inputwidth + 1, x2, nf->CreateTerm(BVMULT, inputwidth + 1, quotient, x1)); x = BVConstEvaluator(x); //fix the inputs to the extended euclidian algo @@ -3973,7 +3790,8 @@ namespace BEEV } //end of MultiplicativeInverse() //returns true if the input is odd - bool Simplifier::BVConstIsOdd(const ASTNode& c) + bool + Simplifier::BVConstIsOdd(const ASTNode& c) { if (BVCONST != c.GetKind()) { @@ -3995,12 +3813,13 @@ namespace BEEV return true; } } //end of BVConstIsOdd() - + // in ext/hash_map, and tr/unordered_map, there is no provision to // shrink down the number of buckets in a hash map. If the hash_map // has previously held a lot of data, then it will have a lot of // buckets. Slowing down iterators and clears() in particular. - void Simplifier::ResetSimplifyMaps() + void + Simplifier::ResetSimplifyMaps() { // clear() is extremely expensive for hash_maps with a lot of // buckets, in the EXT_MAP implementation it visits every bucket, @@ -4017,15 +3836,21 @@ namespace BEEV SimplifyNegMap = new ASTNodeMap(INITIAL_TABLE_SIZE); } - void Simplifier::printCacheStatus() + void + Simplifier::printCacheStatus() { cerr << "SimplifyMap:" << SimplifyMap->size() << ":" << SimplifyMap->bucket_count() << endl; cerr << "SimplifyNegMap:" << SimplifyNegMap->size() << ":" << SimplifyNegMap->bucket_count() << endl; cerr << "AlwaysTrueFormSet" << AlwaysTrueHashSet.size() << ":" << AlwaysTrueHashSet.bucket_count() << endl; cerr << "MultInverseMap" << MultInverseMap.size() << ":" << MultInverseMap.bucket_count() << endl; - cerr << "ReadOverWrite_NewName_Map" << ReadOverWrite_NewName_Map->size() << ":" << ReadOverWrite_NewName_Map->bucket_count() << endl; - cerr << "NewName_ReadOverWrite_Map" << NewName_ReadOverWrite_Map.size() << ":" << NewName_ReadOverWrite_Map.bucket_count() << endl; - cerr << "substn_map" << substitutionMap.Return_SolverMap()->size() << ":" << substitutionMap.Return_SolverMap()->bucket_count() << endl; + cerr << "ReadOverWrite_NewName_Map" << ReadOverWrite_NewName_Map->size() << ":" + << ReadOverWrite_NewName_Map->bucket_count() << endl; + cerr << "NewName_ReadOverWrite_Map" << NewName_ReadOverWrite_Map.size() << ":" + << NewName_ReadOverWrite_Map.bucket_count() << endl; + cerr << "substn_map" << substitutionMap.Return_SolverMap()->size() << ":" + << substitutionMap.Return_SolverMap()->bucket_count() << endl; } //printCacheStatus() -};//end of namespace +} +; +//end of namespace -- 2.47.3