#include "../AST/AST.h"
#include "../AST/ASTUtil.h"
namespace BEEV {
-
- bool BeevMgr::CheckSimplifyMap(const ASTNode& key,
+
+ bool BeevMgr::CheckSimplifyMap(const ASTNode& key,
ASTNode& output, bool pushNeg) {
ASTNodeMap::iterator it, itend;
it = pushNeg ? SimplifyNegMap->find(key) : SimplifyMap->find(key);
itend = pushNeg ? SimplifyNegMap->end() : SimplifyMap->end();
-
+
if(it != itend) {
output = it->second;
CountersAndStats("Successful_CheckSimplifyMap");
}
if(pushNeg && (it = SimplifyMap->find(key)) != SimplifyMap->end()) {
- output =
- (ASTFalse == it->second) ?
- ASTTrue :
+ output =
+ (ASTFalse == it->second) ?
+ ASTTrue :
(ASTTrue == it->second) ? ASTFalse : CreateNode(NOT, it->second);
CountersAndStats("2nd_Successful_CheckSimplifyMap");
return true;
return false;
}
-
+
void BeevMgr::UpdateSimplifyMap(const ASTNode& key, const ASTNode& value, bool pushNeg) {
- if(pushNeg)
+ if(pushNeg)
(*SimplifyNegMap)[key] = value;
else
(*SimplifyMap)[key] = value;
}
return false;
}
-
+
bool BeevMgr::CheckSubstitutionMap(const ASTNode& key) {
- if(SolverMap.find(key) != SolverMap.end())
+ if(SolverMap.find(key) != SolverMap.end())
return true;
else
return false;
}
-
+
bool BeevMgr::UpdateSubstitutionMap(const ASTNode& e0, const ASTNode& e1) {
int i = TermOrder(e0,e1);
if(0 == i)
return false;
//e0 is of the form READ(Arr,const), and e1 is const, or
- //e0 is of the form var, and e1 is const
+ //e0 is of the form var, and e1 is const
if(1 == i && !CheckSubstitutionMap(e0)) {
SolverMap[e0] = e1;
return true;
}
-
+
//e1 is of the form READ(Arr,const), and e0 is const, or
//e1 is of the form var, and e0 is const
- if (-1 == i && !CheckSubstitutionMap(e1)) {
+ if (-1 == i && !CheckSubstitutionMap(e1)) {
SolverMap[e1] = e0;
return true;
}
bool BeevMgr::CheckAlwaysTrueFormMap(const ASTNode& key) {
ASTNodeSet::iterator it = AlwaysTrueFormMap.find(key);
ASTNodeSet::iterator itend = AlwaysTrueFormMap.end();
-
+
if(it != itend) {
//cerr << "found:" << *it << endl;
CountersAndStats("Successful_CheckAlwaysTrueFormMap");
return true;
}
-
+
return false;
}
-
+
void BeevMgr::UpdateAlwaysTrueFormMap(const ASTNode& key) {
AlwaysTrueFormMap.insert(key);
}
//a is of the form READ(Arr,const), and b is const, or
//a is of the form var, and b is const
- if((k1 == READ
- &&
- a[0].GetKind() == SYMBOL &&
+ if((k1 == READ
+ &&
+ a[0].GetKind() == SYMBOL &&
a[1].GetKind() == BVCONST
)
- &&
+ &&
(k2 == BVCONST)
)
return 1;
- if(SYMBOL == k1)
+ if(SYMBOL == k1)
return 1;
//b is of the form READ(Arr,const), and a is const, or
if((k1 == BVCONST)
&&
((k2 == READ
- &&
+ &&
b[0].GetKind() == SYMBOL &&
b[1].GetKind() == BVCONST
- )
+ )
))
return -1;
- if(SYMBOL == k2)
+ if(SYMBOL == k2)
return -1;
return 0;
//the arrayname, and vlaue is a vector of read-indices.
//
//fill the arrayname_readindices vector if e0 is a READ(Arr,index)
- //and index is a BVCONST.
+ //and index is a BVCONST.
//
//Since these arrayreads are being nuked and recorded in the
//substitutionmap, we have to also record the fact that each
if(BOOLEAN_TYPE != b.GetType()) {
FatalError(" SimplifyFormula: You have input a nonformula kind: ",ASTUndefined,kind);
}
-
+
ASTNode a = b;
ASTVec ca = a.GetChildren();
- if(!(IMPLIES == kind ||
+ if(!(IMPLIES == kind ||
ITE == kind ||
isAtomic(kind))) {
SortByArith(ca);
UpdateSimplifyMap(a,output, pushNeg);
return output;
}
-
- ASTNode BeevMgr::SimplifyAtomicFormula(const ASTNode& a, bool pushNeg) {
+
+ ASTNode BeevMgr::SimplifyAtomicFormula(const ASTNode& a, bool pushNeg) {
if(!optimize) {
return a;
}
if(!CheckSolverMap(a,output)) {
output = a;
}
- output = pushNeg ? CreateNode(NOT,output) : output;
+ output = pushNeg ? CreateNode(NOT,output) : output;
break;
case BVGETBIT: {
ASTNode term = SimplifyTerm(a[0]);
output = pushNeg ? ASTTrue : ASTFalse;
else
output = pushNeg ? CreateNode(NOT,output) : output;
- break;
- }
+ break;
+ }
case NEQ: {
output = CreateSimplifiedEQ(left,right);
output = LhsMinusRhs(output);
case BVSGT:
case BVSGE: {
//output = CreateNode(kind,left,right);
- //output = pushNeg ? CreateNode(NOT,output) : output;
+ //output = pushNeg ? CreateNode(NOT,output) : output;
output = CreateSimplifiedINEQ(kind,left,right,pushNeg);
break;
}
default:
FatalError("SimplifyAtomicFormula: NO atomic formula of the kind: ",ASTUndefined,kind);
- break;
+ break;
}
//memoize
return output;
} //end of SimplifyAtomicFormula()
- ASTNode BeevMgr::CreateSimplifiedINEQ(Kind k,
- const ASTNode& left,
- const ASTNode& right,
+ ASTNode BeevMgr::CreateSimplifiedINEQ(Kind k,
+ const ASTNode& left,
+ const ASTNode& right,
bool pushNeg) {
ASTNode output;
if(BVCONST == left.GetKind() && BVCONST == right.GetKind()) {
Kind k2 = in2.GetKind();
if(in1 == in2) {
//terms are syntactically the same
- output = ASTTrue;
+ output = ASTTrue;
}
else if(BVCONST == k1 && BVCONST == k2) {
//here the terms are definitely not syntactically equal but may
//be semantically equal.
output = ASTFalse;
}
- else if(ITE == k1 &&
- BVCONST == in1[1].GetKind() &&
+ 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:
//
// similarly ITE(cond,c,d) = c <=> cond
//
- // c = ITE(cond,d,c) <=> NOT(cond)
+ // c = ITE(cond,d,c) <=> NOT(cond)
//
//similarly ITE(cond,d,c) = d <=> NOT(cond)
ASTNode cond = in1[0];
}
else {
//last resort is to CreateNode
- output = CreateNode(EQ,in1,in2);
- }
- }
- else if(ITE == k2 &&
- BVCONST == in2[1].GetKind() &&
+ output = CreateNode(EQ,in1,in2);
+ }
+ }
+ else if(ITE == k2 &&
+ BVCONST == in2[1].GetKind() &&
BVCONST == in2[2].GetKind() && BVCONST == k1) {
ASTNode cond = in2[0];
if(in2[1] == in1) {
}
else {
//last resort is to CreateNode
- output = CreateNode(EQ,in1,in2);
- }
+ output = CreateNode(EQ,in1,in2);
+ }
}
else {
//last resort is to CreateNode
- output = CreateNode(EQ,in1,in2);
+ output = CreateNode(EQ,in1,in2);
}
-
+
UpdateSimplifyMap(in,output,false);
return output;
} //End of ITEOpts_InEqs()
//Tries to simplify the input to TRUE/FALSE. if it fails, then
//return the constructed equality
ASTNode BeevMgr::CreateSimplifiedEQ(const ASTNode& in1, const ASTNode& in2) {
- CountersAndStats("CreateSimplifiedEQ");
+ CountersAndStats("CreateSimplifiedEQ");
Kind k1 = in1.GetKind();
Kind k2 = in2.GetKind();
if(!optimize) {
return CreateNode(EQ,in1,in2);
}
-
+
if(in1 == in2)
//terms are syntactically the same
- return ASTTrue;
-
+ return ASTTrue;
+
//here the terms are definitely not syntactically equal but may be
- //semantically equal.
+ //semantically equal.
if(BVCONST == k1 && BVCONST == k2)
return ASTFalse;
-
- // can concat have multiple children?
- // so (= (concat bv1[24] x ) bv0[32]) == false
- if((BVCONCAT==k1 && BVCONST== k2) ||(BVCONCAT==k2 && BVCONST== k1) )
- {
- ASTNode concat = (k1 == BVCONCAT)? in1: in2;
- ASTNode constant = (k1 == BVCONST)? in1: in2;
-
- if(concat.GetChildren().size() == 2 &&
- (BVCONST == concat.GetChildren()[0].GetKind() || BVCONST == concat.GetChildren()[1].GetKind()))
- {
- int start;
- CBV partial;
- int partialWidth;
- ASTNode other;
-
- if (BVCONST == concat.GetChildren()[0].GetKind())
- {
- start = concat.GetChildren()[1].GetValueWidth();
- partial = concat.GetChildren()[0].GetBVConst();
- partialWidth = concat.GetChildren()[0].GetValueWidth();
- other = concat.GetChildren()[1];
- }
- else
- {
- start = 0;
- partial = concat.GetChildren()[1].GetBVConst();
- partialWidth = concat.GetChildren()[1].GetValueWidth();
- other = concat.GetChildren()[0];
- }
-
- CBV complete = constant.GetBVConst();
-
- for (int i = 0; i < partialWidth; i++)
- if (CONSTANTBV::BitVector_bit_test(partial,i) != CONSTANTBV::BitVector_bit_test(complete,i+start))
- return ASTFalse;
-
- // if we get to here then the two constants in the equality are the same. Remove the constants.
-
- return CreateNode(EQ,other,CreateTerm(BVEXTRACT,other.GetValueWidth(),constant,CreateBVConst(32, partialWidth+other.GetValueWidth()-1),CreateBVConst(32,partialWidth)));
- }
- }
-
+
+
//last resort is to CreateNode
return CreateNode(EQ,in1,in2);
}
-
+
//accepts cond == t1, then part is t2, and else part is t3
- ASTNode BeevMgr::CreateSimplifiedTermITE(const ASTNode& in0,
+ ASTNode BeevMgr::CreateSimplifiedTermITE(const ASTNode& in0,
const ASTNode& in1, const ASTNode& in2) {
ASTNode t0 = in0;
ASTNode t1 = in1;
if(t0 == ASTTrue)
return t1;
if (t0 == ASTFalse)
- return t2;
+ return t2;
if(t1 == t2)
- return t1;
+ return t1;
if(CheckAlwaysTrueFormMap(t0)) {
return t1;
- }
- if(CheckAlwaysTrueFormMap(CreateNode(NOT,t0)) ||
+ }
+ if(CheckAlwaysTrueFormMap(CreateNode(NOT,t0)) ||
(NOT == t0.GetKind() && CheckAlwaysTrueFormMap(t0[0]))) {
return t2;
}
-
+
return CreateTerm(ITE,t1.GetValueWidth(),t0,t1,t2);
}
Kind k = a.GetKind();
bool isAnd = (k == AND) ? true : false;
- ASTNode annihilator = isAnd ?
- (pushNeg ? ASTTrue : ASTFalse):
+ ASTNode annihilator = isAnd ?
+ (pushNeg ? ASTTrue : ASTFalse):
(pushNeg ? ASTFalse : ASTTrue);
- ASTNode identity = isAnd ?
- (pushNeg ? ASTFalse : ASTTrue):
+ ASTNode identity = isAnd ?
+ (pushNeg ? ASTFalse : ASTTrue):
(pushNeg ? ASTTrue : ASTFalse);
//do the work
ASTNode aaa = *i;
next_it = i+1;
bool nextexists = (next_it < iend);
-
+
aaa = SimplifyFormula(aaa,pushNeg);
if(annihilator == aaa) {
//memoize
ASTNode bbb = ASTFalse;
if(nextexists) {
bbb = SimplifyFormula(*next_it,pushNeg);
- }
+ }
if(nextexists && bbb == aaa) {
//skip the duplicate aaa. *next_it will be included
}
- else if(nextexists &&
+ else if(nextexists &&
((bbb.GetKind() == NOT && bbb[0] == aaa))) {
//memoize
UpdateSimplifyMap(a, annihilator,pushNeg);
// //drop identites
}
else if((!isAnd && !pushNeg) ||
- (isAnd && pushNeg)) {
- outvec.push_back(aaa);
+ (isAnd && pushNeg)) {
+ outvec.push_back(aaa);
}
else if((isAnd && !pushNeg) ||
(!isAnd && pushNeg)) {
- outvec.push_back(aaa);
+ outvec.push_back(aaa);
}
else {
outvec.push_back(aaa);
switch(outvec.size()) {
case 0: {
- //only identities were dropped
+ //only identities were dropped
output = identity;
break;
}
break;
}
default: {
- output = (isAnd) ?
- (pushNeg ? CreateNode(OR,outvec) : CreateNode(AND,outvec)):
+ output = (isAnd) ?
+ (pushNeg ? CreateNode(OR,outvec) : CreateNode(AND,outvec)):
(pushNeg ? CreateNode(AND,outvec) : CreateNode(OR,outvec));
//output = FlattenOneLevel(output);
break;
if(CheckSimplifyMap(a,output,pushNeg))
return output;
- if(!(a.Degree() == 1 && NOT == a.GetKind()))
+ if(!(a.Degree() == 1 && NOT == a.GetKind()))
FatalError("SimplifyNotFormula: input vector with more than 1 node",ASTUndefined);
//if pushNeg is set then there is NOT on top
}
ASTNode a0 = SimplifyFormula(a[0],false);
- ASTNode a1 = SimplifyFormula(a[1],false);
+ ASTNode a1 = SimplifyFormula(a[1],false);
output = pushNeg ? CreateNode(IFF,a0,a1) : CreateNode(XOR,a0,a1);
-
+
if(XOR == output.GetKind()) {
a0 = output[0];
a1 = output[1];
if(!(a.Degree()==2 && IMPLIES==a.GetKind()))
FatalError("SimplifyImpliesFormula: vector with wrong num of nodes",ASTUndefined);
-
+
ASTNode c0,c1;
if(pushNeg) {
c0 = SimplifyFormula(a[0],false);
if(!(a.Degree()==2 && IFF==a.GetKind()))
FatalError("SimplifyIffFormula: vector with wrong num of nodes",ASTUndefined);
-
+
ASTNode c0 = a[0];
ASTNode c1 = SimplifyFormula(a[1],false);
if(pushNeg)
c0 = SimplifyFormula(c0,true);
- else
+ else
c0 = SimplifyFormula(c0,false);
if(ASTTrue == c0) {
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);
ASTNode t1,t2;
t1 = SimplifyFormula(a[1],false);
t2 = SimplifyFormula(a[2],false);
}
-
+
if(ASTTrue == t0) {
output = t1;
}
//memoize
UpdateSimplifyMap(a,output,pushNeg);
- return output;
+ return output;
}
//one level deep flattening
ASTNode BeevMgr::FlattenOneLevel(const ASTNode& a) {
Kind k = a.GetKind();
- if(!(BVPLUS == k ||
+ if(!(BVPLUS == k ||
AND == k || OR == k
- //|| BVAND == k
+ //|| BVAND == k
//|| BVOR == k
)
) {
return a;
}
-
+
ASTNode output;
// if(CheckSimplifyMap(a,output,false)) {
// //check memo table
o.insert(o.end(),ac.begin(),ac.end());
}
else
- o.push_back(aaa);
- }
-
+ o.push_back(aaa);
+ }
+
if(is_Form_kind(k))
output = CreateNode(k,o);
else
//########################################
//########################################
- Kind k = inputterm.GetKind();
+ Kind k = inputterm.GetKind();
if(!is_Term_kind(k)) {
FatalError("SimplifyTerm: You have input a Non-term",ASTUndefined);
}
break;
case BVMULT:
{
- if(2 != inputterm.Degree())
+ if(2 != inputterm.Degree())
{
FatalError("SimplifyTerm: We assume that BVMULT is binary",inputterm);
}
-
+
// Described nicely by Warren, Hacker's Delight pg 135.
// Turn sequences of one bits into subtractions.
// 28*x == 32x - 4x (two instructions), rather than 16x+ 8x+ 4x.
- // When fully implemented. I.e. supporting sequences of 1 anywhere.
+ // When fully implemented. I.e. supporting sequences of 1 anywhere.
// Other simplifications will try to fold these back in. So need to be careful
- // about when the simplifications are applied. But in this version it won't
- // be simplified down by anything else.
+ // about when the simplifications are applied. But in this version it won't
+ // be simplified down by anything else.
+
-
// This (temporary) version only simplifies if all the left most bits are set.
// All the leftmost bits being set simplifies very nicely down.
const ASTNode& n0 = inputterm.GetChildren()[0];
const ASTNode& n1 = inputterm.GetChildren()[1];
-
+
if (BVCONST == n0.GetKind() ^ BVCONST == n1.GetKind())
{
CBV constant = (BVCONST == n0.GetKind())? n0.GetBVConst(): n1.GetBVConst();
ASTNode other = (BVCONST == n0.GetKind())? n1: n0;
-
+
int startSequence = 0;
for (unsigned int i = 0; i < inputValueWidth; i++)
{
if (!CONSTANTBV::BitVector_bit_test(constant,i))
startSequence = i;
}
-
+
if((inputValueWidth - startSequence) > 3)
{
// turn off all bits from "startSequence to the end", then add one.
}
CONSTANTBV::BitVector_increment(maskedPlusOne);
ASTNode temp = CreateTerm(BVMULT,inputValueWidth, CreateBVConst(maskedPlusOne,inputValueWidth),other);
- output = CreateTerm(BVNEG, inputValueWidth, temp);
+ output = CreateTerm(BVNEG, inputValueWidth, temp);
}
}
- if(NULL == output)
- output = inputterm;
-
+
}
- break;
-
+ if(NULL != output)
+ break;
+
case BVPLUS:{
-
+
ASTVec c = FlattenOneLevel(inputterm).GetChildren();
SortByArith(c);
ASTVec constkids, nonconstkids;
nonconstkids.push_back(aaa);
}
}
-
+
ASTNode one = CreateOneConst(inputValueWidth);
ASTNode max = CreateMaxConst(inputValueWidth);
ASTNode zero = CreateZeroConst(inputValueWidth);
if(1 == constkids.size()) {
//only one element in constkids
constoutput = constkids[0];
- }
+ }
else if (1 < constkids.size()) {
//many elements in constkids. simplify it
constoutput = CreateTerm(k,inputterm.GetValueWidth(),constkids);
if(BVMULT == k && zero == constoutput) {
output = zero;
}
- else if(BVMULT == k &&
- 1 == nonconstkids.size() &&
+ 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 = constoutput;
}
}
- if(BVMULT == output.GetKind()
+ if(BVMULT == output.GetKind()
|| BVPLUS == output.GetKind()
) {
ASTVec d = output.GetChildren();
output = CreateTerm(BVMULT,l,a0[0],a0[1][0]);
}
else {
- ASTNode a00 = SimplifyTerm(CreateTerm(BVUMINUS,l,a0[0]));
+ ASTNode a00 = SimplifyTerm(CreateTerm(BVUMINUS,l,a0[0]));
output = CreateTerm(BVMULT,l,a00,a0[1]);
}
break;
o.push_back(aaa);
}
//simplify the bvplus
- output = SimplifyTerm(CreateTerm(BVPLUS,l,o));
+ output = SimplifyTerm(CreateTerm(BVPLUS,l,o));
break;
}
case BVSUB: {
ASTNode a0 = SimplifyTerm(inputterm[0]);
Kind k1 = a0.GetKind();
unsigned int a_len = inputValueWidth;
-
+
//indices for BVEXTRACT
ASTNode i = inputterm[1];
ASTNode j = inputterm[2];
break;
}
case BVPLUS:
- case BVMULT: {
+ 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();
aaa = SimplifyTerm(CreateTerm(BVEXTRACT,i_val+1,aaa,i,zero));
o.push_back(aaa);
}
- output = CreateTerm(a0.GetKind(),i_val+1,o);
+ output = CreateTerm(a0.GetKind(),i_val+1,o);
if(j_val != 0) {
//add extraction only if j is not zero
output = CreateTerm(BVEXTRACT,a_len,output,i,j);
break;
}
// case BVSX:{
-// //(BVSX(t,n)[i:j] <==> BVSX(t,i+1), if n >= i+1 and j=0
+// //(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:"
+// FatalError("SimplifyTerm: BVEXTRACT over BVSX:"
// "the length of BVSX term must be greater than extract-len",inputterm);
// }
// if(j != zero) {
-// output = CreateTerm(BVEXTRACT,a_len,a0,i,j);
+// output = CreateTerm(BVEXTRACT,a_len,a0,i,j);
// }
// else {
// output = CreateTerm(BVSX,a_len,t,CreateBVConst(32,a_len));
// ASTNode cond = a0[0];
// ASTNode thenpart = SimplifyTerm(CreateTerm(BVNEG,len,a0[1]));
// ASTNode elsepart = SimplifyTerm(CreateTerm(BVNEG,len,a0[2]));
-// output = CreateSimplifiedTermITE(cond,thenpart,elsepart);
+// output = CreateSimplifiedTermITE(cond,thenpart,elsepart);
// break;
// }
default:
ASTNode a1 = inputterm[1];
//output length of the BVSX term
unsigned len = inputValueWidth;
-
+
if(a0.GetValueWidth() == len) {
//nothing to signextend
return a0;
CreateTerm(BVSX,len,a0[0],a1),
CreateTerm(BVSX,len,a0[1],a1));
break;
- case BVPLUS: {
+ case BVPLUS: {
//BVSX(m,BVPLUS(n,BVSX(t1),BVSX(t2))) <==> BVPLUS(m,BVSX(m,t1),BVSX(m,t2))
ASTVec c = a0.GetChildren();
bool returnflag = false;
default:
output = CreateTerm(BVSX,len,a0,a1);
break;
- }
+ }
break;
}
case BVAND:
//cerr << "output of SimplifyTerm: " << output << endl;
return output;
}
-
+
if(aaa != identity) {
o.push_back(aaa);
}
}
-
+
switch(o.size()) {
case 0:
output = identity;
output = CreateTerm(k,inputValueWidth,o);
if(constant) {
output = BVConstEvaluator(output);
- }
+ }
break;
}
break;
ASTNode u = SimplifyTerm(inputterm[1]);
Kind tkind = t.GetKind();
Kind ukind = u.GetKind();
-
-
+
+
if(BVCONST == tkind && BVCONST == ukind) {
output = BVConstEvaluator(CreateTerm(BVCONCAT,inputValueWidth,t,u));
}
- else if(BVEXTRACT == tkind &&
- BVEXTRACT == ukind &&
+ else if(BVEXTRACT == tkind &&
+ BVEXTRACT == ukind &&
t[0] == u[0]) {
//to handle the case x[m:n]@x[n-1:k] <==> x[m:k]
ASTNode t_hi = t[1];
ASTNode read1 = CreateTerm(READ,inputValueWidth,inputterm[0][1],index);
ASTNode read2 = CreateTerm(READ,inputValueWidth,inputterm[0][2],index);
-
+
read1 = SimplifyTerm(read1);
read2 = SimplifyTerm(read2);
out1 = CreateSimplifiedTermITE(cond,read1,read2);
//arr is a SYMBOL for sure
ASTNode arr = inputterm[0];
ASTNode index = SimplifyTerm(inputterm[1]);
- out1 = CreateTerm(READ,inputValueWidth,arr,index);
+ out1 = CreateTerm(READ,inputValueWidth,arr,index);
}
}
//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.
+ //substitutionmap once again.
if(!CheckSubstitutionMap(out1,output))
- output = out1;
+ output = out1;
break;
}
case ITE: {
ASTNode t0 = SimplifyFormula(inputterm[0],false);
ASTNode t1 = SimplifyTerm(inputterm[1]);
ASTNode t2 = SimplifyTerm(inputterm[2]);
- output = CreateSimplifiedTermITE(t0,t1,t2);
+ output = CreateSimplifiedTermITE(t0,t1,t2);
break;
}
case SBVREM:
output = CreateTerm(k,inputValueWidth,o);
break;
}
- case WRITE:
+ case WRITE:
default:
FatalError("SimplifyTerm: Control should never reach here:", inputterm, k);
return inputterm;
break;
}
assert(NULL != output);
-
+
//memoize
UpdateSimplifyMap(inputterm,output,false);
return SimplifyTermAux(output);
}
- Kind k = inputterm.GetKind();
+ Kind k = inputterm.GetKind();
if(!is_Term_kind(k)) {
FatalError("SimplifyTerm: You have input a Non-term",ASTUndefined);
}
if(BVMULT == k && 2 != inputterm.Degree()) {
FatalError("SimplifyTerm: We assume that BVMULT is binary",inputterm);
}
-
+
ASTVec c = FlattenOneLevel(inputterm).GetChildren();
SortByArith(c);
ASTVec constkids, nonconstkids;
nonconstkids.push_back(aaa);
}
}
-
+
ASTNode one = CreateOneConst(inputValueWidth);
ASTNode max = CreateMaxConst(inputValueWidth);
ASTNode zero = CreateZeroConst(inputValueWidth);
if(1 == constkids.size()) {
//only one element in constkids
constoutput = constkids[0];
- }
+ }
else if (1 < constkids.size()) {
//many elements in constkids. simplify it
constoutput = CreateTerm(k,inputterm.GetValueWidth(),constkids);
if(BVMULT == k && zero == constoutput) {
output = zero;
}
- else if(BVMULT == k &&
- 1 == nonconstkids.size() &&
+ 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 = constoutput;
}
}
- if(BVMULT == output.GetKind()
+ if(BVMULT == output.GetKind()
|| BVPLUS == output.GetKind()
) {
ASTVec d = output.GetChildren();
output = CreateTerm(BVMULT,l,a0[0],a0[1][0]);
}
else {
- ASTNode a00 = SimplifyTerm(CreateTerm(BVUMINUS,l,a0[0]));
+ ASTNode a00 = SimplifyTerm(CreateTerm(BVUMINUS,l,a0[0]));
output = CreateTerm(BVMULT,l,a00,a0[1]);
}
break;
o.push_back(aaa);
}
//simplify the bvplus
- output = SimplifyTerm(CreateTerm(BVPLUS,l,o));
+ output = SimplifyTerm(CreateTerm(BVPLUS,l,o));
break;
}
case BVSUB: {
ASTNode a0 = SimplifyTerm(inputterm[0]);
Kind k1 = a0.GetKind();
unsigned int a_len = inputValueWidth;
-
+
//indices for BVEXTRACT
ASTNode i = inputterm[1];
ASTNode j = inputterm[2];
break;
}
case BVPLUS:
- case BVMULT: {
+ 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();
aaa = SimplifyTerm(CreateTerm(BVEXTRACT,i_val+1,aaa,i,zero));
o.push_back(aaa);
}
- output = CreateTerm(a0.GetKind(),i_val+1,o);
+ output = CreateTerm(a0.GetKind(),i_val+1,o);
if(j_val != 0) {
//add extraction only if j is not zero
output = CreateTerm(BVEXTRACT,a_len,output,i,j);
break;
}
// case BVSX:{
-// //(BVSX(t,n)[i:j] <==> BVSX(t,i+1), if n >= i+1 and j=0
+// //(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:"
+// FatalError("SimplifyTerm: BVEXTRACT over BVSX:"
// "the length of BVSX term must be greater than extract-len",inputterm);
// }
// if(j != zero) {
-// output = CreateTerm(BVEXTRACT,a_len,a0,i,j);
+// output = CreateTerm(BVEXTRACT,a_len,a0,i,j);
// }
// else {
// output = CreateTerm(BVSX,a_len,t,CreateBVConst(32,a_len));
// ASTNode cond = a0[0];
// ASTNode thenpart = SimplifyTerm(CreateTerm(BVNEG,len,a0[1]));
// ASTNode elsepart = SimplifyTerm(CreateTerm(BVNEG,len,a0[2]));
-// output = CreateSimplifiedTermITE(cond,thenpart,elsepart);
+// output = CreateSimplifiedTermITE(cond,thenpart,elsepart);
// break;
// }
default:
ASTNode a1 = inputterm[1];
//output length of the BVSX term
unsigned len = inputValueWidth;
-
+
if(a0.GetValueWidth() == len) {
//nothing to signextend
return a0;
CreateTerm(BVSX,len,a0[0],a1),
CreateTerm(BVSX,len,a0[1],a1));
break;
- case BVPLUS: {
+ case BVPLUS: {
//BVSX(m,BVPLUS(n,BVSX(t1),BVSX(t2))) <==> BVPLUS(m,BVSX(m,t1),BVSX(m,t2))
ASTVec c = a0.GetChildren();
bool returnflag = false;
default:
output = CreateTerm(BVSX,len,a0,a1);
break;
- }
+ }
break;
}
case BVAND:
output = annihilator;
return output;
}
-
+
if(aaa != identity) {
o.push_back(aaa);
}
}
-
+
switch(o.size()) {
case 0:
output = identity;
output = CreateTerm(k,inputValueWidth,o);
if(constant) {
output = BVConstEvaluator(output);
- }
+ }
break;
}
break;
ASTNode u = SimplifyTerm(inputterm[1]);
Kind tkind = t.GetKind();
Kind ukind = u.GetKind();
-
-
+
+
if(BVCONST == tkind && BVCONST == ukind) {
output = BVConstEvaluator(CreateTerm(BVCONCAT,inputValueWidth,t,u));
}
- else if(BVEXTRACT == tkind &&
- BVEXTRACT == ukind &&
+ else if(BVEXTRACT == tkind &&
+ BVEXTRACT == ukind &&
t[0] == u[0]) {
//to handle the case x[m:n]@x[n-1:k] <==> x[m:k]
ASTNode t_hi = t[1];
ASTNode read1 = CreateTerm(READ,inputValueWidth,inputterm[0][1],index);
ASTNode read2 = CreateTerm(READ,inputValueWidth,inputterm[0][2],index);
-
+
read1 = SimplifyTerm(read1);
read2 = SimplifyTerm(read2);
out1 = CreateSimplifiedTermITE(cond,read1,read2);
//arr is a SYMBOL for sure
ASTNode arr = inputterm[0];
ASTNode index = SimplifyTerm(inputterm[1]);
- out1 = CreateTerm(READ,inputValueWidth,arr,index);
+ out1 = CreateTerm(READ,inputValueWidth,arr,index);
}
}
//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.
+ //substitutionmap once again.
if(!CheckSubstitutionMap(out1,output))
- output = out1;
+ output = out1;
break;
}
case ITE: {
ASTNode t0 = SimplifyFormula(inputterm[0],false);
ASTNode t1 = SimplifyTerm(inputterm[1]);
ASTNode t2 = SimplifyTerm(inputterm[2]);
- output = CreateSimplifiedTermITE(t0,t1,t2);
+ output = CreateSimplifiedTermITE(t0,t1,t2);
break;
}
case SBVREM:
output = CreateTerm(k,inputValueWidth,o);
break;
}
- case WRITE:
+ case WRITE:
default:
FatalError("SimplifyTermAux: Control should never reach here:", inputterm, k);
return inputterm;
}
return output;
- }
+ }
//At the end of each simplification call, we want the output to be
//always smaller or equal to the input in size.
ASTNode BeevMgr::CombineLikeTerms(const ASTNode& a) {
if(BVPLUS != a.GetKind())
return a;
-
+
ASTNode output;
if(CheckSimplifyMap(a,output,false)) {
//check memo table
//cerr << "output of SimplifyTerm Cache: " << output << endl;
return output;
}
-
+
const ASTVec& c = a.GetChildren();
//map from variables to vector of constants
ASTNodeToVecMap vars_to_consts;
if(SYMBOL == aaa.GetKind()) {
vars_to_consts[aaa].push_back(one);
}
- else if(BVMULT == aaa.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() &&
+ else if(BVMULT == aaa.GetKind() &&
BVUMINUS == aaa[1].GetKind() &&
BVCONST == aaa[0].GetKind()) {
//c*(BVUMINUS(y)) <==> compute(BVUMINUS(c))*y
ASTNode cccc = BVConstEvaluator(CreateTerm(BVUMINUS,len,aaa[0]));
- vars_to_consts[aaa[1][0]].push_back(cccc);
- }
+ vars_to_consts[aaa[1][0]].push_back(cccc);
+ }
else if(BVMULT == aaa.GetKind() && BVCONST == aaa[0].GetKind()) {
//assumes that BVMULT is binary
vars_to_consts[aaa[1]].push_back(aaa[0]);
- }
+ }
else if(BVMULT == aaa.GetKind() && BVUMINUS == aaa[0].GetKind()) {
//(-1*x)*(y) <==> -1*(xy)
ASTNode cccc = CreateTerm(BVMULT,len,aaa[0][0],aaa[1]);
ASTNode cccc = CreateTerm(BVMULT,len,aaa[0],aaa[1][0]);
ASTVec cNodes = cccc.GetChildren();
SortByArith(cNodes);
- vars_to_consts[cccc].push_back(max);
+ vars_to_consts[cccc].push_back(max);
}
else if(BVCONST == aaa.GetKind()) {
constkids.push_back(aaa);
//conclude that x + BVUMINUS(x) is 0.
vars_to_consts[aaa[0]].push_back(max);
}
- else
+ else
vars_to_consts[aaa].push_back(one);
} //end of for loop
for(ASTNodeToVecMap::iterator it=vars_to_consts.begin(),itend=vars_to_consts.end();
it!=itend;it++){
ASTVec ccc = it->second;
-
+
ASTNode constant;
if(1 < ccc.size()) {
constant = CreateTerm(BVPLUS,ccc[0].GetValueWidth(),ccc);
}
else
constant = ccc[0];
-
+
//constant * var
ASTNode monom;
- if(zero == constant)
+ if(zero == constant)
monom = zero;
else if (one == constant)
monom = it->first;
else{
- monom =
+ monom =
SimplifyTerm(CreateTerm(BVMULT,constant.GetValueWidth(),constant,it->first));
}
if(zero != monom) {
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 ||
+ if(!(BVPLUS == k_lhs ||
BVPLUS == k_rhs ||
- (BVMULT == k_lhs &&
+ (BVMULT == k_lhs &&
BVMULT == k_rhs)
)) {
return eq;
//cerr << "output of SimplifyTerm Cache: " << output << endl;
return output;
}
-
+
//if the lhs is not a BVPLUS, but the rhs is a BVPLUS, then swap
//the lhs and rhs
bool swap_flag = false;
ASTVec rvec = rhs.GetChildren();
ASTNode lhsplusrhs;
if(BVPLUS != lhs.GetKind() && BVPLUS != rhs.GetKind()) {
- lhsplusrhs = CreateTerm(BVPLUS,len,lhs,rhs);
+ lhsplusrhs = CreateTerm(BVPLUS,len,lhs,rhs);
}
else if(BVPLUS == lhs.GetKind() && BVPLUS == rhs.GetKind()) {
//combine the childnodes of the left and the right
SortByArith(outv);
output = CreateTerm(BVPLUS,len,outv);
}
-
+
//memoize
//UpdateSimplifyMap(eq,output,false);
- return output;
+ return output;
} //end of LhsMinusRHS()
//THis function accepts a BVMULT(t1,t2) and distributes the mult
}
//special case optimization: c1*(c2*t1) <==> (c1*c2)*t1
- if(BVCONST == left_kind &&
- BVMULT == right_kind &&
+ if(BVCONST == left_kind &&
+ BVMULT == right_kind &&
BVCONST == right[0].GetKind()) {
ASTNode c = BVConstEvaluator(CreateTerm(BVMULT,a.GetValueWidth(),left,right[0]));
c = CreateTerm(BVMULT,a.GetValueWidth(),c,right[1]);
left = c[0];
right = c[1];
left_kind = left.GetKind();
- right_kind = right.GetKind();
+ right_kind = right.GetKind();
}
//special case optimization: c1*(t1*c2) <==> (c1*c2)*t1
- if(BVCONST == left_kind &&
- BVMULT == right_kind &&
+ if(BVCONST == left_kind &&
+ BVMULT == right_kind &&
BVCONST == right[1].GetKind()) {
ASTNode c = BVConstEvaluator(CreateTerm(BVMULT,a.GetValueWidth(),left,right[1]));
c = CreateTerm(BVMULT,a.GetValueWidth(),c,right[0]);
left = c[0];
right = c[1];
left_kind = left.GetKind();
- right_kind = right.GetKind();
+ right_kind = right.GetKind();
}
//atleast one of left or right have to be BVPLUS
if(!(BVPLUS == left_kind || BVPLUS == right_kind)) {
return a;
}
-
+
//if left is BVPLUS and right is not, then swap left and right. we
//can do this since BVMULT is communtative
ASTNode swap;
}
}
}
-
+
//compute output here
if(outputvec.size() > 1) {
output = CombineLikeTerms(CreateTerm(BVPLUS,len,outputvec));
//cerr << "output of ConvertBVSXToITE Cache: " << output << endl;
return output;
}
-
+
ASTNode a0 = a[0];
unsigned a_len = a.GetValueWidth();
unsigned a0_len = a0.GetValueWidth();
-
+
if(a0_len > a_len){
FatalError("Trying to sign_extend a larger BV into a smaller BV");
return ASTUndefined; //to stop the compiler from producing bogus warnings
}
-
+
//sign extend
unsigned extensionlen = a_len-a0_len;
if(0 == extensionlen) {
std::string ones;
for(unsigned c=0; c < extensionlen;c++)
- ones += '1';
+ ones += '1';
std::string zeros;
for(unsigned c=0; c < extensionlen;c++)
zeros += '0';
-
+
//string of oness of length extensionlen
BEEV::ASTNode BVOnes = CreateBVConst(ones.c_str(),2);
//string of zeros of length extensionlen
BEEV::ASTNode BVZeros = CreateBVConst(zeros.c_str(),2);
-
+
//string of ones BVCONCAT a0
BEEV::ASTNode concatOnes = CreateTerm(BEEV::BVCONCAT,a_len,BVOnes,a0);
//string of zeros BVCONCAT a0
if(READ != term.GetKind() && WRITE != term[0].GetKind()) {
FatalError("RemovesWrites: Input must be a READ over a WRITE",term);
}
-
- if(!Begin_RemoveWrites &&
- !SimplifyWrites_InPlace_Flag &&
+
+ if(!Begin_RemoveWrites &&
+ !SimplifyWrites_InPlace_Flag &&
!start_abstracting) {
return term;
}
- else if(!Begin_RemoveWrites &&
- SimplifyWrites_InPlace_Flag &&
+ else if(!Begin_RemoveWrites &&
+ SimplifyWrites_InPlace_Flag &&
!start_abstracting) {
//return term;
return SimplifyWrites_InPlace(term);
ASTNodeMultiSet WriteIndicesSeenSoFar;
bool SeenNonConstWriteIndex = false;
- if(READ != term.GetKind() &&
+ if(READ != term.GetKind() &&
WRITE != term[0].GetKind()) {
FatalError("RemovesWrites: Input must be a READ over a WRITE",term);
}
-
+
ASTNode output;
if(CheckSimplifyMap(term,output,false)) {
return output;
ASTNode write = term[0];
unsigned indexwidth = write.GetIndexWidth();
ASTNode readIndex = SimplifyTerm(term[1]);
-
+
do {
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 =
+ ASTNode compare_readwrite_indices =
SimplifyFormula(CreateSimplifiedEQ(writeIndex,readIndex),false);
-
+
//if readIndex and writeIndex are equal
if(ASTTrue == compare_readwrite_indices && !SeenNonConstWriteIndex) {
UpdateSimplifyMap(term,writeVal,false);
return writeVal;
}
- if(!(ASTTrue == compare_readwrite_indices ||
+ if(!(ASTTrue == compare_readwrite_indices ||
ASTFalse == compare_readwrite_indices)) {
SeenNonConstWriteIndex = true;
}
//if (readIndex=writeIndex <=> FALSE)
- if(ASTFalse == compare_readwrite_indices
+ if(ASTFalse == compare_readwrite_indices
||
(WriteIndicesSeenSoFar.find(writeIndex) != WriteIndicesSeenSoFar.end())
) {
writeIndices.push_back(writeIndex);
writeValues.push_back(writeVal);
}
-
+
//record the write indices seen so far
//if(BVCONST == writeIndex.GetKind()) {
WriteIndicesSeenSoFar.insert(writeIndex);
output = CreateTerm(READ,width,write,readIndex);
UpdateSimplifyMap(term,output,false);
return output;
- } //end of SimplifyWrites_In_Place()
+ } //end of SimplifyWrites_In_Place()
//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 BeevMgr::RemoveWrites(const ASTNode& input) {
+ ASTNode BeevMgr::RemoveWrites(const ASTNode& input) {
//unsigned int width = input.GetValueWidth();
if(READ != input.GetKind() || WRITE != input[0].GetKind()) {
FatalError("RemovesWrites: Input must be a READ over a WRITE",input);
if(CheckSimplifyMap(input,output,false)) {
return output;
}
-
+
if(!start_abstracting && Begin_RemoveWrites) {
output= ReadOverWrite_To_ITE(input);
}
// if(CheckSimplifyMap(term,output,false)) {
// return output;
// }
-
+
ASTNode partialITE = term;
ASTNode writeA = ASTTrue;
ASTNode oldRead = term;
writeA = write[0];
ASTNode writeIndex = SimplifyTerm(write[1]);
ASTNode writeVal = SimplifyTerm(write[2]);
-
+
ASTNode cond = SimplifyFormula(CreateSimplifiedEQ(writeIndex,readIndex),false);
ASTNode newRead = CreateTerm(READ,width,writeA,readIndex);
ASTNode newRead_memoized = newRead;
if(CheckSimplifyMap(newRead, newRead_memoized,false)) {
newRead = newRead_memoized;
}
-
+
if(ASTTrue == cond && (term == partialITE)) {
//found the write-value in the first iteration itself. return
//it
UpdateSimplifyMap(term,output,false);
return output;
}
-
+
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);
else {
FatalError("RemoveWrites: Control should not reach here\n");
}
-
+
if(ASTTrue == cond) {
//no more iterations required
output = partialITE;
UpdateSimplifyMap(term,output,false);
return output;
}
-
+
input = newRead;
oldRead = newRead;
} while(READ == input.GetKind() && WRITE == input[0].GetKind());
-
+
output = partialITE;
-
+
//memoize
//UpdateSimplifyMap(term,output,false);
return output;
if(!BVConstIsOdd(c)) {
FatalError("MultiplicativeInverse: Input must be odd: ",c);
}
-
+
//cerr << "input to multinverse function is: " << d << endl;
ASTNode inverse;
if(CheckMultInverseMap(d,inverse)) {
//construct 2^(inputwidth), i.e. a bitvector of length
//'inputwidth+1', which is max(inputwidth)+1
//
- //all 1's
+ //all 1's
ASTNode max = CreateMaxConst(inputwidth);
//zero pad max
max = BVConstEvaluator(CreateTerm(BVCONCAT,inputwidth+1,onebit_zero,max));
//Create a '1' which has leading zeros of length 'inputwidth'
- ASTNode inputwidthplusone_one = CreateOneConst(inputwidth+1);
+ ASTNode inputwidthplusone_one = CreateOneConst(inputwidth+1);
//add 1 to max
max = CreateTerm(BVPLUS,inputwidth+1,max,inputwidthplusone_one);
max = BVConstEvaluator(max);
-
+
ASTNode zero = CreateZeroConst(inputwidth+1);
ASTNode max_bvgt_0 = CreateNode(BVGT,max,zero);
ASTNode quotient, remainder;
c = max;
max = remainder;
max_bvgt_0 = CreateNode(BVGT,max,zero);
-
+
x2 = x1;
x1 = x;
}
-
+
ASTNode hi = CreateBVConst(32,inputwidth-1);
ASTNode low = CreateZeroConst(32);
inverse = CreateTerm(BVEXTRACT,inputwidth,x2,hi,low);
if(BVCONST != c.GetKind()) {
FatalError("Input must be a constant", c);
}
-
+
ASTNode zero = CreateZeroConst(1);
ASTNode hi = CreateZeroConst(32);
ASTNode low = hi;
if(CheckSolverMap(a,output))
return output;
- //traverse a and populate the SubstitutionMap
+ //traverse a and populate the SubstitutionMap
Kind k = a.GetKind();
if(SYMBOL == k && BOOLEAN_TYPE == a.GetType()) {
bool updated = UpdateSubstitutionMap(a,ASTTrue);
- output = updated ? ASTTrue : a;
- return output;
+ output = updated ? ASTTrue : a;
+ return output;
}
if(NOT == k
&& SYMBOL == a[0].GetKind()) {
bool updated = UpdateSubstitutionMap(a[0],ASTFalse);
- output = updated ? ASTTrue : a;
- return output;
+ output = updated ? ASTTrue : a;
+ return output;
}
-
+
if(IFF == k) {
ASTVec c = a.GetChildren();
SortByArith(c);
- if(SYMBOL != c[0].GetKind() ||
+ if(SYMBOL != c[0].GetKind() ||
VarSeenInTerm(c[0],SimplifyFormula_NoRemoveWrites(c[1],false))) {
return a;
}
bool updated = UpdateSubstitutionMap(c[0], SimplifyFormula(c[1],false));
- output = updated ? ASTTrue : a;
- return output;
+ output = updated ? ASTTrue : a;
+ return output;
}
-
+
if(EQ == k) {
//fill the arrayname readindices vector if e0 is a
//READ(Arr,index) and index is a BVCONST
SortByArith(c);
FillUp_ArrReadIndex_Vec(c[0],c[1]);
- if(SYMBOL == c[0].GetKind() &&
+ if(SYMBOL == c[0].GetKind() &&
VarSeenInTerm(c[0],SimplifyTermAux(c[1]))) {
return a;
}
VarSeenInTerm(c[0][0],SimplifyTermAux(c[1]))) {
return a;
}
- bool updated = UpdateSubstitutionMap(c[0], SimplifyTermAux(c[1]));
- output = updated ? ASTTrue : a;
- return output;
+ bool updated = UpdateSubstitutionMap(c[0], SimplifyTermAux(c[1]));
+ output = updated ? ASTTrue : a;
+ return output;
}
if(AND == k){
for(ASTVec::iterator it = c.begin(),itend=c.end();it!=itend;it++) {
UpdateAlwaysTrueFormMap(*it);
ASTNode aaa = CreateSubstitutionMap(*it);
-
+
if(ASTTrue != aaa) {
if(ASTFalse == aaa)
return ASTFalse;
if(o.size() == 1)
return o[0];
-
+
return CreateNode(AND,o);
}
bool BeevMgr::VarSeenInTerm(const ASTNode& var, const ASTNode& term) {
- if(READ == term.GetKind() &&
+ if(READ == term.GetKind() &&
WRITE == term[0].GetKind() && !Begin_RemoveWrites) {
return false;
}
- if(READ == term.GetKind() &&
+ if(READ == term.GetKind() &&
WRITE == term[0].GetKind() && Begin_RemoveWrites) {
return true;
}
- ASTNodeMap::iterator it;
+ ASTNodeMap::iterator it;
if((it = TermsAlreadySeenMap.find(term)) != TermsAlreadySeenMap.end()) {
if(it->second == var) {
return false;
}
// 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
+// 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 BeevMgr::ResetSimplifyMaps()
{
delete SimplifyMap;
SimplifyMap = new ASTNodeMap(INITIAL_SIMPLIFY_MAP_SIZE);
-
+
delete SimplifyNegMap;
SimplifyNegMap = new ASTNodeMap(INITIAL_SIMPLIFY_MAP_SIZE);
}
-
+
};//end of namespace
projects / francis / stp.git / commitdiff