theory_bitvector.cpp

Go to the documentation of this file.

/*****************************************************************************/
/*!
 * \file theory_bitvector.cpp
 * 
 * Author: Vijay Ganesh.
 * 
 * Created: Wed May  5 16:16:59 PST 2004
 *
 * <hr>
 * Copyright (C) 2003 by the Board of Trustees of Leland Stanford
 * Junior University and by New York University. 
 *
 * License to use, copy, modify, sell and/or distribute this software
 * and its documentation for any purpose is hereby granted without
 * royalty, subject to the terms and conditions defined in the \ref
 * LICENSE file provided with this distribution.  In particular:
 *
 * - The above copyright notice and this permission notice must appear
 * in all copies of the software and related documentation.
 *
 * - THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES,
 * EXPRESSED OR IMPLIED.  USE IT AT YOUR OWN RISK.
 * 
 * <hr>
 * 
 */
/*****************************************************************************/


#include "theory_bitvector.h"
#include "bitvector_proof_rules.h"
#include "bitvector_exception.h"
#include "typecheck_exception.h"
#include "parser_exception.h"
#include "smtlib_exception.h"
#include "bitvector_expr_value.h"
#include "command_line_flags.h"


#define HASH_VALUE_ZERO 380
#define HASH_VALUE_ONE  450


using namespace std;
using namespace CVCL;


///////////////////////////////////////////////////////////////////////////////
// TheoryBitvector Private Methods                                           //
///////////////////////////////////////////////////////////////////////////////

int
TheoryBitvector::BVSize(const Expr& e) {
  Type tp(getBaseType(e));
  DebugAssert(tp.getExpr().getOpKind() == BITVECTOR,
              "BVSize: e = "+e.toString());
  return getBitvectorTypeParam(tp);
}


//! accepts a bitvector equation t1 = t2. 
/*! \return a rewrite theorem which is a conjunction of equivalences
 * over the bits of t1,t2 respectively.
 */
Theorem TheoryBitvector::bitBlastEqn(const Expr& e)
{
  TRACE("bitvector", "bitBlastEqn(", e.toString(), ") {"); 
  IF_DEBUG(debugger.counter("bit-blasted eq")++);
  //stat counter
  d_bvBitBlastEq++;

  DebugAssert(e.isEq(),
              "TheoryBitvector::bitBlastEqn:"
              "expecting an equation" + e.toString());
  const Expr& leftBV = e[0];
  const Expr& rightBV = e[1];

  Theorem result = reflexivityRule(e);
  IF_DEBUG(const Type& leftType = getBaseType(leftBV));
  IF_DEBUG(const Type& rightType = getBaseType(rightBV));
  DebugAssert(BITVECTOR == leftType.getExpr().getOpKind() &&
              BITVECTOR == rightType.getExpr().getOpKind(),
              "TheoryBitvector::bitBlastEqn:"
              "lhs & rhs must be bitvectors");
  DebugAssert(BVSize(leftBV) == BVSize(rightBV),
              "TheoryBitvector::bitBlastEqn:\n e = "
              +e.toString());
  Theorem bitBlastLeftThm;
  Theorem bitBlastRightThm;
  std::vector<Theorem> substThms;
  std::vector<Theorem> leftBVrightBVThms;
  int bvLength = BVSize(leftBV);
  int bitPosition = 0;
  Theorem thm0;

  int leftFlag = 0;
  int rightFlag = 0;
  //if(BVPLUS == leftBV.getOpKind())  leftFlag = 1;
  //if(BVPLUS == rightBV.getOpKind()) rightFlag = 2;
  if(leftFlag == 1) d_bvPlusCarryCacheLeftBV.clear();
  if(rightFlag == 2) d_bvPlusCarryCacheRightBV.clear();
  for(; bitPosition < bvLength; bitPosition = bitPosition+1) {
    //bitBlastLeftThm is the theorem 'leftBV[bitPosition] <==> phi'
    bitBlastLeftThm = bitBlastTerm(leftBV, bitPosition,leftFlag);
    //bitBlastRightThm is the theorem 'rightBV[bitPosition] <==> theta'
    bitBlastRightThm = bitBlastTerm(rightBV, bitPosition,rightFlag);
    //collect the two theorems created above in the vector
    //leftBVrightBVthms.
    leftBVrightBVThms.push_back(bitBlastLeftThm); 
    leftBVrightBVThms.push_back(bitBlastRightThm);
    //construct (leftBV[bitPosition] <==> rightBV[bitPosition]) 
    //<====> phi <==> theta
    //and store in the vector substThms.
    Theorem thm = substitutivityRule(IFF, leftBVrightBVThms);
    thm = transitivityRule(thm, rewriteBoolean(thm.getRHS()));    
    leftBVrightBVThms.clear();
    substThms.push_back(thm); 
    //if phi <==> theta is false, then stop bitblasting. immediately
    //exit and return false.
    if(thm.getRHS().isFalse())
      return transitivityRule(result,
                              d_rules->bitvectorFalseRule(thm));
  }
  // AND_0^bvLength(leftBV[bitPosition] <==> rightBV[bitPosition]) <====>
  // AND_0^bvLength(phi <==> theta)
  Theorem thm = substitutivityRule(AND, substThms);
  // AND_0^bvLength(leftBV[bitPosition] <==> rightBV[bitPosition]) <====>
  // rewriteBoolean(AND_0^bvLength(phi <==> theta))
  thm = transitivityRule(thm, rewriteBoolean(thm.getRHS()));
  //call trusted rule for bitblasting equations.
  result = d_rules->bitBlastEqnRule(e, thm.getLHS());
  result = transitivityRule(result, thm);
  TRACE("bitvector", "bitBlastEqn => ", result.toString(), " }"); 
  return result;
}

//! accepts a bitvector equation t1 != t2. 
/*! \return a rewrite theorem which is a conjunction of
 * (dis)-equivalences over the bits of t1,t2 respectively.
 * 
 * A separate rule for disequations for efficiency sake. Obvious
 * implementation using rule for equations and rule for NOT, is not
 * efficient.
 */
Theorem TheoryBitvector::bitBlastDisEqn(const Theorem& notE)
{
  TRACE("bitvector", "bitBlastDisEqn(", notE, ") {"); 
  IF_DEBUG(debugger.counter("bit-blasted diseq")++);
  //stat counter
  d_bvBitBlastDiseq++;

  DebugAssert(notE.getExpr().isNot() && (notE.getExpr())[0].isEq(),
              "TheoryBitvector::bitBlastDisEqn:"
              "expecting an equation" + notE.getExpr().toString());
  //e is the equation
  const Expr& e = (notE.getExpr())[0];
  const Expr& leftBV = e[0];
  const Expr& rightBV = e[1];
  IF_DEBUG(Type leftType = leftBV.getType());
  IF_DEBUG(debugger.counter("bit-blasted diseq bits")+=
           BVSize(leftBV));
  IF_DEBUG(Type rightType = rightBV.getType());
  DebugAssert(BITVECTOR == leftType.getExpr().getOpKind() &&
              BITVECTOR == rightType.getExpr().getOpKind(),
              "TheoryBitvector::bitBlastDisEqn:"
              "lhs & rhs must be bitvectors");
  DebugAssert(BVSize(leftBV) == BVSize(rightBV),
              "TheoryBitvector::bitBlastDisEqn: e = "
              +e.toString());
  Theorem bitBlastLeftThm;
  Theorem bitBlastRightThm;
  std::vector<Theorem> substThms;
  std::vector<Theorem> leftBVrightBVThms;
  int bvLength = BVSize(leftBV);
  int leftFlag = 0;
  int rightFlag = 0;
  //if(BVPLUS == leftBV.getOpKind())  leftFlag = 1;
  //if(BVPLUS == rightBV.getOpKind()) rightFlag = 2;
  if(leftFlag == 1) d_bvPlusCarryCacheLeftBV.clear();
  if(rightFlag == 2) d_bvPlusCarryCacheRightBV.clear();
  int bitPosition = 0;
  for(; bitPosition < bvLength; bitPosition = bitPosition+1) {
    //bitBlastLeftThm is the theorem '~leftBV[bitPosition] <==> ~phi'
    bitBlastLeftThm =
      getCommonRules()->iffContrapositive(bitBlastTerm(leftBV, bitPosition,
                                                       leftFlag));
    //bitBlastRightThm is the theorem 'rightBV[bitPosition] <==> theta'
    bitBlastRightThm = bitBlastTerm(rightBV, bitPosition,rightFlag);
    //collect the two theorems created above in the vector leftBVrightBVthms.
    leftBVrightBVThms.push_back(bitBlastLeftThm); 
    leftBVrightBVThms.push_back(bitBlastRightThm);
    //construct (~leftBV[bitPosition] <==> rightBV[bitPosition]) 
    //<====> ~phi <==> theta
    //and store in the vector substThms.
    //recall that (p <=/=> q) is same as (~p <==> q)
    Theorem thm = substitutivityRule(IFF, leftBVrightBVThms);
    thm = transitivityRule(thm, rewriteBoolean(thm.getRHS()));
    leftBVrightBVThms.clear();
    substThms.push_back(thm); 
    
    //if phi <==> theta is the True theorem, then stop bitblasting. immediately
    //exit and return t1!=t2 <=> true.
    if(thm.getRHS().isTrue())
      return d_rules->bitvectorTrueRule(thm);
  }

  // OR_0^bvLength(~leftBV[bitPosition] <==> rightBV[bitPosition]) <====>
  // OR_0^bvLength(~phi <==> theta)
  Theorem thm1 = substitutivityRule(OR, substThms);
  // Call trusted rule for bitblasting disequations.
  Theorem result = d_rules->bitBlastDisEqnRule(notE, thm1.getLHS());
  Theorem thm2 = transitivityRule(thm1, rewriteBoolean(thm1.getRHS()));
  result = iffMP(result, thm2);
  TRACE("bitvector", "bitBlastDisEqn => ", result.toString(), " }"); 
  return result;
}

/*! \param e1 pred e2, where pred is < or <=.  
 *
 *  if e1,e2 are constants, determine bv2int(e1) pred bv2int(e2). 
 *
 *  most significant bit of ei is denoted by msb(ei) 
 * 
 *  \return (msb(e1) pred msb(e2)) \vee 
 *          (msb(e1)=msb(e2) \wedge e1[n-2:0] pred e2[n-2:0])
 */
Theorem TheoryBitvector::bitBlastIneqn(const Expr& e) {
  TRACE("bitvector", "bitBlastIneqn(", e.toString(), ") {"); 

  if(e.isBoolConst()) {
    Theorem res(reflexivityRule(e));
    TRACE("bitvector", "bitBlastIneqn => ", res.getExpr(), " }");
    return res;
  }

  DebugAssert(BVLT == e.getOpKind() ||
              BVLE == e.getOpKind(),
              "TheoryBitvector::bitBlastIneqn: "
              "input e must be BVLT/BVLE: e = " + e.toString());
  DebugAssert(e.arity() == 2,
              "TheoryBitvector::bitBlastIneqn: "
              "arity of e must be 2: e = " + e.toString());
  int e0len = BVSize(e[0]);
  int e1len = BVSize(e[1]);
  int bvLength = e0len >= e1len ? e0len : e1len;
  
  Expr newE=e;
  Expr lhs = e[0];
  Expr rhs = e[1];
  Theorem thm1 = reflexivityRule(e);
  if(e0len != e1len) {
    Theorem thm0 = d_rules->padBVLTRule(e, bvLength);
    thm1 = rewriteBV(thm0, 3, false);
    newE = thm1.getRHS();
    lhs = newE[0];
    rhs = newE[1];
  }

  int kind = e.getOpKind();
  Theorem res;
  if(lhs == rhs)
    res = 
      transitivityRule(thm1,d_rules->lhsEqRhsIneqn(newE, kind));
  else {
    if(BVCONST == lhs.getKind() && BVCONST == rhs.getKind())
      res = transitivityRule(thm1,d_rules->bvConstIneqn(newE, kind));
    else {
      Theorem lhs_i = bitBlastTerm(lhs,bvLength-1, 0);
      Theorem rhs_i = bitBlastTerm(rhs,bvLength-1, 0);
      Theorem thm2 = d_rules->generalIneqn(newE, lhs_i, rhs_i, kind);
      res = transitivityRule(thm1, thm2);      
      //check if output is TRUE or FALSE theorem, and then simply return
      Theorem output = rewriteBoolean(res.getRHS());
      if(output.getRHS().isBoolConst()) {
        res = transitivityRule(res, output);
        TRACE("bitvector", "bitBlastIneqn => ", res.getExpr(), " }"); 
        return res;
      }

      if(bvLength-1 > 0) {
        // Copy by value, since 'res' will be changing
        Expr resRHS = res.getRHS();
        //resRHS can be of the form (\alpha or (\beta and \gamma)) or
        //resRHS can be of the form (\beta and \gamma) or
        //resRHS can be of the form (\alpha or \gamma) or
        //resRHS can be of the form (\gamma)
        // Our mission is to bitblast \gamma and insert it back to the formula
        vector<unsigned> changed;
        vector<Theorem> thms;
        Expr gamma;
        Theorem gammaThm;
        switch(resRHS.getOpKind()) {
        case OR:
          if(resRHS[1].isAnd()) { // (\alpha or (\beta and \gamma))
            changed.push_back(1);
            gamma = resRHS[1][1];
            // \gamma <=> \gamma'
            gammaThm = rewriteBV(gamma,2,false);
            //\gamma' <=> \gamma"
            Theorem thm3 = bitBlastIneqn(gammaThm.getRHS());
            //Theorem thm3 = bitBlastIneqn(gamma);
            //\gamma <=> \gamma' <=> \gamma"
            thm3 = transitivityRule(gammaThm, thm3);
            thms.push_back(thm3);
            // (\beta and \gamma) <=> (\beta and \gamma")
            thm3 = substitutivityRule(resRHS[1],changed,thms);
            // Now substitute this into the OR.
            // 'changed' is the same, only update thms[0]
            thms[0] = thm3;
            // (a or (b and g)) <=> (a or (b and g"))
            thm3 = substitutivityRule(resRHS,changed,thms);
            res = transitivityRule(res, thm3);
            break;
          }
          // (\alpha or \gamma) - fall through (same as the AND case)
        case AND: { // (\beta and \gamma)
          changed.push_back(1);
          gamma = resRHS[1];
          // \gamma <=> \gamma'
          gammaThm = rewriteBV(gamma,2,false);
          //\gamma' <=> \gamma"
          Theorem thm3 = bitBlastIneqn(gammaThm.getRHS());
          //Theorem thm3 = bitBlastIneqn(gamma);
          //\gamma <=> \gamma' <=> \gamma"
          thm3 = transitivityRule(gammaThm, thm3);
          thms.push_back(thm3);
          // (\beta and \gamma) <=> (\beta and \gamma")
          thm3 = substitutivityRule(resRHS,changed,thms);
          res = transitivityRule(res, thm3);
          break;
        }
        default: // (\gamma)
          IF_DEBUG(gamma = resRHS);
          // \gamma <=> \gamma'
          gammaThm = rewriteBV(resRHS,2,false);
          //\gamma' <=> \gamma"
          Theorem thm3 = bitBlastIneqn(gammaThm.getRHS());
          //Theorem thm3 = bitBlastIneqn(gamma);
          //\gamma <=> \gamma' <=> \gamma"
          thm3 = transitivityRule(gammaThm, thm3);
          res = transitivityRule(res, thm3);
          break;
        }
        
        DebugAssert(kind == gamma.getOpKind(),
                    "TheoryBitvector::bitBlastIneqn: "
                    "gamma must be a BVLT/BVLE. gamma = " +
                    gamma.toString());
      }
    }
  }
  TRACE("bitvector", "bitBlastIneqn => ", res.toString(), " }"); 
  return res;
}


/*! The invariant maintained by this function is: accepts a bitvector
 * term, t,and a bitPosition, i. returns a formula over the set of
 * propositional variables defined using BOOLEXTRACT of bitvector
 * variables in t at the position i.
 *
 * \return Theorem(BOOLEXTRACT(t, bitPosition) <=> phi), where phi is
 * a Boolean formula over the individual bits of bit-vector variables.
 */
