- /********************************************************************
+/********************************************************************
* AUTHORS: Vijay Ganesh
*
* BEGIN DATE: November, 2005
case BVPLUS:
{
-
ASTVec c = FlattenOneLevel(inputterm).GetChildren();
SortByArith(c);
ASTVec constkids, nonconstkids;
output = CreateTerm(output.GetKind(), output.GetValueWidth(), d);
}
break;
+
}
case BVSUB:
{
return output;
} //end of SimplifyTerm()
-ASTNode BeevMgr::SimplifyTermAux(const ASTNode& inputterm)
-{
- //cout << "SimplifyTerm: input: " << a << endl;
- if (!optimize_flag)
- {
- return inputterm;
- }
-
- ASTNode output;
- BVTypeCheck(inputterm);
-
- //########################################
- //########################################
-
- if (wordlevel_solve_flag && CheckSolverMap(inputterm, output))
- {
- return SimplifyTermAux(output);
- }
-
- Kind k = inputterm.GetKind();
- if (!is_Term_kind(k))
- {
- FatalError("SimplifyTerm: You have input a Non-term", ASTUndefined);
- }
-
- unsigned int inputValueWidth = inputterm.GetValueWidth();
- switch (k)
- {
- case BVCONST:
- output = inputterm;
- break;
- case SYMBOL:
- if (CheckSolverMap(inputterm, output))
- {
- return SimplifyTerm(output);
- }
- output = inputterm;
- break;
- case BVMULT:
- case BVPLUS:
- {
- 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;
-
- //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::iterator it = c.begin(), itend = c.end(); it != itend; it++)
- {
- ASTNode aaa = SimplifyTerm(*it);
- if (BVCONST == aaa.GetKind())
- {
- constkids.push_back(aaa);
- }
- else
- {
- nonconstkids.push_back(aaa);
- }
- }
-
- ASTNode one = CreateOneConst(inputValueWidth);
- ASTNode max = CreateMaxConst(inputValueWidth);
- ASTNode zero = 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 = 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 = CreateTerm(BVUMINUS, inputValueWidth, nonconstkids);
- }
- else
- {
- if (0 < nonconstkids.size())
- {
- //nonconstkids is not empty. First, combine const and
- //nonconstkids
- 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
- {
- //more than 1 element in nonconstkids. create BVPLUS term
- SortByArith(nonconstkids);
- output = CreateTerm(k, inputValueWidth, nonconstkids);
- output = FlattenOneLevel(output);
- output = DistributeMultOverPlus(output, true);
- output = CombineLikeTerms(output);
- }
- }
- else
- {
- //nonconstkids was empty, all childnodes were constant, hence
- //constoutput is the output.
- output = constoutput;
- }
- }
- if (BVMULT == output.GetKind() || BVPLUS == output.GetKind())
- {
- ASTVec d = output.GetChildren();
- SortByArith(d);
- output = CreateTerm(output.GetKind(), output.GetValueWidth(), d);
- }
- break;
- }
- case BVSUB:
- {
- ASTVec c = inputterm.GetChildren();
- ASTNode a0 = SimplifyTerm(inputterm[0]);
- ASTNode a1 = SimplifyTerm(inputterm[1]);
- unsigned int l = inputValueWidth;
- if (a0 == a1)
- output = CreateZeroConst(l);
- else
- {
- //covert x-y into x+(-y) and simplify. this transformation
- //triggers more simplifications
- //
- a1 = SimplifyTerm(CreateTerm(BVUMINUS, l, a1));
- output = SimplifyTerm(CreateTerm(BVPLUS, l, a0, 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.
- ASTNode a0 = SimplifyTerm(inputterm[0]);
- Kind k1 = a0.GetKind();
- unsigned int l = a0.GetValueWidth();
- ASTNode one = CreateOneConst(l);
- switch (k1)
- {
- case BVUMINUS:
- output = a0[0];
- break;
- case BVCONST:
- {
- output = BVConstEvaluator(CreateTerm(BVUMINUS, l, a0));
- break;
- }
- case BVNEG:
- {
- output = SimplifyTerm(CreateTerm(BVPLUS, l, a0[0], one));
- break;
- }
- case BVMULT:
- {
- if (BVUMINUS == a0[0].GetKind())
- {
- output = CreateTerm(BVMULT, l, a0[0][0], a0[1]);
- }
- else if (BVUMINUS == a0[1].GetKind())
- {
- output = CreateTerm(BVMULT, l, a0[0], a0[1][0]);
- }
- else
- {
- ASTNode a00 = SimplifyTerm(CreateTerm(BVUMINUS, l, a0[0]));
- output = CreateTerm(BVMULT, l, a00, a0[1]);
- }
- break;
- }
- case BVPLUS:
- {
- //push BVUMINUS over all the monomials of BVPLUS. Simplify
- //along the way
- //
- //BVUMINUS(a1x1 + a2x2 + ...) <=> BVPLUS(BVUMINUS(a1x1) +
- //BVUMINUS(a2x2) + ...
- ASTVec c = a0.GetChildren();
- ASTVec o;
- for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++)
- {
- //Simplify(BVUMINUS(a1x1))
- ASTNode aaa = SimplifyTerm(CreateTerm(BVUMINUS, l, *it));
- o.push_back(aaa);
- }
- //simplify the bvplus
- output = SimplifyTerm(CreateTerm(BVPLUS, l, o));
- break;
- }
- case BVSUB:
- {
- //BVUMINUS(BVSUB(x,y)) <=> BVSUB(y,x)
- output = SimplifyTerm(CreateTerm(BVSUB, l, a0[1], a0[0]));
- break;
- }
- case ITE:
- {
- //BVUMINUS(ITE(c,t1,t2)) <==> ITE(c,BVUMINUS(t1),BVUMINUS(t2))
- ASTNode c = a0[0];
- ASTNode t1 = SimplifyTerm(CreateTerm(BVUMINUS, l, a0[1]));
- ASTNode t2 = SimplifyTerm(CreateTerm(BVUMINUS, l, a0[2]));
- output = CreateSimplifiedTermITE(c, t1, t2);
- break;
- }
- default:
- {
- output = CreateTerm(BVUMINUS, l, a0);
- 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)
- 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];
- ASTNode zero = CreateBVConst(32, 0);
- //recall that the indices of BVEXTRACT are always 32 bits
- //long. therefore doing a GetBVUnsigned is ok.
- unsigned int i_val = GetUnsignedConst(i);
- unsigned int j_val = GetUnsignedConst(j);
-
- // a0[i:0] and len(a0)=i+1, then return a0
- if (0 == j_val && a_len == a0.GetValueWidth())
- return a0;
-
- switch (k1)
- {
- case BVCONST:
- {
- //extract the constant
- output = BVConstEvaluator(CreateTerm(BVEXTRACT, a_len, a0, i, j));
- 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];
- unsigned int len_a0 = a0.GetValueWidth();
- unsigned int len_u = u.GetValueWidth();
-
- if (len_u > i_val)
- {
- //Apply the following rule:
- // (t@u)[i:j] <==> u[i:j], if len(u) > i
- //
- output = SimplifyTerm(CreateTerm(BVEXTRACT, a_len, 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 = CreateBVConst(32, i_val - len_u);
- j = CreateBVConst(32, j_val - len_u);
- output = SimplifyTerm(CreateTerm(BVEXTRACT, a_len, t, i, j));
- }
- else
- {
- //Apply the rule:
- // (t@u)[i:j] <==> t[i-len_u:0] @ u[len_u-1:j]
- i = CreateBVConst(32, i_val - len_u);
- ASTNode m = CreateBVConst(32, len_u - 1);
- t = SimplifyTerm(CreateTerm(BVEXTRACT, i_val - len_u + 1, t, i, zero));
- u = SimplifyTerm(CreateTerm(BVEXTRACT, len_u - j_val, u, m, j));
- output = CreateTerm(BVCONCAT, a_len, t, u);
- }
- break;
- }
- 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++)
- {
- ASTNode aaa = *jt;
- aaa = SimplifyTerm(CreateTerm(BVEXTRACT, i_val + 1, aaa, i, zero));
- o.push_back(aaa);
- }
- 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 BVAND:
- case BVOR:
- case BVXOR:
- {
- //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(CreateTerm(BVEXTRACT, a_len, t, i, j));
- u = SimplifyTerm(CreateTerm(BVEXTRACT, a_len, u, i, j));
- BVTypeCheck(t);
- BVTypeCheck(u);
- output = CreateTerm(k1, a_len, t, u);
- break;
- }
- case BVNEG:
- {
- // (~t)[i:j] <==> ~(t[i:j])
- ASTNode t = a0[0];
- t = SimplifyTerm(CreateTerm(BVEXTRACT, a_len, t, i, j));
- output = CreateTerm(BVNEG, a_len, 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 = CreateTerm(BVEXTRACT,a_len,a0,i,j);
- // }
- // else {
- // output = CreateTerm(BVSX,a_len,t,CreateBVConst(32,a_len));
- // }
- // break;
- // }
- case ITE:
- {
- ASTNode t0 = a0[0];
- ASTNode t1 = SimplifyTerm(CreateTerm(BVEXTRACT, a_len, a0[1], i, j));
- ASTNode t2 = SimplifyTerm(CreateTerm(BVEXTRACT, a_len, a0[2], i, j));
- output = CreateSimplifiedTermITE(t0, t1, t2);
- break;
- }
- default:
- {
- output = CreateTerm(BVEXTRACT, a_len, a0, i, j);
- break;
- }
- }
- break;
- }
- case BVNEG:
- {
- ASTNode a0 = SimplifyTerm(inputterm[0]);
- unsigned len = inputValueWidth;
- switch (a0.GetKind())
- {
- case BVCONST:
- output = BVConstEvaluator(CreateTerm(BVNEG, len, a0));
- break;
- case BVNEG:
- output = a0[0];
- break;
- // case ITE: {
- // 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);
- // break;
- // }
- default:
- output = CreateTerm(BVNEG, len, a0);
- break;
- }
- break;
- }
- case BVZX:
- {
- //a0 is the expr which is being zero extended
- ASTNode a0 = SimplifyTerm(inputterm[0]);
- //a1 represents the length of the term BVZX(a0)
- ASTNode a1 = inputterm[1];
- //output length of the BVSX term
- unsigned len = inputValueWidth;
-
- output = CreateTerm(BVZX, len, a0, a1);
- break;
- }
- break;
-
- case BVSX:
- {
- //a0 is the expr which is being sign extended
- ASTNode a0 = SimplifyTerm(inputterm[0]);
- //a1 represents the length of the term BVSX(a0)
- ASTNode a1 = inputterm[1];
- //output length of the BVSX term
- unsigned len = inputValueWidth;
-
- if (a0.GetValueWidth() == len)
- {
- //nothing to signextend
- return a0;
- }
-
- switch (a0.GetKind())
- {
- case BVCONST:
- output = BVConstEvaluator(CreateTerm(BVSX, len, a0, a1));
- break;
- case BVNEG:
- output = CreateTerm(a0.GetKind(), len, CreateTerm(BVSX, len, a0[0], a1));
- break;
- case BVAND:
- case BVOR:
- //assuming BVAND and BVOR are binary
- output = CreateTerm(a0.GetKind(), len, CreateTerm(BVSX, len, a0[0], a1), CreateTerm(BVSX, len, a0[1], a1));
- break;
- 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;
- for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++)
- {
- if (BVSX != it->GetKind())
- {
- returnflag = true;
- break;
- }
- }
- if (returnflag)
- {
- output = CreateTerm(BVSX, len, a0, a1);
- }
- else
- {
- ASTVec o;
- for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++)
- {
- ASTNode aaa = SimplifyTerm(CreateTerm(BVSX, len, *it, a1));
- o.push_back(aaa);
- }
- output = CreateTerm(a0.GetKind(), len, 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 = SimplifyTerm(a0[0]);
- output = CreateTerm(BVSX, len, a0, a1);
- break;
- }
- case ITE:
- {
- ASTNode cond = a0[0];
- ASTNode thenpart = SimplifyTerm(CreateTerm(BVSX, len, a0[1], a1));
- ASTNode elsepart = SimplifyTerm(CreateTerm(BVSX, len, a0[2], a1));
- output = CreateSimplifiedTermITE(cond, thenpart, elsepart);
- break;
- }
- default:
- output = CreateTerm(BVSX, len, a0, a1);
- break;
- }
- break;
- }
- case BVAND:
- case BVOR:
- {
- ASTNode max = CreateMaxConst(inputValueWidth);
- ASTNode zero = CreateZeroConst(inputValueWidth);
-
- ASTNode identity = (BVAND == k) ? max : zero;
- ASTNode annihilator = (BVAND == k) ? zero : max;
- ASTVec c = FlattenOneLevel(inputterm).GetChildren();
- SortByArith(c);
- ASTVec o;
- bool constant = true;
- for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++)
- {
- ASTNode aaa = SimplifyTerm(*it);
- if (BVCONST != aaa.GetKind())
- {
- constant = false;
- }
-
- if (aaa == annihilator)
- {
- output = annihilator;
- return output;
- }
-
- if (aaa != identity)
- {
- o.push_back(aaa);
- }
- }
-
- switch (o.size())
- {
- case 0:
- output = identity;
- break;
- case 1:
- output = o[0];
- break;
- default:
- SortByArith(o);
- output = CreateTerm(k, inputValueWidth, o);
- if (constant)
- {
- output = BVConstEvaluator(output);
- }
- break;
- }
- break;
- }
- case BVCONCAT:
- {
- ASTNode t = SimplifyTerm(inputterm[0]);
- 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 && t[0] == u[0])
- {
- //to handle the case x[m:n]@x[n-1:k] <==> x[m:k]
- ASTNode t_hi = t[1];
- ASTNode t_low = t[2];
- ASTNode u_hi = u[1];
- ASTNode u_low = u[2];
- ASTNode c = BVConstEvaluator(CreateTerm(BVPLUS, 32, u_hi, CreateOneConst(32)));
- if (t_low == c)
- {
- output = CreateTerm(BVEXTRACT, inputValueWidth, t[0], t_hi, u_low);
- }
- else
- {
- output = CreateTerm(BVCONCAT, inputValueWidth, t, u);
- }
- }
- else
- {
- output = CreateTerm(BVCONCAT, inputValueWidth, t, u);
- }
- break;
- }
- case BVXOR:
- case BVXNOR:
- case BVNAND:
- case BVNOR:
- case BVLEFTSHIFT:
- case BVRIGHTSHIFT:
- case BVVARSHIFT:
- case BVSRSHIFT:
- case BVDIV:
- case BVMOD:
- {
- ASTVec c = inputterm.GetChildren();
- ASTVec o;
- bool constant = true;
- for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++)
- {
- ASTNode aaa = SimplifyTerm(*it);
- if (BVCONST != aaa.GetKind())
- {
- constant = false;
- }
- o.push_back(aaa);
- }
- output = CreateTerm(k, inputValueWidth, o);
- if (constant)
- output = BVConstEvaluator(output);
- break;
- }
- case READ:
- {
- ASTNode out1;
- //process only if not in the substitution map. simplifymap
- //has been checked already
- if (!CheckSubstitutionMap(inputterm, out1))
- {
- if (WRITE == inputterm[0].GetKind())
- {
- //get rid of all writes
- ASTNode nowrites = RemoveWrites_TopLevel(inputterm);
- out1 = nowrites;
- }
- else if (ITE == inputterm[0].GetKind())
- {
- ASTNode cond = SimplifyFormula(inputterm[0][0], false);
- ASTNode index = SimplifyTerm(inputterm[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);
- }
- else
- {
- //arr is a SYMBOL for sure
- ASTNode arr = inputterm[0];
- ASTNode index = SimplifyTerm(inputterm[1]);
- 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.
- if (!CheckSubstitutionMap(out1, output))
- 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);
- break;
- }
- case SBVREM:
- case SBVMOD:
- case SBVDIV:
- {
- ASTVec c = inputterm.GetChildren();
- ASTVec o;
- for (ASTVec::iterator it = c.begin(), itend = c.end(); it != itend; it++)
- {
- ASTNode aaa = SimplifyTerm(*it);
- o.push_back(aaa);
- }
- output = CreateTerm(k, inputValueWidth, o);
- break;
- }
- case WRITE:
- default:
- FatalError("SimplifyTermAux: Control should never reach here:", inputterm, k);
- return inputterm;
- break;
- }
-
- return output;
-}
//At the end of each simplification call, we want the output to be
//always smaller or equal to the input in size.
SortByArith(c);
FillUp_ArrReadIndex_Vec(c[0], c[1]);
- ASTNode c1 = SimplifyTermAux(c[1]);
+ ASTNode c1 = SimplifyTerm(c[1]);
if (SYMBOL == c[0].GetKind() && VarSeenInTerm(c[0], c1))
{
return a;
projects / francis / stp.git / commitdiff