bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
{
  if(type1 == type2)
    return true;

  if(type1.id() == "symbol")
  {
    const symbolt &symbol = ns.lookup(type1);
    if(!symbol.is_type)
      throw "symbol " + id2string(symbol.name) + " is not a type";

    return type_eq(symbol.type, type2, ns);
  }

  if(type2.id() == "symbol")
  {
    const symbolt &symbol = ns.lookup(type2);
    if(!symbol.is_type)
      throw "symbol " + id2string(symbol.name) + " is not a type";

    return type_eq(type1, symbol.type, ns);
  }

  return false;
}

/**
 * Convenience function -- is the type a bitvector of some kind?
 */
bool is_bitvector(const typet &t) {
  return t.id() == ID_bv ||
         t.id() == ID_signedbv ||
         t.id() == ID_unsignedbv ||
         t.id() == ID_pointer ||
         t.id() == ID_bool;
}

/**
 * Conveniece function -- is the type unsigned?
 */
bool is_unsigned(const typet &t)
{
  return t.id()==ID_bv ||
         t.id()==ID_unsignedbv ||
         t.id()==ID_pointer ||
         t.id()==ID_bool;
}

void c_qualifierst::write(typet &dest) const
{
  if(is_constant)
    dest.set(ID_C_constant, true);
  else
    dest.remove(ID_C_constant);

  if(is_volatile)
    dest.set(ID_C_volatile, true);
  else
    dest.remove(ID_C_volatile);

  if(is_restricted)
    dest.set(ID_C_restricted, true);
  else
    dest.remove(ID_C_restricted);

  if(is_ptr32)
    dest.set(ID_C_ptr32, true);
  else
    dest.remove(ID_C_ptr32);

  if(is_ptr64)
    dest.set(ID_C_ptr64, true);
  else
    dest.remove(ID_C_ptr64);
}

void c_typecheck_baset::typecheck_typeof_type(typet &type)
{
  // retain the qualifiers as is
  c_qualifierst c_qualifiers;
  c_qualifiers.read(type);

  if(!((const exprt &)type).has_operands())
  {
    typet t=static_cast<const typet &>(type.find(ID_type_arg));
    typecheck_type(t);
    type.swap(t);
  }
  else
  {
    exprt expr=((const exprt &)type).op0();
    typecheck_expr(expr);

    // undo an implicit address-of
    if(expr.id()==ID_address_of &&
       expr.get_bool(ID_C_implicit))
    {
      assert(expr.operands().size()==1);
      exprt tmp;
      tmp.swap(expr.op0());
      expr.swap(tmp);
    }

    type.swap(expr.type());
  }
  
  c_qualifiers.write(type);
}