Theorem TheoryBitvector::bitBlastTerm(const Expr& t, 
                                      int bitPosition, int preComputed)
{
  TRACE("bitvector", 
        "bitBlastTerm(", t, ", " + int2string(bitPosition) + ") {"); 
  Theorem result;
  
  //check in cache for the theorem t[bitPosition] <=> \theta_i.
  //if yes return the theorem, else produce it.
  Expr t_i = newBoolExtractExpr(t, bitPosition);
  CDMap<Expr,Theorem>::iterator it = d_bitvecCache.find(t_i);
  if(it != d_bitvecCache.end()) {
    result = (*it).second;
    TRACE("bitvector", "bitBlastTerm[cached] => ", result, " }"); 
    DebugAssert(t_i == result.getLHS(),
                "TheoryBitvector::bitBlastTerm:"
                "created wrong theorem" + result.toString() + t_i.toString());
    return result;
  } else {
    //else construct the theorem t[bitPosition] <=> \theta_i. and put it into
    //d_bitvecCache
    IF_DEBUG(Type type = t.getType());
    DebugAssert(BITVECTOR == type.getExpr().getOpKind(),
                "TheoryBitvector::bitBlastTerm: "
                "The type of input to bitBlastTerm must be BITVECTOR.\n t = "
                +t.toString());
    DebugAssert(bitPosition >= 0,
                "TheoryBitvector::bitBlastTerm: "
                "illegal bitExtraction attempted.\n bitPosition = "+
                int2string(bitPosition));
    // First, rewrite t[i] into t[i:i][0], normalize t[i:i], and
    // bitblast the result.
    if(*d_rwBitBlastFlag)
      result = rewriteBV(t_i, false);
    else
      result = reflexivityRule(t_i);

    Expr t2_i = result.getRHS();
    if(t2_i.isBoolConst()) {
      // Record the original expression into the cache
      d_bitvecCache[t_i] = result;
      TRACE("bitvector", "bitBlastTerm[rewrite to const] => ", result, " }"); 
      return result;
    }
      
    DebugAssert(t2_i.getOpKind()==BOOLEXTRACT,
                "bitBlastTerm: t2_i = "+t2_i.toString());
    // Check the cache again
    it = d_bitvecCache.find(t2_i);
    if(it != d_bitvecCache.end()) {
      result = transitivityRule(result, (*it).second);
      // Record the original expression into the cache
      d_bitvecCache[t_i] = result;
      TRACE("bitvector", "bitBlastTerm[cached2] => ", result, " }"); 
      return result;
    }
    // Bit-blast the rewritten version of the term.  We'll merge the
    // two at the end.
    Theorem resTmp(reflexivityRule(t2_i));
    const Expr& t2 = t2_i[0];

    int bitPos2 = getBoolExtractIndex(t2_i);
    // Required depth of simplification for the resulting formula (the
    // depth of the newly generated Boolean formula that needs to be
    // simplified).  For the moment, we distinguish between 1 and many
    // (>1).  Default is 1 (only top node needs simplification).
//     int simplifyDepth(1);
    switch(t2.getOpKind()) {
    case BVCONST:
      //we have a bitvector constant
      resTmp = transitivityRule(resTmp, 
                                d_rules->bitExtractConstant(t2, bitPos2));
      break;
    case BVMULT: {
      Theorem thm;
      if(BVCONST == t2[0].getKind())
        thm = d_rules->bitExtractConstBVMult(t2, bitPos2);
      else
        thm = d_rules->bitExtractBVMult(t2, bitPos2);
      const Expr& boolExtractTerm = thm.getRHS();
      const Expr& term = boolExtractTerm[0];
      const Theorem& bitblastThm = bitBlastTerm(term, bitPos2,preComputed);
      resTmp = transitivityRule(thm, bitblastThm); 
//       simplifyDepth = 2;
    }
      break;
    case BVOR:
    case BVAND: {
      int resKind = (t2.getOpKind()==BVOR)? OR : AND;
      const Theorem& thm = (resKind==AND)?
        d_rules->bitExtractAnd(t2, bitPos2)
        : d_rules->bitExtractOr(t2, bitPos2);
      const Expr& phi = thm.getRHS();
      DebugAssert(phi.getOpKind() == resKind && phi.arity() == t2.arity(),
                  "TheoryBitvector::bitBlastTerm: recursion:"
                  "\n phi = "+phi.toString()
                  +"\n t2 = "+t2.toString());
      vector<Theorem> substThms;
      for(Expr::iterator i=phi.begin(), iend=phi.end(); i!=iend; ++i) {
        if(i->getOpKind() == BOOLEXTRACT)
          substThms.push_back(bitBlastTerm((*i)[0], getBoolExtractIndex(*i), preComputed));
        else
          substThms.push_back(reflexivityRule(*i));
      }
      resTmp = transitivityRule(resTmp, thm);
      resTmp = transitivityRule(resTmp, substitutivityRule(resKind,
                                                           substThms));
      break;
    }
    case BVNEG: {
      const Theorem& thm = d_rules->bitExtractNot(t2, bitPos2);
      const Expr& extractTerm = thm.getRHS();
      DebugAssert(NOT == extractTerm.getKind(),
                  "TheoryBitvector::bitBlastTerm:" 
                  "recursion: term must be NOT");
      const Expr& term0 = extractTerm[0];
      DebugAssert(BOOLEXTRACT == term0.getOpKind(), 
                  "TheoryBitvector::bitBlastTerm: recursion:("
                  "terms must be BOOL-EXTRACT");
      int bitPos0 = getBoolExtractIndex(term0);
      std::vector<Theorem> res;
      res.push_back(bitBlastTerm(term0[0], bitPos0, preComputed));
      resTmp = transitivityRule(resTmp, thm);
      resTmp = transitivityRule(resTmp,
                                substitutivityRule(NOT, res));
      break; 
    }
    case BVSUB:
      DebugAssert(false, "control should not reach here. " 
                  "BVSUB/BVUMINUS have already been translated into BVPLUS");
      break;
    case BVUMINUS: {
      vector<Theorem> thms;
      vector<unsigned> changed;
      // -t = ~t+1
      Theorem thm = d_rules->bvuminusToBVPlus(t2);
      thms.push_back(thm);
      changed.push_back(0);
      // (-t)[i] = (~t+1)[i]
      resTmp = substitutivityRule(t2_i, changed, thms);
      // Bitblast (~t+1)[i]
      resTmp = transitivityRule(resTmp, bitBlastTerm(thm.getRHS(), bitPos2, preComputed));
//       simplifyDepth = 2;
      break;
    }
    case BVPLUS: {
      Expr bvPlusTerm = t2;
      Theorem thm1;
      if(2 < t2.arity()) {
        //this rule makes t2 a binary add. binary add is more suitable
        //for bitblasting.
        const Theorem& thm = d_rules->bvPlusAssociativityRule(bvPlusTerm);
        std::vector<Theorem> thms;
        thms.push_back(thm);
        thm1 = substitutivityRule
          (newBoolExtractExpr(bvPlusTerm, bitPos2).getOp(), thms);
        bvPlusTerm = thm.getRHS();
        TRACE("bitvector", 
              "TheoryBitvector::bitBlastTerm:thm1(", thm1.getExpr(), ")");
      } else
        thm1 = reflexivityRule(newBoolExtractExpr(bvPlusTerm, bitPos2));
      //bitblast each bit of t[0] and t[1] from 0-bit to bitPos2 
      //and store in two separate vectors.
      const Expr& bvplust1 = bvPlusTerm[0];
      const Expr& bvplust2 = bvPlusTerm[1];
      int t1Length = BVSize(bvplust1);
      int t2Length = BVSize(bvplust2);
      if(0 == preComputed) {
        std::vector<Theorem> t1BitExtractThms;
        std::vector<Theorem> t2BitExtractThms;
        for(int i = 0; i <= bitPos2; i=i+1) {
          if(i < t1Length)
            t1BitExtractThms.push_back(bitBlastTerm(bvplust1, i, 0));
          else
            t1BitExtractThms.push_back(d_rules->zeroPaddingRule(bvplust1,i));
          if(i < t2Length)
            t2BitExtractThms.push_back(bitBlastTerm(bvplust2, i, 0));
          else
            t2BitExtractThms.push_back(d_rules->zeroPaddingRule(bvplust2,i));
        }
        Theorem thm2 = 
          d_rules->bitExtractBVPlus(t1BitExtractThms, 
                                    t2BitExtractThms, bvPlusTerm, bitPos2);
        resTmp = transitivityRule(resTmp, thm1);
        resTmp = transitivityRule(resTmp, thm2);
      } else {      
        Theorem t1_i;
        Theorem t2_i;
        if(bitPos2 < t1Length)
          t1_i = bitBlastTerm(bvplust1,bitPos2,preComputed);      
        else
          t1_i = d_rules->zeroPaddingRule(bvplust1,bitPos2);

        if(bitPos2 < t2Length)
          t2_i = bitBlastTerm(bvplust2,bitPos2,preComputed);
        else
          t2_i = d_rules->zeroPaddingRule(bvplust2,bitPos2);

        Theorem thm2 = 
          d_rules->bitExtractBVPlusPreComputed(t1_i,t2_i,
                                               bvPlusTerm,
                                               bitPos2, 
                                               preComputed);
        resTmp = transitivityRule(resTmp, thm1);
        resTmp = transitivityRule(resTmp, thm2);
      }
      break;
    }
    case CONCAT: {
      //we have a bitvector concatenation term
      Theorem thm = d_rules->bitExtractConcatenation(t2, bitPos2);
      const Expr& boolExtractTerm = thm.getRHS();
      DebugAssert(BOOLEXTRACT == boolExtractTerm.getOpKind(),
                  "TheoryBitvector::bitBlastTerm: recursion: term must be"
                  "bool_extract");
      const Expr& term = boolExtractTerm[0];
      int bitPos = getBoolExtractIndex(boolExtractTerm);
      TRACE("bitvector", 
            "term for bitblastTerm recursion:(", term.toString(), ")");
      resTmp = transitivityRule(thm, bitBlastTerm(term, bitPos, preComputed));
    }
      break;
    case EXTRACT:{
      // EXTRACT collapses under BOOLEXTRACT, no more of this case      
      //we have a bitvector extraction term
      Theorem thm = d_rules->bitExtractExtraction(t2, bitPos2);
      const Expr& boolExtractTerm = thm.getRHS();
      DebugAssert(BOOLEXTRACT == boolExtractTerm.getOpKind(),
                  "TheoryBitvector::bitBlastTerm: recursion: term must be"
                  "bool_extract");
      const Expr& term = boolExtractTerm[0];
      int bitPos = getBoolExtractIndex(boolExtractTerm);
      TRACE("bitvector", "term for bitblastTerm recursion:(", term, ")");
      resTmp = transitivityRule(thm, bitBlastTerm(term, bitPos,preComputed));
    }
      break;
    case LEFTSHIFT: {
      resTmp = d_rules->bitExtractFixedLeftShift(t2, bitPos2);
      const Expr& extractTerm = resTmp.getRHS();
      if(BOOLEXTRACT == extractTerm.getOpKind())
        resTmp = 
          transitivityRule(resTmp, 
                           bitBlastTerm(extractTerm[0],
                                        getBoolExtractIndex(extractTerm), preComputed));
    }
      break;
    case RIGHTSHIFT: {
      resTmp = d_rules->bitExtractFixedRightShift(t2, bitPos2);
      const Expr& extractTerm = resTmp.getRHS();
      if(CVCL::BOOLEXTRACT == extractTerm.getOpKind())
        resTmp = 
          transitivityRule(resTmp, 
                           bitBlastTerm(extractTerm[0],
                                        getBoolExtractIndex(extractTerm), preComputed));
    }
      break;
    case SX: {
      resTmp = d_rules->bitExtractSXRule(t2, bitPos2);
      Expr extractTerm = resTmp.getRHS();
      resTmp = 
        transitivityRule(resTmp, 
                         bitBlastTerm(extractTerm[0],
                                      getBoolExtractIndex(extractTerm), preComputed));      
      break;
    }
    default:
      //we have bitvector variable.
      //check if the expr is indeed a BITVECTOR.   
      IF_DEBUG(Type type = t2.getType());
      DebugAssert(BITVECTOR == (type.getExpr()).getOpKind(),
                  "BitvectorTheoremProducer::bitBlastTerm: "
                  "the type must be BITVECTOR");
      //check if 0<= i < length of BITVECTOR
      IF_DEBUG(int bvLength=BVSize(t2));
      DebugAssert(0 <= bitPos2 && bitPos2 < bvLength,
                  "BitvectorTheoremProducer::bitBlastTerm: "
                  "the bitextract position must be legal");
      TRACE("bitvector",
            "bitBlastTerm: blasting variables(", t2, ")");
      const Expr bitExtract = newBoolExtractExpr(t2, bitPos2);
      resTmp = transitivityRule(resTmp, reflexivityRule(bitExtract));
      TRACE("bitvector",
            "bitBlastTerm: blasting variables(", t, ")");
      break;
    }
    DebugAssert(!resTmp.isNull(), "TheoryBitvector::bitBlastTerm()");
    Theorem simpThm;
//     if(simplifyDepth > 1)
//       simpThm = simplifyThm(resTmp.getRHS());
//     else
      simpThm = rewriteBoolean(resTmp.getRHS());

    resTmp = transitivityRule(resTmp, simpThm);
    result = transitivityRule(result, resTmp);
    d_bitvecCache[t_i] = result;
    d_bitvecCache[t2_i] = resTmp;
    DebugAssert(t_i == result.getLHS(),
                "TheoryBitvector::bitBlastTerm: "
                "created wrong theorem.\n result = "
                +result.toString()
                +"\n t_i = "+t_i.toString());
    TRACE("bitvector", "bitBlastTerm => ", result, " }"); 
    return result;
  }
}
  

//! Check that all the kids of e are BVCONST
static bool constantKids(const Expr& e) {
  for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
    if(!i->isRational() && i->getKind() != BVCONST) return false;
  return true;
}


//! Search for all the BVCONST kids of e, and return their indices in idxs
static void constantKids(const Expr& e, vector<int>& idxs) {
  for(int i=0, iend=e.arity(); i<iend; ++i)
    if(e[i].getKind() == BVCONST) idxs.push_back(i);
}

Theorem
TheoryBitvector::normalizeConcat(const Expr& e, bool useFind) {
  TRACE("bitvector rewrite", "normalizeConcat(", e, ") {");
  Theorem res;
  if(*d_concatRewriteFlag) {
    switch(e.getOpKind()) {
    case EXTRACT: {
      DebugAssert(e.arity() == 1, "TheoryBitvector::normalizeConcat: e = "
                  +e.toString());
      if(getExtractLow(e) == 0 && getExtractHi(e) == BVSize(e[0])-1)
        res = d_rules->extractWhole(e);
      else {
        switch(e[0].getOpKind()) {
        case BVCONST:
          res = d_rules->extractConst(e);
          break;
        case EXTRACT:
          res = d_rules->extractExtract(e);
          break;
        case CONCAT:
          // Push extraction through concat, and rewrite the kids
          res = rewriteBV(d_rules->extractConcat(e), 2, useFind);
          break;
        case BVNEG:
          res = rewriteBV(d_rules->extractNeg(e), 2, useFind);
          break;
        case BVAND:
          res = rewriteBV(d_rules->extractAnd(e), 2, useFind);
          break;
        case BVOR:
          res = rewriteBV(d_rules->extractOr(e), 2, useFind);     
          break;
        case BVXOR:
          res = 
            rewriteBV(d_rules->extractBitwise(e, BVXOR,"extract_bvxor"), 
                      2, useFind);
          break;
        case BVMULT: {
          const Expr& bvmult = e[0];
          int hiBit = getExtractHi(e);
          int bvmultLen = BVSize(bvmult);
          // Applicable if it changes anything
          if(hiBit+1 < bvmultLen) {
            res = d_rules->extractBVMult(e);
            // The extraction may be stripped off
            if(res.getRHS().getOpKind() == EXTRACT)
              res = rewriteBV(res, 2, useFind);
            else
              res = rewriteBV(res, 1, useFind);
          } else
            res = reflexivityRule(e);
          break;
        }
        case BVPLUS: {
          const Expr& bvplus = e[0];
          int hiBit = getExtractHi(e);
          int bvplusLen = BVSize(bvplus);
          if(hiBit+1 < bvplusLen) {
            res = d_rules->extractBVPlus(e);
            // The extraction may be stripped off
            if(res.getRHS().getOpKind() == EXTRACT)
              res = rewriteBV(res, 2, useFind);
            else
              res = rewriteBV(res, 1, useFind);
          } else
            res = reflexivityRule(e);
          break;
        }
          
          /*
        case ITE: {
          //ite(c,t1,t2)[i:j] <=> ite(c,t1[i:j],t2[i:j])
          res = simplify(e);
          vector<Theorem> thms;
          vector<unsigned> changed;
          const Expr& e1 = res.getRHS()[1];
          const Expr& e2 = res.getRHS()[2];
          Theorem t = rewriteBV(e1, useFind);
          if(e1 != t.getRHS()) {
            thms.push_back(t);
            changed.push_back(1);
          }
          t = rewriteBV(e2, useFind);
          if(e2 != t.getRHS()) {
            thms.push_back(t);
            changed.push_back(2);
          }
          if(changed.size()>0) {
            t = substitutivityRule(res.getRHS(), changed, thms);
            res = transitivityRule(res, t);
          }
          break;
        }
          */
        default:
          res = reflexivityRule(e);
          break;
        }
      }
      break;
    }
    case BVNEG: {
      switch(e[0].getOpKind()) {
      case BVCONST:
        res = d_rules->negConst(e);
        break;
      case CONCAT:
        // May need to propagate negation in the kids, rewrite 2 levels
        res = rewriteBV(d_rules->negConcat(e), 2, useFind);
      break;
      case BVNEG:
        res = d_rules->negNeg(e);
        break;
      default:
        res = reflexivityRule(e);
        break;
      }
      break;
    }
    case BVAND: {
      // Flatten the bit-wise AND, eliminate duplicates, reorder terms
      res = d_rules->andFlatten(e);
      Expr ee = res.getRHS();
      // Search for constant bitvectors
      vector<int> idxs;
      constantKids(ee, idxs);
      if(idxs.size() >= 2) {
      res = transitivityRule(res, d_rules->andConst(ee, idxs));
      }
      ee = res.getRHS();
      if(ee.getOpKind() == BVAND) {
        // Search for constants again
        idxs.clear();
        constantKids(ee, idxs);
        DebugAssert(idxs.size() <= 1, "TheoryBitvector::normalizeConcat(ee="
                    +ee.toString()+")");
        if(idxs.size() >= 1) {
          int idx(idxs[0]);
          // Check if ee[idx] is a bitvector of 0's or 1's
          bool isZero(true);
          bool isOne(true);
          const Expr& c = ee[idx];
          for(int i=0, iend=getBVConstSize(c);
              (isZero || isOne) && (i<iend); ++i) {
            isZero = (isZero && !getBVConstValue(c, i));
            isOne  = (isOne && getBVConstValue(c, i));
          }
          if(isZero)
            res = transitivityRule(res, d_rules->andZero(ee, idx));
          else if(isOne)
            res = transitivityRule(res, d_rules->andOne(ee, idxs));
        }
      }
      // Lift concatenation over bit-wise AND and rewrite again
      ee = res.getRHS();
      if(ee.getOpKind() == BVAND) {
        int i=0, iend=ee.arity();
        // Search for the first CONCAT child
        for(; (i<iend) && ee[i].getOpKind() != CONCAT; ++i);
        // If found, lift CONCAT over BVAND, and rewrite 3 levels
        // deep.  Reason: the result of andConcat is of the form:
        // (@ (& ... t_k[i:j] ...) ... ), and only t_k is known to be 
        // completely rewritten.  Hence the 3 levels of rewrites.
        if(i<iend)
          res = transitivityRule(res, rewriteBV(d_rules->andConcat(ee, i),
                                                3, useFind));
      }
      break;
    }
    case BVOR: {
      // Flatten the bit-wise OR, eliminate duplicates, reorder terms
      res = d_rules->orFlatten(e);
      Expr ee = res.getRHS();
      // Search for constant bitvectors
      vector<int> idxs;
      constantKids(ee, idxs);
      if(idxs.size() >= 2) {
        res = transitivityRule(res, d_rules->orConst(ee, idxs));
      }
      ee = res.getRHS();
      if(ee.getOpKind() == BVOR) {
        // Search for constants again
        idxs.clear();
        constantKids(ee, idxs);
        DebugAssert(idxs.size() <= 1, "TheoryBitvector::normalizeConcat(ee="
                    +ee.toString()+")");
        if(idxs.size() >= 1) {
          int idx(idxs[0]);
          // Check if ee[idx] is a bitvector of 0's or 1's
          bool isZero(true);
          bool isOne(true);
          const Expr& c = ee[idx];
          for(int i=0, iend=getBVConstSize(c);
              (isZero || isOne) && (i<iend); ++i) {
            isZero = (isZero && !getBVConstValue(c, i));
            isOne  &= (isOne && getBVConstValue(c, i));
          }
          if(isOne)
            res = transitivityRule(res, d_rules->orOne(ee, idx));
          else if(isZero)
            res = transitivityRule(res, d_rules->orZero(ee, idxs));
          
        }
      }
      // Lift concatenation over bit-wise OR and rewrite again
      ee = res.getRHS();
      if(ee.getOpKind() == BVOR) {
        int i=0, iend=ee.arity();
        // Search for the first CONCAT child
        for(; (i<iend) && ee[i].getOpKind() != CONCAT; ++i);
        // If found, lift CONCAT over BVOR, and rewrite 3 levels
        // deep.  Reason: the result of orConcat is of the form:
        // (@ (| ... t_k[i:j] ...) ... ), and only t_k is known to be 
        // completely rewritten.  Hence the 3 levels of rewrites.
        if(i<iend)
          res = transitivityRule(res, rewriteBV(d_rules->orConcat(ee, i),
                                                3, useFind));
      }
      break;
    }

//     case BVXOR: {
//       // Flatten the bit-wise OR, eliminate duplicates, reorder terms
//       res = d_rules->orFlatten(e);
//       Expr ee = res.getRHS();
//       // Search for constant bitvectors
//       vector<int> idxs;
//       constantKids(ee, idxs);
//       if(idxs.size() >= 2) {
//      res = transitivityRule(res, d_rules->orConst(ee, idxs));
//       }
//       ee = res.getRHS();
//       if(ee.getOpKind() == BVOR) {
//      // Search for constants again
//      idxs.clear();
//      constantKids(ee, idxs);
//      DebugAssert(idxs.size() <= 1, "TheoryBitvector::normalizeConcat(ee="
//                  +ee.toString()+")");
//      if(idxs.size() >= 1) {
//        int idx(idxs[0]);
//        // Check if ee[idx] is a bitvector of 0's or 1's
//        bool isZero(true);
//        bool isOne(true);
//        const Expr& c = ee[idx];
//        for(int i=0, iend=c.getIntValueSize();
//            (isZero || isOne) && (i<iend); ++i) {
//          isZero = (isZero && c.getIntValue(i) == 0);
//          isOne  &= (isOne && c.getIntValue(i) == 1);
//        }
//        if(isOne)
//          res = transitivityRule(res, d_rules->orOne(ee, idx));
//        else if(isZero)
//          res = transitivityRule(res, d_rules->orZero(ee, idxs));
          
//      }
//       }
//       // Lift concatenation over bit-wise OR and rewrite again
//       ee = res.getRHS();
//       if(ee.getOpKind() == BVOR) {
//      int i=0, iend=ee.arity();
//      // Search for the first CONCAT child
//      for(; (i<iend) && ee[i].getOpKind() != CONCAT; ++i);
//      // If found, lift CONCAT over BVOR, and rewrite 3 levels
//      // deep.  Reason: the result of orConcat is of the form:
//      // (@ (| ... t_k[i:j] ...) ... ), and only t_k is known to be 
//      // completely rewritten.  Hence the 3 levels of rewrites.
//      if(i<iend)
//        res = transitivityRule(res, rewriteBV(d_rules->orConcat(ee, i),
//                                              3, useFind));
//       }
//       break;
//     }
    case CONCAT: {
      // Congruence closure rewrite
      res = rewriteCC(e);
      // First, flatten concatenation
      res = transitivityRule(res, d_rules->concatFlatten(res.getRHS()));
      TRACE("bitvector rewrite", "normalizeConcat: flattened = ",
            res.getRHS(), "");
      // Search for adjacent constants and accumulate the vector of
      // nested concatenations (@ t1 ... (@ c1 ... ck) ... tn), and the
      // indices of constant concatenations in this new expression.
      // We'll connect this term to 'e' by inverse of flattenning, and
      // rewrite concatenations of constants into bitvector constants.
      vector<unsigned> idxs;
      vector<Expr> kids; // Kids of the new concatenation
      vector<Theorem> thms; // Rewrites of constant concatenations
      vector<Expr> nestedKids; // Kids of the current concatenation of constants
      // res will be overwritten, using const Expr& may be dangerous
      Expr e1 = res.getRHS();
      for(int i=0, iend=e1.arity(); i<iend; ++i) {
        TRACE("bitvector rewrite", "normalizeConcat: e["+int2string(i)+"]=",
              e1[i], "");
        if(e1[i].getKind() == BVCONST) {
          // INVARIANT: if it is the first constant in a batch,
          // then nestedKids must be empty.
          nestedKids.push_back(e1[i]);
          TRACE("bitvector rewrite", "normalizeConcat: queued up BVCONST: ",
                e1[i], "");
        } else { // e1[i] is not a BVCONST
          if(nestedKids.size() > 0) { // This is the end of a batch
            if(nestedKids.size() >= 2) { // Create a nested const concat
              Expr cc = newConcatExpr(nestedKids);
              idxs.push_back(kids.size());
              kids.push_back(cc);
              thms.push_back(d_rules->concatConst(cc));
              TRACE("bitvector rewrite", "normalizeConcat: wrapping ", cc, "");
            } else { // A single constant, add it as it is
              TRACE("bitvector rewrite", "normalizeConcat: single const ",
                    nestedKids[0], "");
              kids.push_back(nestedKids[0]);
            }
            nestedKids.clear();
          }
          // Add the current non-constant BV
          kids.push_back(e1[i]);
        }
      }
      // Handle the last BVCONST
      if(nestedKids.size() > 0) {
        if(nestedKids.size() >= 2) { // Create a nested const concat
          Expr cc = newConcatExpr(nestedKids);
          idxs.push_back(kids.size());
          kids.push_back(cc);
          thms.push_back(d_rules->concatConst(cc));
          TRACE("bitvector rewrite", "normalizeConcat: wrapping ", cc, "");
        } else { // A single constant, add it as it is
          kids.push_back(nestedKids[0]);
          TRACE("bitvector rewrite", "normalizeConcat: single const ",
                nestedKids[0], "");
        }
        nestedKids.clear();
      }
      // If there are any constants to merge, do the merging
      if(idxs.size() > 0) {
        // CONCAT with constants groupped
        if(kids.size() == 1) { // Special case: all elements are constants
          DebugAssert(thms.size() == 1, "TheoryBitvector::normalizeConcat:\n"
                      "case CONCAT: all constants.  thms.size() == "
                      +int2string(thms.size()));
          res = transitivityRule(res, thms[0]);
        } else {
          Expr ee = newConcatExpr(kids);
          
          Theorem constMerge = substitutivityRule(ee, idxs, thms);
          // The inverse flattening of ee
          Theorem unFlatten = symmetryRule(d_rules->concatFlatten(ee));
          // Putting it together: Theorem(e==e'), where e' has constants merged
          res = transitivityRule(res, unFlatten);
          res = transitivityRule(res, constMerge);
        }
      }
      
      // Now do a similar search for mergeable extractions
      idxs.clear();
      thms.clear();
      kids.clear();
      // nestedKids must already be empty
      DebugAssert(nestedKids.size() == 0,
                  "normalizeConcat() case CONCAT, end of const merge");
      Expr prevExpr; // Previous base of extraction (initially Null)
      // The first and the last bit in the batch of mergeable extractions
      int hi(-1), low(-1);
      // Refresh e1
      e1 = res.getRHS();
      for(int i=0, iend=e1.arity(); i<iend; ++i) {
        const Expr& ei = e1[i];
        if(ei.getOpKind() == EXTRACT) {
          if(nestedKids.size() > 0 && ei[0] == prevExpr
             && (low-1) == getExtractHi(ei)) {
            // Continue to accumulate the current batch
            nestedKids.push_back(ei);
            low = getExtractLow(ei);
          } else { // Start a new batch
            // First, check if there was a batch before that
            if(nestedKids.size() >= 2) { // Create a nested const concat
              Expr cc = newConcatExpr(nestedKids);
              idxs.push_back(kids.size());
              kids.push_back(cc);
              thms.push_back(d_rules->concatMergeExtract(cc));
              nestedKids.clear();
            } else if(nestedKids.size() == 1) {
              // A single extraction, add it as it is
              kids.push_back(nestedKids[0]);
              nestedKids.clear();
            }
            // Now, actually start a new batch
            nestedKids.push_back(ei);
            hi = getExtractHi(ei);
            low = getExtractLow(ei);
            prevExpr = ei[0];
          }
        } else { // e1[i] is not an EXTRACT
          if(nestedKids.size() >= 2) { // Create a nested const concat
            Expr cc = newConcatExpr(nestedKids);
            idxs.push_back(kids.size());
            kids.push_back(cc);
            thms.push_back(d_rules->concatMergeExtract(cc));
          } else if(nestedKids.size() == 1) {
            // A single extraction, add it as it is
            kids.push_back(nestedKids[0]);
          }
          nestedKids.clear();
          // Add the current non-EXTRACT BV
          kids.push_back(ei);
        }
      }
      // Handle the last batch of extractions
      if(nestedKids.size() >= 2) { // Create a nested const concat
        Expr cc = newConcatExpr(nestedKids);
        idxs.push_back(kids.size());
        kids.push_back(cc);
        // The extraction may include all the bits, we need to rewrite again
        thms.push_back(rewriteBV(d_rules->concatMergeExtract(cc), 1, useFind));
      } else if(nestedKids.size() == 1) {
        // A single extraction, add it as it is
        kids.push_back(nestedKids[0]);
      }
      // If there are any extractions to merge, do the merging
      if(idxs.size() > 0) {
        // CONCAT with extractions groupped
        if(kids.size() == 1) { // Special case: all elements merge together
          DebugAssert(thms.size() == 1, "TheoryBitvector::normalizeConcat:\n"
                      "case CONCAT: all extracts merge.  thms.size() == "
                      +int2string(thms.size()));
          res = thms[0];
        } else {
          Expr ee = newConcatExpr(kids);
          Theorem extractMerge = substitutivityRule(ee, idxs, thms);
          // The inverse flattening of ee
          Theorem unFlatten = symmetryRule(d_rules->concatFlatten(ee));
          // Putting it together: Theorem(e==e'), where e' has extractions merged
          res = transitivityRule(res, unFlatten);
          res = transitivityRule(res, extractMerge);
        }
      }
      // Check for 0bin00 @ BVPLUS(n, ...).  Most of the time, this
      // case will be handled during the top-down phase
      // (simplifyOp()), but not always.
      const Expr& ee = res.getRHS();
      if(ee.getOpKind()==CONCAT && ee[0].getKind()==BVCONST
         && ee[1].getOpKind()==BVPLUS && computeBVConst(ee[0]) == 0) {
        // Push the concat down through BVPLUS
        Theorem thm = d_rules->bvplusZeroConcatRule(ee);
        if(thm.getLHS()!=thm.getRHS()) {
          thm = transitivityRule(thm, padBVPlus(thm.getRHS()));
          // Kids may need to be rewritten again
          res = rewriteBV(transitivityRule(res, thm), 2, useFind);
        }
      }
      // Since we may have pulled subexpressions from more than one
      // level deep, we cannot guarantee that all the new kids are
      // fully simplified, and have to call simplify explicitly again.
      // Since this is potentially an expensive operation, we try to
      // minimize the need for it: 

      // * check if the result has a find pointer (then kids don't
      //   need to be simplified),
      // * check if any of the kids simplify (if not, don't bother).
      // If kids are already simplified, we'll hit the simplifier
      // cache.  It's only expensive when kids do indeed simplify.
      if(!res.getRHS().hasFind()) {
        const Expr& ee = res.getRHS();
        vector<Theorem> thms;
        vector<unsigned> changed;
        for(int i=0, iend=ee.arity(); i<iend; ++i) {
          Theorem thm = simplify(ee[i]);
          if(thm.getLHS()!=thm.getRHS()) {
            thms.push_back(thm);
            changed.push_back(i);
          }
        }
        if(changed.size()>0) {
          Theorem subst = substitutivityRule(ee, changed, thms);
          res = transitivityRule(res, rewriteBV(subst, 1, useFind));
        }
      }
      // Finally, do another congruence closure rewrite, to guarantee
      // that the kids are fully simplified
      if(res.getRHS().getOpKind()==CONCAT)
        res = transitivityRule(res, rewriteCC(res.getRHS()));
      break;
    }
    default:
      DebugAssert(false, "normalizeConcat: bad expr: "+e.toString());
      res = reflexivityRule(e);
      break;
    }
    DebugAssert(e == res.getLHS(), "normalizeConcat:\n e = "+e.toString()
                +"\n res.getLHS() = "+res.getLHS().toString());
  }
  else
    res = reflexivityRule(e);
  TRACE("bitvector rewrite", "normalizeConcat => ", res.getExpr(), " }");
  return res;
}


