void boolbvt::convert_with(
  const typet &type,
  const exprt &op1,
  const exprt &op2,
  const bvt &prev_bv,
  bvt &next_bv)
{
  // we only do that on arrays, bitvectors, structs, and unions

  next_bv.resize(prev_bv.size());

  if(type.id()==ID_array)
    return convert_with_array(to_array_type(type), op1, op2, prev_bv, next_bv);
  else if(type.id()==ID_bv ||
          type.id()==ID_unsignedbv ||
          type.id()==ID_signedbv)
    return convert_with_bv(type, op1, op2, prev_bv, next_bv);
  else if(type.id()==ID_struct)
    return convert_with_struct(to_struct_type(type), op1, op2, prev_bv, next_bv);
  else if(type.id()==ID_union)
    return convert_with_union(to_union_type(type), op1, op2, prev_bv, next_bv);
  else if(type.id()==ID_symbol)
    return convert_with(ns.follow(type), op1, op2, prev_bv, next_bv);

  error().source_location=type.source_location();
  error() << "unexpected with type: " << type.id();
  throw 0;
}

void boolbvt::convert_with_bv(
  const typet &type,
  const exprt &op1,
  const exprt &op2,
  const bvt &prev_bv,
  bvt &next_bv)
{
  literalt l=convert(op2);

  mp_integer op1_value;
  if(!to_integer(op1, op1_value))
  {
    next_bv=prev_bv;

    if(op1_value<next_bv.size())
      next_bv[integer2size_t(op1_value)]=l;

    return;
  }

  typet counter_type=op1.type();

  for(std::size_t i=0; i<prev_bv.size(); i++)
  {
    exprt counter=from_integer(i, counter_type);

    literalt eq_lit=convert(equal_exprt(op1, counter));

    next_bv[i]=prop.lselect(eq_lit, l, prev_bv[i]);
  }
}

void convert(const bvt &bv, vec<Lit> &dest)
{
  dest.growTo(bv.size());
  
  for(unsigned i=0; i<bv.size(); i++)
    dest[i]=Lit(bv[i].var_no(), bv[i].sign());
}

void bv_utilst::adder_no_overflow(
  bvt &sum,
  const bvt &op,
  bool subtract,
  representationt rep)
{
  const bvt tmp_op=subtract?inverted(op):op;

  if(rep==SIGNED)
  {
    // an overflow occurs if the signs of the two operands are the same
    // and the sign of the sum is the opposite

    literalt old_sign=sum[sum.size()-1];
    literalt sign_the_same=
      prop.lequal(sum[sum.size()-1], tmp_op[tmp_op.size()-1]);

    literalt carry;
    adder(sum, tmp_op, const_literal(subtract), carry);

    // result of addition in sum
    prop.l_set_to_false(
      prop.land(sign_the_same, prop.lxor(sum[sum.size()-1], old_sign)));
  }
  else if(rep==UNSIGNED)
  {
    literalt carry_out;
    adder(sum, tmp_op, const_literal(subtract), carry_out);
    prop.l_set_to(carry_out, subtract);
  }
  else
    assert(false);
}

void cvc_propt::lcnf(const bvt &bv)
{
  if(bv.empty()) return;
  bvt new_bv;

  std::set<literalt> s;

  new_bv.reserve(bv.size());

  for(bvt::const_iterator it=bv.begin(); it!=bv.end(); it++)
  {
    if(s.insert(*it).second)
      new_bv.push_back(*it);

    if(s.find(lnot(*it))!=s.end())
      return; // clause satisfied

    assert(it->var_no()<_no_variables);
  }

  assert(!new_bv.empty());

  out << "%% lcnf" << std::endl;
  out << "ASSERT ";

  for(bvt::const_iterator it=new_bv.begin(); it!=new_bv.end(); it++)
  {
    if(it!=new_bv.begin()) out << " OR ";
    out << cvc_literal(*it);
  }

  out << ";" << std::endl << std::endl;
}

bvt bv_utilst::shift(const bvt &src, const shiftt s, std::size_t dist)
{
  bvt result;
  result.resize(src.size());

  for(std::size_t i=0; i<src.size(); i++)
  {
    literalt l;

    switch(s)
    {
    case LEFT:
      l=(dist<=i?src[i-dist]:const_literal(false));
      break;

    case ARIGHT:
      l=(i+dist<src.size()?src[i+dist]:src[src.size()-1]); // sign bit
      break;

    case LRIGHT:
      l=(i+dist<src.size()?src[i+dist]:const_literal(false));
      break;

    default:
      assert(false);
    }

    result[i]=l;
  }

  return result;
}

