Initial KLEE checkin.

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


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

1 files changed, 812 insertions, 0 deletions

diff --git a/stp/AST/BitBlast.cpp b/stp/AST/BitBlast.cpp
new file mode 100644
index 00000000..de78ec74
--- /dev/null
+++ b/stp/AST/BitBlast.cpp
@@ -0,0 +1,812 @@
+/********************************************************************
+ * AUTHORS: David L. Dill, Vijay Ganesh
+ *
+ * BEGIN DATE: November, 2005
+ *
+ * LICENSE: Please view LICENSE file in the home dir of this Program
+ ********************************************************************/
+// -*- c++ -*-
+
+// BitBlast -- convert bitvector terms and formulas to boolean
+// formulas.  A term is something that can represent a multi-bit
+// bitvector, such as BVPLUS or BVXOR (or a BV variable or constant).
+// A formula (form) represents a boolean value, such as EQ or BVLE.
+// Bit blasting a term representing an n-bit bitvector with BBTerm
+// yields a vector of n boolean formulas (returning ASTVec).
+// Bit blasting a formula returns a single boolean formula (type ASTNode).
+
+// A bitblasted term is a vector of ASTNodes for formulas.
+// The 0th element of the vector corresponds to bit 0 -- the low-order bit.
+
+#include "AST.h"
+namespace BEEV {
+  //  extern void lpvec(ASTVec &vec);
+
+// FIXME: Assert no zero-length bit vectors!!!
+// FIXME: Need top-level functions that create and destroy the memo tables.
+// FIXME:  Check resource limits and generate an exception when exceeded.
+// FIXME:  THis does a lot of unnecessary copying of vectors.
+//    Had to be careful not to modify memoized vectors!
+// FIXME:  Might be some redundant variables.
+
+// accepts a term, and returns a vector of bitblasted bits(ASTVec)
+
+ASTNode ASTJunk;
+const ASTNode BeevMgr::BBTerm(const ASTNode& term) {
+  //CHANGED TermMemo is now an ASTNodeMap. Based on BBFormMemo
+  ASTNodeMap::iterator it = BBTermMemo.find(term);
+  if (it != BBTermMemo.end()) {
+    // already there.  Just return it.
+    return it->second;
+  }
+
+//  ASTNode& result = ASTJunk;
+  ASTNode result;
+
+  Kind k = term.GetKind();
+  if (!is_Term_kind(k))
+    FatalError("BBTerm: Illegal kind to BBTerm",term);
+
+  ASTVec::const_iterator kids_end = term.end(); 
+  unsigned int num_bits = term.GetValueWidth();
+  switch (k) {
+  case BVNEG: {
+    // bitwise complement
+    // bitblast the child.
+    //FIXME Uses a tempory const ASTNode
+    const ASTNode& bbkids = BBTerm(term[0]);
+    result = CreateNode(BOOLVEC, BBNeg(bbkids.GetChildren()));
+    break;
+  }
+  case BVSRSHIFT:
+  case BVVARSHIFT: 
+    FatalError("BBTerm: These kinds have not been implemented in the BitBlaster: ", term);
+    break;
+  case ITE: {
+    // Term version of ITE.
+
+    // Blast the args
+    // FIXME Uses temporary const ASTNodes and an ASTVec&
+    const ASTNode& cond = BBForm(term[0]);
+    const ASTNode& thn = BBTerm(term[1]);
+    const ASTNode& els = BBTerm(term[2]);
+    result = 
+       CreateNode(BOOLVEC, BBITE(cond, thn.GetChildren(), els.GetChildren()));
+    break;
+  }
+  case BVSX: {
+    // Replicate high-order bit as many times as necessary.
+    // Arg 0 is expression to be sign extended.
+    const ASTNode& arg = term[0];
+    unsigned long result_width = term.GetValueWidth();
+    unsigned long arg_width = arg.GetValueWidth();
+    //FIXME Uses a temporary const ASTNode reference
+    const ASTNode& bbarg = BBTerm(arg);
+
+    if (result_width == arg_width) {
+      //nothing to sign extend
+      break;
+    }
+    else {
+      //we need to sign extend
+      const ASTNode& msbX = bbarg.back();
+      //const ASTNode& msb1 = msbX;
+      
+      ASTVec ccc = msbX.GetChildren();
+      const ASTNode& msb = CreateSimpForm(msbX.GetKind(),ccc);
+
+     //  Old version
+     //  ASTNode msb = bbarg.back();
+     //  const ASTNode msb1 = msb;
+      
+     //  ASTVec ccc = msb.GetChildren();
+     //  msb = CreateSimpForm(msb.GetKind(),ccc);
+
+      // DD 1/14/07 Simplify silently drops all but first two args of XOR.
+      // I expanded XOR to N args with flattening optimization.
+      // This bug took 2 days to track down!
+
+      // msb = SimplifyFormula(msb,false);
+
+      // cout << "!!!!!!!!!!!!!!!!" << endl
+      // << "Simplify msb:" << msb2 << endl
+      // << "Simplify result:" << msb << endl;
+
+      //FIXME Dynamically allocate the result vector?
+      //Is this doing multiple copies?
+      //ASTVec& tmp_res = *(new ASTVec(result_width));
+      ASTVec tmp_res(result_width);
+
+      //FIXME Should these be gotten from result?
+      ASTVec::const_iterator bb_it = bbarg.begin();
+      ASTVec::iterator res_it = tmp_res.begin();
+      ASTVec::iterator res_ext = res_it+arg_width; // first bit of extended part
+      ASTVec::iterator res_end = tmp_res.end();
+      // copy LSBs directly from bbvec
+      for( ; res_it < res_ext; (res_it++, bb_it++)) {
+	*res_it = *bb_it;
+      }
+      // repeat MSB to fill up rest of result.
+      for( ; res_it < res_end; (res_it++, bb_it++)) {
+	*res_it = msb;
+      }
+      
+       //Temporary debugging code
+       //    cout << "Sign extending:" << endl 
+       //	        << "  Vec ";
+       //    lpvec( bbarg.GetChildren() );
+       //    cout << "  Extended to ";
+       //    lp(result);
+       //    cout << endl;
+      
+      result = CreateNode(BOOLVEC, tmp_res);
+
+      break;
+    }
+  }
+  case BVEXTRACT: {
+    // bitblast the child, then extract the relevant bits.
+    // Note: This could be optimized by not bitblasting the bits
+    // that aren't fetched.  But that would be tricky, especially
+    // with memo-ization.
+
+    //FIXME Using const ASTNode w/out reference
+    const ASTNode& bbkids = BBTerm(term[0]); 
+    unsigned int high = GetUnsignedConst(term[1]);
+    unsigned int low = GetUnsignedConst(term[2]);
+
+    ASTVec::const_iterator bbkfit = bbkids.begin();
+    // I should have used pointers to ASTVec, to avoid this crock
+    
+    //FIXME Creates a new local ASTVec and does the CreateNode from that
+    result = CreateNode(BOOLVEC, ASTVec(bbkfit+low, bbkfit+high+1));
+    break;
+  }
+  case BVCONCAT: {
+    //FIXME Using temporary const ASTNodes 
+    const ASTNode& vec1 = BBTerm(term[0]);
+    const ASTNode& vec2 = BBTerm(term[1]);
+
+    //FIXME This has to be an unnessecary copy and a memory leak
+    //Leaking ASTVec tmp_res = *(new ASTVec(vec2.GetChildren()));
+    ASTVec tmp_res(vec2.GetChildren());
+    tmp_res.insert(tmp_res.end(), vec1.begin(), vec1.end());
+    result = CreateNode(BOOLVEC, tmp_res);
+    break;
+  }
+  case BVPLUS: {
+    // ASSERT: at least one child.
+    // ASSERT: all children and result are the same size.
+    // Previous phase must make sure this is true.
+    // Add children pairwise and accumulate in BBsum
+
+    // FIXME: Unnecessary array copies.
+    ASTVec::const_iterator it = term.begin();
+    ASTVec tmp_res = BBTerm(*it).GetChildren();
+    for (++it; it < kids_end; it++) {
+      const ASTVec& tmp = BBTerm(*it).GetChildren();
+      BBPlus2(tmp_res, tmp, ASTFalse);
+    }
+
+    result = CreateNode(BOOLVEC, tmp_res);
+    break;
+  }
+  case BVUMINUS: {
+    //FIXME Using const ASTNode reference
+    const ASTNode& bbkid = BBTerm(term[0]);
+    result = CreateNode(BOOLVEC, BBUminus(bbkid.GetChildren()));
+    break;
+  }
+  case BVSUB: {
+    // complement of subtrahend
+    // copy, since BBSub writes into it.
+    
+    //FIXME: Unnecessary array copies?
+    ASTVec tmp_res = BBTerm(term[0]).GetChildren(); 
+
+    const ASTVec& bbkid1 = BBTerm(term[1]).GetChildren();
+    BBSub(tmp_res, bbkid1);
+    result = CreateNode(BOOLVEC, tmp_res);
+    break;
+  }
+  case BVMULT: {
+    // ASSERT 2 arguments, same length, result is same length.
+
+    const ASTNode& t0 = term[0];
+    const ASTNode& t1 = term[1];
+
+    const ASTNode& mpcd1 = BBTerm(t0);
+    const ASTNode& mpcd2 = BBTerm(t1);
+    //Reverese the order of the nodes w/out the need for temporaries
+    //This is needed because t0 an t1 must be const
+    if ((BVCONST != t0.GetKind()) && (BVCONST == t1.GetKind())) {
+      result = CreateNode(BOOLVEC, 
+        BBMult(mpcd2.GetChildren(), mpcd1.GetChildren()) );
+    }else{
+      result = CreateNode(BOOLVEC, 
+        BBMult(mpcd1.GetChildren(), mpcd2.GetChildren()) );
+    }
+    break;
+  }
+  case BVDIV:
+  case BVMOD: {
+    const ASTNode& dvdd = BBTerm(term[0]);
+    const ASTNode& dvsr = BBTerm(term[1]);
+    unsigned int width = dvdd.Degree();
+    ASTVec q(width); 
+    ASTVec r(width); 
+    BBDivMod(dvdd.GetChildren(),  dvsr.GetChildren(), q, r, width);
+    if (k == BVDIV)
+      result = CreateNode(BOOLVEC, q);    
+    else
+      result = CreateNode(BOOLVEC, r);
+    break;
+  }
+  //  n-ary bitwise operators.
+  case BVXOR:
+  case BVXNOR:
+  case BVAND:
+  case BVOR:
+  case BVNOR:
+  case BVNAND: {
+    // Add children pairwise and accumulate in BBsum
+    ASTVec::const_iterator it = term.begin();
+    Kind bk = UNDEFINED;  // Kind of individual bit op.
+    switch (k) {
+    case BVXOR: bk = XOR;  break;
+    case BVXNOR: bk = IFF; break;
+    case BVAND: bk = AND; break;
+    case BVOR: bk = OR; break;
+    case BVNOR: bk = NOR; break;
+    case BVNAND: bk = NAND; break;
+    default:
+      FatalError("BBTerm: Illegal kind to BBTerm",term);
+      break;
+    }
+
+    // Sum is destructively modified in the loop, so make a copy of value
+    // returned by BBTerm.
+    ASTNode temp = BBTerm(*it);
+    ASTVec sum(temp.GetChildren());	// First operand.
+
+    // Iterate over remaining bitvector term operands
+    for (++it; it < kids_end; it++) {
+      //FIXME FIXME FIXME: Why does using a temp. var change the behavior?
+      temp = BBTerm(*it);
+      const ASTVec& y = temp.GetChildren();
+      
+      // Iterate over bits
+      // FIXME: Why is this not using an iterator???
+      int n = y.size();
+      for (int i = 0; i < n; i++) {
+	sum[i] = CreateSimpForm(bk, sum[i], y[i]);
+      }
+    }
+    result = CreateNode(BOOLVEC, sum);
+    break;
+  }
+  case SYMBOL: {
+    // ASSERT: IndexWidth = 0?  Semantic analysis should check.
+    //Leaking ASTVec& bbvec = *(new ASTVec);
+    
+    //FIXME Why is isn't this ASTVEC bbvec(num_bits) ?
+    ASTVec bbvec;
+    for (unsigned int i = 0; i < num_bits; i++) {
+      ASTNode bit_node =
+	CreateNode(BVGETBIT, term, CreateBVConst(32,i));
+      bbvec.push_back(bit_node); 
+    }
+    result = CreateNode(BOOLVEC, bbvec);
+    break;
+  }
+  case BVCONST: {
+    ASTVec tmp_res(num_bits);
+#ifndef NATIVE_C_ARITH
+    CBV bv = term.GetBVConst();
+    for(unsigned int i = 0; i < num_bits; i++){
+      tmp_res[i] = CONSTANTBV::BitVector_bit_test(bv,i) ? ASTTrue : ASTFalse; 
+    }  
+#else
+    const unsigned long long int c = term.GetBVConst();
+    unsigned long long int bitmask = 0x00000000000000001LL;
+    for (unsigned int i = 0; i < num_bits; i++, bitmask <<= 1)
+      tmp_res[i] = ((c & (bitmask)) ? ASTTrue : ASTFalse);    
+#endif
+    result = CreateNode(BOOLVEC, tmp_res);
+    break;
+  }		  
+  case BOOLVEC: {
+    cerr << "Hit a boolvec! what to do?" << endl;
+    break;
+  }
+  default:
+    FatalError("BBTerm: Illegal kind to BBTerm",term);
+  }
+
+  //if(result == ASTJunk)
+  //  cout<<"result does not change"<<endl;
+  // cout << "================" << endl << "BBTerm:" << term << endl;
+  // cout << "----------------" << endl << "BBTerm result:";
+  // lpvec(result);
+  // cout << endl;
+
+  return (BBTermMemo[term] = result);
+
+}
+
+// bit blast a formula (boolean term).  Result is one bit wide,
+// so it returns a single ASTNode.
+// FIXME:  Add IsNegated flag.
+const ASTNode BeevMgr::BBForm(const ASTNode& form)
+{
+
+  ASTNodeMap::iterator it = BBFormMemo.find(form);
+  if (it != BBFormMemo.end()) {
+    // already there.  Just return it.
+    return it->second;
+  }
+
+  ASTNode result = ASTUndefined;
+
+  Kind k = form.GetKind();
+  if (!is_Form_kind(k)) {
+    FatalError("BBForm: Illegal kind: ",form);
+  }
+
+  //  Not returning until end, and memoizing everything, makes it easier
+  // to trace coherently.
+    
+  // Various special cases
+  switch (k) {
+  case TRUE:
+  case FALSE: {
+    result = form;
+    break;
+  }
+
+  case SYMBOL:
+    if (form.GetType() != BOOLEAN_TYPE) {
+      FatalError("BBForm: Symbol represents more than one bit", form);
+    }
+
+    result = form;
+    break;
+
+  case BVGETBIT: {
+    // exactly two children
+    const ASTNode bbchild = BBTerm(form[0]);
+    unsigned int index =  GetUnsignedConst(form[1]);
+    result = bbchild[index];
+    break;
+  }
+
+  case NOT:
+    result = CreateSimpNot(BBForm(form[0]));
+    break;  
+
+  case ITE:
+    // FIXME: SHould this be CreateSimpITE?
+    result = CreateNode(ITE, BBForm(form[0]), BBForm(form[1]), BBForm(form[2]));
+    break;
+
+  case AND: 
+  case OR: 
+  case NAND: 
+  case NOR: 
+  case IFF: 
+  case XOR:
+  case IMPLIES: {
+    ASTVec bbkids;		// bit-blasted children (formulas)
+
+    // FIXME: Put in fast exits for AND/OR/NAND/NOR/IMPLIES
+    ASTVec::const_iterator kids_end = form.end(); 
+    for (ASTVec::const_iterator it = form.begin(); it != kids_end; it++) {
+      bbkids.push_back(BBForm(*it));
+    }
+    result = CreateSimpForm(k, bbkids);
+    break;
+  }
+
+  case NEQ: {
+    ASTNode bbkid = BBForm(CreateNode(EQ, form.GetChildren()));
+    result = CreateSimpNot(bbkid);
+    break;
+  }
+
+  case EQ: {
+    // Common code for binary operations
+    // FIXME:  This ought to be in a semantic analysis phase.
+    const ASTNode left = BBTerm(form[0]);
+    const ASTNode right = BBTerm(form[1]);
+    if (left.Degree() != right.Degree()) {
+      cerr << "BBForm: Size mismatch" << endl << form[0] << endl << form[1] << endl;
+      FatalError("",ASTUndefined);
+    }
+    result = BBEQ(left.GetChildren(), right.GetChildren());
+    break;
+  }
+
+  case BVLE: 
+  case BVGE: 
+  case BVGT: 
+  case BVLT: 
+  case BVSLE:
+  case BVSGE:
+  case BVSGT:
+  case BVSLT: {
+    result = BBcompare(form);
+    break;
+  }
+  default:
+    FatalError("BBForm: Illegal kind: ", form);
+    break;
+  }
+
+  // cout << "================" << endl
+  // << "BBForm: " << form << endl
+  // << "----------------" << endl
+  // << "BBForm Result: " << result << endl;
+
+  return (BBFormMemo[form] = result);
+}
+  
+// Bit blast a sum of two equal length BVs.
+// Update sum vector destructively with new sum.
+void BeevMgr::BBPlus2(ASTVec& sum, const ASTVec& y, ASTNode cin)
+{
+//   cout << "Bitblasting plus.  Operand 1: " << endl;
+//   lpvec(sum);
+//   cout << endl << " operand 2: " << endl;
+//   lpvec(y);
+//   cout << endl << "carry: " << endl << cin << endl;
+
+
+  int n = sum.size();
+  // ASSERT: y.size() == x.size()
+  // FIXME: Don't bother computing i+1 carry, which is discarded.
+  for (int i = 0; i < n; i++) {
+    ASTNode nextcin = Majority(sum[i], y[i], cin); 
+    sum[i] = CreateSimpForm(XOR, CreateSimpForm(XOR, sum[i], y[i]), cin);
+    cin = nextcin;
+  }
+
+//   cout << "----------------" << endl << "Result: " << endl;
+//   lpvec(sum);
+//   cout << endl;
+
+}
+
+// Stores result - x in result, destructively
+void BeevMgr::BBSub(ASTVec& result, const ASTVec& y)
+{
+  ASTVec compsubtrahend  = BBNeg(y);
+  BBPlus2(result, compsubtrahend, ASTTrue);
+}
+
+// Add one bit
+ASTVec BeevMgr::BBAddOneBit(ASTVec& x, ASTNode cin)
+{
+  ASTVec result = ASTVec(0);
+  ASTVec::const_iterator itend = x.end();
+  for (ASTVec::const_iterator it = x.begin(); it < itend; it++) {
+    ASTNode nextcin = CreateSimpForm(AND, *it, cin); 
+    result.push_back(CreateSimpForm(XOR, *it, cin));
+    cin = nextcin;
+  }
+  // FIXME: unnecessary array copy on return?
+  return result;
+}
+
+// Increment bit-blasted vector and return result.
+ASTVec BeevMgr::BBInc(ASTVec& x)
+{
+  return BBAddOneBit(x, ASTTrue);
+}
+
+// Return formula for majority function of three bits.
+// Pass arguments by reference to reduce refcounting.
+ASTNode BeevMgr::Majority(const ASTNode& a, const ASTNode& b,const ASTNode& c)
+{
+  // Checking explicitly for constant a, b and c could
+  // be more efficient, because they are repeated in the logic.
+  if (ASTTrue == a) {
+    return CreateSimpForm(OR, b, c);
+  }
+  else if (ASTFalse == a) {
+    return CreateSimpForm(AND, b, c);
+  }
+  else if (ASTTrue == b) {
+    return CreateSimpForm(OR, a, c);
+  }
+  else if (ASTFalse == b) {
+    return CreateSimpForm(AND, a, c);
+  }
+  else if (ASTTrue == c) {
+    return CreateSimpForm(OR, a, b);
+  }
+  else if (ASTFalse == c) {
+    return CreateSimpForm(AND, a, b);
+  }
+  // there are lots more simplifications, but I'm not sure they're
+  // worth doing explicitly (e.g., a = b, a = ~b, etc.) 
+  else {
+    return
+      CreateSimpForm(OR,
+		     CreateSimpForm(AND, a, b),
+		     CreateSimpForm(AND, b, c),
+		     CreateSimpForm(AND, a, c));
+  }
+}
+
+
+// Bitwise complement
+ASTVec BeevMgr::BBNeg(const ASTVec& x)
+{
+  ASTVec result = ASTVec(0);		// FIXME: faster to preallocate n entries?
+  // Negate each bit.
+  ASTVec::const_iterator xend = x.end();
+  for (ASTVec::const_iterator it = x.begin(); it < xend; it++) {
+    result.push_back(CreateSimpNot(*it));
+  }
+  // FIXME: unecessary array copy when it returns?
+  return result;
+}
+
+// Compute unary minus
+ASTVec BeevMgr::BBUminus(const ASTVec& x)
+{
+  ASTVec xneg = BBNeg(x);
+  return BBInc(xneg);
+}
+
+// Multiply two bitblasted numbers
+ASTVec BeevMgr::BBMult(const ASTVec& x, const ASTVec& y)
+{
+  ASTVec ycopy(y);
+  ASTVec::const_iterator xend = x.end();
+  ASTVec::const_iterator xit = x.begin();
+  // start prod with first partial product.
+  // FIXME: This is unnecessary. Clean it up.
+  ASTVec prod = ASTVec(BBAndBit(y, *xit));
+  // start loop at next bit.
+  for(xit++; xit < xend; xit++) {
+    // shift first
+    BBLShift(ycopy);
+
+    if (ASTFalse == *xit) {
+      // If this bit is zero, the partial product will
+      // be zero.  No reason to add that in.
+      continue;
+    }
+
+    ASTVec pprod = BBAndBit(ycopy, *xit);
+    // accumulate in the product.
+    BBPlus2(prod, pprod, ASTFalse);
+  }
+  return prod;
+}
+
+// This implements a variant of binary long division.
+// q and r are "out" parameters.  rwidth puts a bound on the
+// recursion depth.
+void BeevMgr::BBDivMod(const ASTVec &y, const ASTVec &x, ASTVec &q, ASTVec &r, unsigned int rwidth)
+{
+  unsigned int width = y.size();
+  if (rwidth == 0) {
+    // When we have shifted the entire width, y is guaranteed to be 0.
+    q = BBfill(width, ASTFalse);
+    r = BBfill(width, ASTFalse);
+  }
+  else {
+    ASTVec q1, r1;
+    ASTVec yrshift1(y);
+    BBRShift(yrshift1);
+
+    // recursively divide y/2 by x.
+    BBDivMod(yrshift1, x, q1, r1, rwidth-1);
+
+    ASTVec q1lshift1(q1);
+    BBLShift(q1lshift1);
+
+    ASTVec r1lshift1(r1);
+    BBLShift(r1lshift1);
+    
+    ASTVec r1lshift1plusyodd = BBAddOneBit(r1lshift1, y[0]);
+    ASTVec rminusx(r1lshift1plusyodd);
+    BBSub(rminusx, x);
+
+    // Adjusted q, r values when when r is too large.
+    ASTNode rtoolarge = BBBVLE(x, r1lshift1plusyodd, false);
+    ASTVec ygtrxqval = BBITE(rtoolarge, BBInc(q1lshift1), q1lshift1);
+    ASTVec ygtrxrval = BBITE(rtoolarge, rminusx, r1lshift1plusyodd);
+
+    // q & r values when y >= x
+    ASTNode yeqx = BBEQ(y, x);
+    // *** Problem: the bbfill for qval is wrong.  Should be 1, not -1.
+    ASTVec one = BBfill(width, ASTFalse);
+    one[0] = ASTTrue;
+    ASTVec notylessxqval = BBITE(yeqx, one, ygtrxqval);
+    ASTVec notylessxrval = BBITE(yeqx, BBfill(width, ASTFalse), ygtrxrval);
+    // y < x <=> not x >= y.
+    ASTNode ylessx = CreateSimpNot(BBBVLE(x, y, false));
+    // final values of q and r
+    q = BBITE(ylessx, BBfill(width, ASTFalse), notylessxqval);
+    r = BBITE(ylessx, y, notylessxrval);
+  }
+}
+
+// build ITE's (ITE cond then[i] else[i]) for each i.
+ASTVec BeevMgr::BBITE(const ASTNode& cond, const ASTVec& thn, const ASTVec& els)
+{
+  // Fast exits.
+  if (ASTTrue == cond) {
+    return thn;
+  }
+  else if (ASTFalse == cond) {
+    return els;
+  }
+
+  ASTVec result(0);
+  ASTVec::const_iterator th_it_end = thn.end();
+  ASTVec::const_iterator el_it = els.begin();
+  for (ASTVec::const_iterator th_it = thn.begin(); th_it < th_it_end; th_it++, el_it++) {
+    result.push_back(CreateSimpForm(ITE, cond, *th_it, *el_it));
+  }
+  return result;
+}
+// AND each bit of vector y with single bit b and return the result.
+ASTVec BeevMgr::BBAndBit(const ASTVec& y, ASTNode b)
+{
+  ASTVec result(0); 
+
+  if (ASTTrue == b) {
+    return y;
+  }
+  // FIXME: put in fast exits when b is constant 0. 
+
+  ASTVec::const_iterator yend = y.end();
+  for(ASTVec::const_iterator yit = y.begin(); yit < yend; yit++) {
+    result.push_back(CreateSimpForm(AND, *yit, b));
+  }
+  return result;
+}
+
+
+// Workhorse for comparison routines.  This does a signed BVLE if is_signed
+// is true, else it's unsigned.  All other comparison operators can be reduced
+// to this by swapping args or complementing the result bit.
+// FIXME:  If this were done MSB first, it would enable a fast exit sometimes
+// when the MSB is constant, deciding the result without looking at the rest
+// of the bits.
+ASTNode BeevMgr::BBBVLE(const ASTVec& left, const ASTVec& right, bool is_signed)
+{
+  // "thisbit" represents BVLE of the suffixes of the BVs
+  // from that position .  if R < L, return TRUE, else if L < R
+  // return FALSE, else return BVLE of lower-order bits.  MSB is
+  // treated separately, because signed comparison is done by
+  // complementing the MSB of each BV, then doing an unsigned
+  // comparison.
+  ASTVec::const_iterator lit = left.begin();
+  ASTVec::const_iterator litend = left.end();
+  ASTVec::const_iterator rit = right.begin();
+  ASTNode prevbit = ASTTrue;
+  for ( ; lit  < litend-1; lit++, rit++) {
+    ASTNode neglit = CreateSimpNot(*lit);
+    ASTNode thisbit =
+      CreateSimpForm(OR,
+		 CreateSimpForm(AND,neglit,*rit), // TRUE if l < r
+		 CreateSimpForm(AND,
+			    CreateSimpForm(OR, neglit, *rit), // false if not equal
+			    prevbit)); // else prevbit
+    prevbit = thisbit;
+  }
+
+  // Handle MSB -- negate MSBs if signed comparison
+  // FIXME: make into refs after it's debugged.
+  ASTNode lmsb = *lit;
+  ASTNode rmsb = *rit;
+  if (is_signed) {
+    lmsb = CreateSimpNot(*lit);
+    rmsb = CreateSimpNot(*rit);
+  }
+
+  ASTNode neglmsb = CreateSimpNot(lmsb);
+  ASTNode msb =
+    CreateSimpForm(OR,
+	       CreateSimpForm(AND,neglmsb, rmsb), // TRUE if l < r
+	       CreateSimpForm(AND,
+			  CreateSimpForm(OR, neglmsb, rmsb), // false if not equal
+			  prevbit)); // else prevbit
+  return msb;
+}
+
+// Left shift by 1 within fixed field inserting zeros at LSB.
+// Writes result into first argument.
+// Fixme: generalize to n bits
+void BeevMgr::BBLShift(ASTVec& x)
+{
+  // left shift x (destructively) within width.
+  // loop backwards so that copy to self works correctly. (DON'T use STL insert!)
+  ASTVec::iterator xbeg = x.begin();
+  for(ASTVec::iterator xit = x.end()-1; xit > xbeg; xit--) {
+    *xit = *(xit-1);
+  }
+  *xbeg = ASTFalse;		// new LSB is zero.
+  // cout << "Shifted result" << endl;
+  // lpvec(x);
+}
+
+// Right shift by 1 within fixed field, inserting new zeros at MSB.
+// Writes result into first argument.
+// Fixme: generalize to n bits.
+void BeevMgr::BBRShift(ASTVec& x)
+{
+  ASTVec::iterator xend = x.end() - 1;
+  ASTVec::iterator xit = x.begin();
+  for( ; xit < xend; xit++) {
+    *xit = *(xit+1);
+  }
+  *xit = ASTFalse;		// new MSB is zero.
+}
+
+
+// Return bit-blasted form for BVLE, BVGE, BVGT, SBLE, etc. 
+ASTNode BeevMgr::BBcompare(const ASTNode& form) {
+  const ASTNode lnode = BBTerm(form[0]);
+  const ASTNode rnode = BBTerm(form[1]);
+  const ASTVec& left = lnode.GetChildren();
+  const ASTVec& right = rnode.GetChildren();
+
+  //const ASTVec& left = BBTerm(form[0]).GetChildren();
+  //const ASTVec& right = BBTerm(form[1]).GetChildren();
+
+  Kind k = form.GetKind();
+  switch(k) {
+  case BVLE: { return BBBVLE(left, right, false); break; }
+  case BVGE: { return BBBVLE(right, left, false); break; }
+  case BVGT: { return CreateSimpNot(BBBVLE(left, right, false)); break; }
+  case BVLT: { return CreateSimpNot(BBBVLE(right, left, false)); break; }
+  case BVSLE: { return BBBVLE(left, right, true); break; }
+  case BVSGE: { return BBBVLE(right, left, true); break; }
+  case BVSGT: { return CreateSimpNot(BBBVLE(left, right, true)); break; }
+  case BVSLT: { return CreateSimpNot(BBBVLE(right, left, true)); break; }
+  default:
+    cerr << "BBCompare: Illegal kind" << form << endl;    
+    FatalError("",ASTUndefined);
+  }
+  return ASTUndefined;
+}
+
+
+// return a vector with n copies of fillval
+ASTVec BeevMgr::BBfill(unsigned int width, ASTNode fillval)
+{
+  ASTVec zvec(width, fillval);
+  return zvec;
+}
+
+ASTNode BeevMgr::BBEQ(const ASTVec& left, const ASTVec& right)
+{
+  ASTVec andvec;
+  ASTVec::const_iterator lit = left.begin();
+  ASTVec::const_iterator litend = left.end();
+  ASTVec::const_iterator rit = right.begin();
+  
+  if(left.size() > 1) {
+    for(; lit != litend; lit++, rit++) {
+      ASTNode biteq = CreateSimpForm(IFF, *lit, *rit);
+      // fast path exit
+      if (biteq == ASTFalse) {
+	return ASTFalse;
+      }
+      else {
+	andvec.push_back(biteq);
+      }
+    }
+    ASTNode n = CreateSimpForm(AND, andvec);  
+    return n;
+  }
+  else
+    return CreateSimpForm(IFF,*lit,*rit);
+}
+} // BEEV namespace