/*! accepts an expression e, and returns a theorem e <==>
 *  BVPLUS_NORMAL_FORM(e) we always assume that kids of e are in
 *  bvplus normal form, and only the top-level needs normalization
 */
Theorem
TheoryBitvector::normalizeBVArith(const Expr& e, bool useFind) {
  TRACE("bitvector rewrite", "normalizeBVArith(", e, ") {");
  Theorem res;
  if(*d_bvplusRewriteFlag) {
    switch(e.getOpKind()) {
    case BVPLUS: {
      DebugAssert(e.arity()>=2,
                  "BVPLUS must have atleast 2 kids:\n e = " + e.toString());
      res = padBVPlus(e);
      const Expr& rhs = res.getRHS();
      if(e != rhs)
        return rewriteBV(res, 4, useFind);
      switch(rhs.getOpKind()) {
      case BVPLUS: {
        const Theorem thm0 = flattenBVPlus(rhs);
        res = transitivityRule(res, thm0);
        //res = transitivityRule(res, padBVPlus(res.getRHS()));
        res = transitivityRule(res, combineLikeTerms(res.getRHS()));
        break;
      }
      default:
        return res;
        break;
      }
    }
      break;
    case BVMULT: {
      DebugAssert(e.arity()==2,
                  "BVMULT must have exactly 2 kids: " + e.toString());
      DebugAssert(BITVECTOR==e[0].getType().getExpr().getOpKind() &&
                  BITVECTOR==e[1].getType().getExpr().getOpKind(),
                  "For BVMULT terms e[0], e[1] must be a BV:\n e = "
                  +e.toString());
      if(BVCONST == e[0].getKind() || BVCONST == e[1].getKind()) {
        if(constantKids(e)) {
          res = d_rules->bvmultConst(e);
          TRACE("bitvector rewrite", "normalizeBVArith[const] => ",
                res.getExpr(), " }");
          return res;
        }
        
        if(BVCONST == e[1].getKind()) {
          const Theorem thm = d_rules->flipBVMult(e);
          const Theorem thm1 = normalizeBVArith(thm.getRHS(), useFind);
          res = transitivityRule(thm, thm1);      
          TRACE("bitvector rewrite", "normalizeBVArith[flip] => ",
                res.getExpr(), " }");
          return res;
        }
        const Rational coeff = computeBVConst(e[0]);
        if(0 == coeff) {
          res = d_rules->zeroCoeffBVMult(e);
          TRACE("bitvector rewrite", "normalizeBVArith[c=0] => ",
                res.getExpr(), " }");
          return res;
        }
        else if(1 == coeff) {
          res = d_rules->oneCoeffBVMult(e); 
          TRACE("bitvector rewrite", "normalizeBVArith[c=1] => ",
                res.getExpr(), " }");
          return res;
        }
        
        DebugAssert(coeff > 1,
                    "in BVMULT e[0] must be a rational: " + e.toString());
        const Theorem thm = d_rules->padBVMult(e);
        if(thm.getLHS() != thm.getRHS()) {
          const Theorem thm1 = rewriteBV(thm.getRHS(), 2, useFind);
          res = transitivityRule(thm, thm1);
          TRACE("bitvector rewrite", "normalizeBVArith[pad] => ",
                res.getExpr(), " }");
          return res;
        }
        
        switch(e[1].getOpKind()) {
        case BVMULT: {
          //e is of the form a*(b*t); e cannot be of the form a*(t*b)
          //or a*(b*c) since the kids are always in normal form
          DebugAssert(BVCONST == e[1][0].getKind(),
                      "e[1][0] must be a BVCONST: " + 
                      e.toString());
          //e <==> (a*b)*t
          const Theorem thm2 = 
            d_rules->bvConstMultAssocRule(e);
          res = thm2;
          break;
        }
        case BVPLUS: {
          DebugAssert(BVCONST == e[0].getKind(),
                      "e[0] must be a BVCONST" + e.toString());
          //a*(t1+...+tn) <==> a*t1 + ... + a*tn
          const Theorem thm0 = d_rules->bvMultDistRule(e);
          res = rewriteBV(thm0, 2, useFind);
          break;
        }
        default:
          res = reflexivityRule(e);
          break;
        }
      }
      //nonlinear multiplication
      else
        if(e[1] < e[0])
          res = d_rules->flipBVMult(e);
        else
          res = reflexivityRule(e);
      //        //FIXME: fix this rule later
      //        rhs = res.getRHS();
      //        if(BVMULT == rhs[0].getOpKind() || BVMULT == rhs[1].getOpKind())
      //          res = d_rules->bvMultAssocRule(rhs);
      //       }
      break;
    }
    case BVUMINUS: {
      DebugAssert(e.arity() == 1,
                  "e can atmost have one kid" + e.toString());
      DebugAssert(e[0].getOpKind() != BVUMINUS,
                  "e[0] may not be BVUMINUS, it must be normalized:"+
                  e.toString());
      Theorem thm0 = d_rules->bvuminusToBVPlus(e);
      Theorem temp = pushNegation(thm0.getRHS()[0]);
      if (temp.getLHS() != temp.getRHS()) {
        vector<Theorem> thms;
        vector<unsigned> changed;
        thms.push_back(temp);
        changed.push_back(0);
        Theorem thm1 = substitutivityRule(thm0.getRHS(),changed,thms);
        thm0 = transitivityRule(thm0,thm1);
      }
      Theorem thm2 = rewriteBV(thm0.getRHS(), 2, useFind);
      res= transitivityRule(thm0,thm2);
    }
      break;
    default:
      res = reflexivityRule(e);
      break;
    }
  } 
  else
    res = reflexivityRule(e);
  TRACE("bitvector rewrite", "normalizeBVArith => ", res.getExpr(), " }");
  return res;
}

Theorem TheoryBitvector::combineLikeTerms(const Expr& e) {
  Theorem thm0 = d_rules->combineLikeTermsRule(e);
  return thm0;
}

Theorem TheoryBitvector::padBVPlus(const Expr& e) {
  TRACE("bv pad", "padBVPlus(", e, ") {");
  DebugAssert(BVPLUS == e.getOpKind(),
              "TheoryBitvector::padBVPlus:"
              "input must be a BVPLUS: " + e.toString());
//   bool needPadding = false;
  
//   //loop thru' the subterms to check if they need padding
//   int bvlen = BVSize(e);
//   for(Expr::iterator  i=e.begin(), iend=e.end();i!=iend;++i) {
//     int monomlen = BVSize(*i);
//     if(monomlen != bvlen) {
//       needPadding = true;
//       break;
//     }
//   }
  Theorem res;
//   if(needPadding) {
  res = d_rules->padBVPlus(e);
//   } else
//     res = reflexivityRule(e);
  TRACE("bv pad", "padBVPlus => ", res.getExpr(), " }");
  return res;
}

  
Theorem TheoryBitvector::flattenBVPlus(const Expr& e) {
  DebugAssert(BVPLUS == e.getOpKind(),
              "TheoryBitvector::padBVPlus:"
              "input must be a BVPLUS: " + e.toString());

  bool needFlattening = false;  
  //loop thru' the subterms to check if they need flatten
  for(Expr::iterator  i=e.begin(), iend=e.end();i!=iend;++i) {
    if(BVPLUS == (*i).getOpKind()) {
      needFlattening = true;
      break;
    }
  }
  
  Theorem res;
  if(needFlattening)
    res = d_rules->flattenBVPlus(e);
  else
    res = reflexivityRule(e);

  return res;
}

//! signextend e0 <=(s) e1 appropriately, then normalize and return
Theorem TheoryBitvector::signExtendBVLT(const Expr& e, int len, bool useFind) {
  DebugAssert(e.getOpKind()==SBVLT || e.getOpKind()==SBVLE,
              "TheoryBitvector::signExtendBVLT: input must be BVLT/BVLE"
              + e.toString());
  std::vector<Theorem> thms;
  std::vector<unsigned> changed;

  //e0 <= e1 <==> pad(e0) <= pad(e1)
  Theorem thm = d_rules->padSBVLTRule(e, len);
  Expr paddedE = thm.getRHS();

  //the rest of the code simply normalizes pad(e0) and pad(e1)
  Theorem thm0 = d_rules->signExtendRule(paddedE[0]);
  Expr rhs0 = thm0.getRHS();
  thm0 = transitivityRule(thm0, rewriteBV(rhs0, useFind));
  if(thm0.getLHS() != thm0.getRHS()) {
    thms.push_back(thm0);
    changed.push_back(0);
  }
  
  Theorem thm1 = d_rules->signExtendRule(paddedE[1]);
  Expr rhs1 = thm1.getRHS();
  thm1 = transitivityRule(thm1, rewriteBV(rhs1, useFind));
  if(thm1.getLHS() != thm1.getRHS()) {
    thms.push_back(thm1);
    changed.push_back(1);
  }

  Theorem result;
  if(changed.size() > 0) {
    result = substitutivityRule(paddedE,changed,thms);
    result = transitivityRule(thm, result);
  }
  else
    result = reflexivityRule(e);
  return result;
}

Theorem TheoryBitvector::rewriteConst(const Expr& e)
{
  // Rewrite bitvector operators which have constant arguments
  switch(e.getOpKind()) {
  case EQ:
    if(constantKids(e))
      return d_rules->eqConst(e);
    break;
  case CONCAT:
    if(constantKids(e))
      return d_rules->concatConst(e);
    break;
  case BVAND: {
    vector<int> idxs;
    constantKids(e, idxs);
    if(idxs.size() >= 2)
      return d_rules->andConst(e, idxs);
    break;
  }
  case BVOR: {
    vector<int> idxs;
    constantKids(e, idxs);
    if(idxs.size() >= 2)
      return d_rules->orConst(e, idxs);
    break;
  }
  case BVNEG:
    if(constantKids(e))
      return d_rules->negConst(e);
    break;
  case BOOLEXTRACT:
    if(constantKids(e))
      return d_rules->bitExtractConstant(e[0], getBoolExtractIndex(e));
    break;
  case EXTRACT:
    if(constantKids(e))
      return d_rules->extractConst(e);
    break;
  case BVPLUS:
    if(constantKids(e))
      return d_rules->bvplusConst(e);
    break;
  case BVMULT:
    if(constantKids(e))
      return d_rules->bvmultConst(e);
    break;
  default:
    break;
  }
  return reflexivityRule(e);
}

Theorem TheoryBitvector::rewriteBV(const Expr& e, bool useFind) {
  ExprMap<Theorem> cache;
  return rewriteBV(e, cache, useFind);
}


Theorem TheoryBitvector::rewriteBV(const Expr& e, ExprMap<Theorem>& cache,
                                   bool useFind) {
  TRACE("bitvector rewrite", "TheoryBitvector::rewriteBV(", e, ") {");

  ExprMap<Theorem>::iterator it = cache.find(e);
  if(it!=cache.end()) {
    Theorem res = (*it).second;
    TRACE("bitvector rewrite", "TheoryBitvector::rewriteBV[cached] => ",
          res.getExpr(), " }");
    IF_DEBUG(debugger.counter("bv rewriteBV cache hits")++);
    return res;
  }
    
  Theorem res;
  switch(e.getOpKind()) {
  case EQ: {
    // Rewrite bitvector operators which have constant arguments
    if(constantKids(e)) {
      res = d_rules->eqConst(e);
      IF_DEBUG(debugger.counter("bv rewrite const eq")++);
    } 
    //if both e[0],e[1] are BVPLUS. I disregard other cases like
    //BVPLUS(x,y)=x
    else if (BVPLUS == e[0].getOpKind() && 
             BVPLUS == e[1].getOpKind() &&
             *d_lhsMinusRhsFlag) {
      // e[0]=e[1] <==> e[0]+(-e[1])=0
      res = d_rules->lhsMinusRhsRule(e);
      Theorem  thm0 = rewriteBV(res.getRHS(),2,useFind);
      res = transitivityRule(res,thm0);
    }   
    else
      res = reflexivityRule(e);
    break;
  }
  case BOOLEXTRACT: {
    Expr t(e);
    // Normal form: t[0] for 1-bit t, collapse t[i:i][0] into t[i]
    if(BVSize(e[0]) > 1) { // transform t[i] to t[i:i][0] and rewrite
      res = rewriteBV(d_rules->bitExtractRewrite(e), cache, 2, useFind);
      t = res.getRHS();
    }
    if(t.getOpKind() == BOOLEXTRACT && t[0].getOpKind() == EXTRACT) {
      // Collapse t[i:i][0] to t[i]
      int low = getExtractLow(t[0]);
      if(getExtractHi(t[0]) == low) {
        Theorem thm(d_rules->bitExtractRewrite
                    (newBoolExtractExpr(t[0][0], low)));
        thm = symmetryRule(thm);
        res = (res.isNull())? thm : transitivityRule(res, thm);
        t = res.getRHS()[0];
        // Make sure t in the resulting t[i] is its own find pointer
        // (global invariant)
        if(useFind && t.hasFind()) {
          Theorem findThm = find(t);
          if(t != findThm.getRHS()) {
            vector<Theorem> thms;
            thms.push_back(findThm);
            thm = substitutivityRule(res.getRHS().getOp(), thms);
            res = transitivityRule(res, thm);
          }
        }
      }
    }
    if(!res.isNull()) t = res.getRHS();
    // Rewrite a constant extraction to TRUE or FALSE
    if(t.getOpKind() == BOOLEXTRACT && constantKids(t)) {
      Theorem thm = d_rules->bitExtractConstant(t[0], getBoolExtractIndex(t));
      res = (res.isNull())? thm : transitivityRule(res, thm);
    }
    break;
  }
  case SBVLT:
  case SBVLE:{
    /*! input: e0 <=(s) e1. output depends on whether the topbits(MSB) of
     *  e0 and e1 are constants. If they are constants then optimizations
     *  are done. In general, the following rule is implemented.
     * Step1:
     *                    e0 <=(s) e1 
     *                       <==> 
     *                 pad(e0) <=(s) pad(e1)
     * Step2:
     *                 pad(e0) <=(s) pad(e1) 
     *                       <==> 
     *             (e0[n-1] AND NOT e1[n-1]) OR 
     *             (e0[n-1] AND e1[n-1] AND e1[n-2:0] <= e0[n-2:0]) OR 
     *             (NOT e0[n-1] AND NOT e1[n-1] AND e0[n-2:0] <= e1[n-2:0])
     */
    int e0len = BVSize(e[0]);
    int e1len = BVSize(e[1]);
    int bvlength = e0len>=e1len ? e0len : e1len;
    //e0 <=(s) e1 <=> signpad(e0) <=(s) signpad(e1)
    Theorem thm0 = signExtendBVLT(e, bvlength, useFind);
    //signpad(e0) <= signpad(e1)
    Expr thm0RHS = thm0.getRHS();
    DebugAssert(thm0RHS.getOpKind() == SBVLT || 
                thm0RHS.getOpKind() == SBVLE,
                "TheoryBitvector::RewriteBV");
    //signpad(e0)[bvlength-1:bvlength-1]
    const Expr MSB0 = newBVExtractExpr(thm0RHS[0],bvlength-1,bvlength-1);
    //signpad(e1)[bvlength-1:bvlength-1]
    const Expr MSB1 = newBVExtractExpr(thm0RHS[1],bvlength-1,bvlength-1);
    //rewritten MSB0
    const Theorem topBit0 = rewriteBV(MSB0, 2, useFind);
    //rewritten MSB1
    const Theorem topBit1 = rewriteBV(MSB1, 2, useFind);
    //compute e0 <=(s) e1 <==> signpad(e0) <=(s) signpad(e1) <==>
    //output as given above
    Theorem thm1 = d_rules->signBVLTRule(thm0RHS, topBit0, topBit1);
    thm1 = transitivityRule(thm1,simplify(thm1.getRHS()));
    res = transitivityRule(thm0,thm1);
    break;
  }
  case BVLT:
  case BVLE: {
    Expr lhs = e[0];
    Expr rhs = e[1];
    int e0len = BVSize(lhs);
    int e1len = BVSize(rhs);
    int bvlength = e0len>=e1len ? e0len : e1len;
    //e0 <= e1 <=> pad(e0) <= pad(e1)
    Theorem thm0 = d_rules->padBVLTRule(e, bvlength);
    //pad(e0) <= pad(e1)
    Expr thm0RHS = thm0.getRHS();
    DebugAssert(thm0RHS.getOpKind() == BVLT || 
                thm0RHS.getOpKind() == BVLE,
                "TheoryBitvector::RewriteBV");
    //pad(e0)
    Expr thm0RHS0 = thm0RHS[0];
    //pad(e1)
    Expr thm0RHS1 = thm0RHS[1];    
    //pad(e0) <=> pad(e0)'
    Theorem rhsThm0 = rewriteBV(thm0RHS0, 2, false);
    //pad(e1) <=> pad(e1)'
    Theorem rhsThm1 = rewriteBV(thm0RHS1, 2, false);

    std::vector<Theorem> thms;
    std::vector<unsigned> changed;
    if(rhsThm0.getLHS() != rhsThm0.getRHS()) {
      thms.push_back(rhsThm0);
      changed.push_back(0);
    }    
    if(rhsThm1.getLHS() != rhsThm1.getRHS()) {
      thms.push_back(rhsThm1);
      changed.push_back(1);
    }

    Theorem thm1;
    if(changed.size() > 0) {
      //pad(e0)<pad(e1) <=> pad(e0)' < pad(e1)'
      thm1 = substitutivityRule(thm0RHS, changed, thms);
      thm1 = transitivityRule(thm0,thm1);
    }
    else
      thm1 = thm0;

    lhs = thm1.getRHS()[0];
    rhs = thm1.getRHS()[1];
    Expr newE = thm1.getRHS();

    int kind = newE.getOpKind();
    if(lhs == rhs)
      res = transitivityRule(thm1,d_rules->lhsEqRhsIneqn(newE, kind));
    else if(BVCONST == lhs.getKind() && BVCONST == rhs.getKind())
      res = transitivityRule(thm1,d_rules->bvConstIneqn(newE, kind));
    else
      res = reflexivityRule(e);
    break;
  }
  case SX: {  
    res = d_rules->signExtendRule(e);
    Expr rhs = res.getRHS();
    res = transitivityRule(res, rewriteBV(rhs, useFind));
    break;
  }
  case RIGHTSHIFT:
    res = rewriteBV(d_rules->rightShiftToConcat(e), 1, useFind);
    break;
  case LEFTSHIFT:
    res = rewriteBV(d_rules->leftShiftToConcat(e), 1, useFind);
    break;
  case CONCAT:  
  case BVAND:
  case BVOR:
  case BVNEG:
  case EXTRACT:
    res = normalizeConcat(e, useFind);
    break;
  case BVPLUS:
  case BVUMINUS:
  case BVMULT:
    res = normalizeBVArith(e, useFind);
    break;
  default:
    break;
  }
  if(res.isNull()) res = reflexivityRule(e);
  // Ensure that the result is a find pointer of itself (if it has any)
  const Expr& rhs = res.getRHS();
  // Congruence Closure rewrites for CONCAT
  if(res.getRHS().getOpKind()==CONCAT) {
    res = transitivityRule(res, rewriteCC(res.getRHS()));
  }
  if(useFind && rhs.hasFind())
    res = transitivityRule(res, find(rhs));
  cache[e] = res;
  TRACE("bitvector rewrite", "TheoryBitvector::rewriteBV => ",
        res.getExpr(), " }");
  return res;
}


