Initial KLEE checkin.

 - Lots more tweaks, documentation, and web page content is needed,
   but this should compile & work on OS X & Linux.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8

1 files changed, 714 insertions, 0 deletions

diff --git a/stp/simplifier/bvsolver.cpp b/stp/simplifier/bvsolver.cpp
new file mode 100644
index 00000000..1c08f30b
--- /dev/null
+++ b/stp/simplifier/bvsolver.cpp
@@ -0,0 +1,714 @@
+/********************************************************************
+ * 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