/********************************************************************
 * 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