Theorem
TheoryBitvector::rewriteBV(const Expr& e, int n, bool useFind) {
  ExprMap<Theorem> cache;
  return rewriteBV(e, cache, n, useFind);
}

Theorem
TheoryBitvector::rewriteBV(const Expr& e, ExprMap<Theorem>& cache, int n,
                           bool useFind) {
  TRACE("bitvector rewrite",
        "TheoryBitvector::rewriteBV["+int2string(n)+"](", e, ") {");
  Theorem res;

  if(n > 0) {
    // First, check the cache
    ExprMap<Theorem>::iterator it = cache.find(e);
    if(it!=cache.end()) {
      res = (*it).second;
      TRACE("bitvector rewrite", "TheoryBitvector::rewrite["+int2string(n)
            +"][cached] => ", res.getExpr(), " }");
      IF_DEBUG(debugger.counter("bv rewriteBV[n] cache hits")++);
      return res;
    }
    
    if(n >= 2) {
      // rewrite children recursively
      vector<Theorem> thms;
      vector<unsigned> changed;
      for(int i=0, iend=e.arity(); i<iend; ++i) {
        Theorem thm = rewriteBV(e[i], cache, n-1, useFind);
        if(thm.getLHS() != thm.getRHS()) {
          thms.push_back(thm);
          changed.push_back(i);
        }
      }
      if(changed.size() > 0)
        res = substitutivityRule(e, changed, thms);
    }
    // Rewrite the top node
    if(res.isNull())
      res = rewriteBV(e, cache, useFind);
    else
      res = transitivityRule(res, rewriteBV(res.getRHS(), cache, useFind));
  } else
    res = reflexivityRule(e);

  DebugAssert(!res.isNull(), "TheoryBitvector::rewriteBV(e, cache, n)");
  TRACE("bitvector rewrite",
        "TheoryBitvector::rewriteBV["+int2string(n)+"] => ",
        res.getExpr(), " }");
  // The cache is not updated here, since it's used in rewriteBV(e, cache)
  return res;
}

// Recursively descend into the expression e, keeping track of whether
// we are under even or odd number of negations ('neg' == true means
// odd, the context is "negative").
// Produce a proof of e <==> e' or !e <==> e', depending on whether
// neg is false or true, respectively.
// This function must be called only from the pushNegation function
Theorem TheoryBitvector::pushNegationRec(const Expr& e, bool neg) {
  TRACE("pushNegation", "pushNegationRec(", e,
        ", neg=" + string(neg? "true":"false") + ") {");
  //DebugAssert(isTerm(e), 
  //      "TheoryBitvector::pushNegationRec: input must be a term. e = " + 
  //      e.toString());
  Expr NegExpr = newBVNegExpr(e);
  ExprMap<Theorem>::iterator i = d_pushNegCache.find(neg ? NegExpr : e);
  if(i != d_pushNegCache.end()) { // Found cached result
    TRACE("TheoryBitvector::pushNegation", 
          "pushNegationRec [cached] => ", (*i).second, "}");
    return (*i).second;
  }
  // By default, do not rewrite
  Theorem res(reflexivityRule((neg)? NegExpr : e));
  if(neg) {
    switch(e.getOpKind()) {
    case BVCONST: 
      res = d_rules->negConst(NegExpr); 
      break;
    case BVNEG:{
      Theorem thm0 = d_rules->negNeg(NegExpr);
      res = pushNegationRec(thm0.getRHS(), false);
      res = transitivityRule(thm0,res);
      break;
    }
    case BVAND: {
      //demorgan's laws. 
      Theorem thm0 = d_rules->negBVand(NegExpr);
      Expr ee = thm0.getRHS();
      if (ee.arity() == 0) res = thm0;
      else {
        //process each negated kid
        Op op = ee.getOp();
        vector<Theorem> thms;
        for(Expr::iterator i=ee.begin(), iend=ee.end(); i!=iend; ++i)
          thms.push_back(pushNegationRec((*i)[0], true));
        res = substitutivityRule(op, thms);
        res = transitivityRule(thm0, res);
        res = transitivityRule(res, rewriteAux(res.getRHS()));
      }
      break;
    }
    case BVOR: {
      //demorgan's laws. 
      Theorem thm0 = d_rules->negBVor(NegExpr);
      Expr ee = thm0.getRHS();
      if (ee.arity() == 0) res = thm0;
      else {
        //process each negated kid
        Op op = ee.getOp();
        vector<Theorem> thms;
        for(Expr::iterator i=ee.begin(), iend=ee.end(); i!=iend; ++i)
          thms.push_back(pushNegationRec((*i)[0], true));
        res = substitutivityRule(op, thms);
        res = transitivityRule(thm0, res);
        res = transitivityRule(res, rewriteAux(res.getRHS()));
      }
      break;
    }
    case CONCAT: {
      //demorgan's laws. 
      Theorem thm0 = d_rules->negConcat(NegExpr);
      Expr ee = thm0.getRHS();
      if (ee.arity() == 0) res = thm0;
      else {
        //process each negated kid
        Op op = ee.getOp();
        vector<Theorem> thms;
        for(Expr::iterator i=ee.begin(), iend=ee.end(); i!=iend; ++i)
          thms.push_back(pushNegationRec((*i)[0], true));
        res = substitutivityRule(op, thms);
        res = transitivityRule(thm0, res);
      }
      break;
    }
    case BVPLUS:
      // FIXME: Need to implement the following transformation:
      // ~(x+y) <=> ~x+~y+1
      // (because  ~(x+y)+1= -(x+y) = -x-y = ~x+1+~y+1)
    case BVMULT:
      // FIXME: Need to implement the following transformation:
      // ~(x*y) <=> (~x+1)*y-1 
      // [ where we prefer x to be constant/AND/OR/NEG and then
      //   BVPLUS, and only then everything else].
      // (because  ~(x*y)+1= -(x+y) = (-x)*y = (~x+1)*y)
    default:
      res = reflexivityRule(NegExpr);
      break;
    }
  } else { // if(!neg)
    switch(e.getOpKind()) {
    case BVNEG: 
      res = pushNegationRec(e[0], true); 
      break;
    case CONCAT:
    case BVAND:
    case BVOR: {
      if (e.arity() == 0) res = reflexivityRule(e);
      else {
        Op op = e.getOp();
        vector<Theorem> thms;
        for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
          thms.push_back(pushNegationRec(*i, false));
        res = substitutivityRule(op, thms);
        res = transitivityRule(res, rewriteAux(res.getRHS()));
      }
      break;
    }
    default:
      res = reflexivityRule(e);
      break;
    } // end of switch(e.getOpKind())
  }
  TRACE("TheoryBitvector::pushNegation", "pushNegationRec => ", res, "}");
  d_pushNegCache[neg? NegExpr : e] = res;
  return res;
}

Theorem TheoryBitvector::pushNegationRec(const Theorem& thm, bool neg) {
  DebugAssert(thm.isRewrite(), 
              "TheoryBitvector::pushNegationRec(Theorem): bad theorem: "
              + thm.toString());
  Expr e(thm.getRHS());
  if(neg) {
    DebugAssert(e.isNot(), 
                "TheoryBitvector::pushNegationRec(Theorem, neg = true): bad Theorem: "
                + thm.toString());
    e = e[0];
  }
  return transitivityRule(thm, pushNegationRec(e, neg));
}

// We assume that the cache is initially empty
Theorem TheoryBitvector::pushNegation(const Expr& e) {
  d_pushNegCache.clear();
  Theorem res;
  if(BVNEG == e.getOpKind())
    res = pushNegationRec(e[0], true);
  else if(BITVECTOR == e.getType().getExpr().getOpKind())
    res = pushNegationRec(e, false);
  else
    res = reflexivityRule(e);
  return res;
}

//! Top down simplifier
Theorem TheoryBitvector::simplifyOp(const Expr& e) {
  if (e.arity() > 0) {
    Expr ee(e);
    Theorem thm0;
    switch(e.getOpKind()) {
    case BVNEG:
      if(*d_pushNegationFlag)
        thm0 = pushNegation(e);
      break;
    case EXTRACT:
      switch(e[0].getOpKind()) {
      case BVPLUS:
        thm0 = d_rules->extractBVPlus(e);
        break;
      case BVMULT:
        thm0 = d_rules->extractBVMult(e);
        break;
      default:
        thm0 = reflexivityRule(e);
        break;
      }
      break;
    case BVPLUS:
      thm0 = d_rules->padBVPlus(e);
      break;
    case BVMULT:
      thm0 = d_rules->padBVMult(e);
      break;
    case CONCAT: // 0bin0_[k] @ BVPLUS(n, args) => BVPLUS(n+k, args)
      if(e.arity()==2 && e[0].getKind()==BVCONST && e[1].getOpKind()==BVPLUS
         && computeBVConst(e[0]) == 0) {
        thm0 = d_rules->bvplusZeroConcatRule(e);
        if(thm0.getLHS()!=thm0.getRHS())
          thm0 = transitivityRule(thm0, padBVPlus(thm0.getRHS()));
      }
      break;
    case RIGHTSHIFT:
      thm0 = d_rules->rightShiftToConcat(e);
      break;
    case LEFTSHIFT:
      thm0 = d_rules->leftShiftToConcat(e);
      break;
    default:
      thm0 = reflexivityRule(e);
      break;
    }
    vector<Theorem> newChildrenThm;
    vector<unsigned> changed;
    if(thm0.isNull()) thm0 = reflexivityRule(e);
    ee = thm0.getRHS();
    int ar = ee.arity();
    for(int k = 0; k < ar; ++k) {
      // Recursively simplify the kids  
      Theorem thm = simplifyRec(ee[k]);
      if (thm.getLHS() != thm.getRHS()) {
        newChildrenThm.push_back(thm);
        changed.push_back(k);
      }
    }
    if(changed.size() > 0) {
      Theorem thm1 = substitutivityRule(ee, changed, newChildrenThm);
      return transitivityRule(thm0,thm1);
    } else
      return thm0;
  }
  return reflexivityRule(e);
}

///////////////////////////////////////////////////////////////////////////////
// TheoryBitvector Public Methods                                            //
///////////////////////////////////////////////////////////////////////////////
TheoryBitvector::TheoryBitvector(TheoryCore* core)
  : Theory(core, "Bitvector"),
    d_bvDelayEq(core->getStatistics().counter("bv delayed assert eqs")),
    d_bvAssertEq(core->getStatistics().counter("bv eager assert eqs")),
    d_bvDelayDiseq(core->getStatistics().counter("bv delayed assert diseqs")),
    d_bvAssertDiseq(core->getStatistics().counter("bv eager assert diseqs")),
    d_bvTypePreds(core->getStatistics().counter("bv type preds enqueued")),
    d_bvDelayTypePreds(core->getStatistics().counter("bv type preds delayed")),
    d_bvBitBlastEq(core->getStatistics().counter("bv bitblast eqs")),
    d_bvBitBlastDiseq(core->getStatistics().counter("bv bitblast diseqs")),
    d_simplifyFlag(&(core->getFlags()["bv-simplify"].getBool())),
    d_booleanRWFlag(&(core->getFlags()["boolean-rewrite"].getBool())),
    //d_boolExtractCacheFlag(&(core->getFlags()["use-boolextract-cache"].getBool())),
    d_bv32Flag(&(core->getFlags()["bv32-flag"].getBool())),
    d_rewriteFlag(&(core->getFlags()["bv-rewrite"].getBool())),
    d_concatRewriteFlag(&(core->getFlags()["bv-concatnormal-rewrite"].getBool())),
    d_bvplusRewriteFlag(&(core->getFlags()["bv-plusnormal-rewrite"].getBool())),
    d_rwBitBlastFlag(&(core->getFlags()["bv-rw-bitblast"].getBool())),
    d_cnfBitBlastFlag(&(core->getFlags()["bv-cnf-bitblast"].getBool())),
    d_lhsMinusRhsFlag(&(core->getFlags()["bv-lhs-minus-rhs"].getBool())),
    d_updateFlag(&(core->getFlags()["bv-update"].getBool())),
    d_setupFlag(&(core->getFlags()["bv-setup"].getBool())),
    d_setupSharedFlag(&(core->getFlags()["bv-shared-setup"].getBool())),
    d_pushNegationFlag(&(core->getFlags()["bv-pushnegation"].getBool())),
    d_bitvecCache(core->getCM()->getCurrentContext()),
    d_eq(core->getCM()->getCurrentContext()),
    d_eqIdx(core->getCM()->getCurrentContext(), 0, 0),
    d_eqBlastIdx(core->getCM()->getCurrentContext(), 0, 0),
    d_diseq(core->getCM()->getCurrentContext()),
    d_diseqIdx(core->getCM()->getCurrentContext(), 0, 0),
    d_staleDB(core->getCM()->getCurrentContext()),
    d_tccs(core->getCM()->getCurrentContext()),
    d_tccsIdx(core->getCM()->getCurrentContext(), 0, 0),
    d_sharedSubterms(core->getCM()->getCurrentContext()),
    d_typePredsCache(core->getCM()->getCurrentContext())
{
  getEM()->newKind(BITVECTOR, "BITVECTOR", true);
  getEM()->newKind(BVCONST, "BVCONST");
  getEM()->newKind(HEXBVCONST, "HEXBVCONST");
  getEM()->newKind(CONCAT, "CONCAT");
  getEM()->newKind(BVOR, "BVOR");
  getEM()->newKind(BVAND, "BVAND");
  getEM()->newKind(BVXOR, "BVXOR");
  getEM()->newKind(BVNAND, "BVNAND");
  getEM()->newKind(BVNOR, "BVNOR");
  getEM()->newKind(BVXNOR, "BVXNOR");
  getEM()->newKind(BVNEG, "BVNEG");
  getEM()->newKind(EXTRACT, "EXTRACT");
  getEM()->newKind(LEFTSHIFT, "LEFTSHIFT");
  getEM()->newKind(RIGHTSHIFT, "RIGHTSHIFT");
  getEM()->newKind(VARSHIFT, "VARSHIFT");
  getEM()->newKind(BVPLUS, "BVPLUS");
  getEM()->newKind(BVMULT, "BVMULT");
  getEM()->newKind(BVSUB, "BVSUB");
  getEM()->newKind(BVUMINUS, "BVUMINUS");
  getEM()->newKind(BOOLEXTRACT, "BOOLEXTRACT");
  getEM()->newKind(SX,"SX");
  getEM()->newKind(SBVLT, "SBVLT");
  getEM()->newKind(SBVLE, "SBVLE");
  getEM()->newKind(SBVGT, "SBVGT");
  getEM()->newKind(SBVGE, "SBVGE");
  getEM()->newKind(BVLT, "BVLT");
  getEM()->newKind(BVLE, "BVLE");
  getEM()->newKind(BVGT, "BVGT");
  getEM()->newKind(BVGE, "BVGE");
  getEM()->newKind(INTTOBV, "INTTOBV");
  getEM()->newKind(BVTOINT, "BVTOINT");
  getEM()->newKind(BVTYPEPRED, "BVTYPEPRED");
  getEM()->newKind(BVPARAMOP, "BVPARAMOP");

 
  std::vector<int> kinds;
  kinds.push_back(BITVECTOR);
  kinds.push_back(BVCONST);
  kinds.push_back(HEXBVCONST);
  kinds.push_back(CONCAT);
  kinds.push_back(BVOR);
  kinds.push_back(BVAND);
  kinds.push_back(BVXOR);
  kinds.push_back(BVXNOR);
  kinds.push_back(BVNAND);
  kinds.push_back(BVNOR);
  kinds.push_back(BVNEG);
  kinds.push_back(EXTRACT);
  kinds.push_back(LEFTSHIFT);
  kinds.push_back(RIGHTSHIFT);
  kinds.push_back(VARSHIFT);
  kinds.push_back(BVPLUS);
  kinds.push_back(BVMULT);
  kinds.push_back(BVSUB);
  kinds.push_back(BVUMINUS);
  kinds.push_back(BOOLEXTRACT);
  kinds.push_back(SX);
  kinds.push_back(SBVLT);
  kinds.push_back(SBVLE);
  kinds.push_back(SBVGT);
  kinds.push_back(SBVGE);
  kinds.push_back(BVLT);
  kinds.push_back(BVLE);
  kinds.push_back(BVGT);
  kinds.push_back(BVGE);
  kinds.push_back(INTTOBV);
  kinds.push_back(BVTOINT);
  kinds.push_back(BVTYPEPRED);
  kinds.push_back(BVPARAMOP);

  registerTheory(this, kinds);
 
  d_bvConstExprIndex = getEM()->registerSubclass(sizeof(BVConstExpr));

  // Cache constants 0bin0 and 0bin1
  vector<bool> bits(1);
  bits[0]=false;
  d_bvZero = newBVConstExpr(bits);
  bits[0]=true;
  d_bvOne = newBVConstExpr(bits);

  // Instantiate the rules after all expression creation is
  // registered, since the constructor creates some bit-vector
  // expressions.
  d_rules = createProofRules();
}


// Destructor: delete the proof rules class if it's present
TheoryBitvector::~TheoryBitvector() {
  if(d_rules != NULL) delete d_rules;
}


