void cpp_typecheckt::new_temporary(
  const source_locationt &source_location,
  const typet &type,
  const exprt::operandst &ops,
  exprt &temporary)
{
  // create temporary object
  exprt tmp_object_expr=exprt(ID_side_effect, type);
  tmp_object_expr.set(ID_statement, ID_temporary_object);
  tmp_object_expr.add_source_location()= source_location;

  exprt new_object(ID_new_object);
  new_object.add_source_location()=tmp_object_expr.source_location();
  new_object.set(ID_C_lvalue, true);
  new_object.type()=tmp_object_expr.type();

  already_typechecked(new_object);

  codet new_code =
    cpp_constructor(source_location, new_object, ops);

  if(new_code.is_not_nil())
  {
    if(new_code.get(ID_statement)==ID_assign)
      tmp_object_expr.move_to_operands(new_code.op1());
    else
      tmp_object_expr.add(ID_initializer)=new_code;
  }

  temporary.swap(tmp_object_expr);
}

void guardt::add(const exprt &expr)
{
  if(expr.id()==ID_and && expr.type().id()==ID_bool)
  {
    forall_operands(it, expr)
      add(*it);

    return;
  }

  if(expr.is_true())
  {
  }
  else
    guard_list.push_back(expr);
}

bool simplify_exprt::simplify_isinf(exprt &expr)
{
  if(expr.operands().size()!=1) return true;

  if(ns.follow(expr.op0().type()).id()!=ID_floatbv)
    return true;
 
  if(expr.op0().is_constant())
  {
    ieee_floatt value(to_constant_expr(expr.op0()));
    expr.make_bool(value.is_infinity());
    return false;
  }
  
  return true; 
}

void base_type(exprt &expr, const namespacet &ns)
{
  base_type(expr.type(), ns);

  Forall_operands(it, expr)
    base_type(*it, ns);
}

void boolbvt::convert_index(
  const exprt &array,
  const mp_integer &index,
  bvt &bv)
{
  const array_typet &array_type=
    to_array_type(ns.follow(array.type()));

  unsigned width=boolbv_width(array_type.subtype());

  if(width==0)
    return conversion_failed(array, bv);

  bv.resize(width);
  
  const bvt &tmp=convert_bv(array); // recursive call

  mp_integer offset=index*width;

  if(offset>=0 &&
     offset+width<=mp_integer(tmp.size()))
  {
    // in bounds
    for(unsigned i=0; i<width; i++)
      bv[i]=tmp[integer2long(offset+i)];
  }
  else
  {
    // out of bounds
    for(unsigned i=0; i<width; i++)
      bv[i]=prop.new_variable();
  }
}

bool clang_c_convertert::convert_integer_literal(
  const clang::IntegerLiteral &integer_literal,
  exprt &dest)
{
  typet type;
  if(get_type(integer_literal.getType(), type))
    return true;

  assert(type.is_unsignedbv() || type.is_signedbv());

  llvm::APInt val = integer_literal.getValue();

  exprt the_val;
  if (type.is_unsignedbv())
  {
    the_val =
      constant_exprt(
        integer2binary(val.getZExtValue(), bv_width(type)),
        integer2string(val.getZExtValue()),
        type);
  }
  else
  {
    the_val =
      constant_exprt(
        integer2binary(val.getSExtValue(), bv_width(type)),
        integer2string(val.getSExtValue()),
        type);
  }

  dest.swap(the_val);
  return false;
}

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

bool symex_dereference_statet::has_failed_symbol(
  const exprt &expr,
  const symbolt *&symbol)
{
  renaming_nst renaming_ns(goto_symex.ns, state);

  if(expr.id()==ID_symbol)
  {
    const symbolt &ptr_symbol=
      renaming_ns.lookup(to_symbol_expr(expr).get_identifier());

    const irep_idt &failed_symbol=
      ptr_symbol.type.get("#failed_symbol");    
      
    if(failed_symbol!="" &&
        !renaming_ns.lookup(failed_symbol, symbol))
    {
      symbolt sym=*symbol;
      symbolt *sym_ptr=0;
      sym.name=state.rename(sym.name, renaming_ns, goto_symex_statet::L1);
      goto_symex.new_symbol_table.move(sym, sym_ptr);
      symbol=sym_ptr;
      return true;
    }
  }
  
  return false;
}

