bvt float_utilst::sticky_right_shift(
  const bvt &op,
  const bvt &dist,
  literalt &sticky)
{
  std::size_t d=1;
  bvt result=op;
  sticky=const_literal(false);

  for(std::size_t stage=0; stage<dist.size(); stage++)
  {
    if(dist[stage]!=const_literal(false))
    {
      bvt tmp=bv_utils.shift(result, bv_utilst::LRIGHT, d);

      bvt lost_bits;

      if(d<=result.size())
        lost_bits=bv_utils.extract(result, 0, d-1);
      else
        lost_bits=result;

      sticky=prop.lor(
          prop.land(dist[stage],prop.lor(lost_bits)),
          sticky);

      result=bv_utils.select(dist[stage], tmp, result);
    }

    d=d<<1;
  }

  return result;
}

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
}

literalt z3_propt::lxor(literalt a, literalt b)
{
  if(a==const_literal(false)) return b;
  if(b==const_literal(false)) return a;
  if(a==const_literal(true)) return lnot(b);
  if(b==const_literal(true)) return lnot(a);

  literalt o=new_variable();
  lxor(a, b, o);
  return o;
}

std::string cvc_propt::cvc_literal(literalt l)
{
  if(l==const_literal(false))
    return "FALSE";
  else if(l==const_literal(true))
    return "TRUE";

  if(l.sign())
    return "(NOT l"+i2string(l.var_no())+")";  

  return "l"+i2string(l.var_no());
}

bvt float_utilst::build_constant(const ieee_floatt &src)
{
  unbiased_floatt result;

  result.sign=const_literal(src.get_sign());
  result.NaN=const_literal(src.is_NaN());
  result.infinity=const_literal(src.is_infinity());
  result.exponent=bv_utils.build_constant(src.get_exponent(), spec.e);
  result.fraction=bv_utils.build_constant(src.get_fraction(), spec.f+1);

  return pack(bias(result));
}

std::string dplib_propt::dplib_literal(literalt l)
{
  if(l==const_literal(false))
    return "FALSE";
  else if(l==const_literal(true))
    return "TRUE";

  if(l.sign())
    return "(NOT l"+std::to_string(l.var_no())+")";

  return "l"+std::to_string(l.var_no());
}

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;
}

literalt z3_propt::lselect(literalt a, literalt b, literalt c)
{
  // a?b:c = (a AND b) OR (/a AND c)
  if(a==const_literal(true)) return b;
  if(a==const_literal(false)) return c;
  if(b==c) return b;

  bvt bv;
  bv.reserve(2);
  bv.push_back(land(a, b));
  bv.push_back(land(lnot(a), c));
  return lor(bv);
}

literalt z3_propt::lxor(const bvt &bv)
{
  if(bv.size()==0) 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);

  for(unsigned i=0; i<bv.size(); i++)
    literal=lxor(bv[i], literal);

  return literal;
}

literalt aig_prop_baset::lxor(literalt a, literalt b)
{
  if(a.is_false()) return b;
  if(b.is_false()) return a;
  if(a.is_true()) return neg(b);
  if(b.is_true()) return neg(a);

  if(a==b) return const_literal(false);
  if(a==neg(b)) return const_literal(true);

  // This produces up to three nodes!
  // See convert_node for where this overhead is removed
  return lor(land(a, neg(b)), land(neg(a), b));
}

std::string smt1_propt::smt1_literal(literalt l)
{
  if(l==const_literal(false))
    return "false";
  else if(l==const_literal(true))
    return "true";
    
  std::string v="B"+i2string(l.var_no());

  if(l.sign())
    return "(not "+v+")";  

  return v;
}

void cvc_convt::convert_literal(const literalt l)
{
    if(l==const_literal(false))
        out << "FALSE";
    else if(l==const_literal(true))
        out << "TRUE";

    if(l.sign())
        out << "(NOT ";

    out << "l" << l.var_no();

    if(l.sign())
        out << ")";
}

literalt boolector_propt::lxor(literalt a, literalt b)
{
  if(a==const_literal(false)) return b;
  if(b==const_literal(false)) return a;
  if(a==const_literal(true)) return lnot(b);
  if(b==const_literal(true)) return lnot(a);

  literalt l=new_variable();
  BtorExp *result;

  result = boolector_xor(boolector_ctx, boolector_literal(a), boolector_literal(b));
  boolector_assert(boolector_ctx, boolector_iff(boolector_ctx, boolector_literal(l), result));


  return l;
}

literalt dplib_propt::lxor(literalt a, literalt b)
{
  if(a==const_literal(false))
    return b;
  if(b==const_literal(false))
    return a;
  if(a==const_literal(true))
    return !b;
  if(b==const_literal(true))
    return !a;

  literalt o=def_dplib_literal();
  out << "!(" << dplib_literal(a) << " <-> " << dplib_literal(b)
      << ");\n\n";

  return o;
}

literalt cvc_propt::lselect(literalt a, literalt b, literalt c)
{ 
  if(a==const_literal(true)) return b;
  if(a==const_literal(false)) return c;
  if(b==c) return b;

  out << "%% lselect" << std::endl;

  literalt o=def_cvc_literal();

  out << "IF " << cvc_literal(a) << " THEN "
      << cvc_literal(b) << " ELSE "
      << cvc_literal(c) << " ENDIF;"
      << std::endl << std::endl;

  return o;
}

BtorExp* boolector_propt::boolector_literal(literalt l)
{
  BtorExp *literal_l;
  std::string literal_s;

  if(l==const_literal(false))
    return boolector_false(boolector_ctx);
  else if(l==const_literal(true))
	return boolector_true(boolector_ctx);

  literal_l = convert_literal(l.var_no());

  if(l.sign())
    return boolector_not(boolector_ctx, literal_l);

  return literal_l;
}

void arrayst::add_array_Ackermann_constraints()
{
  // this is quadratic!

  // iterate over arrays
  for(unsigned i=0; i<arrays.size(); i++)
  {
    const index_sett &index_set=index_map[arrays.find_number(i)];
    
    // iterate over indices, 2x!
    for(index_sett::const_iterator
        i1=index_set.begin();
        i1!=index_set.end();
        i1++)
      for(index_sett::const_iterator
          i2=index_set.begin();
          i2!=index_set.end();
          i2++)
        if(i1!=i2)
        {
          // skip if both are constants
          if(i1->is_constant() && i2->is_constant())
            continue;
        
          // index equality
          equality_exprt indices_equal(*i1, *i2);

          if(indices_equal.op0().type()!=
             indices_equal.op1().type())
          {
            indices_equal.op1().
              make_typecast(indices_equal.op0().type());
          }
          
          literalt indices_equal_lit=convert(indices_equal);
          
          if(indices_equal_lit!=const_literal(false))
          {
            index_exprt index_expr1;
            index_expr1.type()=ns.follow(arrays[i].type()).subtype();
            index_expr1.array()=arrays[i];
            index_expr1.index()=*i1;

            index_exprt index_expr2=index_expr1;
            index_expr2.index()=*i2;
          
            equality_exprt values_equal(index_expr1, index_expr2);

            bvt implication;
            implication.reserve(2);
            implication.push_back(prop.lnot(indices_equal_lit));
            implication.push_back(convert(values_equal));
            prop.lcnf(implication);
          }
        }
  }
}