void
TheoryBitvector::collectSharedSubterms(const Expr& e) {
  TRACE("bitvector shared", "TheoryBitvector::collectSharedSubterms(", e.toString(), ")");
  if(d_sharedSubterms.count(e)>0) return;
  IF_DEBUG(debugger.counter("bv shared subterms")++);
  d_sharedSubterms[e]=true;

  if(d_typePredsCache.count(e) > 0) {
    Theorem pred = d_typePredsCache[e];
    if((pred.getExpr()).isFalse())
      setInconsistent(pred);
    else if(!(pred.getExpr()).isTrue())
      assertTypePred(e,pred);
  }

  if(!isLeaf(e)) {
    for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
      collectSharedSubterms(*i);
  }
  setupExpr(e);
  if(d_sharedSubterms[e])
    TRACE("bitvector shared", "TheoryBitvector::collectSharedSubterms =>", "true" , ")");
  else
    TRACE("bitvector shared", "TheoryBitvector::collectSharedSubterms =>", "false" , ")");
}

void TheoryBitvector::addSharedTerm(const Expr& e) {
  IF_DEBUG(debugger.counter("bv shared terms")++);
  collectSharedSubterms(e);
}


void TheoryBitvector::assertFact(const Theorem& e) {
  TRACE("bitvector", "TheoryBitvector::assertFact(", e.getExpr(), ")");
  const Expr& expr = e.getExpr();

  //strategy
  Theorem result;
  switch(expr.getOpKind()) {
  case BVTYPEPRED:
    enqueueFact(d_rules->expandTypePred(e));
    IF_DEBUG(debugger.counter("bv expand type pred")++);
    break;
  case NOT: {
    const Expr& e0 = expr[0];
    switch(e0.getOpKind()) {
    case BOOLEXTRACT:
      // Assert e0[i:i] = 0bin0
      IF_DEBUG(debugger.counter("bv received NOT BOOLEXTRACT")++);
      if(theoryCore()->getFlags()["bv-assert"].getBool())
        enqueueFact(d_rules->bitExtractToExtract(e));
      break;
    case EQ:
      // enqueueFact(bitBlastDisEqn(e));
      IF_DEBUG(debugger.counter("bv received diseq")++);
      if(theoryCore()->getFlags()["bv-delay-diseq"].getBool()) {
        d_bvDelayDiseq++;
        d_diseq.push_back(e);
      }
      else {
        d_bvAssertDiseq++;
        result = bitBlastDisEqn(e);
      }
      break;
    case BVLT:
    case BVLE:
      result = d_rules->notBVLTRule(expr, expr[0].getOpKind());
      result = iffMP(e, result);
      result = iffMP(result, bitBlastIneqn(result.getExpr()));
      break;
    case BVTYPEPRED:
      enqueueFact(d_rules->expandTypePred(e));
      IF_DEBUG(debugger.counter("bv expand type pred")++);
      break;
    default: // Ignore other facts
      break;
    }
    break;
  }
  case BOOLEXTRACT:
    // Assert e0[i:i] = 0bin1
    if(theoryCore()->getFlags()["bv-assert"].getBool())
      enqueueFact(d_rules->bitExtractToExtract(e));
    IF_DEBUG(debugger.counter("bv received BOOLEXTRACT")++);
    break;
  case EQ:
    IF_DEBUG(debugger.counter("bv received eq")++);
    if(theoryCore()->getFlags()["bv-delay-eq"].getBool()) {
      d_bvDelayEq++;
      // d_eq.push_back(e);
      int size(BVSize(e.getLHS()));
      if(size >= 2 && theoryCore()->getFlags()["bv-bit-eq"].getBool()) {
        IF_DEBUG(debugger.counter("bv assert eq wide")++);
        // Enqueue equalities over individual bits
        Theorem thm = d_rules->eqToBits(e);
        for(int i=0; i<size; ++i) {
          IF_DEBUG(debugger.counter("bv delay eq 1-bit")++);
          Theorem ti(getCommonRules()->andElim(thm, i));
          ti = iffMP(ti, rewriteBV(ti.getExpr(), 2, true));
          // ti may simplify to TRUE or FALSE
          if(ti.isRewrite()) d_eq.push_back(ti);
          else enqueueFact(ti);
        }
      } else
        d_eq.push_back(e);
    } else {
      d_bvAssertEq++;
      result = iffMP(e, bitBlastEqn(e.getExpr()));
    }
    break;
  case BVLT:
  case BVLE:
    result = iffMP(e, bitBlastIneqn(e.getExpr()));
    break;
  default: // Ignore other facts
    break;
  }

  if(result.isNull()) return;

  // Simplifying bit-blasted expressions makes things easier for the
  // CNF converter
  if(*d_simplifyFlag)
    result = iffMP(result, simplify(result.getExpr()));
  else if (*d_booleanRWFlag)
    result = iffMP(result, rewriteBoolean(result.getExpr()));
  enqueueFact(result);
}


void
TheoryBitvector::assertTypePred(const Expr& e, const Theorem& pred) {
  TRACE("bv asserttypepred", "TheoryBitvector::assertTypePred(", e.toString(), ")");
  // Ignore bitvector constants (they always satisfy type predicates)
  // and bitvector operators.  When rewrites and updates are enabled.
  // their type predicates will be implicitly derived from the type
  // predicates of the arguments.
  switch(e.getOpKind()) {
  case BVCONST:
    return;
  case CONCAT:
  case BVOR:
  case BVAND:
  case BVNEG:
  case EXTRACT:
  case LEFTSHIFT:
  case RIGHTSHIFT:
  case BVPLUS:
  case BVUMINUS:
  case BVSUB:
  case BVXOR:
  case BVXNOR:
  case BVNAND:
  case BVMULT:
  case BOOLEXTRACT:
  case SX:
  case SBVLT:
  case SBVLE:
  case SBVGT:
  case SBVGE:
  case BVLT:
  case BVLE:
  case BVGT:
  case BVGE:
//   case VAR_SHIFT:
    if(*d_setupFlag && *d_updateFlag) return;
    break;
  default:
    break;
  }
  // If the variable is not a part of a shared term, don't bother
     if(d_sharedSubterms.count(e) == 0) {
       d_typePredsCache[e] = pred;
       return;
     }
  //The remaining type predicates are important
  if(!theoryCore()->getFlags()["bv-delay-typepred"].getBool()) {
    d_bvTypePreds++;
    enqueueFact(pred);
  }
  else {
    d_bvDelayTypePreds++;
    d_tccs.push_back(pred);
  }
}


void TheoryBitvector::checkSat(bool fullEffort) {
  if(fullEffort) {
    // Bit-blast equalities first
    if(d_eqIdx<d_eq.size()) {
      for(; d_eqIdx<d_eq.size(); d_eqIdx = d_eqIdx + 1) {
        IF_DEBUG(debugger.counter("bv enqueue eq 1-bit")++);
        enqueueFact(d_eq[d_eqIdx]);
      }
    } else if(d_eqBlastIdx<d_eq.size()) {
      for(; d_eqBlastIdx<d_eq.size(); d_eqBlastIdx = d_eqBlastIdx + 1) {
        Theorem result = iffMP(d_eq[d_eqBlastIdx], 
                               bitBlastEqn(d_eq[d_eqBlastIdx].getExpr()));
        if(*d_simplifyFlag)
          result = iffMP(result, simplify(result.getExpr()));
        else if (*d_booleanRWFlag)
          result = iffMP(result, rewriteBoolean(result.getExpr()));     
        enqueueFact(result);
      }
      // Only if there are no more equalities, deal with disequalities
    } else if(d_diseqIdx<d_diseq.size()) {
      // None of the disequalities is violated due to equal find
      // pointers, since otherwise TheoryCore would have detected that
      // already.  Therefore, we can only hope to simplify the
      // expressions.
      for(; d_diseqIdx<d_diseq.size(); d_diseqIdx = d_diseqIdx + 1) {
        Theorem diseq = d_diseq[d_diseqIdx];
        Expr diseqExpr = diseq.getExpr();
        const Expr& eqExpr = diseqExpr[0];
        const Theorem& thm0 = find(eqExpr[0]);
        const Theorem& thm1 = find(eqExpr[1]);
        vector<Theorem> thms;
        vector<unsigned> changed;
        if(thm0.getLHS() != thm0.getRHS()) {
          changed.push_back(0);
          thms.push_back(thm0);
        }
        if(thm1.getLHS() != thm1.getRHS()) {
          changed.push_back(1);
          thms.push_back(thm1);
        }
        if(changed.size() > 0) {
          IF_DEBUG(debugger.counter("bv simplified diseq")++);
          Theorem subst = substitutivityRule(eqExpr, changed, thms);
          thms.clear();
          thms.push_back(subst);
          diseq = iffMP(diseq, substitutivityRule(diseqExpr.getOp(), thms));
        }
        Theorem result = bitBlastDisEqn(diseq);
        if(*d_simplifyFlag)
          result = iffMP(result, simplify(result.getExpr()));
        else if (*d_booleanRWFlag)
          result = iffMP(result, rewriteBoolean(result.getExpr()));
        enqueueFact(result);
      }
    } else {
      // Finally, if there is nothing else to do, assert all the
      // remaining type predicates on the bits, for completeness
      for(; d_tccsIdx<d_tccs.size(); d_tccsIdx = d_tccsIdx + 1) {
        Theorem tcc(d_tccs[d_tccsIdx]);
        tcc = iffMP(tcc, simplify(tcc.getExpr()));
        if(!tcc.getExpr().isTrue()) {
          IF_DEBUG(debugger.counter("bv enqueue type pred")++);
          d_bvTypePreds++;
          enqueueFact(d_tccs[d_tccsIdx]);
        }
      }
    }
  }
}


Theorem TheoryBitvector::rewrite(const Expr& e) {
  return rewriteAux(e);
}


Theorem TheoryBitvector::rewriteAux(const Expr& e) {
  Theorem res;
  if(*d_rewriteFlag)
    res = rewriteBV(e, true);
  else {
    res = rewriteConst(e);
    IF_DEBUG(if(res.getRHS()!=res.getLHS())
             debugger.counter("bv rewrite const")++);
    // Ensure that the result is a find pointer of itself (if it has any)
    const Expr& rhs = res.getRHS();
    if(rhs.hasFind())
      res = transitivityRule(res, find(rhs));
  }
  return res;
}

Theorem TheoryBitvector::rewriteAtomic(const Expr& e) {
  TRACE("bv rewriteatomic", "rewriteAtomic(", e.toString(), ") {"); 
  
  Theorem res = reflexivityRule(e);
  if(*d_cnfBitBlastFlag && res.getRHS().isEq()) {
    //res = rewriteAux(e);
    res = transitivityRule(res, bitBlastEqn(res.getRHS()));
    res = transitivityRule(res, simplify(res.getRHS()));
  }
  else if(*d_cnfBitBlastFlag && 
          (BVLT== res.getRHS().getOpKind() || BVLE==res.getRHS().getOpKind())) {
    //res = rewriteAux(e);
    res = transitivityRule(res, bitBlastIneqn(res.getRHS()));
    res = transitivityRule(res, simplify(res.getRHS()));
  }
  TRACE("bv rewriteatomic", "rewriteAtomic => ", res.toString(), "}"); 
  return res;
}

// We set up only shared terms
void TheoryBitvector::setup(const Expr& e) {
  if(!*d_setupSharedFlag) {
    if(e.getOpKind()==CONCAT) {
      setupCC(e);
    } else {      
      for (int k=0, ar=e.arity(); k < ar; ++k) {
        // Constants never change
        if(e[k].getKind() == BVCONST) continue;
        e[k].addToNotify(this, e);
        TRACE("bv setup", "e["+int2string(k)+"]="+e[k].toString()+": ",
              *(e[k].getNotify()), "");
      }
    }
  }
}


void TheoryBitvector::setupExpr(const Expr& e) {
  TRACE("bv setup", "setupExpr(", e, ") {");
  if(!(*d_setupFlag)) {
    TRACE_MSG("bv setup", "setupExpr[-bv-setup] => }");
    return;
  }
  // Process only terms.  If not a term, nothing to do.
  if(!e.isTerm()) {
    TRACE_MSG("bv setup", "setupExpr[not term] => }");
    return;
  }
  // Do not setup constants
  if(e.getKind()==BVCONST) {
    TRACE_MSG("bv setup", "setupExpr[const] => }");
    return;
  }
  // Only setup subterms of shared terms

  // First, set up notification for the kids (the usual stuff)
  if(*d_setupSharedFlag) {
    if(e.getOpKind()==CONCAT)
      setupCC(e); 
    else {      
      for (int k=0, ar=e.arity(); k < ar; ++k) {
        // Constants never change
        if(e[k].getKind() == BVCONST) continue;
        e[k].addToNotify(this, e);
        TRACE("bv setup", "e["+int2string(k)+"] = "+e[k].toString()+": ",
              *(e[k].getNotify()), "");
      }
    }
  }
  // Next, set up additional notifications for individual bits.  Skip
  // CONCAT expressions, since the bits of their kids have already
  // been setup.
  Type tp(getBaseType(e));
  if( e.getOpKind() != CONCAT  && 
      e.getOpKind() != BVCONST && 
      tp.getExpr().getOpKind() == BITVECTOR) {
    int size = BVSize(e);
    if(size >= 2) {
      IF_DEBUG(debugger.counter("setup long bitvectors")++);
      // Assert an equality e = e[n-1:n-1]@...@e[0:0] with individual
      // bits fully simplified
      vector<Expr> kids;
      vector<unsigned> changed; // for simplification
      vector<Theorem> thms; // simplification of kids
      for(int i=size-1; i>=0; i=i-1) {
        Expr k = newBVExtractExpr(e, i, i);
        Theorem thm = rewriteAux(k);
        if(thm.getLHS() != thm.getRHS()) {
          changed.push_back(kids.size());
          thms.push_back(thm);
        }
        kids.push_back(k);
      }
      Expr concat(newConcatExpr(kids));
      // Construct a Theorem(concat = e)
      Theorem thm = d_rules->concatMergeExtract(concat);
      thm = transitivityRule(thm, d_rules->extractWhole(thm.getRHS()));
      // If bits simplified, substitute the new bits
      if(changed.size() > 0) {
        thm = symmetryRule(thm);
        Theorem subst = substitutivityRule(thm.getRHS(), changed, thms);
        thm = transitivityRule(thm, subst);
        thm = symmetryRule(thm);
      }
      // Get the latest version of the concatenation of bits
      concat = thm.getLHS();
      // HACK ATTACK: we want 'concat' to be setup the way it is, but
      // we cannot use enqueueEquality() [since those are not
      // processed at this point] or enqueueFact() [since it will
      // simplify the equality to TRUE and ignore it].  Hence, we'll
      // do setup here.
      //
      // It involves: setting find pointers and calling setup() on the
      // bits and on the 'concat', unless they already have find
      // pointers.
      if(!concat.hasFind()) {
        theoryCore()->setupTerm(concat, this);
        // Set up notification for the bits
        if(*d_setupSharedFlag)
          setupCC(concat);       
        // Set the find pointer properly
        // if(concat > e)
        concat.setFind(thm);
        if(constantKids(concat)) {
          thm = symmetryRule(thm);
          Theorem t1 = d_rules->concatConst(thm.getRHS());
          thm = transitivityRule(thm,t1);
          enqueueFact(thm);
        }
        //else {
        //        concat.setFind(reflexivityRule(concat));
        //        e.setFind(symmetryRule(thm));
        //      }
      } 
      else 
        // Both e and concat have find pointers.  Just enqueue the equality.
        enqueueFact(thm);       
    }
  }
  TRACE_MSG("bv setup", "setupExpr => }");
}


void TheoryBitvector::update(const Theorem& e, const Expr& d) {
  // Constants should never change their find pointers to non-constant
  // expressions
  DebugAssert(e.getLHS().getOpKind()!=BVCONST || e.getRHS().getKind()==BVCONST,
              "TheoryBitvector::update(e="+e.getExpr().toString()
              +", d="+d.toString());
  if(!(*d_updateFlag)) return;

  IF_DEBUG(debugger.counter("bv update total")++);
  IF_DEBUG(if(d_sharedSubterms.count(d) > 0)
           debugger.counter("bv update shared")++);
  // Catch CONCAT updates: those are done using congruence closure
  if(d.getOpKind()==CONCAT) {
    updateCC(e, d);
    Theorem thm1 = updateHelper(d);
    if(constantKids(thm1.getRHS())){
      Theorem t1 = d_rules->concatConst(thm1.getRHS());
      t1 = transitivityRule(thm1,t1);
      Theorem t2 = find(d);
      t2 = symmetryRule(t2);
      t1 = transitivityRule(t2,t1);
      enqueueEquality(t1);
      //enqueueFact(t1);
    } 
    return;
  }
  Theorem thm = updateHelper(d);  // |- d = d'
  DebugAssert(thm.getRHS() != d,
              "TheoryBitvector::update(e,d):\n thm = "+thm.toString());
  // If find(d) == d, enqueue thm as a new equality directly.
  // Otherwise, enqueue thm as a fact (postpone its processing, and
  // process it later sequentially).  This is needed to guarantee the
  // internal invariants of assertEqualities().
  DebugAssert(d.hasFind(), "TheoryBitvector::update: d = "+d.toString());
  if(d.getFind().getRHS() == d) {
  // Rewrite the RHS to keep it fully simplified
    thm = transitivityRule(thm, rewriteAux(thm.getRHS()));
    TRACE("bv update", "TheoryBitvector::update[find(d)==d]: thm = ",
          thm.getExpr(), "");
    const Expr& rhs = thm.getRHS();
    if(d != rhs) {
      DebugAssert(find(rhs).getRHS() == rhs,
                  "TheoryBitvector::update(e,d):\n thm = "+thm.toString()
                  +"\n find(rhs) = "
                  +find(rhs).getRHS().toString()
                  +"\n e = "+e.getExpr().toString()
                  +"\n d = "+d.toString());
      // It may happen that in the same batch of equalities a
      // non-canonical d will simplify to the same rhs, in which case
      // we want to enqueue it as a fact rather than setting it up and
      // not reporting to the core.  To detect this situation, we
      // setup rhs immediately.
      if(!rhs.hasFind()) theoryCore()->setupTerm(rhs, this);
      enqueueEquality(thm);
      IF_DEBUG(debugger.counter("bv update equality")++);
    }
  } else if(d_staleDB.count(d) == 0) {
    if(constantKids(thm.getRHS()))
      thm = transitivityRule(thm, rewriteAux(thm.getRHS()));
    const Expr& rhs = thm.getRHS();
    TRACE("bv update", "TheoryBitvector::update[not stale]: thm = ",
          thm.getExpr(), "");
    if(rhs.hasFind() || rhs.getKind() == BVCONST) {
      IF_DEBUG(debugger.counter("bv update fact")++);
      enqueueFact(thm);
    } else {
      // Do not enqueue fact; instead, setup and assign the find
      // pointer "manually"
      Theorem rhsFindThm(transitivityRule(symmetryRule(thm), find(d)));
      TRACE("bv update", "TheoryBitvector::update[setup]:\n rhs find thm = ",
            rhsFindThm.getExpr(), "");
      IF_DEBUG(debugger.counter("bv update setup")++);
      theoryCore()->setupTerm(rhs, this);
      rhs.setFind(rhsFindThm);
    }
    d_staleDB[d] = true;
  } else {
    TRACE("bv update", "TheoryBitvector::update[stale] d = ", d, "");
    IF_DEBUG(debugger.counter("bv update stale")++);
  }
}


Theorem TheoryBitvector::solve(const Theorem& e)
{
  const Expr& lhs = e.getLHS();
  const Expr& rhs = e.getRHS();
  bool constLHS(lhs.getKind()==BVCONST);
  bool constRHS(rhs.getKind()==BVCONST);
  if(lhs != rhs) {
    if(constLHS && constRHS)
      return iffMP(e, d_rules->eqConst(e.getExpr()));
    else if(constLHS) // Put a constant on the RHS
      return symmetryRule(e);
  }
  // Otherwise don't do anything
  return e;
}


void TheoryBitvector::checkType(const Expr& e)
{
  switch (e.getOpKind()) {
    case BITVECTOR: 
      //TODO: check that this is a well-formed type
      break;
    default:
      DebugAssert(false, "Unexpected kind in TheoryBitvector::checkType"
                  +getEM()->getKindName(e.getOpKind()));
  }
}


