diff options
Diffstat (limited to 'stp/simplifier/bvsolver.cpp')
| -rw-r--r-- | stp/simplifier/bvsolver.cpp | 714 |
1 files changed, 0 insertions, 714 deletions
diff --git a/stp/simplifier/bvsolver.cpp b/stp/simplifier/bvsolver.cpp deleted file mode 100644 index 369251db..00000000 --- a/stp/simplifier/bvsolver.cpp +++ /dev/null @@ -1,714 +0,0 @@ -/******************************************************************** - * AUTHORS: Vijay Ganesh, David L. Dill - * - * BEGIN DATE: November, 2005 - * - * LICENSE: Please view LICENSE file in the home dir of this Program - ********************************************************************/ -// -*- c++ -*- - -#include "../AST/AST.h" -#include "../AST/ASTUtil.h" -#include "bvsolver.h" - - //This file contains the implementation of member functions of - //bvsolver class, which represents the bitvector arithmetic linear - //solver. Please also refer the STP's CAV 2007 paper for the - //complete description of the linear solver algorithm - // - //The bitvector solver is a partial solver, i.e. it does not solve - //for all variables in the system of equations. it is - //best-effort. it relies on the SAT solver to be complete. - // - //The BVSolver assumes that the input equations are normalized, and - //have liketerms combined etc. - // - //0. Traverse top-down over the input DAG, looking for a conjunction - //0. of equations. if you find one, then for each equation in the - //0. conjunction, do the following steps. - // - //1. check for Linearity of the input equation - // - //2. Solve for a "chosen" variable. The variable should occur - //2. exactly once and must have an odd coeff. Refer STP's CAV 2007 - //2. paper for actual solving procedure - // - //4. Outside the solver, Substitute and Re-normalize the input DAG -namespace BEEV { - //check the solver map for 'key'. If key is present, then return the - //value by reference in the argument 'output' - bool BVSolver::CheckAlreadySolvedMap(const ASTNode& key, ASTNode& output) { - ASTNodeMap::iterator it; - if((it = FormulasAlreadySolvedMap.find(key)) != FormulasAlreadySolvedMap.end()) { - output = it->second; - return true; - } - return false; - } //CheckAlreadySolvedMap() - - void BVSolver::UpdateAlreadySolvedMap(const ASTNode& key, const ASTNode& value) { - FormulasAlreadySolvedMap[key] = value; - } //end of UpdateAlreadySolvedMap() - - //FIXME This is doing way more arithmetic than it needs to. - //accepts an even number "in", and splits it into an odd number and - //a power of 2. i.e " in = b.(2^k) ". returns the odd number, and - //the power of two by reference - ASTNode BVSolver::SplitEven_into_Oddnum_PowerOf2(const ASTNode& in, - unsigned int& number_shifts) { - if(BVCONST != in.GetKind() || _bm->BVConstIsOdd(in)) { - FatalError("BVSolver:SplitNum_Odd_PowerOf2: input must be a BVCONST and even\n",in); - } - - unsigned int len = in.GetValueWidth(); - ASTNode zero = _bm->CreateZeroConst(len); - ASTNode two = _bm->CreateTwoConst(len); - ASTNode div_by_2 = in; - ASTNode mod_by_2 = - _bm->BVConstEvaluator(_bm->CreateTerm(BVMOD,len,div_by_2,two)); - while(mod_by_2 == zero) { - div_by_2 = - _bm->BVConstEvaluator(_bm->CreateTerm(BVDIV,len,div_by_2,two)); - number_shifts++; - mod_by_2 = - _bm->BVConstEvaluator(_bm->CreateTerm(BVMOD,len,div_by_2,two)); - } - return div_by_2; - } //end of SplitEven_into_Oddnum_PowerOf2() - - //Checks if there are any ARRAYREADS in the term, after the - //alreadyseenmap is cleared, i.e. traversing a new term altogether - bool BVSolver::CheckForArrayReads_TopLevel(const ASTNode& term) { - TermsAlreadySeenMap.clear(); - return CheckForArrayReads(term); - } - - //Checks if there are any ARRAYREADS in the term - bool BVSolver::CheckForArrayReads(const ASTNode& term) { - ASTNode a = term; - ASTNodeMap::iterator it; - if((it = TermsAlreadySeenMap.find(term)) != TermsAlreadySeenMap.end()) { - //if the term has been seen, then simply return true, else - //return false - if(ASTTrue == (it->second)) { - return true; - } - else { - return false; - } - } - - switch(term.GetKind()) { - case READ: - //an array read has been seen. Make an entry in the map and - //return true - TermsAlreadySeenMap[term] = ASTTrue; - return true; - default: { - ASTVec c = term.GetChildren(); - for(ASTVec::iterator it=c.begin(),itend=c.end();it!=itend;it++) { - if(CheckForArrayReads(*it)) { - return true; - } - } - break; - } - } - - //If control is here, then it means that no arrayread was seen for - //the input 'term'. Make an entry in the map with the term as key - //and FALSE as value. - TermsAlreadySeenMap[term] = ASTFalse; - return false; - } //end of CheckForArrayReads() - - //check the solver map for 'key'. If key is present, then return the - //value by reference in the argument 'output' - bool BeevMgr::CheckSolverMap(const ASTNode& key, ASTNode& output) { - ASTNodeMap::iterator it; - if((it = SolverMap.find(key)) != SolverMap.end()) { - output = it->second; - return true; - } - return false; - } //end of CheckSolverMap() - - bool BeevMgr::CheckSolverMap(const ASTNode& key) { - if(SolverMap.find(key) != SolverMap.end()) - return true; - else - return false; - } //end of CheckSolverMap() - - //update solvermap with (key,value) pair - bool BeevMgr::UpdateSolverMap(const ASTNode& key, const ASTNode& value) { - ASTNode var = (BVEXTRACT == key.GetKind()) ? key[0] : key; - if(!CheckSolverMap(var) && key != value) { - SolverMap[key] = value; - return true; - } - return false; - } //end of UpdateSolverMap() - - //collects the vars in the term 'lhs' into the multiset Vars - void BVSolver::VarsInTheTerm_TopLevel(const ASTNode& lhs, ASTNodeMultiSet& Vars) { - TermsAlreadySeenMap.clear(); - VarsInTheTerm(lhs,Vars); - } - - //collects the vars in the term 'lhs' into the multiset Vars - void BVSolver::VarsInTheTerm(const ASTNode& term, ASTNodeMultiSet& Vars) { - ASTNode a = term; - ASTNodeMap::iterator it; - if((it = TermsAlreadySeenMap.find(term)) != TermsAlreadySeenMap.end()) { - //if the term has been seen, then simply return - return; - } - - switch(term.GetKind()) { - case BVCONST: - return; - case SYMBOL: - //cerr << "debugging: symbol added: " << term << endl; - Vars.insert(term); - break; - case READ: - //skip the arrayname, provided the arrayname is a SYMBOL - if(SYMBOL == term[0].GetKind()) { - VarsInTheTerm(term[1],Vars); - } - else { - VarsInTheTerm(term[0],Vars); - VarsInTheTerm(term[1],Vars); - } - break; - default: { - ASTVec c = term.GetChildren(); - for(ASTVec::iterator it=c.begin(),itend=c.end();it!=itend;it++) { - VarsInTheTerm(*it,Vars); - } - break; - } - } - - //ensures that you don't double count. if you have seen the term - //once, then memoize - TermsAlreadySeenMap[term] = ASTTrue; - return; - } //end of VarsInTheTerm() - - bool BVSolver::DoNotSolveThis(const ASTNode& var) { - if(DoNotSolve_TheseVars.find(var) != DoNotSolve_TheseVars.end()) { - return true; - } - return false; - } - - //chooses a variable in the lhs and returns the chosen variable - ASTNode BVSolver::ChooseMonom(const ASTNode& eq, ASTNode& modifiedlhs) { - if(!(EQ == eq.GetKind() && BVPLUS == eq[0].GetKind())) { - FatalError("ChooseMonom: input must be a EQ",eq); - } - - ASTNode lhs = eq[0]; - ASTNode rhs = eq[1]; - ASTNode zero = _bm->CreateZeroConst(32); - - //collect all the vars in the lhs and rhs - ASTNodeMultiSet Vars; - VarsInTheTerm_TopLevel(lhs,Vars); - - //handle BVPLUS case - ASTVec c = lhs.GetChildren(); - ASTVec o; - ASTNode outmonom = _bm->CreateNode(UNDEFINED); - bool chosen_symbol = false; - bool chosen_odd = false; - - //choose variables with no coeffs - for(ASTVec::iterator it=c.begin(),itend=c.end();it!=itend;it++) { - ASTNode monom = *it; - if(SYMBOL == monom.GetKind() && - Vars.count(monom) == 1 && - !_bm->VarSeenInTerm(monom,rhs) && - !DoNotSolveThis(monom) && - !chosen_symbol) { - outmonom = monom; - chosen_symbol = true; - } - else if(BVUMINUS == monom.GetKind() && - SYMBOL == monom[0].GetKind() && - Vars.count(monom[0]) == 1 && - !DoNotSolveThis(monom[0]) && - !_bm->VarSeenInTerm(monom[0],rhs) && - !chosen_symbol) { - //cerr << "Chosen Monom: " << monom << endl; - outmonom = monom; - chosen_symbol = true; - } - else { - o.push_back(monom); - } - } - - //try to choose only odd coeffed variables first - if(!chosen_symbol) { - o.clear(); - for(ASTVec::iterator it=c.begin(),itend=c.end();it!=itend;it++) { - ASTNode monom = *it; - ASTNode var = (BVMULT == monom.GetKind()) ? monom[1] : _bm->CreateNode(UNDEFINED); - - if(BVMULT == monom.GetKind() && - BVCONST == monom[0].GetKind() && - _bm->BVConstIsOdd(monom[0]) && - ((SYMBOL == var.GetKind() && - Vars.count(var) == 1) - || - (BVEXTRACT == var.GetKind() && - SYMBOL == var[0].GetKind() && - BVCONST == var[1].GetKind() && - zero == var[2] && - !_bm->VarSeenInTerm(var[0],rhs) && - !DoNotSolveThis(var[0])) - ) && - !DoNotSolveThis(var) && - !_bm->VarSeenInTerm(var,rhs) && - !chosen_odd) { - //monom[0] is odd. - outmonom = monom; - chosen_odd = true; - } - else { - o.push_back(monom); - } - } - } - - modifiedlhs = (o.size() > 1) ? _bm->CreateTerm(BVPLUS,lhs.GetValueWidth(),o) : o[0]; - return outmonom; - } //end of choosemonom() - - //solver function which solves for variables with odd coefficient - ASTNode BVSolver::BVSolve_Odd(const ASTNode& input) { - ASTNode eq = input; - //cerr << "Input to BVSolve_Odd()" << eq << endl; - if(!(wordlevel_solve && EQ == eq.GetKind())) { - return input; - } - - ASTNode output = input; - if(CheckAlreadySolvedMap(input,output)) { - return output; - } - - //get the lhs and the rhs, and case-split on the lhs kind - ASTNode lhs = eq[0]; - ASTNode rhs = eq[1]; - if(BVPLUS == lhs.GetKind()) { - ASTNode chosen_monom = _bm->CreateNode(UNDEFINED); - ASTNode leftover_lhs; - - //choose monom makes sure that it gets only those vars that - //occur exactly once in lhs and rhs put together - chosen_monom = ChooseMonom(eq, leftover_lhs); - if(chosen_monom == _bm->CreateNode(UNDEFINED)) { - //no monomial was chosen - return eq; - } - - //if control is here then it means that a monom was chosen - // - //construct: rhs - (lhs without the chosen monom) - unsigned int len = lhs.GetValueWidth(); - leftover_lhs = _bm->SimplifyTerm_TopLevel(_bm->CreateTerm(BVUMINUS,len,leftover_lhs)); - ASTNode newrhs = _bm->SimplifyTerm(_bm->CreateTerm(BVPLUS,len,rhs,leftover_lhs)); - lhs = chosen_monom; - rhs = newrhs; - } //end of if(BVPLUS ...) - - if(BVUMINUS == lhs.GetKind()) { - //equation is of the form (-lhs0) = rhs - ASTNode lhs0 = lhs[0]; - rhs = _bm->SimplifyTerm(_bm->CreateTerm(BVUMINUS,rhs.GetValueWidth(),rhs)); - lhs = lhs0; - } - - switch(lhs.GetKind()) { - case SYMBOL: { - //input is of the form x = rhs first make sure that the lhs - //symbol does not occur on the rhs or that it has not been - //solved for - if(_bm->VarSeenInTerm(lhs,rhs)) { - //found the lhs in the rhs. Abort! - DoNotSolve_TheseVars.insert(lhs); - return eq; - } - - //rhs should not have arrayreads in it. it complicates matters - //during transformation - // if(CheckForArrayReads_TopLevel(rhs)) { - // return eq; - // } - - DoNotSolve_TheseVars.insert(lhs); - if(!_bm->UpdateSolverMap(lhs,rhs)) { - return eq; - } - - output = ASTTrue; - break; - } - case BVEXTRACT: { - ASTNode zero = _bm->CreateZeroConst(32); - - if(!(SYMBOL == lhs[0].GetKind() && - BVCONST == lhs[1].GetKind() && - zero == lhs[2] && - !_bm->VarSeenInTerm(lhs[0],rhs) && - !DoNotSolveThis(lhs[0]))) { - return eq; - } - - if(_bm->VarSeenInTerm(lhs[0],rhs)) { - DoNotSolve_TheseVars.insert(lhs[0]); - return eq; - } - - DoNotSolve_TheseVars.insert(lhs[0]); - if(!_bm->UpdateSolverMap(lhs,rhs)) { - return eq; - } - - //if the extract of x[i:0] = t is entered into the solvermap, - //then also add another entry for x = x1@t - ASTNode var = lhs[0]; - ASTNode newvar = NewVar(var.GetValueWidth() - lhs.GetValueWidth()); - newvar = _bm->CreateTerm(BVCONCAT,var.GetValueWidth(),newvar,rhs); - _bm->UpdateSolverMap(var,newvar); - output = ASTTrue; - break; - } - case BVMULT: { - //the input is of the form a*x = t. If 'a' is odd, then compute - //its multiplicative inverse a^-1, multiply 't' with it, and - //update the solver map - if(BVCONST != lhs[0].GetKind()) { - return eq; - } - - if(!(SYMBOL == lhs[1].GetKind() || - (BVEXTRACT == lhs[1].GetKind() && - SYMBOL == lhs[1][0].GetKind()))) { - return eq; - } - - bool ChosenVar_Is_Extract = (BVEXTRACT == lhs[1].GetKind()) ? true : false; - - //if coeff is even, then we know that all the coeffs in the eqn - //are even. Simply return the eqn - if(!_bm->BVConstIsOdd(lhs[0])) { - return eq; - } - - ASTNode a = _bm->MultiplicativeInverse(lhs[0]); - ASTNode chosenvar = (BVEXTRACT == lhs[1].GetKind()) ? lhs[1][0] : lhs[1]; - ASTNode chosenvar_value = - _bm->SimplifyTerm(_bm->CreateTerm(BVMULT,rhs.GetValueWidth(),a,rhs)); - - //if chosenvar is seen in chosenvar_value then abort - if(_bm->VarSeenInTerm(chosenvar,chosenvar_value)) { - //abort solving - DoNotSolve_TheseVars.insert(lhs); - return eq; - } - - //rhs should not have arrayreads in it. it complicates matters - //during transformation - // if(CheckForArrayReads_TopLevel(chosenvar_value)) { - // return eq; - // } - - //found a variable to solve - DoNotSolve_TheseVars.insert(chosenvar); - chosenvar = lhs[1]; - if(!_bm->UpdateSolverMap(chosenvar,chosenvar_value)) { - return eq; - } - - if(ChosenVar_Is_Extract) { - ASTNode var = lhs[1][0]; - ASTNode newvar = NewVar(var.GetValueWidth() - lhs[1].GetValueWidth()); - newvar = _bm->CreateTerm(BVCONCAT,var.GetValueWidth(),newvar,chosenvar_value); - _bm->UpdateSolverMap(var,newvar); - } - output = ASTTrue; - break; - } - default: - output = eq; - break; - } - - UpdateAlreadySolvedMap(input,output); - return output; - } //end of BVSolve_Odd() - - //Create a new variable of ValueWidth 'n' - ASTNode BVSolver::NewVar(unsigned int n) { - std:: string c("v"); - char d[32]; - sprintf(d,"%d",_symbol_count++); - std::string ccc(d); - c += "_solver_" + ccc; - - ASTNode CurrentSymbol = _bm->CreateSymbol(c.c_str()); - CurrentSymbol.SetValueWidth(n); - CurrentSymbol.SetIndexWidth(0); - return CurrentSymbol; - } //end of NewVar() - - //The toplevel bvsolver(). Checks if the formula has already been - //solved. If not, the solver() is invoked. If yes, then simply drop - //the formula - ASTNode BVSolver::TopLevelBVSolve(const ASTNode& input) { - if(!wordlevel_solve) { - return input; - } - - Kind k = input.GetKind(); - if(!(EQ == k || AND == k)) { - return input; - } - - ASTNode output = input; - if(CheckAlreadySolvedMap(input,output)) { - //output is TRUE. The formula is thus dropped - return output; - } - ASTVec o; - ASTVec c; - if(EQ == k) - c.push_back(input); - else - c = input.GetChildren(); - ASTVec eveneqns; - ASTNode solved = ASTFalse; - for(ASTVec::iterator it = c.begin(), itend = c.end();it != itend;it++) { - //_bm->ASTNodeStats("Printing before calling simplifyformula inside the solver:", *it); - ASTNode aaa = (ASTTrue == solved && EQ == it->GetKind()) ? _bm->SimplifyFormula(*it,false) : *it; - //ASTNode aaa = *it; - //_bm->ASTNodeStats("Printing after calling simplifyformula inside the solver:", aaa); - aaa = BVSolve_Odd(aaa); - //_bm->ASTNodeStats("Printing after oddsolver:", aaa); - bool even = false; - aaa = CheckEvenEqn(aaa, even); - if(even) { - eveneqns.push_back(aaa); - } - else { - if(ASTTrue != aaa) { - o.push_back(aaa); - } - } - solved = aaa; - } - - ASTNode evens; - if(eveneqns.size() > 0) { - //if there is a system of even equations then solve them - evens = (eveneqns.size() > 1) ? _bm->CreateNode(AND,eveneqns) : eveneqns[0]; - //evens = _bm->SimplifyFormula(evens,false); - evens = BVSolve_Even(evens); - _bm->ASTNodeStats("Printing after evensolver:", evens); - } - else { - evens = ASTTrue; - } - output = (o.size() > 0) ? ((o.size() > 1) ? _bm->CreateNode(AND,o) : o[0]) : ASTTrue; - output = _bm->CreateNode(AND,output,evens); - - UpdateAlreadySolvedMap(input,output); - return output; - } //end of TopLevelBVSolve() - - ASTNode BVSolver::CheckEvenEqn(const ASTNode& input, bool& evenflag) { - ASTNode eq = input; - //cerr << "Input to BVSolve_Odd()" << eq << endl; - if(!(wordlevel_solve && EQ == eq.GetKind())) { - evenflag = false; - return eq; - } - - ASTNode lhs = eq[0]; - ASTNode rhs = eq[1]; - ASTNode zero = _bm->CreateZeroConst(rhs.GetValueWidth()); - //lhs must be a BVPLUS, and rhs must be a BVCONST - if(!(BVPLUS == lhs.GetKind() && zero == rhs)) { - evenflag = false; - return eq; - } - - ASTVec lhs_c = lhs.GetChildren(); - ASTNode savetheconst = rhs; - for(ASTVec::iterator it=lhs_c.begin(),itend=lhs_c.end();it!=itend;it++) { - ASTNode aaa = *it; - Kind itk = aaa.GetKind(); - - if(BVCONST == itk){ - //check later if the constant is even or not - savetheconst = aaa; - continue; - } - - if(!(BVMULT == itk && - BVCONST == aaa[0].GetKind() && - SYMBOL == aaa[1].GetKind() && - !_bm->BVConstIsOdd(aaa[0]))) { - //If the monomials of the lhs are NOT of the form 'a*x' where - //'a' is even, then return the false - evenflag = false; - return eq; - } - }//end of for loop - - //if control is here then it means that all coeffs are even. the - //only remaining thing is to check if the constant is even or not - if(_bm->BVConstIsOdd(savetheconst)) { - //the constant turned out to be odd. we have UNSAT eqn - evenflag = false; - return ASTFalse; - } - - //all is clear. the eqn in even, through and through - evenflag = true; - return eq; - } //end of CheckEvenEqn - - //solve an eqn whose monomials have only even coefficients - ASTNode BVSolver::BVSolve_Even(const ASTNode& input) { - if(!wordlevel_solve) { - return input; - } - - if(!(EQ == input.GetKind() || AND == input.GetKind())) { - return input; - } - - ASTNode output; - if(CheckAlreadySolvedMap(input,output)) { - return output; - } - - ASTVec input_c; - if(EQ == input.GetKind()) { - input_c.push_back(input); - } - else { - input_c = input.GetChildren(); - } - - //power_of_2 holds the exponent of 2 in the coeff - unsigned int power_of_2 = 0; - //we need this additional variable to find the lowest power of 2 - unsigned int power_of_2_lowest = 0xffffffff; - //the monom which has the least power of 2 in the coeff - ASTNode monom_with_best_coeff; - for(ASTVec::iterator jt=input_c.begin(),jtend=input_c.end();jt!=jtend;jt++) { - ASTNode eq = *jt; - ASTNode lhs = eq[0]; - ASTNode rhs = eq[1]; - ASTNode zero = _bm->CreateZeroConst(rhs.GetValueWidth()); - //lhs must be a BVPLUS, and rhs must be a BVCONST - if(!(BVPLUS == lhs.GetKind() && zero == rhs)) { - return input; - } - - ASTVec lhs_c = lhs.GetChildren(); - ASTNode odd; - for(ASTVec::iterator it=lhs_c.begin(),itend=lhs_c.end();it!=itend;it++) { - ASTNode aaa = *it; - Kind itk = aaa.GetKind(); - if(!(BVCONST == itk && - !_bm->BVConstIsOdd(aaa)) && - !(BVMULT == itk && - BVCONST == aaa[0].GetKind() && - SYMBOL == aaa[1].GetKind() && - !_bm->BVConstIsOdd(aaa[0]))) { - //If the monomials of the lhs are NOT of the form 'a*x' or 'a' - //where 'a' is even, then return the eqn - return input; - } - - //we are gauranteed that if control is here then the monomial is - //of the form 'a*x' or 'a', where 'a' is even - ASTNode coeff = (BVCONST == itk) ? aaa : aaa[0]; - odd = SplitEven_into_Oddnum_PowerOf2(coeff,power_of_2); - if(power_of_2 < power_of_2_lowest) { - power_of_2_lowest = power_of_2; - monom_with_best_coeff = aaa; - } - power_of_2 = 0; - }//end of inner for loop - } //end of outer for loop - - //get the exponent - power_of_2 = power_of_2_lowest; - - //if control is here, we are gauranteed that we have chosen a - //monomial with fewest powers of 2 - ASTVec formula_out; - for(ASTVec::iterator jt=input_c.begin(),jtend=input_c.end();jt!=jtend;jt++) { - ASTNode eq = *jt; - ASTNode lhs = eq[0]; - ASTNode rhs = eq[1]; - ASTNode zero = _bm->CreateZeroConst(rhs.GetValueWidth()); - //lhs must be a BVPLUS, and rhs must be a BVCONST - if(!(BVPLUS == lhs.GetKind() && zero == rhs)) { - return input; - } - - unsigned len = lhs.GetValueWidth(); - ASTNode hi = _bm->CreateBVConst(32,len-1); - ASTNode low = _bm->CreateBVConst(32,len - power_of_2); - ASTNode low_minus_one = _bm->CreateBVConst(32,len - power_of_2 - 1); - ASTNode low_zero = _bm->CreateZeroConst(32); - unsigned newlen = len - power_of_2; - ASTNode two_const = _bm->CreateTwoConst(len); - - unsigned count = power_of_2; - ASTNode two = two_const; - while(--count) { - two = _bm->BVConstEvaluator(_bm->CreateTerm(BVMULT,len,two_const,two)); - } - ASTVec lhs_c = lhs.GetChildren(); - ASTVec lhs_out; - for(ASTVec::iterator it=lhs_c.begin(),itend=lhs_c.end();it!=itend;it++) { - ASTNode aaa = *it; - Kind itk = aaa.GetKind(); - if(BVCONST == itk) { - aaa = _bm->BVConstEvaluator(_bm->CreateTerm(BVDIV,len,aaa,two)); - aaa = _bm->BVConstEvaluator(_bm->CreateTerm(BVEXTRACT,newlen,aaa,low_minus_one,low_zero)); - } - else { - //it must be of the form a*x - ASTNode coeff = _bm->BVConstEvaluator(_bm->CreateTerm(BVDIV,len,aaa[0],two)); - coeff = _bm->BVConstEvaluator(_bm->CreateTerm(BVEXTRACT,newlen,coeff,low_minus_one,low_zero)); - ASTNode upper_x, lower_x; - //upper_x = _bm->SimplifyTerm(_bm->CreateTerm(BVEXTRACT, power_of_2, aaa[1], hi, low)); - lower_x = _bm->SimplifyTerm(_bm->CreateTerm(BVEXTRACT, newlen,aaa[1],low_minus_one,low_zero)); - aaa = _bm->CreateTerm(BVMULT,newlen,coeff,lower_x); - } - lhs_out.push_back(aaa); - }//end of inner forloop() - rhs = _bm->CreateZeroConst(newlen); - lhs = _bm->CreateTerm(BVPLUS,newlen,lhs_out); - formula_out.push_back(_bm->CreateSimplifiedEQ(lhs,rhs)); - } //end of outer forloop() - - output = - (formula_out.size() > 0) ? (formula_out.size() > 1) ? _bm->CreateNode(AND,formula_out) : formula_out[0] : ASTTrue; - - UpdateAlreadySolvedMap(input,output); - return output; - } //end of BVSolve_Even() -} //end of namespace BEEV |