void boolbv_mapt::get_literals(
  const irep_idt &identifier,
  const typet &type,
  const unsigned width,
  bvt &literals)
{
  map_entryt &map_entry=get_map_entry(identifier, type);

  assert(literals.size()==width);
  Forall_literals(it, literals)
  {
    literalt &l=*it;
    const unsigned bit=it-literals.begin();

    assert(bit<map_entry.literal_map.size());
    map_bitt &mb=map_entry.literal_map[bit];

    if(mb.is_set)
    {
      l=mb.l;
      continue;
    }

    l=prop.new_variable();

    mb.is_set=true;
    mb.l=l;

    #ifdef DEBUG
    std::cout << "NEW: " << identifier << ":" << bit
              << "=" << l << std::endl;
    #endif
  }

void dplib_propt::lcnf(const bvt &bv)
{
  if(bv.empty())
    return;
  bvt new_bv;

  std::set<literalt> s;

  new_bv.reserve(bv.size());

  for(bvt::const_iterator it=bv.begin(); it!=bv.end(); it++)
  {
    if(s.insert(*it).second)
      new_bv.push_back(*it);

    if(s.find(!*it)!=s.end())
      return; // clause satisfied

    assert(it->var_no()<=_no_variables);
  }

  assert(!new_bv.empty());

  out << "// lcnf\n";
  out << "AXIOM ";

  for(bvt::const_iterator it=new_bv.begin(); it!=new_bv.end(); it++)
  {
    if(it!=new_bv.begin())
      out << " | ";
    out << dplib_literal(*it);
  }

  out << ";\n\n";
}

literalt cnft::land(const bvt &bv)
{
  if(bv.size()==0) return const_literal(true);
  if(bv.size()==1) return bv[0];
  if(bv.size()==2) return land(bv[0], bv[1]);

  forall_literals(it, bv)
    if(it->is_false())
      return *it;

  if(is_all(bv, const_literal(true)))
    return const_literal(true);

  bvt new_bv;

  eliminate_duplicates(bv, new_bv);

  bvt lits(2);
  literalt literal=new_variable();
  lits[1]=neg(literal);

  forall_literals(it, new_bv)
  {
    lits[0]=pos(*it);
    lcnf(lits);
  }

void boolbvt::convert_replication(const exprt &expr, bvt &bv)
{
  unsigned width=boolbv_width(expr.type());
  
  if(width==0)
    return conversion_failed(expr, bv);

  if(expr.operands().size()!=2)
    throw "replication takes two operands";

  mp_integer times;
  if(to_integer(expr.op0(), times))
    throw "replication takes constant as first parameter";
  const unsigned u_times=integer2unsigned(times);

  const bvt &op=convert_bv(expr.op1());

  unsigned offset=0;
  bv.resize(width);

  for(unsigned i=0; i<u_times; i++)
  {
    if(op.size()+offset>width)
      throw "replication operand width too big";

    for(unsigned i=0; i<op.size(); i++)
      bv[i+offset]=op[i];

    offset+=op.size();
  }    

  if(offset!=bv.size())
    throw "replication operand width too small";
}

void boolbvt::convert_cond(const exprt &expr, bvt &bv)
{
  const exprt::operandst &operands=expr.operands();

  unsigned width=boolbv_width(expr.type());
  
  if(width==0)
    return conversion_failed(expr, bv);

  bv.resize(width);

  // make it free variables
  Forall_literals(it, bv)
    *it=prop.new_variable();

  if(operands.size()<2)
    throw "cond takes at least two operands";

  if((operands.size()%2)!=0)
    throw "number of cond operands must be even";

  if(prop.has_set_to())
  {
    bool condition=true;
    literalt previous_cond=const_literal(false);
    literalt cond_literal=const_literal(false);

    forall_operands(it, expr)
    {
      if(condition)
      {
        cond_literal=convert(*it);
        cond_literal=prop.land(prop.lnot(previous_cond), cond_literal);

        previous_cond=prop.lor(previous_cond, cond_literal);
      }
      else
      {
        const bvt &op=convert_bv(*it);

        if(bv.size()!=op.size())
        {
          std::cerr << "result size: " << bv.size()
                    << std::endl
                    << "operand: " << op.size() << std::endl
                    << it->pretty()
                    << std::endl;

          throw "size of value operand does not match";
        }

        literalt value_literal=bv_utils.equal(bv, op);

        prop.l_set_to_true(prop.limplies(cond_literal, value_literal));
      }

      condition=!condition;
    }
  }

literalt float_utilst::fraction_rounding_decision(
  const std::size_t dest_bits,
  const literalt sign,
  const bvt &fraction)
{
  assert(dest_bits<fraction.size());

  // we have too many fraction bits
  std::size_t extra_bits=fraction.size()-dest_bits;

  // more than two extra bits are superflus, and are
  // turned into a sticky bit

  literalt sticky_bit=const_literal(false);

  if(extra_bits>=2)
  {
    // We keep most-significant bits, and thus the tail is made
    // of least-significant bits.
    bvt tail=bv_utils.extract(fraction, 0, extra_bits-2);
    sticky_bit=prop.lor(tail);
  }

  // the rounding bit is the last extra bit
  assert(extra_bits>=1);
  literalt rounding_bit=fraction[extra_bits-1];

  // we get one bit of the fraction for some rounding decisions
  literalt rounding_least=fraction[extra_bits];

  // round-to-nearest (ties to even)
  literalt round_to_even=
    prop.land(rounding_bit,
              prop.lor(rounding_least, sticky_bit));

  // round up
  literalt round_to_plus_inf=
    prop.land(!sign,
              prop.lor(rounding_bit, sticky_bit));

  // round down
  literalt round_to_minus_inf=
    prop.land(sign,
              prop.lor(rounding_bit, sticky_bit));

  // round to zero
  literalt round_to_zero=
    const_literal(false);

  // now select appropriate one
  return prop.lselect(rounding_mode_bits.round_to_even, round_to_even,
         prop.lselect(rounding_mode_bits.round_to_plus_inf, round_to_plus_inf,
         prop.lselect(rounding_mode_bits.round_to_minus_inf, round_to_minus_inf,
         prop.lselect(rounding_mode_bits.round_to_zero, round_to_zero,
           prop.new_variable())))); // otherwise non-det
}

void z3_propt::eliminate_duplicates(const bvt &bv, bvt &dest)
{
  std::set<literalt> s;

  dest.reserve(bv.size());

  for(bvt::const_iterator it=bv.begin(); it!=bv.end(); it++)
  {
    if(s.insert(*it).second)
      dest.push_back(*it);
  }
}

bvt bv_utilst::select(literalt s, const bvt &a, const bvt &b)
{
  assert(a.size()==b.size());

  bvt result;

  result.resize(a.size());
  for(std::size_t i=0; i<result.size(); i++)
    result[i]=prop.lselect(s, a[i], b[i]);

  return result;
}

void float_utilst::set_rounding_mode(const bvt &src)
{
  bvt round_to_even=bv_utils.build_constant(ieee_floatt::ROUND_TO_EVEN, src.size());
  bvt round_to_plus_inf=bv_utils.build_constant(ieee_floatt::ROUND_TO_PLUS_INF, src.size());
  bvt round_to_minus_inf=bv_utils.build_constant(ieee_floatt::ROUND_TO_MINUS_INF, src.size());
  bvt round_to_zero=bv_utils.build_constant(ieee_floatt::ROUND_TO_ZERO, src.size());

  rounding_mode_bits.round_to_even=bv_utils.equal(src, round_to_even);
  rounding_mode_bits.round_to_plus_inf=bv_utils.equal(src, round_to_plus_inf);
  rounding_mode_bits.round_to_minus_inf=bv_utils.equal(src, round_to_minus_inf);
  rounding_mode_bits.round_to_zero=bv_utils.equal(src, round_to_zero);
}

literalt cvc_propt::lxor(const bvt &bv)
{
  if(bv.empty()) return const_literal(false);
  if(bv.size()==1) return bv[0];
  if(bv.size()==2) return lxor(bv[0], bv[1]);

  literalt literal=const_literal(false);

  forall_literals(it, bv)
    literal=lxor(*it, literal);

  return literal;
}

bvt bv_utilst::extract(const bvt &a, std::size_t first, std::size_t last)
{
  // preconditions
  assert(first<a.size());
  assert(last<a.size());
  assert(first<=last);

  bvt result=a;
  result.resize(last+1);
  if(first!=0) result.erase(result.begin(), result.begin()+first);

  assert(result.size()==last-first+1);
  return result;
}

bvt bv_utilst::concatenate(const bvt &a, const bvt &b) const
{
  bvt result;

  result.resize(a.size()+b.size());

  for(std::size_t i=0; i<a.size(); i++)
    result[i]=a[i];

  for(std::size_t i=0; i<b.size(); i++)
    result[i+a.size()]=b[i];

  return result;
}

literalt bv_utilst::carry_out(
  const bvt &op0,
  const bvt &op1,
  literalt carry_in)
{
  assert(op0.size()==op1.size());

  literalt carry_out=carry_in;

  for(std::size_t i=0; i<op0.size(); i++)
    carry_out=carry(op0[i], op1[i], carry_out);

  return carry_out;
}

void bv_utilst::adder(
  bvt &sum,
  const bvt &op,
  literalt carry_in,
  literalt &carry_out)
{
  assert(sum.size()==op.size());

  carry_out=carry_in;

  for(std::size_t i=0; i<sum.size(); i++)
  {
    sum[i] = full_adder(sum[i], op[i], carry_out, carry_out);
  }
}