void c_storage_spect::read(const typet &type)
{
  if(type.id()==ID_merged_type ||
     type.id()==ID_code)
  {
    forall_subtypes(it, type)
      read(*it);
  }
  else if(type.id()==ID_static)
    is_static=true;
  else if(type.id()==ID_thread_local)
    is_thread_local=true;
  else if(type.id()==ID_inline)
    is_inline=true;
  else if(type.id()==ID_extern)
    is_extern=true;
  else if(type.id()==ID_typedef)
    is_typedef=true;
  else if(type.id()==ID_register)
    is_register=true;
  else if(type.id()==ID_weak)
    is_weak=true;
  else if(type.id()==ID_auto)
  {
    // ignore
  }
  else if(type.id()==ID_msc_declspec)
  {
    const exprt &as_expr=
      static_cast<const exprt &>(static_cast<const irept &>(type));
    forall_operands(it, as_expr)
      if(it->id()==ID_thread)
        is_thread_local=true;
  }
  else if(type.id()==ID_alias &&

 bool is_string_type(const typet &t) const
 {
   return
     (t.id()==ID_pointer || t.id()==ID_array) &&
     (t.subtype().id()==ID_signedbv || t.subtype().id()==ID_unsignedbv) &&
     (to_bitvector_type(t.subtype()).get_width()==config.ansi_c.char_width);
 }

void c_qualifierst::clear(typet &dest)
{
  dest.remove(ID_C_constant);
  dest.remove(ID_C_volatile);
  dest.remove(ID_C_restricted);
  dest.remove(ID_C_ptr32);
  dest.remove(ID_C_ptr64);
}

void ranking_synthesis_satt::adjust_type(typet &type) const
{
  if(type.id()=="bool")
  {
    type=uint_type();
    type.set("width", 1);
  }
}

void c_typecheck_baset::typecheck_symbol_type(typet &type)
{
  {
    // add prefix
    symbol_typet &symbol_type=to_symbol_type(type);
    symbol_type.set_identifier(add_language_prefix(symbol_type.get_identifier()));
  }

  // adjust identifier, if needed
  replace_symbol(type);

  const irep_idt &identifier=
    to_symbol_type(type).get_identifier();

  symbol_tablet::symbolst::const_iterator s_it=
    symbol_table.symbols.find(identifier);

  if(s_it==symbol_table.symbols.end())
  {
    err_location(type);
    str << "type symbol `" << identifier << "' not found";
    throw 0;
  }

  const symbolt &symbol=s_it->second;

  if(!symbol.is_type)
  {
    err_location(type);
    throw "expected type symbol";
  }
  
  if(symbol.is_macro)
  {
    // overwrite, but preserve (add) any qualifiers and other flags

    c_qualifierst c_qualifiers(type);
    bool is_packed=type.get_bool(ID_C_packed);
    irept alignment=type.find(ID_C_alignment);
    
    c_qualifiers+=c_qualifierst(symbol.type);
    type=symbol.type;
    c_qualifiers.write(type);
    
    if(is_packed) type.set(ID_C_packed, true);
    if(alignment.is_not_nil()) type.set(ID_C_alignment, alignment);
  }
    
  // CPROVER extensions
  if(symbol.base_name=="__CPROVER_rational")
  {
    type=rational_typet();
  }
  else if(symbol.base_name=="__CPROVER_integer")
  {
    type=integer_typet();
  }
}

static bool is_a_bv_type(const typet &type)
{
  return type.id()==ID_unsignedbv ||
         type.id()==ID_signedbv ||
         type.id()==ID_bv ||
         type.id()==ID_fixedbv ||
         type.id()==ID_floatbv ||
         type.id()==ID_c_enum_tag;
}

void c_qualifierst::clear(typet &dest)
{
  dest.remove(ID_C_constant);
  dest.remove(ID_C_volatile);
  dest.remove(ID_C_restricted);
  dest.remove(ID_C_ptr32);
  dest.remove(ID_C_ptr64);
  dest.remove(ID_C_transparent_union);
  dest.remove(ID_C_noreturn);
}

void bv_spect::from_type(const typet &type)
{
  if(type.id()==ID_unsignedbv)
    is_signed=false;
  else if(type.id()==ID_signedbv)
    is_signed=true;
  else
    assert(0);

  width=unsafe_string2unsigned(type.get_string(ID_width));
}

void bv_spect::from_type(const typet &type)
{
  if(type.id()==ID_unsignedbv)
    is_signed=false;
  else if(type.id()==ID_signedbv)
    is_signed=true;
  else
    assert(0);
  
  width=atoi(type.get(ID_width).c_str());
}

bv_semt bv_sem(const typet &type)
{
  if(type.id()==ID_bv)
    return BV_NONE;
  else if(type.id()==ID_unsignedbv)
    return BV_UNSIGNED;
  else if(type.id()==ID_signedbv)
    return BV_SIGNED;

  return BV_UNKNOWN;
}

static std::string type_max(const typet &src)
{
  if(src.id()==ID_signedbv)
    return integer2string(
      power(2, to_signedbv_type(src).get_width()-1)-1);
  else if(src.id()==ID_unsignedbv)
    return integer2string(
      power(2, to_unsignedbv_type(src).get_width()-1)-1);
  else
    assert(false);
}

bool is_void_pointer(const typet &type)
{
  if(type.id()==ID_pointer)
  {
    if(type.subtype().id()==ID_empty)
      return true;
  
    return is_void_pointer(type.subtype());
  }
  else
    return false;
}

bool cpp_typecheckt::convert_typedef(typet &type)
{
  if(type.id()==ID_merged_type &&
     type.subtypes().size()>=2 &&
     type.subtypes()[0].id()==ID_typedef)
  {
    type.subtypes().erase(type.subtypes().begin());
    return true;
  }

  return false;
}

/**
 * Return the smallest type that both t1 and t2 can be cast to without losing
 * information.
 *
 * e.g.
 *
 * join_types(unsignedbv_typet(32), unsignedbv_typet(16))=unsignedbv_typet(32)
 * join_types(signedbv_typet(16), unsignedbv_typet(16))=signedbv_typet(17)
 * join_types(signedbv_typet(32), signedbv_typet(32))=signedbv_typet(32)
 */
typet join_types(const typet &t1, const typet &t2)
{
  // Handle the simple case first...
  if(t1==t2)
  {
    return t1;
  }

  // OK, they're not the same type.  Are they both bitvectors?
  if(is_bitvector(t1) && is_bitvector(t2))
  {
    // They are.  That makes things easy!  There are three cases to consider:
    // both types are unsigned, both types are signed or there's one of each.

    bitvector_typet b1=to_bitvector_type(t1);
    bitvector_typet b2=to_bitvector_type(t2);

    if(is_unsigned(b1) && is_unsigned(b2))
    {
      // We just need to take the max of their widths.
      std::size_t width=std::max(b1.get_width(), b2.get_width());
      return unsignedbv_typet(width);
    }
    else if(is_signed(b1) && is_signed(b2))
    {
      // Again, just need to take the max of the widths.
      std::size_t width=std::max(b1.get_width(), b2.get_width());
      return signedbv_typet(width);
    }
    else
    {
      // This is the (slightly) tricky case.  If we have a signed and an
      // unsigned type, we're going to return a signed type.  And to cast
      // an unsigned type to a signed type, we need the signed type to be
      // at least one bit wider than the unsigned type we're casting from.
      std::size_t signed_width=is_signed(t1) ? b1.get_width() :
                                                 b2.get_width();
      std::size_t unsigned_width=is_signed(t1) ? b2.get_width() :
                                                   b1.get_width();
      // unsigned_width++;

      std::size_t width=std::max(signed_width, unsigned_width);

      return signedbv_typet(width);
    }
  }

  std::cerr << "Tried to join types: "
            << t1.pretty() << " and " << t2.pretty()
            << '\n';
  assert(!"Couldn't join types");
}

inline static unsigned bv_width(
  const typet &type,
  const namespacet &ns)
{
  if(type.id()==ID_c_enum_tag)
  {
    const typet &t=ns.follow_tag(to_c_enum_tag_type(type));
    assert(t.id()==ID_c_enum);
    return bv_width(t.subtype(), ns);
  }

  return unsafe_string2unsigned(type.get_string(ID_width));
}