void TheoryBitvector::computeType(const Expr& e)
{
  TRACE("bitvector", "TheoryBitvector::computeType(", e.toString(), ") {"); 
  switch(e.getOpKind()) {
  case BOOLEXTRACT: {
    if(!(1 == e.arity() &&
         BITVECTOR == getBaseType(e[0]).getExpr().getOpKind()))
      throw TypecheckException("Type Checking error:"\
                               "attempted extraction from non-bitvector \n"+ 
                               e.toString());
    int extractLength = getBoolExtractIndex(e);
    if(!(0 <= extractLength))
      throw TypecheckException("Type Checking error: \n"
                               "attempted out of range extraction  \n"+ 
                               e.toString());
    e.setType(boolType());
  }
    break;
  case BVCONST: {
    Type bvType = newBitvectorType(getBVConstSize(e));
    e.setType(bvType);
  }
    break;
  case CONCAT: {
    if(e.arity() < 2) 
      throw TypecheckException
        ("Concatenation must have at least 2 bit-vectors:\n\n  "+e.toString());

    // Compute the total length of concatenation
    int bvLength(0);
    for(int i=0, iend=e.arity(); i<iend; ++i) {
      if(BITVECTOR != getBaseType(e[i]).getExpr().getOpKind())
        throw TypecheckException
          ("Not a bit-vector expression (child #"+int2string(i+1)
           +") in concatenation:\n\n  "+e[i].toString()
           +"\n\nIn the expression:\n\n  "+e.toString());
      bvLength += BVSize(e[i]);
    }
    Type bvType = newBitvectorType(bvLength);
    e.setType(bvType);
    break;
  }
   case BVMULT:{
    if(!(2 == e.arity() &&
         BITVECTOR == getBaseType(e[0]).getExpr().getOpKind() &&
         BITVECTOR == getBaseType(e[1]).getExpr().getOpKind()))
      throw TypecheckException
        ("Not a bit-vector expression in BVMULT:\n\n  "
         +e.toString());
    int bvLen = getBVMultParam(e);
    Type bvType = newBitvectorType(bvLen);
    e.setType(bvType);
  }
    break;
  case BVUMINUS:{
    Type bvType(getBaseType(e[0]));
    if(!(1 == e.arity() &&
         BITVECTOR == bvType.getExpr().getOpKind()))
      throw TypecheckException
        ("Not a bit-vector expression in BVUMINUS:\n\n  "
         +e.toString());
    e.setType(bvType);
  }
    break;
  case EXTRACT:{
    if(!(1 == e.arity() && 
         BITVECTOR == getBaseType(e[0]).getExpr().getOpKind()))
      throw TypecheckException
        ("Not a bit-vector expression in bit-vector extraction:\n\n  "
         + e.toString());
    int bvLength = BVSize(e[0]);
    int leftExtract = getExtractHi(e);
    int rightExtract = getExtractLow(e);
    if(!(0 <= rightExtract && 
         rightExtract <= leftExtract && leftExtract < bvLength))
      throw TypecheckException
        ("Wrong bounds in bit-vector extract:\n\n  "+e.toString());
    int extractLength = leftExtract - rightExtract + 1;
    Type bvType = newBitvectorType(extractLength);
    e.setType(bvType);
    break;
  }
  case BVNEG:{
    if(!(1 == e.arity() && 
         BITVECTOR == getBaseType(e[0]).getExpr().getOpKind()))
      throw TypecheckException
        ("Not a bit-vector expression in bit-wise negation:\n\n  "
         + e.toString());
    e.setType(e[0].getType());
    break; 
  }
  case BVAND:
  case BVOR: {
    string kindStr((e.getOpKind()==BVAND)? "AND" : "OR");
    if(e.arity() < 2) 
      throw TypecheckException
        ("Bit-wise "+kindStr+" must have at least 2 bit-vectors:\n\n  "
         +e.toString());

    int bvLength(0);
    bool first(true);
    for(int i=0, iend=e.arity(); i<iend; ++i) {
      if(BITVECTOR != getBaseType(e[i]).getExpr().getOpKind())
        throw TypecheckException
          ("Not a bit-vector expression (child #"+int2string(i+1)
           +") in bit-wise "+kindStr+":\n\n  "+e[i].toString()
           +"\n\nIn the expression:\n\n  "+e.toString());
      if(first) {
        bvLength = BVSize(e[i]);
        first=false;
      } else { // Check that the size is the same for all subsequent BVs
        if(BVSize(e[i]) != bvLength)
          throw TypecheckException
            ("Mismatched bit-vector size in bit-wise "+kindStr+" (child #"
             +int2string(i)+").\nExpected type: "
             +newBitvectorType(bvLength).toString()
             +"\nFound: "+e[i].getType().toString()
             +"\nIn the following expression:\n\n  "+e.toString());
      }
    }
    e.setType(newBitvectorType(bvLength));
    break; 
  }
  case BVPLUS: {
    int bvPlusLength = getBVPlusParam(e);
    if(!(0 <= bvPlusLength))
      throw TypecheckException
        ("Bad bit-vector length specified in BVPLUS expression:\n\n  "
         + e.toString());
    for(Expr::iterator i=e.begin(), iend=e.end(); i != iend; ++i) {
      if(BITVECTOR != getBaseType(*i).getExpr().getOpKind())
        throw TypecheckException
          ("Not a bit-vector expression in BVPLUS:\n\n  "+e.toString());
    }
    Type bvType = newBitvectorType(bvPlusLength);
    e.setType(bvType);
    break;
  }
  case LEFTSHIFT: {
    if(!(1 == e.arity() && 
         BITVECTOR == getBaseType(e[0]).getExpr().getOpKind()))
      throw TypecheckException
        ("Not a bit-vector expression in bit-vector shift:\n\n  "
         +e.toString());
    int bvLength = BVSize(e[0]);
    int shiftLength = getFixedLeftShiftParam(e);
    if(!(shiftLength >= 0))
      throw TypecheckException("Bad shift value in bit-vector shift:\n\n  "
                               +e.toString());
    int newLength = bvLength + shiftLength;
    Type bvType = newBitvectorType(newLength);
    e.setType(bvType);
  }
    break;
  case RIGHTSHIFT: {
    if(!(1 == e.arity() && 
         BITVECTOR == getBaseType(e[0]).getExpr().getOpKind()))
      throw TypecheckException
        ("Not a bit-vector expression in bit-vector shift:\n\n  "
         +e.toString());
    int bvLength = BVSize(e[0]);
    int shiftLength = getFixedRightShiftParam(e);
    if(!(shiftLength >= 0))
      throw TypecheckException("Bad shift value in bit-vector shift:\n\n  "
                               +e.toString());
    //int newLength = bvLength + shiftLength;
    Type bvType = newBitvectorType(bvLength);
    e.setType(bvType);
  }
    break;
  case BVTYPEPRED:    
    e.setType(boolType());
    break;
  case SX: {
    if(!(1 == e.arity() &&
         BITVECTOR == getBaseType(e[0]).getExpr().getOpKind()))
      throw TypecheckException("Type Checking error:"\
                               "non-bitvector \n"+ e.toString());
    int bvLength = getSXIndex(e);
    if(!(0 <= bvLength))
      throw TypecheckException("Type Checking error: \n"
                               "out of range\n"+ e.toString());
    Type bvType = newBitvectorType(bvLength);
    e.setType(bvType);
    break;
  }
  case SBVLT:
  case SBVLE:
  case BVLT:
  case BVLE:
    if(!(2 == e.arity() &&
         BITVECTOR == getBaseType(e[0]).getExpr().getOpKind() &&
         BITVECTOR == getBaseType(e[1]).getExpr().getOpKind()))
      throw TypecheckException
        ("BVLT/BVLE expressions must have arity=2, and"
         "each subterm must be a bitvector term:\n"
         "e = " +e.toString());
    e.setType(boolType());
    break;
  default:
    DebugAssert(false,
                "TheoryBitvector::computeType: wrong input" +
                int2string(e.getOpKind()));
    break;
  }
  TRACE("bitvector", "TheoryBitvector::computeType => ", e.getType(), " }"); 
}


void TheoryBitvector::computeModelTerm(const Expr& e, std::vector<Expr>& v) {
  switch(e.getOpKind()) {
  case BVPLUS:
  case BVSUB:
  case BVUMINUS:
  case BVMULT:
  case LEFTSHIFT:
  case RIGHTSHIFT:
  case BVOR:
  case BVAND:
  case BVXOR:
  case BVXNOR:
  case BVNAND:
  case BVNOR:
  case BVNEG:
  case VARSHIFT:
  case CONCAT:
  case EXTRACT:
  case SBVLT:
  case SBVLE:
  case SBVGT:
  case SBVGE:
  case BVLT:
  case BVLE:
  case BVGT:
  case BVGE:
  case INTTOBV:
  case BVTOINT:
    for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i)
      // getModelTerm(*i, v);
      v.push_back(*i);
    return;
  case HEXBVCONST:
  case BVCONST: // No model variables here
    return;
  default: break; // It's a variable; continue processing
  }
  
  Type tp(e.getType());
  switch(tp.getExpr().getOpKind()) {
  case BITVECTOR: {
    int n = getBitvectorTypeParam(tp);
    for(int i=0; i<n; i = i+1)
      v.push_back(newBoolExtractExpr(e, i));
    break;
  }
  default:
    v.push_back(e);
  }
}


void TheoryBitvector::computeModel(const Expr& e, std::vector<Expr>& v) {
  switch(e.getOpKind()) {
  case BVPLUS:
  case BVSUB:
  case BVUMINUS:
  case BVMULT:
  case LEFTSHIFT:
  case RIGHTSHIFT:
  case BVOR:
  case BVAND:
  case BVXOR:
  case BVXNOR:
  case BVNAND:
  case BVNOR:
  case BVNEG:
  case VARSHIFT:
  case CONCAT:
  case EXTRACT:
  case SX:
  case SBVLT:
  case SBVLE:
  case SBVGT:
  case SBVGE:
  case BVLT:
  case BVLE:
  case BVGT:
  case BVGE:
  case INTTOBV:
  case BVTOINT: {
    // More primitive vars are kids, and they should have been
    // assigned concrete values
    assignValue(simplify(e));
    v.push_back(e);
    return;
  }
  case HEXBVCONST:
  case BVCONST: // No model variables here
    return;
  default: break; // It's a variable; continue processing
  }
  
  Type tp(e.getType());
  switch(tp.getExpr().getOpKind()) {
  case BITVECTOR: {
    const Rational& n = getBitvectorTypeParam(tp);
    vector<bool> bits;
    // FIXME: generate concrete assignment from bits using proof
    // rules. For now, just create a new assignment.
    for(int i=0; i<n; i++) {
      Theorem val(getModelValue(newBoolExtractExpr(e, i)));
      DebugAssert(val.getRHS().isBoolConst(), 
                  "TheoryBitvector::computeModel: unassigned bit: "
                  +val.getExpr().toString());
      bits.push_back(val.getRHS().isTrue());
    }
    Expr c(newBVConstExpr(bits));
    assignValue(e, c);
    v.push_back(e);
    break;
  }
  default:
    DebugAssert(false, "TheoryBitvector::computeModel[not BITVECTOR type]("
                +e.toString()+")");
  }
}


Expr
TheoryBitvector::computeTypePred(const Type& t, const Expr& e) {
  DebugAssert(t.getExpr().getOpKind() == BITVECTOR,
              "TheoryBitvector::computeTypePred: t = "+t.toString());
//   switch(e.getKind()) {
//   case BVCONST:
//     return getEM()->trueExpr();
//   default:
    return newBitvectorTypePred(t, e);
    //  }
}


Expr
TheoryBitvector::computeTCC(const Expr& e) {
  Expr tcc(Theory::computeTCC(e));
  switch(e.getOpKind()) {
  default:
    return tcc;
  }
}

///////////////////////////////////////////////////////////////////////////////
// Pretty-printing                                                           //
///////////////////////////////////////////////////////////////////////////////

ExprStream&
TheoryBitvector::print(ExprStream& os, const Expr& e) {
  switch(os.lang()) {
  case PRESENTATION_LANG:
    switch(e.getOpKind()) {
    case BVCONST: {
      std::ostringstream ss;
      ss << "0bin";
      for(int i=(int)getBVConstSize(e)-1; i>=0; --i)
        ss << (getBVConstValue(e, i) ? "1" : "0");
      os << ss.str();
      break;
    }
    case CONCAT:
      if(e.arity() <= 1) e.printAST(os);
      else {
        os << "(" << push;
        bool first(true);
        for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
          if(first) first=false;
          else os << space << "@" << space;
          os << (*i);
        }
        os << push << ")";
      }
      break;
    case BVUMINUS:
      os << "BVUMINUS(" << push << e[0] << push << ")";
      break;
    case BVSUB:
      break;
    case BVMULT:
      os << "BVMULT(" << push
         << getBVMultParam(e) << "," << e[0] << "," << e[1]<<push<<")"; 
      break;
    case BVAND:
      if(e.arity() <= 1) e.printAST(os);
      else {
        os << "(" << push;
        bool first(true);
        for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
          if(first) first=false;
          else os << space << "&" << space;
          os << (*i);
        }
        os << push << ")";
      }
      break;
    case BVOR:
      if(e.arity() <= 1) e.printAST(os);
      else {
        os << "(" << push;
        bool first(true);
        for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
          if(first) first=false;
          else os << space << "|" << space;
          os << (*i);
        }
        os << push << ")";
      }
      break;
    case BVNEG:
      os << "(~(" << push << e[0] << push << "))";
      break;
    case BVLT:
      os << "BVLT(" << push << e[0] << "," << e[1] << push << ")";
      break;
    case BVLE:
      os << "BVLE(" << push << e[0] << "," << e[1] << push << ")";
      break;
    case SBVLT:
      os << "SBVLT(" << push << e[0] << "," << e[1] << push << ")";
      break;
    case SBVLE:
      os << "SBVLE(" << push << e[0] << "," << e[1] << push << ")";
      break;
    case EXTRACT:
      os << "(" << push << e[0] << push << ")" << pop << pop
         << "[" << push << getExtractHi(e) << ":";
      os << getExtractLow(e) << push << "]";
      break;
    case BOOLEXTRACT:
      os << "BOOLEXTRACT(" << push  << e[0] << "," 
         << getBoolExtractIndex(e) << push << ")";
      break;
    case SX:
      os << "SX(" << push  << e[0] << "," 
         << push <<  getSXIndex(e) << ")";
      break;
    case LEFTSHIFT:
      os <<  "(" << push << e[0] << space << "<<" << space
         << getFixedLeftShiftParam(e) << push << ")";
      break;
    case RIGHTSHIFT:
      os <<  "(" << push << e[0] << space << ">>" << space
         << getFixedRightShiftParam(e) << push << ")";
      break;
    case BITVECTOR: //printing type expression
      os << "BITVECTOR(" << push
         << getBitvectorTypeParam(e) << push << ")";
      break;
    case INTTOBV:
      break;
    case BVTOINT:
      break;
    case BVPLUS:
      os << "BVPLUS(" << push << getBVPlusParam(e);
      for(Expr::iterator i=e.begin(), iend=e.end(); i!=iend; ++i) {
        os << push << "," << pop << space << (*i);
      }
      os << push << ")";
      break;
    case BVTYPEPRED:
      if(e.isApply()) {
        os << "BVTYPEPRED[" << push << e.getOp().getExpr()
           << push << "," << pop << space << e[0]
           << push << "]";
      } else
        e.printAST(os);
      break;
    default:
      e.printAST(os);
      break;
    }
    break;
  case SMTLIB_LANG:
    d_theoryUsed = true;
    throw SmtlibException("TheoryBitvector::print: SMTLIB not supported");
    break;
  default:
    switch(e.getOpKind()) {
    case BVCONST: {
      os << "0bin";
      for(int i=(int)getBVConstSize(e)-1; i>=0; --i)
        os << (getBVConstValue(e, i) ? "1" : "0");
      break;
    }
    default:
      e.printAST(os);
      break;
    }
  }
  return os;
}


