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

4 files changed, 3354 insertions, 0 deletions

diff --git a/stp/simplifier/Makefile b/stp/simplifier/Makefile
new file mode 100644
index 00000000..aba07e1b
--- /dev/null
+++ b/stp/simplifier/Makefile
@@ -0,0 +1,11 @@
+include ../Makefile.common
+
+SRCS = simplifier.cpp bvsolver.cpp
+OBJS = $(SRCS:.cpp=.o)
+
+libsimplifier.a: $(OBJS)
+	$(AR) rc $@ $^
+	$(RANLIB) $@
+
+clean:	
+	rm -rf *.o *~ *.a .#*
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
diff --git a/stp/simplifier/bvsolver.h b/stp/simplifier/bvsolver.h
new file mode 100644
index 00000000..a8981b12
--- /dev/null
+++ b/stp/simplifier/bvsolver.h
@@ -0,0 +1,134 @@
+/********************************************************************
+ * 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"
+namespace BEEV {
+
+  //This class represents the bitvector arithmetic linear solver.
+  //
+  //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 
+  class BVSolver {
+    //Ptr to toplevel manager that manages bit-vector expressions
+    //(i.e. construct various kinds of expressions), and also has
+    //member functions that simplify bit-vector expressions
+    BeevMgr * _bm;
+    ASTNode ASTTrue, ASTFalse;
+
+    //Those formulas which have already been solved. If the same
+    //formula occurs twice then do not solve the second occurence, and
+    //instead drop it
+    ASTNodeMap FormulasAlreadySolvedMap;
+
+    //this map is useful while traversing terms and uniquely
+    //identifying variables in the those terms. Prevents double
+    //counting.
+    ASTNodeMap TermsAlreadySeenMap;
+    ASTNodeMap TermsAlreadySeenMap_ForArrays;
+
+    //count is used in the creation of new variables
+    unsigned int _symbol_count;
+
+    //solved variables list: If a variable has been solved for then do
+    //not solve for it again
+    ASTNodeSet DoNotSolve_TheseVars;
+
+    //checks if var has been solved for or not. if yes, then return
+    //true else return false
+    bool DoNotSolveThis(const ASTNode& var);
+
+    //traverses a term, and creates a multiset of all variables in the
+    //term. Does memoization to avoid double counting.
+    void VarsInTheTerm(const ASTNode& lhs, ASTNodeMultiSet& v);
+    void VarsInTheTerm_TopLevel(const ASTNode& lhs, ASTNodeMultiSet& v);
+
+    //choose a suitable var from the term
+    ASTNode ChooseMonom(const ASTNode& eq, ASTNode& modifiedterm);
+    //accepts an equation and solves for a variable or a monom in it
+    ASTNode BVSolve_Odd(const ASTNode& eq);
+
+    //solves equations of the form a*x=t where 'a' is even. Has a
+    //return value, unlike the normal BVSolve()
+    ASTNode BVSolve_Even(const ASTNode& eq);
+    ASTNode CheckEvenEqn(const ASTNode& input, bool& evenflag);
+
+    //Checks for arrayreads in a term. if yes then returns true, else
+    //return false
+    bool CheckForArrayReads(const ASTNode& term);
+    bool CheckForArrayReads_TopLevel(const ASTNode& term);
+
+    //Creates new variables used in solving
+    ASTNode NewVar(unsigned int n);
+
+    //this function return true if the var occurs in term, else the
+    //function returns false
+    bool VarSeenInTerm(const ASTNode& var, const ASTNode& term);
+    
+    //takes an even number "in" as input, and returns an odd number
+    //(return value) and a power of 2 (as number_shifts by reference),
+    //such that in = (odd_number * power_of_2).
+    //
+    //Refer STP's CAV 2007 (or Clark Barrett's 1998 paper on
+    //bit-vector arithmetic published in DAC 1998) paper for precise
+    //understanding of the algorithm
+    ASTNode SplitEven_into_Oddnum_PowerOf2(const ASTNode& in, unsigned int& number_shifts);
+
+    //Once a formula has been solved, then update the alreadysolvedmap
+    //with the formula, and the solved value. The solved value can be
+    //described using the following example: Suppose input to the
+    //solver is
+    //
+    // input key: x = 2 AND y = x + t
+    //
+    // output value: y = 2 + t
+    void UpdateAlreadySolvedMap(const ASTNode& key, const ASTNode& value);
+
+    //This function checks if the key (formula) has already been
+    //solved for.
+    //
+    //If yes it returns TRUE and fills the "output" with the
+    //solved-value (call by reference argument),
+    //
+    //else returns FALSE
+    bool CheckAlreadySolvedMap(const ASTNode& key, ASTNode& output);
+  public:
+    //constructor
+    BVSolver(BeevMgr * bm) : _bm(bm), _symbol_count(0) {
+      ASTTrue = _bm->CreateNode(TRUE);
+      ASTFalse = _bm->CreateNode(FALSE);
+    };
+
+    //Destructor
+    ~BVSolver() {
+      TermsAlreadySeenMap.clear();
+      DoNotSolve_TheseVars.clear();
+    }
+
+    //Top Level Solver: Goes over the input DAG, identifies the
+    //equation to be solved, solves them,
+    ASTNode TopLevelBVSolve(const ASTNode& a);
+  }; //end of class bvsolver
+};//end of namespace BEEV
diff --git a/stp/simplifier/simplifier.cpp b/stp/simplifier/simplifier.cpp
new file mode 100644
index 00000000..2a627398
--- /dev/null
+++ b/stp/simplifier/simplifier.cpp
@@ -0,0 +1,2495 @@
+/********************************************************************
+ * 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"
+namespace BEEV {
+  
+  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");
+      return true;
+    }
+
+    if(pushNeg && (it = SimplifyMap.find(key)) != SimplifyMap.end()) {
+      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) 
+      SimplifyNegMap[key] = value;
+    else
+      SimplifyMap[key] = value;
+  }
+
+  bool BeevMgr::CheckSubstitutionMap(const ASTNode& key, ASTNode& output) {
+    ASTNodeMap::iterator it;
+    if((it = SolverMap.find(key)) != SolverMap.end()) {
+      output = it->second;
+      return true;
+    }
+    return false;
+  }
+  
+  bool BeevMgr::CheckSubstitutionMap(const ASTNode& key) {
+    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    
+    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)) { 
+      SolverMap[e1] = e0;
+      return true;
+    }
+
+    return false;
+  }
+
+  bool BeevMgr::CheckMultInverseMap(const ASTNode& key, ASTNode& output) {
+    ASTNodeMap::iterator it;
+    if((it = MultInverseMap.find(key)) != MultInverseMap.end()) {
+      output = it->second;
+      return true;
+    }
+    return false;
+  }
+
+  void BeevMgr::UpdateMultInverseMap(const ASTNode& key, const ASTNode& value) {
+      MultInverseMap[key] = value;
+  }
+
+
+  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);
+  }
+
+  //if a is READ(Arr,const) or SYMBOL, and b is BVCONST then return 1
+  //if b is READ(Arr,const) or SYMBOL, and a is BVCONST then return -1
+  //
+  //else return 0 by default
+   int BeevMgr::TermOrder(const ASTNode& a, const ASTNode& b) {
+    Kind k1 = a.GetKind();
+    Kind k2 = b.GetKind();
+
+    //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 && 
+	a[1].GetKind() == BVCONST
+	)
+       && 
+       (k2 == BVCONST)
+       )
+      return 1;
+
+    if(k1 == SYMBOL) 
+      return 1;
+
+    //b is of the form READ(Arr,const), and a is const, or
+    //b is of the form var, and a is const
+    if((k1  == BVCONST)
+       &&
+       ((k2 == READ
+	 && 
+	 b[0].GetKind() == SYMBOL &&
+	 b[1].GetKind() == BVCONST
+	 ) 
+	 ||
+	k2 == SYMBOL
+	))
+      return -1;
+    return 0;
+  }
+
+  //This function records all the const-indices seen so far for each
+  //array. It populates the map '_arrayname_readindices' whose key is
+  //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.  
+  //
+  //Since these arrayreads are being nuked and recorded in the
+  //substitutionmap, we have to also record the fact that each
+  //arrayread (e0 is of the form READ(Arr,const) here is represented
+  //by a BVCONST (e1). This is necessary for later Leibnitz Axiom
+  //generation
+  void BeevMgr::FillUp_ArrReadIndex_Vec(const ASTNode& e0, const ASTNode& e1) {
+    int i = TermOrder(e0,e1);
+    if(0 == i) return;
+
+    if(1 == i && e0.GetKind() != SYMBOL && !CheckSubstitutionMap(e0)) {
+      _arrayname_readindices[e0[0]].push_back(e0[1]);
+      //e0 is the array read : READ(A,i) and e1 is a bvconst
+      _arrayread_symbol[e0] = e1;
+      return;
+    }
+    if(-1 == i && e1.GetKind() != SYMBOL &&  !CheckSubstitutionMap(e1)) {
+      _arrayname_readindices[e1[0]].push_back(e1[1]);
+      //e0 is the array read : READ(A,i) and e1 is a bvconst
+      _arrayread_symbol[e1] = e0;
+      return;
+    }
+  }
+
+  ASTNode BeevMgr::SimplifyFormula_NoRemoveWrites(const ASTNode& b, bool pushNeg) {
+    Begin_RemoveWrites = false;
+    ASTNode out = SimplifyFormula(b,pushNeg);
+    return out;
+  }
+
+  ASTNode BeevMgr::SimplifyFormula_TopLevel(const ASTNode& b, bool pushNeg) {
+    SimplifyMap.clear();
+    SimplifyNegMap.clear();
+    ASTNode out = SimplifyFormula(b,pushNeg);
+    SimplifyMap.clear();
+    SimplifyNegMap.clear();
+    return out;
+  }
+
+  ASTNode BeevMgr::SimplifyFormula(const ASTNode& b, bool pushNeg){
+    if(!optimize)
+      return b;
+
+    Kind kind = b.GetKind();
+    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 || 
+	 ITE == kind ||
+	 isAtomic(kind))) {
+      SortByExprNum(ca);
+      a = CreateNode(kind,ca);
+    }
+
+    ASTNode output;
+    if(CheckSimplifyMap(a,output,pushNeg))
+      return output;
+
+    switch(kind){
+    case AND:
+    case OR:
+      output = SimplifyAndOrFormula(a,pushNeg);
+      break;
+    case NOT:
+      output = SimplifyNotFormula(a,pushNeg);
+      break;
+    case XOR:
+      output = SimplifyXorFormula(a,pushNeg);
+      break;
+    case NAND:
+      output = SimplifyNandFormula(a,pushNeg);
+      break;
+    case NOR:
+      output = SimplifyNorFormula(a,pushNeg);
+      break;
+    case IFF:
+      output = SimplifyIffFormula(a,pushNeg);
+      break;
+    case IMPLIES:
+      output = SimplifyImpliesFormula(a,pushNeg);
+      break;
+    case ITE:
+      output = SimplifyIteFormula(a,pushNeg);
+      break;
+    default:
+      //kind can be EQ,NEQ,BVLT,BVLE,... or a propositional variable
+      output = SimplifyAtomicFormula(a,pushNeg);
+      //output = pushNeg ? CreateNode(NOT,a) : a;
+      break;
+    }
+
+    //memoize
+    UpdateSimplifyMap(a,output, pushNeg);
+    return output;
+  }
+    
+  ASTNode BeevMgr::SimplifyAtomicFormula(const ASTNode& a, bool pushNeg) {    
+    if(!optimize) {
+      return a;
+    }
+
+    ASTNode output;
+    if(CheckSimplifyMap(a,output,pushNeg)) {
+      return output;
+    }
+
+    ASTNode left,right;
+    if(a.Degree() == 2) {
+      //cerr << "Input to simplifyterm: left: " << a[0] << endl;
+      left = SimplifyTerm(a[0]);
+      //cerr << "Output of simplifyterm:left: " << left << endl;
+      //cerr << "Input to simplifyterm: right: " << a[1] << endl;
+      right = SimplifyTerm(a[1]);
+      //cerr << "Output of simplifyterm:left: " << right << endl;
+    }
+
+    Kind kind = a.GetKind();
+    switch(kind) {
+    case TRUE:
+      output = pushNeg ? ASTFalse : ASTTrue;
+      break;
+    case FALSE:
+      output = pushNeg ? ASTTrue : ASTFalse;
+      break;
+    case SYMBOL:
+      if(!CheckSolverMap(a,output)) {
+	output = a;
+      }
+      output = pushNeg ? CreateNode(NOT,output) : output;           
+      break;
+    case BVGETBIT: {
+      ASTNode term = SimplifyTerm(a[0]);
+      ASTNode thebit = a[1];
+      ASTNode zero = CreateZeroConst(1);
+      ASTNode one = CreateOneConst(1);
+      ASTNode getthebit = SimplifyTerm(CreateTerm(BVEXTRACT,1,term,thebit,thebit));
+      if(getthebit == zero)
+	output = pushNeg ? ASTTrue : ASTFalse;
+      else if(getthebit == one)
+	output = pushNeg ? ASTFalse : ASTTrue;
+      else {
+	output = CreateNode(BVGETBIT,term,thebit);
+	output = pushNeg ? CreateNode(NOT,output) : output;
+      }
+      break;
+    }
+    case EQ:{
+      output = CreateSimplifiedEQ(left,right);
+      output = LhsMinusRhs(output);
+      output = ITEOpt_InEqs(output);
+      if(output == ASTTrue)
+	output = pushNeg ? ASTFalse : ASTTrue;
+      else if (output == ASTFalse)
+	output = pushNeg ? ASTTrue : ASTFalse;
+      else
+	output = pushNeg ? CreateNode(NOT,output) : output;
+      break;  
+    } 
+    case NEQ: {
+      output = CreateSimplifiedEQ(left,right);
+      output = LhsMinusRhs(output);
+      if(output == ASTTrue)
+      	output = pushNeg ? ASTTrue : ASTFalse;
+      else if (output == ASTFalse)
+      	output = pushNeg ? ASTFalse : ASTTrue;
+      else
+	output = pushNeg ? output : CreateNode(NOT,output);
+      break;
+    }
+    case BVLT:
+    case BVLE:
+    case BVGT:
+    case BVGE:
+    case BVSLT:
+    case BVSLE:
+    case BVSGT:
+    case BVSGE: {
+      //output = CreateNode(kind,left,right);
+      //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;      
+    }
+
+    //memoize
+    UpdateSimplifyMap(a,output,pushNeg);
+    return output;
+  } //end of SimplifyAtomicFormula()
+
+  ASTNode BeevMgr::CreateSimplifiedINEQ(Kind k, 
+					const ASTNode& left, 
+					const ASTNode& right, 
+					bool pushNeg) {
+    ASTNode output;
+    if(BVCONST == left.GetKind() && BVCONST == right.GetKind()) {
+      output = BVConstEvaluator(CreateNode(k,left,right));
+      output = pushNeg ? (ASTFalse == output) ? ASTTrue : ASTFalse : output;
+      return output;
+    }
+
+    unsigned len = left.GetValueWidth();
+    ASTNode zero = CreateZeroConst(len);
+    ASTNode one = CreateOneConst(len);
+    ASTNode max = CreateMaxConst(len);
+    switch(k){
+    case BVLT:
+      if(right == zero) {
+	output = pushNeg ? ASTTrue : ASTFalse;
+      }
+      else if(left == right) {
+	output = pushNeg ? ASTTrue : ASTFalse;
+      }
+      else if(one == right) {
+	output = CreateSimplifiedEQ(left,zero);
+	output = pushNeg ? CreateNode(NOT,output) : output;
+      }
+      else {
+	output = pushNeg ? CreateNode(BVLE,right,left) : CreateNode(BVLT,left,right);
+      }
+      break;
+    case BVLE:
+      if(left == zero) {
+	output = pushNeg ? ASTFalse : ASTTrue;
+      }
+      else if(left == right) {
+	output = pushNeg ? ASTFalse : ASTTrue;
+      }
+      else if(max == right) {
+	output = pushNeg ? ASTFalse : ASTTrue;
+      }
+      else if(zero == right) {
+	output = CreateSimplifiedEQ(left,zero);
+	output = pushNeg ? CreateNode(NOT,output) : output;
+      }
+      else {
+	output = pushNeg ? CreateNode(BVLT,right,left) : CreateNode(BVLE,left,right);
+      }
+      break;
+    case BVGT:
+      if(left == zero) {
+	output = pushNeg ? ASTTrue : ASTFalse;
+      }
+      else if(left == right) {
+	output = pushNeg ? ASTTrue : ASTFalse;
+      }
+      else {
+      output = pushNeg ? CreateNode(BVLE,left,right) : CreateNode(BVLT,right,left);
+      }
+      break;
+    case BVGE:
+      if(right == zero) {
+	output = pushNeg ? ASTFalse : ASTTrue;
+      }
+      else if(left == right) {
+	output = pushNeg ? ASTFalse : ASTTrue;
+      }
+      else {
+      output = pushNeg ? CreateNode(BVLT,left,right) : CreateNode(BVLE,right,left);
+      }
+      break;
+    case BVSLT:
+    case BVSLE:
+    case BVSGE:
+    case BVSGT: {
+      output = CreateNode(k,left,right);
+      output = pushNeg ? CreateNode(NOT,output) : output;
+    }
+      break;
+    default:
+      FatalError("Wrong Kind");
+      break;
+    }
+
+    return output;
+  }
+
+  //takes care of some simple ITE Optimizations in the context of equations
+  ASTNode BeevMgr::ITEOpt_InEqs(const ASTNode& in) {
+    CountersAndStats("ITEOpts_InEqs");
+
+    if(!(EQ == in.GetKind() && optimize)) {
+      return in;
+    }
+
+    ASTNode output;
+    if(CheckSimplifyMap(in,output,false)) {
+      return output;
+    }
+
+    ASTNode in1 = in[0];
+    ASTNode in2 = in[1];
+    Kind k1 = in1.GetKind();
+    Kind k2 = in2.GetKind();
+    if(in1 == in2) {
+      //terms are syntactically the same
+      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() && 
+	    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:
+      //
+      // c = ITE(cond,c,d) <=> cond
+      //
+      // similarly ITE(cond,c,d) = c <=> cond
+      //
+      // c = ITE(cond,d,c) <=> NOT(cond) 
+      //
+      //similarly ITE(cond,d,c) = d <=> NOT(cond)
+      ASTNode cond = in1[0];
+      if(in1[1] == in2) {
+	//ITE(cond, c, d) = c <=> cond
+	output = cond;
+      }
+      else if(in1[2] == in2) {
+	cond = SimplifyFormula(cond,true);
+	output = cond;
+      }
+      else {
+	//last resort is to CreateNode
+	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) {
+	//ITE(cond, c, d) = c <=> cond
+	output = cond;
+      }
+      else if(in2[2] == in1) {
+	cond = SimplifyFormula(cond,true);
+	output = cond;
+      }
+      else {
+	//last resort is to CreateNode
+	output = CreateNode(EQ,in1,in2);   
+      }    
+    }
+    else {
+      //last resort is to CreateNode
+      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");        
+    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;    
+    
+    //here the terms are definitely not syntactically equal but may be
+    //semantically equal.    
+    if(BVCONST == k1 && BVCONST == k2)
+      return ASTFalse;
+    
+    //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, 
+					   const ASTNode& in1, const ASTNode& in2) {
+    ASTNode t0 = in0;
+    ASTNode t1 = in1;
+    ASTNode t2 = in2;
+    CountersAndStats("CreateSimplifiedITE");
+    if(!optimize) {
+      if(t1.GetValueWidth() != t2.GetValueWidth()) {
+	cerr << "t2 is : = " << t2;
+	FatalError("CreateSimplifiedTermITE: the lengths of then and else branches don't match",t1);
+      }
+      if(t1.GetIndexWidth() != t2.GetIndexWidth()) {
+	cerr << "t2 is : = " << t2;
+	FatalError("CreateSimplifiedTermITE: the lengths of then and else branches don't match",t1);
+      }
+      return CreateTerm(ITE,t1.GetValueWidth(),t0,t1,t2);
+    }
+
+    if(t0 == ASTTrue)
+      return t1;
+    if (t0 == ASTFalse)
+      return t2;    
+    if(t1 == t2)
+      return t1;    
+    if(CheckAlwaysTrueFormMap(t0)) {
+	return t1;
+    }     
+    if(CheckAlwaysTrueFormMap(CreateNode(NOT,t0)) || 
+       (NOT == t0.GetKind() && CheckAlwaysTrueFormMap(t0[0]))) {
+      return t2;
+    }
+    
+    return CreateTerm(ITE,t1.GetValueWidth(),t0,t1,t2);
+  }
+
+  ASTNode BeevMgr::SimplifyAndOrFormula(const ASTNode& a, bool pushNeg) {
+    ASTNode output;
+    //cerr << "input:\n" << a << endl;
+
+    if(CheckSimplifyMap(a,output,pushNeg))
+      return output;
+
+    ASTVec c, outvec;
+    c = a.GetChildren();
+    ASTNode flat = FlattenOneLevel(a);
+    c = flat.GetChildren();
+    SortByExprNum(c);
+
+    Kind k = a.GetKind();
+    bool isAnd = (k == AND) ? true : false;
+
+    ASTNode annihilator = isAnd ? 
+      (pushNeg ? ASTTrue : ASTFalse): 
+      (pushNeg ? ASTFalse : ASTTrue);
+
+    ASTNode identity = isAnd ? 
+      (pushNeg ? ASTFalse : ASTTrue): 
+      (pushNeg ? ASTTrue : ASTFalse);
+
+    //do the work
+    ASTVec::const_iterator next_it;
+    for(ASTVec::const_iterator i=c.begin(),iend=c.end();i!=iend;i++) {
+      ASTNode aaa = *i;
+      next_it = i+1;
+      bool nextexists = (next_it < iend);
+      
+      aaa = SimplifyFormula(aaa,pushNeg);
+      if(annihilator == aaa) {
+	//memoize
+	UpdateSimplifyMap(*i,annihilator,pushNeg);
+	UpdateSimplifyMap(a, annihilator,pushNeg);
+	//cerr << "annihilator1: output:\n" << annihilator << endl;
+	return annihilator;
+      }
+      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 && 
+      	      ((bbb.GetKind() == NOT && bbb[0] == aaa))) {
+      	//memoize
+      	UpdateSimplifyMap(a, annihilator,pushNeg);
+      	//cerr << "annihilator2: output:\n" << annihilator << endl;
+      	return annihilator;
+      }
+      else if(identity == aaa) {
+	// //drop identites
+      }
+      else if((!isAnd && !pushNeg) ||
+	      (isAnd && pushNeg)) { 
+	outvec.push_back(aaa);	
+      }
+      else if((isAnd && !pushNeg) ||
+	      (!isAnd && pushNeg)) {
+	outvec.push_back(aaa);	
+      }
+      else {
+	outvec.push_back(aaa);
+      }
+    }
+
+    switch(outvec.size()) {
+    case 0: {
+      //only identities were dropped 
+      output = identity;
+      break;
+    }
+    case 1: {
+      output = SimplifyFormula(outvec[0],false);
+      break;
+    }
+    default: {
+      output = (isAnd) ? 
+	(pushNeg ? CreateNode(OR,outvec) : CreateNode(AND,outvec)): 
+	(pushNeg ? CreateNode(AND,outvec) : CreateNode(OR,outvec));
+      //output = FlattenOneLevel(output);
+      break;
+    }
+    }
+    //memoize
+    UpdateSimplifyMap(a,output,pushNeg);
+    //cerr << "output:\n" << output << endl;
+    return output;
+  } //end of SimplifyAndOrFormula
+
+
+  ASTNode BeevMgr::SimplifyNotFormula(const ASTNode& a, bool pushNeg) {
+    ASTNode output;
+    if(CheckSimplifyMap(a,output,pushNeg))
+      return output;
+
+    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
+    unsigned int NotCount = pushNeg ? 1 : 0;
+    ASTNode o = a;
+    //count the number of NOTs in 'a'
+    while(NOT == o.GetKind()) {
+      o = o[0];
+      NotCount++;
+    }
+
+    //pushnegation if there are odd number of NOTs
+    bool pn = (NotCount % 2 == 0) ? false : true;
+
+    if(CheckAlwaysTrueFormMap(o)) {
+      output = pn ? ASTFalse : ASTTrue;
+      return output;
+    }
+
+    if(CheckSimplifyMap(o,output,pn)) {
+      return output;
+    }
+
+    if (ASTTrue == o) {
+      output = pn ? ASTFalse : ASTTrue;
+    }
+    else if (ASTFalse == o) {
+      output = pn ? ASTTrue : ASTFalse;
+    }
+    else {
+      output = SimplifyFormula(o,pn);
+    }
+    //memoize
+    UpdateSimplifyMap(o,output,pn);
+    UpdateSimplifyMap(a,output,pushNeg);
+    return output;
+  }
+
+  ASTNode BeevMgr::SimplifyXorFormula(const ASTNode& a, bool pushNeg) {
+    ASTNode output;
+    if(CheckSimplifyMap(a,output,pushNeg))
+      return output;
+
+    if (a.GetChildren().size() > 2) {
+      FatalError("Simplify got an XOR with more than two children.");
+    }
+
+    ASTNode a0 = SimplifyFormula(a[0],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(a0 == a1)
+	output = ASTFalse;
+      else if((a0 == ASTTrue  && a1 == ASTFalse) ||
+	      (a0 == ASTFalse && a1 == ASTTrue))
+	output = ASTTrue;
+    }
+
+    //memoize
+    UpdateSimplifyMap(a,output,pushNeg);
+    return output;
+  }
+
+  ASTNode BeevMgr::SimplifyNandFormula(const ASTNode& a, bool pushNeg) {
+    ASTNode output,a0,a1;
+    if(CheckSimplifyMap(a,output,pushNeg))
+      return output;
+
+    //the two NOTs cancel out
+    if(pushNeg) {
+      a0 = SimplifyFormula(a[0],false);
+      a1 = SimplifyFormula(a[1],false);
+      output = CreateNode(AND,a0,a1);
+    }
+    else {
+      //push the NOT implicit in the NAND
+      a0 = SimplifyFormula(a[0],true);
+      a1 = SimplifyFormula(a[1],true);
+      output = CreateNode(OR,a0,a1);
+    }
+
+    //memoize
+    UpdateSimplifyMap(a,output,pushNeg);
+    return output;
+  }
+
+  ASTNode BeevMgr::SimplifyNorFormula(const ASTNode& a, bool pushNeg) {
+    ASTNode output,a0,a1;
+    if(CheckSimplifyMap(a,output,pushNeg))
+      return output;
+
+    //the two NOTs cancel out
+    if(pushNeg) {
+      a0 = SimplifyFormula(a[0],false);
+      a1 = SimplifyFormula(a[1],false);
+      output = CreateNode(OR,a0,a1);
+    }
+    else {
+      //push the NOT implicit in the NAND
+      a0 = SimplifyFormula(a[0],true);
+      a1 = SimplifyFormula(a[1],true);
+      output = CreateNode(AND,a0,a1);
+    }
+
+    //memoize
+    UpdateSimplifyMap(a,output,pushNeg);
+    return output;
+  }
+
+  ASTNode BeevMgr::SimplifyImpliesFormula(const ASTNode& a, bool pushNeg) {
+    ASTNode output;
+    if(CheckSimplifyMap(a,output,pushNeg))
+      return output;
+
+    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);
+      c1 = SimplifyFormula(a[1],true);
+      output = CreateNode(AND,c0,c1);
+    }
+    else {
+      c0 = SimplifyFormula(a[0],false);
+      c1 = SimplifyFormula(a[1],false);
+      if(ASTFalse == c0) {
+	output = ASTTrue;
+      }
+      else if (ASTTrue == c0) {
+	output = c1;
+      }
+      else if (c0 == c1) {
+	output = ASTTrue;
+      }
+      else if(CheckAlwaysTrueFormMap(c0)) {
+	// c0 AND (~c0 OR c1) <==> c1
+	//
+	//applying modus ponens
+	output = c1;
+      }
+      else if(CheckAlwaysTrueFormMap(c1)	||
+	      CheckAlwaysTrueFormMap(CreateNode(NOT,c0)) ||
+	      (NOT == c0.GetKind() && CheckAlwaysTrueFormMap(c0[0]))) {
+	//(~c0 AND (~c0 OR c1)) <==> TRUE
+	//
+	//(c0 AND ~c0->c1) <==> TRUE
+	output = ASTTrue;
+      }
+      else if (CheckAlwaysTrueFormMap(CreateNode(NOT,c1)) ||
+	       (NOT == c1.GetKind() && CheckAlwaysTrueFormMap(c1[0]))) {
+	//(~c1 AND c0->c1) <==> (~c1 AND ~c1->~c0) <==> ~c0
+	//(c1 AND c0->~c1) <==> (c1 AND c1->~c0) <==> ~c0
+	output = CreateNode(NOT,c0);
+      }
+      else {
+	if(NOT == c0.GetKind()) {
+	  output = CreateNode(OR,c0[0],c1);
+	}
+	else {
+	  output = CreateNode(OR,CreateNode(NOT,c0),c1);
+	}
+      }
+    }
+
+    //memoize
+    UpdateSimplifyMap(a,output,pushNeg);
+    return output;
+  }
+
+  ASTNode BeevMgr::SimplifyIffFormula(const ASTNode& a, bool pushNeg) {
+    ASTNode output;
+    if(CheckSimplifyMap(a,output,pushNeg))
+      return output;
+
+    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 
+      c0 = SimplifyFormula(c0,false);
+
+    if(ASTTrue == c0) {
+      output = c1;
+    }
+    else if (ASTFalse == c0) {
+      output = SimplifyFormula(c1,true);
+    }
+    else if (ASTTrue == c1) {
+      output = c0;
+    }
+    else if (ASTFalse == c1) {
+      output = SimplifyFormula(c0,true);
+    }
+    else if (c0 == c1) {
+      output = ASTTrue;
+    }
+    else if((NOT == c0.GetKind() && c0[0] == c1) ||
+	    (NOT == c1.GetKind() && c0 == c1[0])) {
+      output = ASTFalse;
+    }
+    else if(CheckAlwaysTrueFormMap(c0)) {
+      output = c1;
+    }
+    else if(CheckAlwaysTrueFormMap(c1)) {
+      output = c0;
+    }
+    else if(CheckAlwaysTrueFormMap(CreateNode(NOT,c0))) {
+      output = CreateNode(NOT,c1);
+    }
+    else if(CheckAlwaysTrueFormMap(CreateNode(NOT,c1))) {
+      output = CreateNode(NOT,c0);
+    }
+    else {
+      output = CreateNode(IFF,c0,c1);
+    }
+
+    //memoize
+    UpdateSimplifyMap(a,output,pushNeg);
+    return output;
+  }
+
+  ASTNode BeevMgr::SimplifyIteFormula(const ASTNode& b, bool pushNeg) {
+    if(!optimize)
+      return b;
+
+    ASTNode output;
+    if(CheckSimplifyMap(b,output,pushNeg))
+      return output;
+
+    if(!(b.Degree() == 3 && ITE == b.GetKind()))
+      FatalError("SimplifyIteFormula: vector with wrong num of nodes",ASTUndefined);    
+    
+    ASTNode a = b;
+    ASTNode t0 = SimplifyFormula(a[0],false);
+    ASTNode t1,t2;
+    if(pushNeg) {
+      t1 = SimplifyFormula(a[1],true);
+      t2 = SimplifyFormula(a[2],true);
+    }
+    else {
+      t1 = SimplifyFormula(a[1],false);
+      t2 = SimplifyFormula(a[2],false);
+    }
+    
+    if(ASTTrue == t0) {
+      output = t1;
+    }
+    else if (ASTFalse == t0) {
+      output = t2;
+    }
+    else if (t1 == t2) {
+      output = t1;
+    }
+    else if(ASTTrue == t1 && ASTFalse == t2) {
+      output = t0;
+    }
+    else if(ASTFalse == t1 && ASTTrue == t2) {
+      output = SimplifyFormula(t0,true);
+    }
+    else if(ASTTrue == t1) {
+      output = CreateNode(OR,t0,t2);
+    }
+    else if(ASTFalse == t1) {
+      output = CreateNode(AND,CreateNode(NOT,t0),t2);
+    }
+    else if(ASTTrue == t2) {
+      output = CreateNode(OR,CreateNode(NOT,t0),t1);
+    }
+    else if(ASTFalse == t2) {
+      output = CreateNode(AND,t0,t1);
+    }
+    else if(CheckAlwaysTrueFormMap(t0)) {
+      output = t1;
+    }
+    else if(CheckAlwaysTrueFormMap(CreateNode(NOT,t0)) ||
+    	    (NOT == t0.GetKind() && CheckAlwaysTrueFormMap(t0[0]))) {
+      output = t2;
+    }
+    else {
+      output = CreateNode(ITE,t0,t1,t2);
+    }
+
+    //memoize
+    UpdateSimplifyMap(a,output,pushNeg);
+    return output;    
+  }
+
+  //one level deep flattening
+  ASTNode BeevMgr::FlattenOneLevel(const ASTNode& a) {
+    Kind k = a.GetKind();
+    if(!(BVPLUS == k || 
+	 AND == k || OR == k
+	 //|| BVAND == k 
+	 //|| BVOR == k
+	 )
+       ) {
+      return a;
+    }
+    
+    ASTNode output;
+    // if(CheckSimplifyMap(a,output,false)) {
+    //       //check memo table
+    //       //cerr << "output of SimplifyTerm Cache: " << output << endl;
+    //       return output;
+    //     }
+
+    ASTVec c = a.GetChildren();
+    ASTVec o;
+    for(ASTVec::iterator it=c.begin(),itend=c.end();it!=itend;it++) {
+      ASTNode aaa = *it;
+      if(k == aaa.GetKind()) {
+	ASTVec ac = aaa.GetChildren();
+	o.insert(o.end(),ac.begin(),ac.end());
+      }
+      else
+	o.push_back(aaa);      
+    } 
+    
+    if(is_Form_kind(k))
+      output = CreateNode(k,o);
+    else
+      output = CreateTerm(k,a.GetValueWidth(),o);
+
+    //UpdateSimplifyMap(a,output,false);
+    return output;
+    //memoize
+  } //end of flattenonelevel()
+
+  ASTNode BeevMgr::SimplifyTerm_TopLevel(const ASTNode& b) {
+    SimplifyMap.clear();
+    SimplifyNegMap.clear();
+    ASTNode out = SimplifyTerm(b);
+    SimplifyNegMap.clear();
+    SimplifyMap.clear();
+    return out;
+  }
+
+  //This function simplifies terms based on their kind
+  ASTNode BeevMgr::SimplifyTerm(const ASTNode& inputterm) {
+    //cout << "SimplifyTerm: input: " << a << endl;
+    if(!optimize) {
+      return inputterm;
+    }
+
+    BVTypeCheck(inputterm);
+    ASTNode output;
+    if(wordlevel_solve && CheckSolverMap(inputterm,output)) {
+      //cout << "SimplifyTerm: output: " << output << endl;
+      return SimplifyTerm(output);     
+    }
+
+    if(CheckSimplifyMap(inputterm,output,false)) {
+      //cerr << "output of SimplifyTerm Cache: " << output << endl;
+      return 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();
+      SortByExprNum(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
+	    SortByExprNum(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();
+	SortByExprNum(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 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();
+      SortByExprNum(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;
+	  //memoize
+	  UpdateSimplifyMap(inputterm,output,false);
+	  //cerr << "output of SimplifyTerm: " << output << endl;
+	  return output;
+	}
+	
+	if(aaa != identity) {
+	  o.push_back(aaa);
+	}
+      }
+      
+      switch(o.size()) {
+      case 0:
+	output = identity;
+	break;
+      case 1:
+	output = o[0];
+	break;
+      default:
+	SortByExprNum(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 arr1 = SimplifyTerm(inputterm[0][1]);
+	  ASTNode arr2 = SimplifyTerm(inputterm[0][2]);
+
+	  ASTNode index = SimplifyTerm(inputterm[1]);
+	  
+	  ASTNode read1 = CreateTerm(READ,inputValueWidth,arr1,index);
+	  ASTNode read2 = CreateTerm(READ,inputValueWidth,arr2,index);
+	  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 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("SimplifyTerm: Control should never reach here:", inputterm, k);
+      return inputterm;
+      break;
+    }
+
+    //memoize
+    UpdateSimplifyMap(inputterm,output,false);
+    //cerr << "SimplifyTerm: output" << output << endl;
+    return output;
+  } //end of SimplifyTerm()
+
+
+  //At the end of each simplification call, we want the output to be
+  //always smaller or equal to the input in size.
+  void BeevMgr::CheckSimplifyInvariant(const ASTNode& a, const ASTNode& output) {
+    //Don't do the check in optimized mode
+    if(optimize)
+      return;
+
+    if(NodeSize(a,true) < NodeSize(output,true)) {
+      cerr << "lhs := " << a << endl;
+      cerr << "NodeSize of lhs is: " << NodeSize(a, true) << endl;
+      cerr << endl;
+      cerr << "rhs := " << output << endl;
+      cerr << "NodeSize of rhs is: " << NodeSize(output, true) << endl;
+      FatalError("SimplifyFormula: The nodesize shoudl decrease from lhs to rhs: ",ASTUndefined);
+    }
+  }
+
+  //this function assumes that the input is a vector of childnodes of
+  //a BVPLUS term. it combines like terms and returns a bvplus
+  //term. e.g. 1.x + 2.x is converted to 3.x
+  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;
+    }
+    
+    ASTVec c = a.GetChildren();
+    //map from variables to vector of constants
+    ASTNodeToVecMap vars_to_consts;
+    //vector to hold constants
+    ASTVec constkids;
+    ASTVec outputvec;
+
+    //useful constants
+    unsigned int len = c[0].GetValueWidth();
+    ASTNode one = CreateOneConst(len);
+    ASTNode zero = CreateZeroConst(len);
+    ASTNode max = CreateMaxConst(len);
+
+    //go over the childnodes of the input bvplus, and collect like
+    //terms in a map. the key of the map are the variables, and the
+    //values are stored in a ASTVec
+    for(ASTVec::const_iterator it=c.begin(),itend=c.end();it!=itend;it++){
+      ASTNode aaa = *it;
+      if(SYMBOL == aaa.GetKind()) {
+	vars_to_consts[aaa].push_back(one);
+      }
+      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() && 
+	      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);      
+      }      
+      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]);
+	ASTVec cNodes = cccc.GetChildren();
+	SortByExprNum(cNodes);
+	vars_to_consts[cccc].push_back(max);
+      }
+      else if(BVMULT == aaa.GetKind() && BVUMINUS == aaa[1].GetKind()) {
+	//x*(-1*y) <==> -1*(xy)
+	ASTNode cccc = CreateTerm(BVMULT,len,aaa[0],aaa[1][0]);
+	ASTVec cNodes = cccc.GetChildren();
+	SortByExprNum(cNodes);
+	vars_to_consts[cccc].push_back(max);      
+      }
+      else if(BVCONST == aaa.GetKind()) {
+	constkids.push_back(aaa);
+      }
+      else if(BVUMINUS == aaa.GetKind()) {
+	//helps to convert BVUMINUS into a BVMULT. here the max
+	//constant represents -1. this transformation allows us to
+	//conclude that x + BVUMINUS(x) is 0.
+	vars_to_consts[aaa[0]].push_back(max);
+      }
+      else 
+	vars_to_consts[aaa].push_back(one);
+    } //end of for loop
+
+    //go over the map from variables to vector of values. combine the
+    //vector of values, multiply to the variable, and put the
+    //resultant monomial in the output BVPLUS.
+    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);
+	constant = BVConstEvaluator(constant);
+      }
+      else
+	constant = ccc[0];
+      
+      //constant * var
+      ASTNode monom;
+      if(zero == constant) 
+	monom = zero;
+      else if (one == constant)
+	monom = it->first;
+      else
+	monom = 
+	  SimplifyTerm(CreateTerm(BVMULT,constant.GetValueWidth(),constant,it->first));
+      if(zero != monom) {
+	outputvec.push_back(monom);
+      }
+    } //end of for loop
+
+    if(constkids.size() > 1) {
+      ASTNode output = CreateTerm(BVPLUS,constkids[0].GetValueWidth(),constkids);
+      output = BVConstEvaluator(output);
+      if(output != zero)
+	outputvec.push_back(output);
+    }
+    else if (constkids.size() == 1) {
+      if(constkids[0] != zero)
+	outputvec.push_back(constkids[0]);
+    }
+
+    if (outputvec.size() > 1) {
+      output = CreateTerm(BVPLUS,len,outputvec);
+    }
+    else if(outputvec.size() == 1) {
+      output = outputvec[0];
+    }
+    else {
+      output = zero;
+    }
+
+    //memoize
+    //UpdateSimplifyMap(a,output,false);
+    return output;
+  } //end of CombineLikeTerms()
+
+  //accepts lhs and rhs, and returns lhs - rhs = 0. The function
+  //assumes that lhs and rhs have already been simplified. although
+  //this assumption is not needed for correctness, it is essential for
+  //performance. The function also assumes that lhs is a BVPLUS
+  ASTNode BeevMgr::LhsMinusRhs(const ASTNode& eq) {
+    //if input is not an equality, simply return it
+    if(EQ != eq.GetKind())
+      return eq;
+
+    ASTNode lhs = eq[0];
+    ASTNode rhs = eq[1];
+    Kind k_lhs = lhs.GetKind();
+    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 || 
+	 BVPLUS == k_rhs ||
+	 (BVMULT == k_lhs && 
+	  BVMULT == k_rhs)
+	 )) {
+      return eq;
+    }
+
+    ASTNode output;
+    if(CheckSimplifyMap(eq,output,false)) {
+      //check memo table
+      //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;
+    if(BVPLUS != k_lhs && BVPLUS == k_rhs) {
+      ASTNode swap = lhs;
+      lhs = rhs;
+      rhs = swap;
+      swap_flag = true;
+    }
+
+    unsigned int len = lhs.GetValueWidth();
+    ASTNode zero = CreateZeroConst(len);
+    //right is -1*(rhs): Simplify(-1*rhs)
+    rhs = SimplifyTerm(CreateTerm(BVUMINUS,len,rhs));
+
+    ASTVec lvec = lhs.GetChildren();
+    ASTVec rvec = rhs.GetChildren();
+    ASTNode lhsplusrhs;
+    if(BVPLUS != lhs.GetKind() && BVPLUS != rhs.GetKind()) {
+      lhsplusrhs = CreateTerm(BVPLUS,len,lhs,rhs); 
+    }
+    else if(BVPLUS == lhs.GetKind() && BVPLUS == rhs.GetKind()) {
+      //combine the childnodes of the left and the right
+      lvec.insert(lvec.end(),rvec.begin(),rvec.end());
+      lhsplusrhs = CreateTerm(BVPLUS,len,lvec);
+    }
+    else if(BVPLUS == lhs.GetKind() && BVPLUS != rhs.GetKind()){
+      lvec.push_back(rhs);
+      lhsplusrhs = CreateTerm(BVPLUS,len,lvec);
+    }
+    else {
+      //Control should never reach here
+      FatalError("LhsMinusRhs: Control should never reach here\n");
+    }
+
+    //combine like terms
+    output = CombineLikeTerms(lhsplusrhs);
+    output = SimplifyTerm(output);
+    //
+    //Now make output into: lhs-rhs = 0
+    output = CreateSimplifiedEQ(output,zero);
+    //sort if BVPLUS
+    if(BVPLUS == output.GetKind()) {
+      ASTVec outv = output.GetChildren();
+      SortByExprNum(outv);
+      output = CreateTerm(BVPLUS,len,outv);
+    }
+    
+    //memoize
+    //UpdateSimplifyMap(eq,output,false);
+    return output;  
+  } //end of LhsMinusRHS()
+
+  //THis function accepts a BVMULT(t1,t2) and distributes the mult
+  //over plus if either or both t1 and t2 are BVPLUSes.
+  //
+  // x*(y1 + y2 + ...+ yn) <==> x*y1 + x*y2 + ... + x*yn
+  //
+  // (y1 + y2 + ...+ yn)*x <==> x*y1 + x*y2 + ... + x*yn
+  //
+  // The function assumes that the BVPLUSes have been flattened
+  ASTNode BeevMgr::DistributeMultOverPlus(const ASTNode& a, bool startdistribution) {
+    if(!startdistribution)
+      return a;
+    Kind k = a.GetKind();
+    if(BVMULT != k)
+      return a;
+
+    ASTNode left = a[0];
+    ASTNode right = a[1];
+    Kind left_kind = left.GetKind();
+    Kind right_kind = right.GetKind();
+
+    ASTNode output;
+    if(CheckSimplifyMap(a,output,false)) {
+      //check memo table
+      //cerr << "output of SimplifyTerm Cache: " << output << endl;
+      return output;
+    }
+
+    //special case optimization: c1*(c2*t1) <==> (c1*c2)*t1
+    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]);
+      return c;
+      left = c[0];
+      right = c[1];
+      left_kind = left.GetKind();
+      right_kind = right.GetKind();    
+    }
+
+    //special case optimization: c1*(t1*c2) <==> (c1*c2)*t1
+    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]);
+      return c;
+      left = c[0];
+      right = c[1];
+      left_kind = left.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;
+    if(BVPLUS == left_kind && BVPLUS != right_kind) {
+      swap = left;
+      left = right;
+      right = swap;
+    }
+    left_kind = left.GetKind();
+    right_kind = right.GetKind();
+
+    //by this point we are gauranteed that right is a BVPLUS, but left
+    //may not be
+    ASTVec rightnodes = right.GetChildren();
+    ASTVec outputvec;
+    unsigned len = a.GetValueWidth();
+    ASTNode zero = CreateZeroConst(len);
+    ASTNode one = CreateOneConst(len);
+    if(BVPLUS != left_kind) {
+      //if the multiplier is not a BVPLUS then we have a special case
+      // x*(y1 + y2 + ...+ yn) <==> x*y1 + x*y2 + ... + x*yn
+      if(zero == left) {
+	outputvec.push_back(zero);
+      }
+      else if(one == left) {
+	outputvec.push_back(left);
+      }
+      else {
+	for(ASTVec::iterator j=rightnodes.begin(),jend=rightnodes.end();
+	    j!=jend;j++) {
+	  ASTNode out = SimplifyTerm(CreateTerm(BVMULT,len,left,*j));
+	  outputvec.push_back(out);
+	}
+      }
+    }
+    else {
+      ASTVec leftnodes = left.GetChildren();
+      // (x1 + x2 + ... + xm)*(y1 + y2 + ...+ yn) <==> x1*y1 + x1*y2 +
+      // ... + x2*y1 + ... + xm*yn
+      for(ASTVec::iterator i=leftnodes.begin(),iend=leftnodes.end();
+	  i!=iend;i++) {
+	ASTNode multiplier = *i;
+	for(ASTVec::iterator j=rightnodes.begin(),jend=rightnodes.end();
+	    j!=jend;j++) {
+	  ASTNode out = SimplifyTerm(CreateTerm(BVMULT,len,multiplier,*j));
+	  outputvec.push_back(out);
+	}
+      }
+    }
+    
+    //compute output here
+    if(outputvec.size() > 1) {
+      output = CombineLikeTerms(CreateTerm(BVPLUS,len,outputvec));
+      output = SimplifyTerm(output);
+    }
+    else
+      output = SimplifyTerm(outputvec[0]);
+
+    //memoize
+    //UpdateSimplifyMap(a,output,false);
+    return output;
+  } //end of distributemultoverplus()
+
+  //converts the BVSX(len, a0) operator into ITE( check top bit,
+  //extend a0 by 1, extend a0 by 0)
+  ASTNode BeevMgr::ConvertBVSXToITE(const ASTNode& a) {
+    if(BVSX != a.GetKind())
+      return a;
+
+    ASTNode output;
+    if(CheckSimplifyMap(a,output,false)) {
+      //check memo table
+      //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) {
+      UpdateSimplifyMap(a,output,false);
+      return a;
+    }
+
+    std::string ones;
+    for(unsigned c=0; c < extensionlen;c++)
+      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
+    BEEV::ASTNode concatZeros = CreateTerm(BEEV::BVCONCAT,a_len,BVZeros,a0);
+
+    //extract top bit of a0
+    BEEV::ASTNode hi = CreateBVConst(32,a0_len-1);
+    BEEV::ASTNode low = CreateBVConst(32,a0_len-1);
+    BEEV::ASTNode topBit = CreateTerm(BEEV::BVEXTRACT,1,a0,hi,low);
+
+    //compare topBit of a0 with 0bin1
+    BEEV::ASTNode condition = CreateSimplifiedEQ(CreateBVConst(1,1),topBit);
+
+    //ITE(topbit = 0bin1, 0bin1111...a0, 0bin000...a0)
+    output = CreateSimplifiedTermITE(condition,concatOnes,concatZeros);
+    UpdateSimplifyMap(a,output,false);
+    return output;
+  } //end of ConvertBVSXToITE()
+
+
+  ASTNode BeevMgr::RemoveWrites_TopLevel(const ASTNode& term) {
+    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 && 
+       !start_abstracting) {
+      return term;
+    }
+    else if(!Begin_RemoveWrites && 
+	    SimplifyWrites_InPlace_Flag && 
+	    !start_abstracting) {
+      //return term;
+      return SimplifyWrites_InPlace(term);
+    }
+    else {
+      return RemoveWrites(term);
+    }
+  } //end of RemoveWrites_TopLevel()
+
+  ASTNode BeevMgr::SimplifyWrites_InPlace(const ASTNode& term) {
+    ASTNodeMultiSet WriteIndicesSeenSoFar;
+    bool SeenNonConstWriteIndex = false;
+
+    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;
+    }
+
+    ASTVec writeIndices, writeValues;
+    unsigned int width = term.GetValueWidth();
+    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 = 
+	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 || 
+	   ASTFalse == compare_readwrite_indices)) {
+	SeenNonConstWriteIndex = true;
+      }
+
+      //if (readIndex=writeIndex <=> FALSE)
+      if(ASTFalse == compare_readwrite_indices 
+	 ||
+	 (WriteIndicesSeenSoFar.find(writeIndex) != WriteIndicesSeenSoFar.end())
+	 ) {
+	//drop the current level write
+	//do nothing
+      }
+      else {
+	writeIndices.push_back(writeIndex);
+	writeValues.push_back(writeVal);
+      }
+      
+      //record the write indices seen so far
+      //if(BVCONST == writeIndex.GetKind()) {
+	WriteIndicesSeenSoFar.insert(writeIndex);
+	//}
+
+      //Setup the write for the new iteration, one level inner write
+      write = write[0];
+    }while (SYMBOL != write.GetKind());
+
+    ASTVec::reverse_iterator it_index = writeIndices.rbegin();
+    ASTVec::reverse_iterator itend_index = writeIndices.rend();
+    ASTVec::reverse_iterator it_values = writeValues.rbegin();
+    ASTVec::reverse_iterator itend_values = writeValues.rend();
+
+    //"write" must be a symbol at the control point before the
+    //begining of the "for loop"
+
+    for(;it_index!=itend_index;it_index++,it_values++) {
+      write = CreateTerm(WRITE,width,write,*it_index,*it_values);
+      write.SetIndexWidth(indexwidth);
+    }
+
+    output = CreateTerm(READ,width,write,readIndex);
+    UpdateSimplifyMap(term,output,false);
+    return output;
+  } //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) {   
+    //unsigned int width = input.GetValueWidth();
+    if(READ != input.GetKind() || WRITE != input[0].GetKind()) {
+      FatalError("RemovesWrites: Input must be a READ over a WRITE",input);
+    }
+
+    ASTNodeMap::iterator it;
+    ASTNode output = input;
+    if(CheckSimplifyMap(input,output,false)) {
+      return output;
+    }
+        
+    if(!start_abstracting && Begin_RemoveWrites) {
+      output= ReadOverWrite_To_ITE(input);
+    }
+
+    if(start_abstracting) {
+      ASTNode newVar;
+      if(!CheckSimplifyMap(input,newVar,false)) {
+	newVar = NewVar(input.GetValueWidth());
+	ReadOverWrite_NewName_Map[input] = newVar;
+	NewName_ReadOverWrite_Map[newVar] = input;
+
+	UpdateSimplifyMap(input,newVar,false);
+	ASTNodeStats("New Var Name which replace Read_Over_Write: ", newVar);
+      }
+      output = newVar;
+    } //end of start_abstracting if condition
+
+    //memoize
+    UpdateSimplifyMap(input,output,false);
+    return output;
+  } //end of RemoveWrites()
+
+  ASTNode BeevMgr::ReadOverWrite_To_ITE(const ASTNode& term) {
+    unsigned int width = term.GetValueWidth();
+    ASTNode input = term;
+    if(READ != term.GetKind() || WRITE != term[0].GetKind()) {
+      FatalError("RemovesWrites: Input must be a READ over a WRITE",term);
+    }
+
+    ASTNodeMap::iterator it;
+    ASTNode output;
+    // if(CheckSimplifyMap(term,output,false)) {
+    //       return output;
+    //     }
+    
+    ASTNode partialITE = term;
+    ASTNode writeA = ASTTrue;
+    ASTNode oldRead = term;
+    //iteratively expand read-over-write
+    do {
+      ASTNode write = input[0];
+      ASTNode readIndex = SimplifyTerm(input[1]);
+      //DO NOT CALL SimplifyTerm() on write[0]. You will go into an
+      //infinite loop
+      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
+	output = writeVal;
+	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 if (ITE == partialITE.GetKind()){
+	//ITE(i1 = j, v1, R(A,j))
+	ASTNode ElseITE = CreateSimplifiedTermITE(cond, writeVal, newRead);
+	//R(W(A,i1,v1),j) <==> ITE(i1 = j, v1, R(A,j))
+	UpdateSimplifyMap(oldRead,ElseITE,false);
+	//ITE(i2 = j, v2, R(W(A,i1,v1),j)) <==> ITE(i2 = j, v2, ITE(i1 = j, v1, R(A,j)))
+	partialITE = SimplifyTerm(partialITE);
+      }
+      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;
+  } //ReadOverWrite_To_ITE()
+
+  //compute the multiplicative inverse of the input
+  ASTNode BeevMgr::MultiplicativeInverse(const ASTNode& d) {
+    ASTNode c = d;
+    if(BVCONST != c.GetKind()) {
+      FatalError("Input must be a constant", c);
+    }
+
+    if(!BVConstIsOdd(c)) {
+      FatalError("MultiplicativeInverse: Input must be odd: ",c);
+    }
+    
+    //cerr << "input to multinverse function is: " << d << endl;
+    ASTNode inverse;
+    if(CheckMultInverseMap(d,inverse)) {
+      //cerr << "found the inverse of: " << d << "and it is: " << inverse << endl;
+      return inverse;
+    }
+
+    inverse = c;
+    unsigned inputwidth = c.GetValueWidth();
+
+#ifdef NATIVE_C_ARITH
+    ASTNode one = CreateOneConst(inputwidth);
+    while(c != one) {
+      //c = c*c
+      c = BVConstEvaluator(CreateTerm(BVMULT,inputwidth,c,c));
+      //inverse = invsere*c
+      inverse = BVConstEvaluator(CreateTerm(BVMULT,inputwidth,inverse,c));
+    }
+#else
+    //Compute the multiplicative inverse of c using the extended
+    //euclidian algorithm
+    //
+    //create a '0' which is 1 bit long
+    ASTNode onebit_zero = CreateZeroConst(1);
+    //zero pad t0, i.e. 0 @ t0
+    c = BVConstEvaluator(CreateTerm(BVCONCAT,inputwidth+1,onebit_zero,c));
+
+    //construct 2^(inputwidth), i.e. a bitvector of length
+    //'inputwidth+1', which is max(inputwidth)+1
+    //
+    //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);    
+    //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;
+    ASTNode x, x1, x2;
+
+    //x1 initialized to zero
+    x1 = zero;
+    //x2 initialized to one
+    x2 = CreateOneConst(inputwidth+1);
+    while (ASTTrue == BVConstEvaluator(max_bvgt_0)) {
+      //quotient = (c divided by max)
+      quotient = BVConstEvaluator(CreateTerm(BVDIV,inputwidth+1, c, max));
+
+      //remainder of (c divided by max)
+      remainder = BVConstEvaluator(CreateTerm(BVMOD,inputwidth+1, c, max));
+
+      //x = x2 - q*x1
+      x = CreateTerm(BVSUB,inputwidth+1,x2,CreateTerm(BVMULT,inputwidth+1,quotient,x1));
+      x = BVConstEvaluator(x);
+
+      //fix the inputs to the extended euclidian algo
+      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);
+    inverse = BVConstEvaluator(inverse);
+#endif
+
+    UpdateMultInverseMap(d,inverse);
+    //cerr << "output of multinverse function is: " << inverse << endl;
+    return inverse;
+  } //end of MultiplicativeInverse()
+
+  //returns true if the input is odd
+  bool BeevMgr::BVConstIsOdd(const ASTNode& c) {
+    if(BVCONST != c.GetKind()) {
+      FatalError("Input must be a constant", c);
+    }
+   
+    ASTNode zero = CreateZeroConst(1);
+    ASTNode hi = CreateZeroConst(32);
+    ASTNode low = hi;
+    ASTNode lowestbit = CreateTerm(BVEXTRACT,1,c,hi,low);
+    lowestbit =  BVConstEvaluator(lowestbit);
+
+    if(lowestbit == zero) {
+      return false;
+    }
+    else {
+      return true;
+    }
+  } //end of BVConstIsOdd()
+
+  //The big substitution function
+  ASTNode BeevMgr::CreateSubstitutionMap(const ASTNode& a){
+    if(!optimize)
+      return a;
+
+    ASTNode output = a;
+    //if the variable has been solved for, then simply return it
+    if(CheckSolverMap(a,output))
+      return output;
+
+    //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;          
+    }
+    if(NOT == k
+       && SYMBOL == a[0].GetKind()) {
+      bool updated = UpdateSubstitutionMap(a[0],ASTFalse);
+      output = updated ? ASTTrue : a;      
+      return output;          
+    }
+    
+    if(IFF == k) {
+      ASTVec c = a.GetChildren();
+      SortByExprNum(c);
+      if(SYMBOL != c[0].GetKind() || 
+    	 VarSeenInTerm(c[0],SimplifyFormula_NoRemoveWrites(c[1],false))) {
+	return a;
+      }
+      bool updated = UpdateSubstitutionMap(c[0],c[1]);
+      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
+      ASTVec c = a.GetChildren();
+      SortByExprNum(c);
+      FillUp_ArrReadIndex_Vec(c[0],c[1]);
+
+      if(SYMBOL == c[0].GetKind() && 
+	 VarSeenInTerm(c[0],SimplifyTerm(c[1]))) {
+	return a;
+      }
+
+      if(1 == TermOrder(c[0],c[1]) &&
+	 READ == c[0].GetKind() &&
+	 VarSeenInTerm(c[0][0],SimplifyTerm(c[1]))) {
+	return a;
+      }
+      bool updated = UpdateSubstitutionMap(c[0],c[1]);      
+      output = updated ? ASTTrue : a;      
+      return output;      
+    }
+
+    if(AND == k){
+      ASTVec o;
+      ASTVec c = a.GetChildren();
+      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;
+	  else
+	    o.push_back(aaa);
+	}
+      }
+      if(o.size() == 0)
+	return ASTTrue;
+
+      if(o.size() == 1)
+	return o[0];
+      
+      return CreateNode(AND,o);
+    }
+    return output;
+  } //end of CreateSubstitutionMap()
+
+
+  bool BeevMgr::VarSeenInTerm(const ASTNode& var, const ASTNode& term) {
+    if(READ == term.GetKind() && 
+       WRITE == term[0].GetKind() && !Begin_RemoveWrites) {
+      return false;
+    }
+
+    if(READ == term.GetKind() && 
+       WRITE == term[0].GetKind() && Begin_RemoveWrites) {
+      return true;
+    }
+
+    ASTNodeMap::iterator it;    
+    if((it = TermsAlreadySeenMap.find(term)) != TermsAlreadySeenMap.end()) {
+      if(it->second == var) {
+	return false;
+      }
+    }
+
+    if(var == term) {
+      return true;
+    }
+
+    for(ASTVec::const_iterator it=term.begin(),itend=term.end();it!=itend;it++){
+      if(VarSeenInTerm(var,*it)) {
+	return true;
+      }
+      else {
+	TermsAlreadySeenMap[*it] = var;
+      }
+    }
+
+    TermsAlreadySeenMap[term] = var;
+    return false;
+  }
+};//end of namespace