void cone_of_influencet::gather_rvalues(const exprt &expr, expr_sett &rvals)
{
  if(expr.id() == ID_symbol ||
     expr.id() == ID_index ||
     expr.id() == ID_member ||
     expr.id() == ID_dereference)
  {
    rvals.insert(expr);
  }
  else
  {
    forall_operands(it, expr)
    {
      gather_rvalues(*it, rvals);
    }
  }

exprt dereferencet::dereference_typecast(
  const typecast_exprt &expr,
  const exprt &offset,
  const typet &type)
{
  const exprt &op=expr.op();
  const typet &op_type=ns.follow(op.type());

  // pointer type cast?
  if(op_type.id()==ID_pointer)
    return dereference_rec(op, offset, type); // just pass down
  else if(op_type.id()==ID_signedbv || op_type.id()==ID_unsignedbv)
  {
    // We got an integer-typed address A. We turn this back (!)
    // into *(type *)(A+offset), and then let some other layer
    // worry about it.

    exprt integer=
      plus_exprt(offset, typecast_exprt(op, offset.type()));

    exprt new_typecast=
      typecast_exprt(integer, pointer_typet(type));

    return dereference_exprt(new_typecast, type);
  }
  else
    throw "dereferencet: unexpected cast";
}

void boolbvt::convert_with_union(
  const union_typet &type,
  const exprt &op1,
  const exprt &op2,
  const bvt &prev_bv,
  bvt &next_bv)
{
  next_bv=prev_bv;

  const bvt &op2_bv=convert_bv(op2);

  if(next_bv.size()<op2_bv.size())
  {
    error().source_location=type.source_location();
    error() << "convert_with_union: unexpected operand op2 width" << eom;
    throw 0;
  }

  if(config.ansi_c.endianness==configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN)
  {
    for(std::size_t i=0; i<op2_bv.size(); i++)
      next_bv[i]=op2_bv[i];
  }
  else
  {
    assert(config.ansi_c.endianness==configt::ansi_ct::endiannesst::IS_BIG_ENDIAN);

    endianness_mapt map_u(type, false, ns);
    endianness_mapt map_op2(op2.type(), false, ns);

    for(std::size_t i=0; i<op2_bv.size(); i++)
      next_bv[map_u.map_bit(i)]=op2_bv[map_op2.map_bit(i)];
  }
}

bvt bv_refinementt::convert_mult(const exprt &expr)
{
  if(!do_arithmetic_refinement || expr.type().id()==ID_fixedbv)
    return SUB::convert_mult(expr);

  // we catch any multiplication
  // unless it involves a constant

  const exprt::operandst &operands=expr.operands();

  const typet &type=ns.follow(expr.type());

  assert(operands.size()>=2);

  if(operands.size()>2)
    return convert_mult(make_binary(expr)); // make binary

  // we keep multiplication by a constant for integers
  if(type.id()!=ID_floatbv)
    if(operands[0].is_constant() || operands[1].is_constant())
      return SUB::convert_mult(expr);

  bvt bv;
  approximationt &a=add_approximation(expr, bv);

  // initially, we have a partial interpretation for integers
  if(type.id()==ID_signedbv ||
     type.id()==ID_unsignedbv)
  {
    // x*0==0 and 0*x==0
    literalt op0_zero=bv_utils.is_zero(a.op0_bv);
    literalt op1_zero=bv_utils.is_zero(a.op1_bv);
    literalt res_zero=bv_utils.is_zero(a.result_bv);
    prop.l_set_to_true(
      prop.limplies(prop.lor(op0_zero, op1_zero), res_zero));

    // x*1==x and 1*x==x
    literalt op0_one=bv_utils.is_one(a.op0_bv);
    literalt op1_one=bv_utils.is_one(a.op1_bv);
    literalt res_op0=bv_utils.equal(a.op0_bv, a.result_bv);
    literalt res_op1=bv_utils.equal(a.op1_bv, a.result_bv);
    prop.l_set_to_true(prop.limplies(op0_one, res_op1));
    prop.l_set_to_true(prop.limplies(op1_one, res_op0));
  }

  return bv;
}

bool languaget::from_expr(
  const exprt &expr,
  std::string &code,
  const namespacet &ns)
{
  code=expr.pretty();
  return false;
}

bool goto_convertt::needs_cleaning(const exprt &expr)
{
  if(expr.id()==ID_index ||
     expr.id()==ID_dereference ||
     expr.id()==ID_sideeffect ||
     expr.id()==ID_struct ||
     expr.id()==ID_array ||
     expr.id()==ID_union ||
     expr.id()==ID_comma)
    return true;
  
  forall_operands(it, expr)
    if(needs_cleaning(*it))
      return true;
      
  return false;
}

void termination_baset::replace_nondet_sideeffects(exprt &expr)
{
  if(expr.id()=="sideeffect" &&
     expr.get("statement")=="nondet")
  {
    symbolt symbol;
    symbol.name=std::string("termination::nondet")+i2string(++nondet_counter);
    symbol.base_name=std::string("nondet")+i2string(nondet_counter);
    symbol.type=expr.type();

    expr=symbol_expr(symbol);
    shadow_context.move(symbol);
  }
  else
    Forall_operands(it, expr)
      replace_nondet_sideeffects(*it);
}

void component_exprt::gen_comp_var(
    exprt &comp_var, 
    const exprt &expr,  
    std::string suffix)
{
  std::string base;
  if (expr.id()==ID_symbol)
    base="."+id2string(to_symbol_expr(expr).get_identifier());
  else if (expr.id()==ID_constant)
    base=".const";
  else if(id_maps.find(expr.id())!=id_maps.end())
    base=".OPERATOR."+id_maps[expr.id()];
  else
    base=".OPERATOR."+id2string(expr.id());
  std::string final_name="C."+id2string(source_location.get_line())+"."+i2string(instruction_number)+"_"+i2string(component_cnt)+"_"+i2string(unique_identifier)+base+suffix;
  to_symbol_expr(comp_var).set_identifier(final_name);
}

exprt boolbvt::get(const exprt &expr) const
{
    if(expr.id()==ID_symbol ||
            expr.id()==ID_nondet_symbol)
    {
        const irep_idt &identifier=expr.get(ID_identifier);

        boolbv_mapt::mappingt::const_iterator it=
            map.mapping.find(identifier);

        if(it!=map.mapping.end())
        {
            const boolbv_mapt::map_entryt &map_entry=it->second;

            if(is_unbounded_array(map_entry.type))
                return bv_get_unbounded_array(expr);

            std::vector<bool> unknown;
            bvt bv;
            std::size_t width=map_entry.width;

            bv.resize(width);
            unknown.resize(width);

            for(std::size_t bit_nr=0; bit_nr<width; bit_nr++)
            {
                assert(bit_nr<map_entry.literal_map.size());

                if(map_entry.literal_map[bit_nr].is_set)
                {
                    unknown[bit_nr]=false;
                    bv[bit_nr]=map_entry.literal_map[bit_nr].l;
                }
                else
                {
                    unknown[bit_nr]=true;
                    bv[bit_nr].clear();
                }
            }

            return bv_get_rec(bv, unknown, 0, map_entry.type);
        }
    }

    return SUB::get(expr);
}

void goto_convertt::make_temp_symbol(
  exprt &expr,
  goto_programt &dest)
{
  const locationt location=expr.find_location();

  symbolt &new_symbol=new_tmp_symbol(expr.type());

  code_assignt assignment;
  assignment.lhs()=symbol_expr(new_symbol);
  assignment.rhs()=expr;
  assignment.location()=location;

  convert(assignment, dest);

  expr=symbol_expr(new_symbol);
}

bool simplify_exprt::simplify_sign(exprt &expr)
{
  if(expr.operands().size()!=1) return true;

  if(expr.op0().is_constant())
  {
    const typet &type=ns.follow(expr.op0().type());

    if(type.id()==ID_floatbv)
    {
      ieee_floatt value(to_constant_expr(expr.op0()));
      expr.make_bool(value.get_sign());
      return false;
    }
    else if(type.id()==ID_signedbv ||
            type.id()==ID_unsignedbv)
    {
      mp_integer value;
      if(!to_integer(expr.op0(), value))
      {
        expr.make_bool(value>=0);
        return false;
      }
    }
  }

  return true;
}

/// checks whether a termination argument implies termination
threevalt summarizer_fw_termt::check_termination_argument(exprt expr)
{
  if(expr.is_false())
    return YES;

  // should be of the form /\_i g_i=> R_i
  if(expr.id()==ID_and)
  {
    threevalt result=YES;
    for(exprt::operandst::iterator it=expr.operands().begin();
        it!=expr.operands().end(); it++)
    {
      if(it->is_true())
        result=UNKNOWN;
      if(it->id()==ID_implies)
      {
        if(it->op1().is_true())
          result=UNKNOWN;
      }
    }
    return result;
  }
  else
  {
    if(expr.id()==ID_implies)
    {
      if(expr.op1().is_true())
        return UNKNOWN;
    }
    else
      return !expr.is_true() ? YES : UNKNOWN;
  }
  return YES;
}