///////////////////////////////////////////////////////////////////////////////
//parseExprOp:
//translating special Exprs to regular EXPR??
///////////////////////////////////////////////////////////////////////////////
Expr
TheoryBitvector::parseExprOp(const Expr& e) {
  TRACE("parser", "TheoryBitvector::parseExprOp(", e, ")");
  
  // If the expression is not a list, it must have been already
  // parsed, so just return it as is.
  if(RAW_LIST != e.getKind()) return e;

  if(!(e.arity() > 0))      
    throw ParserException("TheoryBitvector::parseExprOp: wrong input:\n\n"
                          +e.toString());
  
  const Expr& c1 = e[0][0];
  int kind = getEM()->getKind(c1.getString());
  switch(kind) {
  case BITVECTOR:
    if(!(e.arity() == 2))
      throw ParserException("TheoryBitvector::parseExprOp: BITVECTOR" 
                            "kind should have exactly 1 arg:\n\n" 
                            + e.toString());    
    if(!(e[1].isRational() && e[1].getRational().isInteger()))
      throw ParserException("BITVECTOR TYPE must have an integer constant" 
                            "as its first argument:\n\n"
                            +e.toString());    
    if(!(e[1].getRational().getInt() >=0 ))
      throw ParserException("parameter must be an integer constant >= 0.\n"
                            +e.toString());    
    return newBitvectorTypeExpr(e[1].getRational().getInt());
    break;
  case CONCAT: {
    if(!(e.arity() >= 3))
      throw ParserException("TheoryBitvector::parseExprOp: CONCAT" 
                            "kind should have at least 2 args:\n\n" 
                            + e.toString());
    vector<Expr> kids;
    Expr::iterator i=e.begin(), iend=e.end();
    DebugAssert(i!=iend, "TheoryBitvector::parseExprOp("+e.toString()+")");
    ++i; // Skip the first element - the operator name
    for(; i!=iend; ++i)
      kids.push_back(parseExpr(*i));
    return newConcatExpr(kids);
    break;
  }
  case BVAND: {
    if(!(e.arity() >= 3))
      throw ParserException("TheoryBitvector::parseExprOp: BVAND " 
                            "kind should have at least 2 arg:\n\n" 
                            + e.toString());
    vector<Expr> kids;
    for(int i=1, iend=e.arity(); i<iend; ++i)
      kids.push_back(parseExpr(e[i]));
    return newBVAndExpr(kids);
    break;
  }
  case BVOR: {
    if(!(e.arity() >= 3))
      throw ParserException("TheoryBitvector::parseExprOp: BVOR " 
                            "kind should have at least 2 arg:\n\n" 
                            + e.toString());
    vector<Expr> kids;
    for(int i=1, iend=e.arity(); i<iend; ++i)
      kids.push_back(parseExpr(e[i]));
    return newBVOrExpr(kids);
    break;
  }
  case BVXOR: {
    if(!(e.arity() == 3))
      throw ParserException("TheoryBitvector::parseExprOp: BVXOR " 
                            "kind should have exactly 2 arg:\n\n" 
                            + e.toString());
//     Expr e1 = parseExpr(e[1]);
//     Expr e2 = parseExpr(e[2]);
//     return newBVXorExpr(e1,e2);
    Expr or1 = 
      newBVAndExpr(newBVNegExpr(parseExpr(e[1])), parseExpr(e[2]));
    or1 = rewriteBV(or1,3).getRHS();
    Expr or2 = 
      newBVAndExpr(parseExpr(e[1]), newBVNegExpr(parseExpr(e[2])));
    or2 = rewriteBV(or2,3).getRHS();
    return rewrite(newBVOrExpr(or1, or2)).getRHS();
    break;
  }
  case BVXNOR: {
    if(!(e.arity() == 3))
      throw ParserException("TheoryBitvector::parseExprOp: BVXNOR" 
                            "kind should have exactly 2 arg:\n\n" 
                            + e.toString());    
//     Expr e1 = parseExpr(e[1]);
//     Expr e2 = parseExpr(e[2]);
//     return newBVXorExpr(e1,e2).notExpr();
    Expr or1 = 
      newBVAndExpr(newBVNegExpr(parseExpr(e[1])), 
                   newBVNegExpr(parseExpr(e[2])));
    Expr or2 = newBVAndExpr(parseExpr(e[1]), parseExpr(e[2]));
    return newBVOrExpr(or1, or2);
    break;
  }
  case BVNAND:
    if(!(e.arity() == 3))
      throw ParserException("TheoryBitvector::parseExprOp: BVNAND" 
                            "kind should have exactly 2 arg:\n\n" 
                            + e.toString());    
    return newBVNegExpr(newBVAndExpr(parseExpr(e[1]),parseExpr(e[2])));
    break;
  case BVNOR:
    if(!(e.arity() == 3))
      throw ParserException("TheoryBitvector::parseExprOp: BVNOR" 
                            "kind should have exactly 2 arg:\n\n" 
                            + e.toString());
    return newBVNegExpr(newBVOrExpr(parseExpr(e[1]),parseExpr(e[2])));    
    break;
  case BVLT:
    if(!(e.arity() == 3))
      throw ParserException("TheoryBitvector::parseExprOp: BVLT" 
                            "kind should have exactly 2 arg:\n\n" 
                            + e.toString());
    return newBVLTExpr(parseExpr(e[1]),parseExpr(e[2]));    
    break;
  case BVLE:
    if(!(e.arity() == 3))
      throw ParserException("TheoryBitvector::parseExprOp: BVLE" 
                            "kind should have exactly 2 arg:\n\n" 
                            + e.toString());
    return newBVLEExpr(parseExpr(e[1]),parseExpr(e[2]));    
    break;
  case BVGT:
    if(!(e.arity() == 3))
      throw ParserException("TheoryBitvector::parseExprOp: BVGT" 
                            "kind should have exactly 2 arg:\n\n" 
                            + e.toString());
    return newBVLTExpr(parseExpr(e[2]),parseExpr(e[1]));    
    break;
  case BVGE:
    if(!(e.arity() == 3))
      throw ParserException("TheoryBitvector::parseExprOp: BVGE" 
                            "kind should have exactly 2 arg:\n\n" 
                            + e.toString());
    return newBVLEExpr(parseExpr(e[2]),parseExpr(e[1]));    
    break;
  case SX:
    if(!(e.arity() == 3))
      throw ParserException("TheoryBitvector::parseExprOp: SX" 
                            "kind should have exactly 2 arg:\n\n" 
                            + e.toString());    
    if(!e[2].isRational() || !e[2].getRational().isInteger())
      throw ParserException("SX must have an integer constant as its"
                            " 2nd argument:\n\n"
                            +e.toString());    
    if(!(e[2].getRational().getInt() >=0 ))
      throw ParserException("SX must have an integer constant as its"
                            " 2nd argument >= 0:\n\n"
                            +e.toString());    
    return newSXExpr(parseExpr(e[1]), e[2].getRational().getInt());
    break;
  case SBVLT:
    if(!(e.arity() == 3))
      throw ParserException("TheoryBitvector::parseExprOp: BVLT" 
                            "kind should have exactly 2 arg:\n\n" 
                            + e.toString());
    return newSBVLTExpr(parseExpr(e[1]),parseExpr(e[2]));    
    break;
  case SBVLE:
    if(!(e.arity() == 3))
      throw ParserException("TheoryBitvector::parseExprOp: BVLE" 
                            "kind should have exactly 2 arg:\n\n" 
                            + e.toString());
    return newSBVLEExpr(parseExpr(e[1]),parseExpr(e[2]));    
    break;
  case SBVGT:
    if(!(e.arity() == 3))
      throw ParserException("TheoryBitvector::parseExprOp: BVGT" 
                            "kind should have exactly 2 arg:\n\n" 
                            + e.toString());
    return newSBVLTExpr(parseExpr(e[2]),parseExpr(e[1]));    
    break;
  case SBVGE:
    if(!(e.arity() == 3))
      throw ParserException("TheoryBitvector::parseExprOp: BVGE" 
                            "kind should have exactly 2 arg:\n\n" 
                            + e.toString());
    return newSBVLEExpr(parseExpr(e[2]),parseExpr(e[1]));    
    break;
  case BVNEG:
    if(!(e.arity() == 2))
      throw ParserException("TheoryBitvector::parseExprOp: BVNEG" 
                            "kind should have exactly 1 arg:\n\n" 
                            + e.toString());    
    return newBVNegExpr(parseExpr(e[1]));
    break;
  case BVCONST:
    if(!(e.arity() == 2 || e.arity() == 3))
      throw ParserException("TheoryBitvector::parseExprOp: BVCONST "
                            "kind should have 1 or 2 args:\n\n"
                            + e.toString());
    if(!(e[1].isRational() || e[1].isString()))
      throw ParserException("TheoryBitvector::parseExprOp: BVCONST "
                            "kind should have arg of type Rational "
                            "or String:\n\n" + e.toString());
    if(e[1].isRational()) { // ("BVCONST" value [bitwidth])
      if(e.arity()==3) {
        if(!e[2].isRational() || !e[2].getRational().isInteger())
          throw ParserException("TheoryBitvector::parseExprOp: BVCONST "
                                "2nd argument must be an integer:\n\n"
                                +e.toString());
        return newBVConstExpr(e[1].getRational(), e[2].getRational().getInt());
      } else
        return newBVConstExpr(e[1].getRational());
    } else if(e[1].isString()) { // ("BVCONST" string [base])
      if(e.arity() == 3) {
        if(!e[2].isRational() || !e[2].getRational().isInteger())
          throw ParserException("TheoryBitvector::parseExprOp: BVCONST "
                                "2nd argument must be an integer:\n\n"
                                +e.toString());
        return newBVConstExpr(e[1].getString(), e[2].getRational().getInt());
      } else
        return newBVConstExpr(e[1].getString());
    }
    break;
  case HEXBVCONST:
    if(!(e.arity() == 2))
      throw ParserException("TheoryBitvector::parseExprOp: BVCONST" 
                            "kind should have exactly 1 arg:\n\n" 
                            + e.toString());    
    if(!(e[1].isRational() || e[1].isString()))
      throw ParserException("TheoryBitvector::parseExprOp: BVCONST" 
                            "kind should have arg of type Rational" 
                            "or String:\n\n" + e.toString());    
    if(e[1].isRational()) 
      return newBVConstExpr(e[1].getRational());
    if(e[1].isString())
      return newBVConstExpr(e[1].getString(),16);
    break;
  case LEFTSHIFT:
    if(!(e.arity() == 3))
      throw ParserException("TheoryBitvector::parseExprOp: LEFTSHIFT" 
                            "kind should have exactly 2 arg:\n\n" 
                            + e.toString());    
    if(!e[2].isRational() || !e[2].getRational().isInteger())
      throw ParserException("LEFTSHIFT must have an integer constant as its "
                            "2nd argument:\n\n"
                            +e.toString());    
    if(!(e[2].getRational().getInt() >=0 ))
      throw ParserException("parameter must be an integer constant >= 0.\n"
                            +e.toString());    
    return newFixedLeftShiftExpr(parseExpr(e[1]), e[2].getRational().getInt());
    break;
  case RIGHTSHIFT:
    if(!(e.arity() == 3))
      throw ParserException("TheoryBitvector::parseExprOp: RIGHTSHIFT" 
                            "kind should have exactly 2 arg:\n\n" 
                            + e.toString());    
    if(!e[2].isRational() || !e[2].getRational().isInteger())
      throw ParserException("RIGHTSHIFT must have an integer constant as its "
                            "2nd argument:\n\n"
                            +e.toString());    
    if(!(e[2].getRational().getInt() >=0 ))
      throw ParserException("parameter must be an integer constant >= 0.\n"
                            +e.toString());    
    return newFixedRightShiftExpr(parseExpr(e[1]), e[2].getRational().getInt());
    break;
  case BOOLEXTRACT:
    if(!(e.arity() == 3))
      throw ParserException("TheoryBitvector::parseExprOp: BOOLEXTRACT" 
                            "kind should have exactly 2 arg:\n\n" 
                            + e.toString());    
    if(!e[2].isRational() || !e[2].getRational().isInteger())
      throw ParserException("BOOLEXTRACT must have an integer constant as its"
                            " 2nd argument:\n\n"
                            +e.toString());    
    if(!(e[2].getRational().getInt() >=0 ))
      throw ParserException("parameter must be an integer constant >= 0.\n"
                            +e.toString());    
    return newBoolExtractExpr(parseExpr(e[1]), e[2].getRational().getInt());
    break;
  case EXTRACT:
    if(!(e.arity() == 4))
      throw ParserException("TheoryBitvector::parseExprOp: EXTRACT" 
                            "kind should have exactly 3 arg:\n\n" 
                            + e.toString());    
    if(!e[2].isRational() || !e[2].getRational().isInteger())
      throw ParserException("EXTRACT must have an integer constant as its "
                            "2nd argument:\n\n"
                            +e.toString());    
    if(!e[3].isRational() || !e[3].getRational().isInteger())
      throw ParserException("EXTRACT must have an integer constant as its "
                            "3nd argument:\n\n"
                            +e.toString());    
    if(!(e[2].getRational().getInt() >=0 && e[3].getRational().getInt() >=0))
      throw ParserException("parameter must be an integer constant >= 0.\n"
                            +e.toString());    
    return newBVExtractExpr(parseExpr(e[1]), 
                            e[2].getRational().getInt(), 
                            e[3].getRational().getInt());
    break;
  case BVSUB: {
    if(e.arity() != 4)
      throw ParserException("BVSUB must have 3 arguments:\n\n"
                            +e.toString());
    if(!e[1].isRational() || !e[1].getRational().isInteger())
      throw ParserException("BVSUB must have an integer constant as its "
                            "first argument:\n\n"
                            +e.toString());
    if(!(e[1].getRational().getInt() >=0))
      throw ParserException("parameter must be an integer constant >= 0.\n"
                            +e.toString());    
    int bvsublength = e[1].getRational().getInt();
    std::vector<Expr> k;
    Expr summand1 = parseExpr(e[2]);
    summand1 = pad(bvsublength, summand1);
    k.push_back(summand1);    
    Expr summand2 = parseExpr(e[3]);
    summand2 = pad(bvsublength, summand2);
    Expr bvuminus = newBVUminusExpr(summand2);
    k.push_back(bvuminus);
    return newBVPlusExpr(bvsublength, k);
  }
    break;
  case BVUMINUS:
    if(!(e.arity() == 2))
      throw ParserException("TheoryBitvector::parseExprOp: BVUMINUS" 
                            "kind should have exactly 1 arg:\n\n" 
                            + e.toString());    
    return newBVUminusExpr(parseExpr(e[1]));
    break;
  case BVPLUS: {
    vector<Expr> k;
    Expr::iterator i = e.begin(), iend=e.end();
    if(!(e.arity() >= 4))
      throw ParserException("BVPLUS must have at least 3 args:\n\n"
                            +e.toString());
    if(!e[1].isRational() || !e[1].getRational().isInteger())
      throw ParserException
        ("BVPLUS must have an integer constant as its first argument:\n\n"
         +e.toString());
    if(!(e[1].getRational().getInt() >=0))
      throw ParserException("parameter must be an integer constant >= 0.\n"
                            +e.toString());    
    // Skip first two elements of the vector of kids in 'e'.
    // The first element is the kind, and the second is the
    // numOfBits of the bvplus operator.
    ++i;++i; 
    // Parse the kids of e and push them into the vector 'k'
    for(; i!=iend; ++i) k.push_back(parseExpr(*i));
    return newBVPlusExpr(e[1].getRational().getInt(), k);
  }
    break;
  case BVMULT:
    if(!(e.arity() == 4))
      throw ParserException("TheoryBitvector::parseExprOp: BVMULT" 
                            "kind should have exactly 3 arg:\n\n" 
                            + e.toString());    
    if(!e[1].isRational() || !e[1].getRational().isInteger())
      throw ParserException("BVMULT must have an integer constant" 
                            "as its first argument:\n\n"
                            +e.toString());
    if(!(e[1].getRational().getInt() >=0))
      throw ParserException("parameter must be an integer constant >= 0.\n"
                            +e.toString());        
    return newBVMultExpr(e[1].getRational().getInt(), 
                         parseExpr(e[2]), parseExpr(e[3]));
    break;
  default:
    DebugAssert(false,
                "TheoryBitvector::parseExprOp: input must be either"\
                "not be a bitvector:" + int2string(e.getKind()));
    break;
  }
  return e;
}


///////////////////////////////////////////////////////////////////////////////
//helper functions
///////////////////////////////////////////////////////////////////////////////
Expr TheoryBitvector::newBitvectorTypeExpr(int bvLength) {
  DebugAssert(bvLength > 0,
              "TheoryBitvector::newBitvectorTypeExpr:\n"
              "len of a BV must be a positive integer:\n bvlength = "+
              int2string(bvLength));
  return Expr(BITVECTOR, getEM()->newRatExpr(bvLength));
}

Expr TheoryBitvector::newBitvectorTypePred(const Type& t, const Expr& e) {
  return Expr(Expr(BVTYPEPRED, t.getExpr()).mkOp(), e);
}


Expr TheoryBitvector::newBVAndExpr(const Expr& t1, const Expr& t2) {
  DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind() &&
              BITVECTOR == t2.getType().getExpr().getOpKind(),
              "TheoryBitvector::newBVAndExpr:"
              "inputs must have type BITVECTOR:\n t1 = " +
              t1.toString() + "\n t2 = " +t2.toString());
  DebugAssert(BVSize(t1) == BVSize(t2),
              "TheoryBitvector::bitwise operator"
              "inputs must have same length:\n t1 = " + t1.toString()
              + "\n t2 = " + t2.toString());
  return Expr(CVCL::BVAND, t1, t2);
}

Expr TheoryBitvector::newBVAndExpr(const vector<Expr>& kids) {
  DebugAssert(kids.size() >= 2,
              "TheoryBitvector::newBVAndExpr:"
              "# of subterms must be at least 2");
  for(unsigned int i=0; i<kids.size(); ++i) {
    DebugAssert(BITVECTOR == kids[i].getType().getExpr().getOpKind(),
                "TheoryBitvector::newBVAndExpr:"
                "inputs must have type BITVECTOR:\n t1 = " +
                kids[i].toString());
    if(i < kids.size()-1) {
      DebugAssert(BVSize(kids[i]) == BVSize(kids[i+1]),
                  "TheoryBitvector::bitwise operator"
                  "inputs must have same length:\n t1 = " + kids[i].toString()
                  + "\n t2 = " + kids[i+1].toString());
    }
  }
  return Expr(CVCL::BVAND, kids, getEM());
}

Expr TheoryBitvector::newBVOrExpr(const Expr& t1, const Expr& t2) {
  DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind() &&
              BITVECTOR == t2.getType().getExpr().getOpKind(),
              "TheoryBitvector::newBVOrExpr: "
              "inputs must have type BITVECTOR:\n t1 = " +
              t1.toString() + "\n t2 = " +t2.toString());
  DebugAssert(BVSize(t1) == BVSize(t2),
              "TheoryBitvector::bitwise OR operator: "
              "inputs must have same length:\n t1 = " + t1.toString()
              + "\n t2 = " + t2.toString());
  return Expr(CVCL::BVOR, t1, t2);
}

Expr TheoryBitvector::newBVOrExpr(const vector<Expr>& kids) {
  DebugAssert(kids.size() >= 2,
              "TheoryBitvector::newBVOrExpr: "
              "# of subterms must be at least 2");
  for(unsigned int i=0; i<kids.size(); ++i) {
    DebugAssert(BITVECTOR == kids[i].getType().getExpr().getOpKind(),
                "TheoryBitvector::newBVOrExpr: "
                "inputs must have type BITVECTOR:\n t1 = " +
                kids[i].toString());
    if(i < kids.size()-1) {
      DebugAssert(BVSize(kids[i]) == BVSize(kids[i+1]),
                  "TheoryBitvector::bitwise operator"
                  "inputs must have same length:\n t1 = " + kids[i].toString()
                  + "\n t2 = " + kids[i+1].toString());
    }
  }
  return Expr(CVCL::BVOR, kids, getEM());
}


Expr TheoryBitvector::newBVNandExpr(const Expr& t1, const Expr& t2) {
  DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind() &&
              BITVECTOR == t2.getType().getExpr().getOpKind(),
              "TheoryBitvector::newBVNandExpr:"
              "inputs must have type BITVECTOR:\n t1 = " +
              t1.toString() + "\n t2 = " +t2.toString());
  DebugAssert(BVSize(t1) == BVSize(t2),
              "TheoryBitvector::bitwise operator"
              "inputs must have same length:\n t1 = " + t1.toString()
              + "\n t2 = " + t2.toString());
  return Expr(CVCL::BVNAND, t1, t2);
}

Expr TheoryBitvector::newBVNandExpr(const vector<Expr>& kids) {
  DebugAssert(kids.size() >= 2,
              "TheoryBitvector::newBVNandExpr:"
              "# of subterms must be at least 2");
  for(unsigned int i=0; i<kids.size(); ++i) {
    DebugAssert(BITVECTOR == kids[i].getType().getExpr().getOpKind(),
                "TheoryBitvector::newBVNandExpr:"
                "inputs must have type BITVECTOR:\n t1 = " +
                kids[i].toString());
    if(i < kids.size()-1) {
      DebugAssert(BVSize(kids[i]) == BVSize(kids[i+1]),
                  "TheoryBitvector::bitwise operator"
                  "inputs must have same length:\n t1 = " + kids[i].toString()
                  + "\n t2 = " + kids[i+1].toString());
    }
  }
  return Expr(CVCL::BVNAND, kids, getEM());
}

Expr TheoryBitvector::newBVNorExpr(const Expr& t1, const Expr& t2) {
  DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind() &&
              BITVECTOR == t2.getType().getExpr().getOpKind(),
              "TheoryBitvector::newBVNorExpr:"
              "inputs must have type BITVECTOR:\n t1 = " +
              t1.toString() + "\n t2 = " +t2.toString());
  DebugAssert(BVSize(t1) == BVSize(t2),
              "TheoryBitvector::bitwise operator"
              "inputs must have same length:\n t1 = " + t1.toString()
              + "\n t2 = " + t2.toString());
  return Expr(CVCL::BVNOR, t1, t2);
}

Expr TheoryBitvector::newBVNorExpr(const vector<Expr>& kids) {
  DebugAssert(kids.size() >= 2,
              "TheoryBitvector::newBVNorExpr:"
              "# of subterms must be at least 2");
  for(unsigned int i=0; i<kids.size(); ++i) {
    DebugAssert(BITVECTOR == kids[i].getType().getExpr().getOpKind(),
                "TheoryBitvector::newBVNorExpr:"
                "inputs must have type BITVECTOR:\n t1 = " +
                kids[i].toString());
    if(i < kids.size()-1) {
      DebugAssert( BVSize(kids[i]) ==  BVSize(kids[i+1]),
                  "TheoryBitvector::bitwise operator"
                  "inputs must have same length:\n t1 = " + kids[i].toString()
                  + "\n t2 = " + kids[i+1].toString());
    }
  }
  return Expr(CVCL::BVNOR, kids, getEM());
}

Expr TheoryBitvector::newBVXorExpr(const Expr& t1, const Expr& t2) {
  DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind() &&
              BITVECTOR == t2.getType().getExpr().getOpKind(),
              "TheoryBitvector::newBVXorExpr:"
              "inputs must have type BITVECTOR:\n t1 = " +
              t1.toString() + "\n t2 = " +t2.toString());
  DebugAssert(BVSize(t1) == BVSize(t2),
              "TheoryBitvector::bitwise operator"
              "inputs must have same length:\n t1 = " + t1.toString()
              + "\n t2 = " + t2.toString());
  return Expr(CVCL::BVXOR, t1, t2);
}

Expr TheoryBitvector::newBVXorExpr(const vector<Expr>& kids) {
  DebugAssert(kids.size() >= 2,
              "TheoryBitvector::newBVXorExpr:"
              "# of subterms must be at least 2");
  for(unsigned int i=0; i<kids.size(); ++i) {
    DebugAssert(BITVECTOR == kids[i].getType().getExpr().getOpKind(),
                "TheoryBitvector::newBVXorExpr:"
                "inputs must have type BITVECTOR:\n t1 = " +
                kids[i].toString());
    if(i < kids.size()-1) {
      DebugAssert(BVSize(kids[i]) ==  BVSize(kids[i+1]),
                  "TheoryBitvector::bitwise operator"
                  "inputs must have same length:\n t1 = " + kids[i].toString()
                  + "\n t2 = " + kids[i+1].toString());
    }
  }
  return Expr(CVCL::BVXOR, kids, getEM());
}

Expr TheoryBitvector::newBVXnorExpr(const Expr& t1, const Expr& t2) {
  DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind() &&
              BITVECTOR == t2.getType().getExpr().getOpKind(),
              "TheoryBitvector::newBVXnorExpr:"
              "inputs must have type BITVECTOR:\n t1 = " +
              t1.toString() + "\n t2 = " +t2.toString());
  DebugAssert(BVSize(t1) == BVSize(t2),
              "TheoryBitvector::bitwise operator"
              "inputs must have same length:\n t1 = " + t1.toString()
              + "\n t2 = " + t2.toString());
  return Expr(CVCL::BVXNOR, t1, t2);
}
 
Expr TheoryBitvector::newBVXnorExpr(const vector<Expr>& kids) {
  DebugAssert(kids.size() >= 2,
              "TheoryBitvector::newBVXnorExpr:"
              "# of subterms must be at least 2");
  for(unsigned int i=0; i<kids.size(); ++i) {
    DebugAssert(BITVECTOR == kids[i].getType().getExpr().getOpKind(),
                "TheoryBitvector::newBVXnorExpr:"
                "inputs must have type BITVECTOR:\n t1 = " +
                kids[i].toString());
    if(i < kids.size()-1) {
      DebugAssert(BVSize(kids[i]) == BVSize(kids[i+1]),
                  "TheoryBitvector::bitwise operator"
                  "inputs must have same length:\n t1 = " + kids[i].toString()
                  + "\n t2 = " + kids[i+1].toString());
    }
  }
  return Expr(CVCL::BVXNOR, kids, getEM());
}

Expr TheoryBitvector::newBVLTExpr(const Expr& t1, const Expr& t2) {
  DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind() &&
              BITVECTOR == t2.getType().getExpr().getOpKind(),
              "TheoryBitvector::newBVLTExpr:"
              "inputs must have type BITVECTOR:\n t1 = " +
              t1.toString() + "\n t2 = " +t2.toString());
  return Expr(CVCL::BVLT, t1, t2);
}

Expr TheoryBitvector::newBVLEExpr(const Expr& t1, const Expr& t2) {
  DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind() &&
              BITVECTOR == t2.getType().getExpr().getOpKind(),
              "TheoryBitvector::newBVLEExpr:"
              "inputs must have type BITVECTOR:\n t1 = " +
              t1.toString() + "\n t2 = " +t2.toString());
  return Expr(CVCL::BVLE, t1, t2);
}

Expr TheoryBitvector::newSXExpr(const Expr& t1, int len) {
  DebugAssert(len >=0,
              " TheoryBitvector::newSXExpr:" 
              "SX index must be a non-negative integer"+
              int2string(len));
  DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind(),
              "TheoryBitvector::newBVFixedleftshiftExpr:"
              "inputs must have type BITVECTOR:\n t1 = " +
              t1.toString());
  if(len==0) return t1;
  return Expr(Expr(SX, getEM()->newRatExpr(len)).mkOp(), t1);
}

Expr TheoryBitvector::newSBVLTExpr(const Expr& t1, const Expr& t2) {
  DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind() &&
              BITVECTOR == t2.getType().getExpr().getOpKind(),
              "TheoryBitvector::newSBVLTExpr:"
              "inputs must have type BITVECTOR:\n t1 = " +
              t1.toString() + "\n t2 = " +t2.toString());
  return Expr(CVCL::SBVLT, t1, t2);
}

Expr TheoryBitvector::newSBVLEExpr(const Expr& t1, const Expr& t2) {
  DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind() &&
              BITVECTOR == t2.getType().getExpr().getOpKind(),
              "TheoryBitvector::newSBVLEExpr:"
              "inputs must have type BITVECTOR:\n t1 = " +
              t1.toString() + "\n t2 = " +t2.toString());
  return Expr(CVCL::SBVLE, t1, t2);
}

Expr TheoryBitvector::newBVNegExpr(const Expr& t1) {
  DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind(),
              "TheoryBitvector::newBVNegExpr:"
              "inputs must have type BITVECTOR:\n t1 = " +
              t1.toString());
  return Expr(CVCL::BVNEG, t1);
}


Expr TheoryBitvector::newBVUminusExpr(const Expr& t1) {
  DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind(),
              "TheoryBitvector::newBVNegExpr:"
              "inputs must have type BITVECTOR:\n t1 = " +
              t1.toString());
  return Expr(CVCL::BVUMINUS, t1);
}

