From: trevor_hansen Date: Wed, 2 Sep 2009 12:53:15 +0000 (+0000) Subject: Deleting SimplifyTermAux(), which seems redundant. X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=5a2a5cb3ab352b52b9182dadf44e47876940f3b0;p=francis%2Fstp.git Deleting SimplifyTermAux(), which seems redundant. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@167 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp index 6e73afc..0264f64 100644 --- a/src/simplifier/simplifier.cpp +++ b/src/simplifier/simplifier.cpp @@ -1,4 +1,4 @@ - /******************************************************************** +/******************************************************************** * AUTHORS: Vijay Ganesh * * BEGIN DATE: November, 2005 @@ -1398,7 +1398,6 @@ ASTNode BeevMgr::SimplifyTerm(const ASTNode& actualInputterm) case BVPLUS: { - ASTVec c = FlattenOneLevel(inputterm).GetChildren(); SortByArith(c); ASTVec constkids, nonconstkids; @@ -1497,6 +1496,7 @@ ASTNode BeevMgr::SimplifyTerm(const ASTNode& actualInputterm) output = CreateTerm(output.GetKind(), output.GetValueWidth(), d); } break; + } case BVSUB: { @@ -2056,702 +2056,6 @@ ASTNode BeevMgr::SimplifyTerm(const ASTNode& actualInputterm) 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. @@ -3608,7 +2912,7 @@ ASTNode BeevMgr::CreateSubstitutionMap(const ASTNode& a) 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;