Expr TheoryBitvector::newBoolExtractExpr(const Expr& t1, int index) {
  DebugAssert(index >=0,
              " TheoryBitvector::newBoolExtractExpr:" 
              "bool_extract index must be a non-negative integer"+
              int2string(index));
  DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind(),
              "TheoryBitvector::newBVBoolExtractExpr:"
              "inputs must have type BITVECTOR:\n t1 = " +
              t1.toString());
//   if(*d_boolExtractCacheFlag && isLeaf(t1)) {
//     std::vector<Expr> bits = d_boolExtractCache[t1];
//     int bitsSize = bits.size();
//     if(bitsSize < index+1) {
//       //if bits is empty then populate with empty Expr
//       for(int i=bitsSize;i < index+1; ++i)
//      bits.push_back(Expr());
//       //now put boolextract(t1,index) in bits[index]
//       BVParameterExpr 
//      bv(getEM(), t1, index, d_bvParameterExprIndex, CVCL::BOOLEXTRACT);
//       bits[index] = Expr(&bv);
//     } else {
//       if(bits[index].isNull()) {
//      BVParameterExpr 
//        bv(getEM(), t1, index, d_bvParameterExprIndex, CVCL::BOOLEXTRACT);
//      bits[index] = Expr(&bv);
//       } else {
//      IF_DEBUG(const Expr e = bits[index]);
//      DebugAssert(BOOLEXTRACT == e.getOpKind() &&
//                  t1 == e[0] &&
//                  index == getBoolExtractIndex(e),
//                  "TheoryBitvector::newBoolExtractExpr:"
//                  "the d_boolExtractCache has the wrong bool extract:\n"
//                  "e = " + e.toString());
//       }
//     }
//     return bits[index];
//   } else {
  return Expr(Expr(BOOLEXTRACT, getEM()->newRatExpr(index)).mkOp(), t1);
}

Expr TheoryBitvector::newFixedLeftShiftExpr(const Expr& t1, int shiftLength) {
  DebugAssert(shiftLength >=0,
              " TheoryBitvector::newFixedleftshift:" 
              "fixed_shift index must be a non-negative integer"+
              int2string(shiftLength));
  DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind(),
              "TheoryBitvector::newBVFixedleftshiftExpr:"
              "inputs must have type BITVECTOR:\n t1 = " +
              t1.toString());
  if(shiftLength==0) return t1;
  return Expr(Expr(LEFTSHIFT, getEM()->newRatExpr(shiftLength)).mkOp(), t1);
}

Expr TheoryBitvector::newFixedRightShiftExpr(const Expr& t1, int shiftLength) {
  DebugAssert(shiftLength >=0,
              " TheoryBitvector::newFixedleftshift:" 
              "fixed_shift index must be a non-negative integer"+
              int2string(shiftLength));
  DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind(),
              "TheoryBitvector::newBVFixedleftshiftExpr:"
              "inputs must have type BITVECTOR:\n t1 = " +
              t1.toString());
  if(shiftLength==0) return t1;
  return Expr(Expr(RIGHTSHIFT, getEM()->newRatExpr(shiftLength)).mkOp(), t1);
}

Expr TheoryBitvector::newConcatExpr(const Expr& t1, const Expr& t2) {
  DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind() &&
              BITVECTOR == t2.getType().getExpr().getOpKind(),
              "TheoryBitvector::newBVConcatExpr:"
              "inputs must have type BITVECTOR:\n t1 = " +
              t1.toString() + "\n t2 = " +t2.toString());
  return Expr(CONCAT, t1, t2);
}

Expr TheoryBitvector::newConcatExpr(const Expr& t1, const Expr& t2,
                                    const Expr& t3) {
  DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind() &&
              BITVECTOR == t2.getType().getExpr().getOpKind() &&
              BITVECTOR == t3.getType().getExpr().getOpKind(),
              "TheoryBitvector::newBVConcatExpr:"
              "inputs must have type BITVECTOR:\n t1 = " +
              t1.toString() + 
              "\n t2 = " +t2.toString() + 
              "\n t3 =" + t3.toString());
  return Expr(CONCAT, t1, t2, t3);
}

Expr TheoryBitvector::newConcatExpr(const vector<Expr>& kids) {
  DebugAssert(kids.size() >= 2,
              "TheoryBitvector::newBVConcatExpr:"
              "# of subterms must be at least 2");
  for(unsigned int i=0; i<kids.size(); ++i) {
    DebugAssert(BITVECTOR == kids[i].getType().getExpr().getOpKind(),
                "TheoryBitvector::newBVConcatExpr:"
                "inputs must have type BITVECTOR:\n t1 = " +
                kids[i].toString());
  }
  return Expr(CONCAT, kids, getEM());
}

Expr TheoryBitvector::newBVMultExpr(int bvLength,
                                    const Expr& t1, const Expr& t2) {
  DebugAssert(bvLength > 0,
              "TheoryBitvector::newBVmultExpr:"
              "bvLength must be an integer > 0: bvLength = " +
              int2string(bvLength));
  DebugAssert(BITVECTOR == t1.getType().getExpr().getOpKind() &&
              BITVECTOR == t2.getType().getExpr().getOpKind(),
              "TheoryBitvector::newBVmultExpr:"
              "inputs must have type BITVECTOR:\n t1 = " +
              t1.toString() + "\n t2 = " +t2.toString());
  return Expr(Expr(BVMULT, getEM()->newRatExpr(bvLength)).mkOp(), t1, t2);
}

//! produces a string of 0's of length bvLength
Expr TheoryBitvector::newBVZeroString(int bvLength) {
  DebugAssert(bvLength > 0,
              "TheoryBitvector::newZeroBVExpr:must be >= 0: "
              + int2string(bvLength));
  std::vector<bool> bits;
  for(int count=0; count < bvLength; count++) {
    bits.push_back(false);
  }
  return newBVConstExpr(bits);
}

//! produces a string of 1's of length bvLength
Expr TheoryBitvector::newBVOneString(int bvLength) {
  DebugAssert(bvLength > 0,
              "TheoryBitvector::newOneBVExpr:must be >= 0: "
              + int2string(bvLength));
  std::vector<bool> bits;
  for(int count=0; count < bvLength; count++) {
    bits.push_back(true);
  }
  return newBVConstExpr(bits);
}

Expr TheoryBitvector::newBVConstExpr(const vector<bool>& bits) {
  DebugAssert(bits.size() > 0,
              "TheoryBitvector::newBVConstExpr:"
              "# of subterms must be at least 2");
  BVConstExpr bv(getEM(), bits, d_bvConstExprIndex);
  return getEM()->newExpr(&bv);
}

Expr TheoryBitvector::newBVConstExpr(const Rational& r, int bvLength) {
  DebugAssert(r.isInteger(),
              "TheoryBitvector::newBVConstExpr: not an integer: "
              + r.toString());
  DebugAssert(bvLength > 0,
              "TheoryBitvector::newBVConstExpr: bvLength = "
              + int2string(bvLength));
  string s(r.toString(2));
  size_t strsize = s.size();
  size_t length = bvLength;
  Expr res;
  if(length > 0 && length != strsize) {
    //either (length > strsize) or (length < strsize)
    if(length < strsize) {
      s = s.substr((strsize-length), length);
    } else {
      string zeros("");
      for(size_t i=0, pad=length-strsize; i < pad; ++i)
        zeros += "0";
      s = zeros+s;
    }
    res = newBVConstExpr(s, 2);
  } 
  else
    res = newBVConstExpr(s, 2);
  
  return res;
}

Expr TheoryBitvector::newBVConstExpr(const std::string& s, int base) {
  DebugAssert(s.size() > 0,
              "TheoryBitvector::newBVConstExpr:"
              "# of subterms must be at least 2");
  DebugAssert(base == 2 || base == 16, 
              "TheoryBitvector::newBVConstExpr: base = "
              +int2string(base));
  //hexadecimal
  std::string str = s;
  if(16 == base) {
    Rational r(str, 16);
    return newBVConstExpr(r, str.size()*4);
  } 
  else {
    BVConstExpr bv(getEM(), str, d_bvConstExprIndex);
    return getEM()->newExpr(&bv);
  }
}

Expr 
TheoryBitvector::
newBVExtractExpr(const Expr& e, int hi, int low){
  DebugAssert(low>=0 && hi>=low,
              " TheoryBitvector::newBVExtractExpr: " 
              "bad bv_extract indices: hi = " 
              + int2string(hi)
              + ", low = " 
              + int2string(low));
  DebugAssert(BITVECTOR == e.getType().getExpr().getOpKind(),
              "TheoryBitvector::newBVExtractExpr:"
              "inputs must have type BITVECTOR:\n e = " +
              e.toString());
  return Expr(Expr(EXTRACT,
                   getEM()->newRatExpr(hi),
                   getEM()->newRatExpr(low)).mkOp(), e);
}

Expr TheoryBitvector::newBVPlusExpr(int bvLength, 
                                    const std::vector<Expr>& k) {
  DebugAssert(bvLength > 0,
              " TheoryBitvector::newBVPlusExpr:" 
              "bvplus length must be a positive integer: "+
              int2string(bvLength));
  DebugAssert(k.size() > 1,
              " TheoryBitvector::newBVPlusExpr:" 
              " size of input vector must be greater than 0: ");
  for(unsigned int i=0; i<k.size(); ++i) {
    DebugAssert(BITVECTOR == k[i].getType().getExpr().getOpKind(),
                "TheoryBitvector::newBVPlusExpr:"
                "inputs must have type BITVECTOR:\n t1 = " +
                k[i].toString());
  }
  return Expr(Expr(BVPLUS, getEM()->newRatExpr(bvLength)).mkOp(), k);
}

//! Converts e into a BITVECTOR of length 'len'
/*!
 * \param len is the desired length of the resulting bitvector
 * \param e is the original bitvector of arbitrary length
 */
Expr 
TheoryBitvector::pad(int len, const Expr& e) {
  DebugAssert(len >=0,
              "TheoryBitvector::newBVPlusExpr:" 
              "padding length must be a non-negative integer: "+
              int2string(len));
  DebugAssert(BITVECTOR == e.getType().getExpr().getOpKind(),
              "TheoryBitvector::newBVPlusExpr:" 
              "input must be a BITVECTOR: " + e.toString());
              
  int size = BVSize(e);
  Expr res;
  if(size == len)
    res = e;
  else if (len < size)
    res = newBVExtractExpr(e,len-1,0);
  else {
    // size < len
    Expr zero = newBVZeroString(len-size);
    res = newConcatExpr(zero,e);
  }
  return res;
}


// Accessors for expression parameters
int TheoryBitvector::getBitvectorTypeParam(const Expr& e) {
  DebugAssert(BITVECTOR == e.getKind(),
              "TheoryBitvector::getBitvectorTypeParam: wrong kind: " +
              e.toString());
  return e[0].getRational().getInt();
}


Type TheoryBitvector::getTypePredType(const Expr& tp) {
  DebugAssert(tp.getOpKind()==BVTYPEPRED && tp.isApply(),
              "TheoryBitvector::getTypePredType:\n tp = "+tp.toString());
  return Type(tp.getOpExpr()[0]);
}


const Expr& TheoryBitvector::getTypePredExpr(const Expr& tp) {
  DebugAssert(tp.getOpKind()==BVTYPEPRED,
              "TheoryBitvector::getTypePredType:\n tp = "+tp.toString());
  return tp[0];
}

int TheoryBitvector::getBoolExtractIndex(const Expr& e) {
  DebugAssert(BOOLEXTRACT == e.getOpKind() && e.isApply(),
              "TheoryBitvector::getBoolExtractIndex: wrong kind" +
              e.toString());
  return e.getOpExpr()[0].getRational().getInt();
}

int TheoryBitvector::getSXIndex(const Expr& e) {
  DebugAssert(SX == e.getOpKind() && e.isApply(),
              "TheoryBitvector::getSXIndex: wrong kind\n"+e.toString());
  return e.getOpExpr()[0].getRational().getInt();
}

int TheoryBitvector::getFixedLeftShiftParam(const Expr& e) {
  DebugAssert(LEFTSHIFT == e.getOpKind() && e.isApply(),
              "TheoryBitvector::getFixedLeftShiftParam: wrong kind" +
              e.toString());
  return e.getOpExpr()[0].getRational().getInt();
}


int TheoryBitvector::getFixedRightShiftParam(const Expr& e) {
  DebugAssert(RIGHTSHIFT == e.getOpKind() && e.isApply(),
              "TheoryBitvector::getFixedRightShiftParam: wrong kind" +
              e.toString());
  return e.getOpExpr()[0].getRational().getInt();
}

int TheoryBitvector::getExtractLow(const Expr& e) {
  DebugAssert(EXTRACT == e.getOpKind() && e.isApply(),
              "TheoryBitvector::getExtractLow: wrong kind" +
              e.toString());
  return e.getOpExpr()[1].getRational().getInt();
}

int TheoryBitvector::getExtractHi(const Expr& e) {
  DebugAssert(EXTRACT == e.getOpKind() && e.isApply(),
              "TheoryBitvector::getExtractHi: wrong kind" +
              e.toString());
  return e.getOpExpr()[0].getRational().getInt();
}

int TheoryBitvector::getBVPlusParam(const Expr& e) {
  DebugAssert(BVPLUS == e.getOpKind() && e.isApply(),
              "TheoryBitvector::getBVPlusParam: wrong kind" +
              e.toString());
  return e.getOpExpr()[0].getRational().getInt();
}


int TheoryBitvector::getBVMultParam(const Expr& e) {
  DebugAssert(BVMULT == e.getOpKind() && e.isApply(),
              "TheoryBitvector::getBVMultParam: wrong kind " +
              e.toString(AST_LANG));
  return e.getOpExpr()[0].getRational().getInt();
}

//////////////////////////////////////////////////////////////////////
// class BVConstExpr methods
/////////////////////////////////////////////////////////////////////
//! Constructor
BVConstExpr::BVConstExpr(ExprManager* em, std::string bvconst,
                         size_t mmIndex, ExprIndex idx)
  : ExprValue(em, BVCONST, idx), d_MMIndex(mmIndex) {
  std::string::reverse_iterator i = bvconst.rbegin();
  std::string::reverse_iterator iend = bvconst.rend();
  DebugAssert(bvconst.size() > 0,
              "TheoryBitvector::newBVConstExpr:"
              "# of subterms must be at least 2");
  
  for(;i != iend; ++i) {
    TRACE("bitvector", "BVConstExpr: bit ", *i, "");
    if('0' == *i)
      d_bvconst.push_back(false);
    else { 
      if('1' == *i)
        d_bvconst.push_back(true);
      else
        DebugAssert(false, "BVConstExpr: bad binary bit-vector: "
                    + bvconst);
    }
  }
  TRACE("bitvector", "BVConstExpr: #bits ", d_bvconst.size(), "");
}

BVConstExpr::BVConstExpr(ExprManager* em, std::vector<bool> bvconst,
                         size_t mmIndex, ExprIndex idx)
  : ExprValue(em, BVCONST, idx), d_bvconst(bvconst), d_MMIndex(mmIndex) {
  TRACE("bitvector", "BVConstExpr(vector<bool>): arg. size = ", bvconst.size(),
        ", d_bvconst.size = "+int2string(d_bvconst.size()));
}
  
size_t BVConstExpr::computeHash() const {
  std::vector<bool>::const_iterator i = d_bvconst.begin();
  std::vector<bool>::const_iterator iend = d_bvconst.end(); 
  size_t hash_value = 0;
  hash_value = ExprValue::hash(BVCONST);
  for (;i != iend; i++)
    if(*i)
      hash_value = PRIME*hash_value + HASH_VALUE_ONE;
    else 
      hash_value = PRIME*hash_value + HASH_VALUE_ZERO;
  return hash_value;
}

namespace CVCL {

unsigned TheoryBitvector::getBVConstSize(const Expr& e)
{
  DebugAssert(BVCONST == e.getKind(), "getBVConstSize called on non-bvconst");
  const BVConstExpr* bvc = dynamic_cast<const BVConstExpr*>(e.getExprValue());
  DebugAssert(bvc, "getBVConstSize: cast failed");
  return bvc->size();
}

bool TheoryBitvector::getBVConstValue(const Expr& e, int i)
{
  DebugAssert(BVCONST == e.getKind(), "getBVConstSize called on non-bvconst");
  const BVConstExpr* bvc = dynamic_cast<const BVConstExpr*>(e.getExprValue());
  DebugAssert(bvc, "getBVConstSize: cast failed");
  return bvc->getValue(i);
}

// Computes the integer value of a bitvector constant
Rational TheoryBitvector::computeBVConst(const Expr& e) {
//   DebugAssert(BITVECTOR == e.getType().getExpr().getOpKind(),
//            "TheoryBitvector::computeBVConst:" 
//            "input must be a BITVECTOR: " + e.toString());
  DebugAssert(BVCONST == e.getKind(),
              "TheoryBitvector::computeBVConst:" 
              "input must be a BITVECTOR CONST: " + e.toString());
  if(*d_bv32Flag) {
    int c(0);
    for(int j=(int)getBVConstSize(e)-1; j>=0; j--)
      c = 2*c + getBVConstValue(e, j) ? 1 : 0;
    Rational d(c);
    return d;
  } else {
    Rational c(0);
    for(int j=(int)getBVConstSize(e)-1; j>=0; j--)
      c = 2*c + (getBVConstValue(e, j) ? Rational(1) : Rational(0));
    return c;
  }
}

// Computes the integer value of ~c+1
Rational TheoryBitvector::computeNegBVConst(const Expr& e) {
//   DebugAssert(BITVECTOR == e.getType().getExpr().getOpKind(),
//            "TheoryBitvector::computeBVConst:" 
//            "input must be a BITVECTOR: " + e.toString());
  DebugAssert(BVCONST == e.getKind(),
              "TheoryBitvector::computeBVConst:" 
              "input must be a BITVECTOR CONST: " + e.toString());
  if(*d_bv32Flag) {
    int c(0);
    for(int j=(int)getBVConstSize(e)-1; j>=0; j--)
      c = 2*c + getBVConstValue(e, j) ? 0 : 1;
    Rational d(c+1);
    return d;
  } else {
    Rational c(0);
    for(int j=(int)getBVConstSize(e)-1; j>=0; j--)
      c = 2*c + (getBVConstValue(e, j) ? Rational(0) : Rational(1));
    return c+1;
  }
}

// Computes the integer value of a bitvector constant
Rational computeBVConst(const Expr& e) {
//   DebugAssert(BITVECTOR == e.getType().getExpr().getOpKind(),
//            "TheoryBitvector::computeBVConst:" 
//            "input must be a BITVECTOR: " + e.toString());
  DebugAssert(BVCONST == e.getKind(),
              "TheoryBitvector::computeBVConst:" 
              "input must be a BITVECTOR CONST: " + e.toString());
  Rational c(0);

  const BVConstExpr* bvc = dynamic_cast<const BVConstExpr*>(e.getExprValue());
  DebugAssert(bvc, "getBVConstSize: cast failed");

  for(int j=(int)bvc->size()-1; j>=0; j--)
    c = 2*c + (bvc->getValue(j) ? Rational(1) : Rational(0));
  return c;
}

Theorem
TheoryBitvector::rewriteBoolean(const Expr& e) {
  if(!*d_booleanRWFlag)
    return reflexivityRule(e);

  Theorem thm;
  switch (e.getKind()) {
  case NOT:
    if (e[0].isTrue())
      thm = getCommonRules()->rewriteNotTrue(e);
    else if (e[0].isFalse())
      thm = getCommonRules()->rewriteNotFalse(e);
    else if (e[0].isNot())
      thm = getCommonRules()->rewriteNotNot(e);
    break;
  case IFF: {
    thm = getCommonRules()->rewriteIff(e);
    const Expr& rhs = thm.getRHS();
    // The only time we need to rewrite the result (rhs) is when
    // e==(FALSE<=>e1) or (e1<=>FALSE), so rhs==!e1.
    if (e != rhs && rhs.isNot())
      thm = transitivityRule(thm, rewriteBoolean(rhs));
    break;
  }
//   case AND:
//     thm = rewriteAnd(e);
//     break;
//   case OR:
//     thm = rewriteOr(e);
//     break;
  case AND:{
    std::vector<Theorem> newK;
    std::vector<unsigned> changed;
    unsigned count(0);
    for(Expr::iterator ii=e.begin(),iiend=e.end();ii!=iiend;ii++,count++) {
      Theorem temp = rewriteBoolean(*ii);
      if(temp.getLHS() != temp.getRHS()) {
        newK.push_back(temp);
        changed.push_back(count);
      }
    }
    if(changed.size() > 0) {
      Theorem res = substitutivityRule(e,changed,newK);
      thm = transitivityRule(res, rewriteAnd(res.getRHS()));
    } else
      thm = rewriteAnd(e);
  }
    break;
  case OR:{
    std::vector<Theorem> newK;
    std::vector<unsigned> changed;
    unsigned count(0);
    for(Expr::iterator ii=e.begin(),iiend=e.end();ii!=iiend;ii++,count++) {
      Theorem temp = rewriteBoolean(*ii);
      if(temp.getLHS() != temp.getRHS()) {
        newK.push_back(temp);
        changed.push_back(count);
      }
    }
    if(changed.size() > 0) {
      Theorem res = substitutivityRule(e,changed,newK);
      thm = transitivityRule(res, rewriteOr(res.getRHS()));
    } else
      thm = rewriteOr(e);
  }
    break;

  default:
    break;
  }
  if(thm.isNull()) thm = reflexivityRule(e);
  
  return thm;
}

} // end of namespace CVCL

---