std_expr.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: API to expression classes
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
 
#ifndef CPROVER_UTIL_STD_EXPR_H
#define CPROVER_UTIL_STD_EXPR_H
 
 
#include "expr_cast.h"
#include "invariant.h"
#include "std_types.h"
 
class nullary_exprt : public expr_protectedt
{
public:
  nullary_exprt(const irep_idt &_id, typet _type)
    : expr_protectedt(_id, std::move(_type))
  {
  }
 
  static void check(
    const exprt &expr,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    DATA_CHECK(
      vm,
      expr.operands().size() == 0,
      "nullary expression must not have operands");
  }
 
  static void validate(
    const exprt &expr,
    const namespacet &,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    check(expr, vm);
  }
 
  operandst &operands() = delete;
  const operandst &operands() const = delete;
 
  const exprt &op0() const = delete;
  exprt &op0() = delete;
  const exprt &op1() const = delete;
  exprt &op1() = delete;
  const exprt &op2() const = delete;
  exprt &op2() = delete;
  const exprt &op3() const = delete;
  exprt &op3() = delete;
 
  void copy_to_operands(const exprt &expr) = delete;
  void copy_to_operands(const exprt &, const exprt &) = delete;
  void copy_to_operands(const exprt &, const exprt &, const exprt &) = delete;
};
 
class ternary_exprt : public expr_protectedt
{
public:
  // constructor
  ternary_exprt(
    const irep_idt &_id,
    exprt _op0,
    exprt _op1,
    exprt _op2,
    typet _type)
    : expr_protectedt(
        _id,
        std::move(_type),
        {std::move(_op0), std::move(_op1), std::move(_op2)})
  {
  }
 
  // make op0 to op2 public
  using exprt::op0;
  using exprt::op1;
  using exprt::op2;
 
  const exprt &op3() const = delete;
  exprt &op3() = delete;
 
  static void check(
    const exprt &expr,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    DATA_CHECK(
      vm,
      expr.operands().size() == 3,
      "ternary expression must have three operands");
  }
 
  static void validate(
    const exprt &expr,
    const namespacet &,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    check(expr, vm);
  }
};
 
inline const ternary_exprt &to_ternary_expr(const exprt &expr)
{
  ternary_exprt::check(expr);
  return static_cast<const ternary_exprt &>(expr);
}
 
inline ternary_exprt &to_ternary_expr(exprt &expr)
{
  ternary_exprt::check(expr);
  return static_cast<ternary_exprt &>(expr);
}
 
class symbol_exprt : public nullary_exprt
{
public:
  explicit symbol_exprt(typet type) : nullary_exprt(ID_symbol, std::move(type))
  {
  }
 
  symbol_exprt(const irep_idt &identifier, typet type)
    : nullary_exprt(ID_symbol, std::move(type))
  {
    set_identifier(identifier);
  }
 
  static symbol_exprt typeless(const irep_idt &id)
  {
    return symbol_exprt(id, typet());
  }
 
  void set_identifier(const irep_idt &identifier)
  {
    set(ID_identifier, identifier);
  }
 
  const irep_idt &get_identifier() const
  {
    return get(ID_identifier);
  }
 
  symbol_exprt &with_source_location(source_locationt location) &
  {
    if(location.is_not_nil())
      add_source_location() = std::move(location);
    return *this;
  }
 
  symbol_exprt &&with_source_location(source_locationt location) &&
  {
    if(location.is_not_nil())
      add_source_location() = std::move(location);
    return std::move(*this);
  }
 
  symbol_exprt &with_source_location(const exprt &other) &
  {
    if(other.source_location().is_not_nil())
      add_source_location() = other.source_location();
    return *this;
  }
 
  symbol_exprt &&with_source_location(const exprt &other) &&
  {
    if(other.source_location().is_not_nil())
      add_source_location() = other.source_location();
    return std::move(*this);
  }
};
 
// NOLINTNEXTLINE(readability/namespace)
namespace std
{
template <>
// NOLINTNEXTLINE(readability/identifiers)
struct hash<::symbol_exprt>
{
  size_t operator()(const ::symbol_exprt &sym)
  {
    return irep_id_hash()(sym.get_identifier());
  }
};
} // namespace std
 
class decorated_symbol_exprt:public symbol_exprt
{
public:
  decorated_symbol_exprt(const irep_idt &identifier, typet type)
    : symbol_exprt(identifier, std::move(type))
  {
  }
 
  bool is_static_lifetime() const
  {
    return get_bool(ID_C_static_lifetime);
  }
 
  void set_static_lifetime()
  {
    return set(ID_C_static_lifetime, true);
  }
 
  void clear_static_lifetime()
  {
    remove(ID_C_static_lifetime);
  }
 
  bool is_thread_local() const
  {
    return get_bool(ID_C_thread_local);
  }
 
  void set_thread_local()
  {
    return set(ID_C_thread_local, true);
  }
 
  void clear_thread_local()
  {
    remove(ID_C_thread_local);
  }
};
 
template <>
inline bool can_cast_expr<symbol_exprt>(const exprt &base)
{
  return base.id() == ID_symbol;
}
 
inline void validate_expr(const symbol_exprt &value)
{
  validate_operands(value, 0, "Symbols must not have operands");
}
 
inline const symbol_exprt &to_symbol_expr(const exprt &expr)
{
  PRECONDITION(expr.id()==ID_symbol);
  const symbol_exprt &ret = static_cast<const symbol_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
inline symbol_exprt &to_symbol_expr(exprt &expr)
{
  PRECONDITION(expr.id()==ID_symbol);
  symbol_exprt &ret = static_cast<symbol_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
 
class nondet_symbol_exprt : public nullary_exprt
{
public:
  nondet_symbol_exprt(const irep_idt &identifier, typet type)
    : nullary_exprt(ID_nondet_symbol, std::move(type))
  {
    set_identifier(identifier);
  }
 
  nondet_symbol_exprt(
    irep_idt identifier,
    typet type,
    source_locationt location)
    : nullary_exprt(ID_nondet_symbol, std::move(type))
  {
    set_identifier(std::move(identifier));
    add_source_location() = std::move(location);
  }
 
  void set_identifier(const irep_idt &identifier)
  {
    set(ID_identifier, identifier);
  }
 
  const irep_idt &get_identifier() const
  {
    return get(ID_identifier);
  }
};
 
template <>
inline bool can_cast_expr<nondet_symbol_exprt>(const exprt &base)
{
  return base.id() == ID_nondet_symbol;
}
 
inline void validate_expr(const nondet_symbol_exprt &value)
{
  validate_operands(value, 0, "Symbols must not have operands");
}
 
inline const nondet_symbol_exprt &to_nondet_symbol_expr(const exprt &expr)
{
  PRECONDITION(expr.id()==ID_nondet_symbol);
  nondet_symbol_exprt::check(expr);
  return static_cast<const nondet_symbol_exprt &>(expr);
}
 
inline nondet_symbol_exprt &to_nondet_symbol_expr(exprt &expr)
{
  PRECONDITION(expr.id()==ID_symbol);
  nondet_symbol_exprt::check(expr);
  return static_cast<nondet_symbol_exprt &>(expr);
}
 
 
class unary_exprt : public expr_protectedt
{
public:
  unary_exprt(const irep_idt &_id, const exprt &_op)
    : expr_protectedt(_id, _op.type(), {_op})
  {
  }
 
  unary_exprt(const irep_idt &_id, exprt _op, typet _type)
    : expr_protectedt(_id, std::move(_type), {std::move(_op)})
  {
  }
 
  static void check(
    const exprt &expr,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    DATA_CHECK(
      vm,
      expr.operands().size() == 1,
      "unary expression must have one operand");
  }
 
  static void validate(
    const exprt &expr,
    const namespacet &,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    check(expr, vm);
  }
 
  const exprt &op() const
  {
    return op0();
  }
 
  exprt &op()
  {
    return op0();
  }
 
  const exprt &op1() const = delete;
  exprt &op1() = delete;
  const exprt &op2() const = delete;
  exprt &op2() = delete;
  const exprt &op3() const = delete;
  exprt &op3() = delete;
};
 
template <>
inline bool can_cast_expr<unary_exprt>(const exprt &base)
{
  return base.operands().size() == 1;
}
 
inline void validate_expr(const unary_exprt &value)
{
  unary_exprt::check(value);
}
 
inline const unary_exprt &to_unary_expr(const exprt &expr)
{
  unary_exprt::check(expr);
  return static_cast<const unary_exprt &>(expr);
}
 
inline unary_exprt &to_unary_expr(exprt &expr)
{
  unary_exprt::check(expr);
  return static_cast<unary_exprt &>(expr);
}
 
 
class abs_exprt:public unary_exprt
{
public:
  explicit abs_exprt(exprt _op) : unary_exprt(ID_abs, std::move(_op))
  {
  }
};
 
template <>
inline bool can_cast_expr<abs_exprt>(const exprt &base)
{
  return base.id() == ID_abs;
}
 
inline void validate_expr(const abs_exprt &value)
{
  validate_operands(value, 1, "Absolute value must have one operand");
}
 
inline const abs_exprt &to_abs_expr(const exprt &expr)
{
  PRECONDITION(expr.id()==ID_abs);
  abs_exprt::check(expr);
  return static_cast<const abs_exprt &>(expr);
}
 
inline abs_exprt &to_abs_expr(exprt &expr)
{
  PRECONDITION(expr.id()==ID_abs);
  abs_exprt::check(expr);
  return static_cast<abs_exprt &>(expr);
}
 
 
class unary_minus_exprt:public unary_exprt
{
public:
  unary_minus_exprt(exprt _op, typet _type)
    : unary_exprt(ID_unary_minus, std::move(_op), std::move(_type))
  {
  }
 
  explicit unary_minus_exprt(exprt _op)
    : unary_exprt(ID_unary_minus, std::move(_op))
  {
  }
};
 
template <>
inline bool can_cast_expr<unary_minus_exprt>(const exprt &base)
{
  return base.id() == ID_unary_minus;
}
 
inline void validate_expr(const unary_minus_exprt &value)
{
  validate_operands(value, 1, "Unary minus must have one operand");
}
 
inline const unary_minus_exprt &to_unary_minus_expr(const exprt &expr)
{
  PRECONDITION(expr.id()==ID_unary_minus);
  unary_minus_exprt::check(expr);
  return static_cast<const unary_minus_exprt &>(expr);
}
 
inline unary_minus_exprt &to_unary_minus_expr(exprt &expr)
{
  PRECONDITION(expr.id()==ID_unary_minus);
  unary_minus_exprt::check(expr);
  return static_cast<unary_minus_exprt &>(expr);
}
 
class unary_plus_exprt : public unary_exprt
{
public:
  explicit unary_plus_exprt(exprt op)
    : unary_exprt(ID_unary_plus, std::move(op))
  {
  }
};
 
template <>
inline bool can_cast_expr<unary_plus_exprt>(const exprt &base)
{
  return base.id() == ID_unary_plus;
}
 
inline void validate_expr(const unary_plus_exprt &value)
{
  validate_operands(value, 1, "unary plus must have one operand");
}
 
inline const unary_plus_exprt &to_unary_plus_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_unary_plus);
  unary_plus_exprt::check(expr);
  return static_cast<const unary_plus_exprt &>(expr);
}
 
inline unary_plus_exprt &to_unary_plus_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_unary_plus);
  unary_plus_exprt::check(expr);
  return static_cast<unary_plus_exprt &>(expr);
}
 
class predicate_exprt : public expr_protectedt
{
public:
  explicit predicate_exprt(const irep_idt &_id)
    : expr_protectedt(_id, bool_typet())
  {
  }
};
 
class unary_predicate_exprt:public unary_exprt
{
public:
  unary_predicate_exprt(const irep_idt &_id, exprt _op)
    : unary_exprt(_id, std::move(_op), bool_typet())
  {
  }
};
 
class sign_exprt:public unary_predicate_exprt
{
public:
  explicit sign_exprt(exprt _op)
    : unary_predicate_exprt(ID_sign, std::move(_op))
  {
  }
};
 
template <>
inline bool can_cast_expr<sign_exprt>(const exprt &base)
{
  return base.id() == ID_sign;
}
 
inline void validate_expr(const sign_exprt &expr)
{
  validate_operands(expr, 1, "sign expression must have one operand");
}
 
inline const sign_exprt &to_sign_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_sign);
  sign_exprt::check(expr);
  return static_cast<const sign_exprt &>(expr);
}
 
inline sign_exprt &to_sign_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_sign);
  sign_exprt::check(expr);
  return static_cast<sign_exprt &>(expr);
}
 
class binary_exprt : public expr_protectedt
{
public:
  binary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
    : expr_protectedt(_id, _lhs.type(), {_lhs, std::move(_rhs)})
  {
  }
 
  binary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
    : expr_protectedt(_id, std::move(_type), {std::move(_lhs), std::move(_rhs)})
  {
  }
 
  static void check(
    const exprt &expr,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    DATA_CHECK(
      vm,
      expr.operands().size() == 2,
      "binary expression must have two operands");
  }
 
  static void validate(
    const exprt &expr,
    const namespacet &,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    check(expr, vm);
  }
 
  exprt &lhs()
  {
    return exprt::op0();
  }
 
  const exprt &lhs() const
  {
    return exprt::op0();
  }
 
  exprt &rhs()
  {
    return exprt::op1();
  }
 
  const exprt &rhs() const
  {
    return exprt::op1();
  }
 
  // make op0 and op1 public
  using exprt::op0;
  using exprt::op1;
 
  const exprt &op2() const = delete;
  exprt &op2() = delete;
  const exprt &op3() const = delete;
  exprt &op3() = delete;
};
 
template <>
inline bool can_cast_expr<binary_exprt>(const exprt &base)
{
  return base.operands().size() == 2;
}
 
inline void validate_expr(const binary_exprt &value)
{
  binary_exprt::check(value);
}
 
inline const binary_exprt &to_binary_expr(const exprt &expr)
{
  binary_exprt::check(expr);
  return static_cast<const binary_exprt &>(expr);
}
 
inline binary_exprt &to_binary_expr(exprt &expr)
{
  binary_exprt::check(expr);
  return static_cast<binary_exprt &>(expr);
}
 
class binary_predicate_exprt:public binary_exprt
{
public:
  binary_predicate_exprt(exprt _op0, const irep_idt &_id, exprt _op1)
    : binary_exprt(std::move(_op0), _id, std::move(_op1), bool_typet())
  {
  }
 
  static void check(
    const exprt &expr,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    binary_exprt::check(expr, vm);
  }
 
  static void validate(
    const exprt &expr,
    const namespacet &ns,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    binary_exprt::validate(expr, ns, vm);
 
    DATA_CHECK(
      vm,
      expr.is_boolean(),
      "result of binary predicate expression should be of type bool");
  }
};
 
class binary_relation_exprt:public binary_predicate_exprt
{
public:
  binary_relation_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs)
    : binary_predicate_exprt(std::move(_lhs), _id, std::move(_rhs))
  {
  }
 
  static void check(
    const exprt &expr,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    binary_predicate_exprt::check(expr, vm);
  }
 
  static void validate(
    const exprt &expr,
    const namespacet &ns,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    binary_predicate_exprt::validate(expr, ns, vm);
 
    // we now can safely assume that 'expr' is a binary predicate
    const auto &expr_binary = static_cast<const binary_predicate_exprt &>(expr);
 
    // check that the types of the operands are the same
    DATA_CHECK(
      vm,
      expr_binary.op0().type() == expr_binary.op1().type(),
      "lhs and rhs of binary relation expression should have same type");
  }
};
 
template <>
inline bool can_cast_expr<binary_relation_exprt>(const exprt &base)
{
  return can_cast_expr<binary_exprt>(base);
}
 
inline void validate_expr(const binary_relation_exprt &value)
{
  binary_relation_exprt::check(value);
}
 
class greater_than_exprt : public binary_relation_exprt
{
public:
  greater_than_exprt(exprt _lhs, exprt _rhs)
    : binary_relation_exprt{std::move(_lhs), ID_gt, std::move(_rhs)}
  {
  }
};
 
template <>
inline bool can_cast_expr<greater_than_exprt>(const exprt &base)
{
  return base.id() == ID_gt;
}
 
inline void validate_expr(const greater_than_exprt &value)
{
  binary_relation_exprt::check(value);
}
 
class greater_than_or_equal_exprt : public binary_relation_exprt
{
public:
  greater_than_or_equal_exprt(exprt _lhs, exprt _rhs)
    : binary_relation_exprt{std::move(_lhs), ID_ge, std::move(_rhs)}
  {
  }
};
 
template <>
inline bool can_cast_expr<greater_than_or_equal_exprt>(const exprt &base)
{
  return base.id() == ID_ge;
}
 
inline void validate_expr(const greater_than_or_equal_exprt &value)
{
  binary_relation_exprt::check(value);
}
 
class less_than_exprt : public binary_relation_exprt
{
public:
  less_than_exprt(exprt _lhs, exprt _rhs)
    : binary_relation_exprt{std::move(_lhs), ID_lt, std::move(_rhs)}
  {
  }
};
 
template <>
inline bool can_cast_expr<less_than_exprt>(const exprt &base)
{
  return base.id() == ID_lt;
}
 
inline void validate_expr(const less_than_exprt &value)
{
  binary_relation_exprt::check(value);
}
 
class less_than_or_equal_exprt : public binary_relation_exprt
{
public:
  less_than_or_equal_exprt(exprt _lhs, exprt _rhs)
    : binary_relation_exprt{std::move(_lhs), ID_le, std::move(_rhs)}
  {
  }
};
 
template <>
inline bool can_cast_expr<less_than_or_equal_exprt>(const exprt &base)
{
  return base.id() == ID_le;
}
 
inline void validate_expr(const less_than_or_equal_exprt &value)
{
  binary_relation_exprt::check(value);
}
 
inline const binary_relation_exprt &to_binary_relation_expr(const exprt &expr)
{
  binary_relation_exprt::check(expr);
  return static_cast<const binary_relation_exprt &>(expr);
}
 
inline binary_relation_exprt &to_binary_relation_expr(exprt &expr)
{
  binary_relation_exprt::check(expr);
  return static_cast<binary_relation_exprt &>(expr);
}
 
 
class multi_ary_exprt : public expr_protectedt
{
public:
  multi_ary_exprt(const irep_idt &_id, operandst _operands, typet _type)
    : expr_protectedt(_id, std::move(_type))
  {
    operands() = std::move(_operands);
  }
 
  multi_ary_exprt(const irep_idt &_id, operandst _operands)
    : expr_protectedt(_id, typet{})
  {
    PRECONDITION(!_operands.empty());
    type() = _operands.front().type();
    operands() = std::move(_operands);
  }
 
  multi_ary_exprt(const exprt &_lhs, const irep_idt &_id, exprt _rhs)
    : expr_protectedt(_id, _lhs.type(), {_lhs, std::move(_rhs)})
  {
  }
 
  multi_ary_exprt(exprt _lhs, const irep_idt &_id, exprt _rhs, typet _type)
    : expr_protectedt(_id, std::move(_type), {std::move(_lhs), std::move(_rhs)})
  {
  }
 
  // In contrast to exprt::opX, the methods
  // below check the size.
  exprt &op0()
  {
    PRECONDITION(operands().size() >= 1);
    return operands().front();
  }
 
  exprt &op1()
  {
    PRECONDITION(operands().size() >= 2);
    return operands()[1];
  }
 
  exprt &op2()
  {
    PRECONDITION(operands().size() >= 3);
    return operands()[2];
  }
 
  exprt &op3()
  {
    PRECONDITION(operands().size() >= 4);
    return operands()[3];
  }
 
  const exprt &op0() const
  {
    PRECONDITION(operands().size() >= 1);
    return operands().front();
  }
 
  const exprt &op1() const
  {
    PRECONDITION(operands().size() >= 2);
    return operands()[1];
  }
 
  const exprt &op2() const
  {
    PRECONDITION(operands().size() >= 3);
    return operands()[2];
  }
 
  const exprt &op3() const
  {
    PRECONDITION(operands().size() >= 4);
    return operands()[3];
  }
};
 
inline const multi_ary_exprt &to_multi_ary_expr(const exprt &expr)
{
  return static_cast<const multi_ary_exprt &>(expr);
}
 
inline multi_ary_exprt &to_multi_ary_expr(exprt &expr)
{
  return static_cast<multi_ary_exprt &>(expr);
}
 
 
class plus_exprt:public multi_ary_exprt
{
public:
  plus_exprt(exprt _lhs, exprt _rhs)
    : multi_ary_exprt(std::move(_lhs), ID_plus, std::move(_rhs))
  {
  }
 
  plus_exprt(exprt _lhs, exprt _rhs, typet _type)
    : multi_ary_exprt(
        std::move(_lhs),
        ID_plus,
        std::move(_rhs),
        std::move(_type))
  {
  }
 
  explicit plus_exprt(operandst _operands)
    : multi_ary_exprt(ID_plus, std::move(_operands))
  {
  }
 
  plus_exprt(operandst _operands, typet _type)
    : multi_ary_exprt(ID_plus, std::move(_operands), std::move(_type))
  {
  }
};
 
template <>
inline bool can_cast_expr<plus_exprt>(const exprt &base)
{
  return base.id() == ID_plus;
}
 
inline void validate_expr(const plus_exprt &value)
{
  validate_operands(value, 2, "Plus must have two or more operands", true);
}
 
inline const plus_exprt &to_plus_expr(const exprt &expr)
{
  PRECONDITION(expr.id()==ID_plus);
  const plus_exprt &ret = static_cast<const plus_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
inline plus_exprt &to_plus_expr(exprt &expr)
{
  PRECONDITION(expr.id()==ID_plus);
  plus_exprt &ret = static_cast<plus_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
 
class minus_exprt:public binary_exprt
{
public:
  minus_exprt(exprt _lhs, exprt _rhs)
    : binary_exprt(std::move(_lhs), ID_minus, std::move(_rhs))
  {
  }
};
 
template <>
inline bool can_cast_expr<minus_exprt>(const exprt &base)
{
  return base.id() == ID_minus;
}
 
inline void validate_expr(const minus_exprt &value)
{
  validate_operands(value, 2, "Minus must have two or more operands", true);
}
 
inline const minus_exprt &to_minus_expr(const exprt &expr)
{
  PRECONDITION(expr.id()==ID_minus);
  const minus_exprt &ret = static_cast<const minus_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
inline minus_exprt &to_minus_expr(exprt &expr)
{
  PRECONDITION(expr.id()==ID_minus);
  minus_exprt &ret = static_cast<minus_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
 
class mult_exprt:public multi_ary_exprt
{
public:
  mult_exprt(exprt _lhs, exprt _rhs)
    : multi_ary_exprt(std::move(_lhs), ID_mult, std::move(_rhs))
  {
  }
 
  explicit mult_exprt(exprt::operandst factors)
    : multi_ary_exprt(ID_mult, std::move(factors))
  {
  }
 
  mult_exprt(exprt::operandst factors, typet type)
    : multi_ary_exprt(ID_mult, std::move(factors), std::move(type))
  {
  }
};
 
template <>
inline bool can_cast_expr<mult_exprt>(const exprt &base)
{
  return base.id() == ID_mult;
}
 
inline void validate_expr(const mult_exprt &value)
{
  validate_operands(value, 2, "Multiply must have two or more operands", true);
}
 
inline const mult_exprt &to_mult_expr(const exprt &expr)
{
  PRECONDITION(expr.id()==ID_mult);
  const mult_exprt &ret = static_cast<const mult_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
inline mult_exprt &to_mult_expr(exprt &expr)
{
  PRECONDITION(expr.id()==ID_mult);
  mult_exprt &ret = static_cast<mult_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
 
class div_exprt:public binary_exprt
{
public:
  div_exprt(exprt _lhs, exprt _rhs)
    : binary_exprt(std::move(_lhs), ID_div, std::move(_rhs))
  {
  }
 
  exprt &dividend()
  {
    return op0();
  }
 
  const exprt &dividend() const
  {
    return op0();
  }
 
  exprt &divisor()
  {
    return op1();
  }
 
  const exprt &divisor() const
  {
    return op1();
  }
};
 
template <>
inline bool can_cast_expr<div_exprt>(const exprt &base)
{
  return base.id() == ID_div;
}
 
inline void validate_expr(const div_exprt &value)
{
  validate_operands(value, 2, "Divide must have two operands");
}
 
inline const div_exprt &to_div_expr(const exprt &expr)
{
  PRECONDITION(expr.id()==ID_div);
  const div_exprt &ret = static_cast<const div_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
inline div_exprt &to_div_expr(exprt &expr)
{
  PRECONDITION(expr.id()==ID_div);
  div_exprt &ret = static_cast<div_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
class mod_exprt:public binary_exprt
{
public:
  mod_exprt(exprt _lhs, exprt _rhs)
    : binary_exprt(std::move(_lhs), ID_mod, std::move(_rhs))
  {
  }
 
  exprt &dividend()
  {
    return op0();
  }
 
  const exprt &dividend() const
  {
    return op0();
  }
 
  exprt &divisor()
  {
    return op1();
  }
 
  const exprt &divisor() const
  {
    return op1();
  }
};
 
template <>
inline bool can_cast_expr<mod_exprt>(const exprt &base)
{
  return base.id() == ID_mod;
}
 
inline void validate_expr(const mod_exprt &value)
{
  validate_operands(value, 2, "Modulo must have two operands");
}
 
inline const mod_exprt &to_mod_expr(const exprt &expr)
{
  PRECONDITION(expr.id()==ID_mod);
  const mod_exprt &ret = static_cast<const mod_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
inline mod_exprt &to_mod_expr(exprt &expr)
{
  PRECONDITION(expr.id()==ID_mod);
  mod_exprt &ret = static_cast<mod_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
class euclidean_mod_exprt : public binary_exprt
{
public:
  euclidean_mod_exprt(exprt _lhs, exprt _rhs)
    : binary_exprt(std::move(_lhs), ID_euclidean_mod, std::move(_rhs))
  {
  }
 
  exprt &dividend()
  {
    return op0();
  }
 
  const exprt &dividend() const
  {
    return op0();
  }
 
  exprt &divisor()
  {
    return op1();
  }
 
  const exprt &divisor() const
  {
    return op1();
  }
};
 
template <>
inline bool can_cast_expr<euclidean_mod_exprt>(const exprt &base)
{
  return base.id() == ID_euclidean_mod;
}
 
inline void validate_expr(const euclidean_mod_exprt &value)
{
  validate_operands(value, 2, "Modulo must have two operands");
}
 
inline const euclidean_mod_exprt &to_euclidean_mod_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_euclidean_mod);
  const euclidean_mod_exprt &ret =
    static_cast<const euclidean_mod_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
inline euclidean_mod_exprt &to_euclidean_mod_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_euclidean_mod);
  euclidean_mod_exprt &ret = static_cast<euclidean_mod_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
 
class equal_exprt:public binary_relation_exprt
{
public:
  equal_exprt(exprt _lhs, exprt _rhs)
    : binary_relation_exprt(std::move(_lhs), ID_equal, std::move(_rhs))
  {
    PRECONDITION(lhs().type() == rhs().type());
  }
 
  static void check(
    const exprt &expr,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    binary_relation_exprt::check(expr, vm);
  }
 
  static void validate(
    const exprt &expr,
    const namespacet &ns,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    binary_relation_exprt::validate(expr, ns, vm);
  }
};
 
template <>
inline bool can_cast_expr<equal_exprt>(const exprt &base)
{
  return base.id() == ID_equal;
}
 
inline void validate_expr(const equal_exprt &value)
{
  equal_exprt::check(value);
}
 
inline const equal_exprt &to_equal_expr(const exprt &expr)
{
  PRECONDITION(expr.id()==ID_equal);
  equal_exprt::check(expr);
  return static_cast<const equal_exprt &>(expr);
}
 
inline equal_exprt &to_equal_expr(exprt &expr)
{
  PRECONDITION(expr.id()==ID_equal);
  equal_exprt::check(expr);
  return static_cast<equal_exprt &>(expr);
}
 
 
class notequal_exprt:public binary_relation_exprt
{
public:
  notequal_exprt(exprt _lhs, exprt _rhs)
    : binary_relation_exprt(std::move(_lhs), ID_notequal, std::move(_rhs))
  {
  }
};
 
template <>
inline bool can_cast_expr<notequal_exprt>(const exprt &base)
{
  return base.id() == ID_notequal;
}
 
inline void validate_expr(const notequal_exprt &value)
{
  validate_operands(value, 2, "Inequality must have two operands");
}
 
inline const notequal_exprt &to_notequal_expr(const exprt &expr)
{
  PRECONDITION(expr.id()==ID_notequal);
  const notequal_exprt &ret = static_cast<const notequal_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
inline notequal_exprt &to_notequal_expr(exprt &expr)
{
  PRECONDITION(expr.id()==ID_notequal);
  notequal_exprt &ret = static_cast<notequal_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
 
class index_exprt:public binary_exprt
{
public:
  // _array must have either index or vector type.
  // When _array has array_type, the type of _index
  // must be array_type.index_type().
  // This will eventually be enforced using a precondition.
  index_exprt(const exprt &_array, exprt _index)
    : binary_exprt(
        _array,
        ID_index,
        std::move(_index),
        to_type_with_subtype(_array.type()).subtype())
  {
    const auto &array_op_type = _array.type();
    PRECONDITION(
      array_op_type.id() == ID_array || array_op_type.id() == ID_vector);
  }
 
  index_exprt(exprt _array, exprt _index, typet _type)
    : binary_exprt(
        std::move(_array),
        ID_index,
        std::move(_index),
        std::move(_type))
  {
    const auto &array_op_type = array().type();
    PRECONDITION(
      array_op_type.id() == ID_array || array_op_type.id() == ID_vector);
  }
 
  exprt &array()
  {
    return op0();
  }
 
  const exprt &array() const
  {
    return op0();
  }
 
  exprt &index()
  {
    return op1();
  }
 
  const exprt &index() const
  {
    return op1();
  }
};
 
template <>
inline bool can_cast_expr<index_exprt>(const exprt &base)
{
  return base.id() == ID_index;
}
 
inline void validate_expr(const index_exprt &value)
{
  validate_operands(value, 2, "Array index must have two operands");
}
 
inline const index_exprt &to_index_expr(const exprt &expr)
{
  PRECONDITION(expr.id()==ID_index);
  const index_exprt &ret = static_cast<const index_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
inline index_exprt &to_index_expr(exprt &expr)
{
  PRECONDITION(expr.id()==ID_index);
  index_exprt &ret = static_cast<index_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
 
class array_of_exprt:public unary_exprt
{
public:
  explicit array_of_exprt(exprt _what, array_typet _type)
    : unary_exprt(ID_array_of, std::move(_what), std::move(_type))
  {
  }
 
  const array_typet &type() const
  {
    return static_cast<const array_typet &>(unary_exprt::type());
  }
 
  array_typet &type()
  {
    return static_cast<array_typet &>(unary_exprt::type());
  }
 
  exprt &what()
  {
    return op0();
  }
 
  const exprt &what() const
  {
    return op0();
  }
};
 
template <>
inline bool can_cast_expr<array_of_exprt>(const exprt &base)
{
  return base.id() == ID_array_of;
}
 
inline void validate_expr(const array_of_exprt &value)
{
  validate_operands(value, 1, "'Array of' must have one operand");
}
 
inline const array_of_exprt &to_array_of_expr(const exprt &expr)
{
  PRECONDITION(expr.id()==ID_array_of);
  array_of_exprt::check(expr);
  return static_cast<const array_of_exprt &>(expr);
}
 
inline array_of_exprt &to_array_of_expr(exprt &expr)
{
  PRECONDITION(expr.id()==ID_array_of);
  array_of_exprt::check(expr);
  return static_cast<array_of_exprt &>(expr);
}
 
 
class array_exprt : public multi_ary_exprt
{
public:
  array_exprt(operandst _operands, array_typet _type)
    : multi_ary_exprt(ID_array, std::move(_operands), std::move(_type))
  {
  }
 
  const array_typet &type() const
  {
    return static_cast<const array_typet &>(multi_ary_exprt::type());
  }
 
  array_typet &type()
  {
    return static_cast<array_typet &>(multi_ary_exprt::type());
  }
 
  array_exprt &with_source_location(const exprt &other) &
  {
    if(other.source_location().is_not_nil())
      add_source_location() = other.source_location();
    return *this;
  }
 
  array_exprt &&with_source_location(const exprt &other) &&
  {
    if(other.source_location().is_not_nil())
      add_source_location() = other.source_location();
    return std::move(*this);
  }
};
 
template <>
inline bool can_cast_expr<array_exprt>(const exprt &base)
{
  return base.id() == ID_array;
}
 
inline const array_exprt &to_array_expr(const exprt &expr)
{
  PRECONDITION(expr.id()==ID_array);
  return static_cast<const array_exprt &>(expr);
}
 
inline array_exprt &to_array_expr(exprt &expr)
{
  PRECONDITION(expr.id()==ID_array);
  return static_cast<array_exprt &>(expr);
}
 
class array_list_exprt : public multi_ary_exprt
{
public:
  array_list_exprt(operandst _operands, array_typet _type)
    : multi_ary_exprt(ID_array_list, std::move(_operands), std::move(_type))
  {
  }
 
  const array_typet &type() const
  {
    return static_cast<const array_typet &>(multi_ary_exprt::type());
  }
 
  array_typet &type()
  {
    return static_cast<array_typet &>(multi_ary_exprt::type());
  }
 
  void add(exprt index, exprt value)
  {
    add_to_operands(std::move(index), std::move(value));
  }
};
 
template <>
inline bool can_cast_expr<array_list_exprt>(const exprt &base)
{
  return base.id() == ID_array_list;
}
 
inline void validate_expr(const array_list_exprt &value)
{
  PRECONDITION(value.operands().size() % 2 == 0);
}
 
inline const array_list_exprt &to_array_list_expr(const exprt &expr)
{
  PRECONDITION(can_cast_expr<array_list_exprt>(expr));
  auto &ret = static_cast<const array_list_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
inline array_list_exprt &to_array_list_expr(exprt &expr)
{
  PRECONDITION(can_cast_expr<array_list_exprt>(expr));
  auto &ret = static_cast<array_list_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
class vector_exprt : public multi_ary_exprt
{
public:
  vector_exprt(operandst _operands, vector_typet _type)
    : multi_ary_exprt(ID_vector, std::move(_operands), std::move(_type))
  {
  }
};
 
template <>
inline bool can_cast_expr<vector_exprt>(const exprt &base)
{
  return base.id() == ID_vector;
}
 
inline const vector_exprt &to_vector_expr(const exprt &expr)
{
  PRECONDITION(expr.id()==ID_vector);
  return static_cast<const vector_exprt &>(expr);
}
 
inline vector_exprt &to_vector_expr(exprt &expr)
{
  PRECONDITION(expr.id()==ID_vector);
  return static_cast<vector_exprt &>(expr);
}
 
 
class union_exprt:public unary_exprt
{
public:
  union_exprt(const irep_idt &_component_name, exprt _value, typet _type)
    : unary_exprt(ID_union, std::move(_value), std::move(_type))
  {
    set_component_name(_component_name);
  }
 
  irep_idt get_component_name() const
  {
    return get(ID_component_name);
  }
 
  void set_component_name(const irep_idt &component_name)
  {
    set(ID_component_name, component_name);
  }
 
  std::size_t get_component_number() const
  {
    return get_size_t(ID_component_number);
  }
 
  void set_component_number(std::size_t component_number)
  {
    set_size_t(ID_component_number, component_number);
  }
};
 
template <>
inline bool can_cast_expr<union_exprt>(const exprt &base)
{
  return base.id() == ID_union;
}
 
inline void validate_expr(const union_exprt &value)
{
  validate_operands(value, 1, "Union constructor must have one operand");
}
 
inline const union_exprt &to_union_expr(const exprt &expr)
{
  PRECONDITION(expr.id()==ID_union);
  union_exprt::check(expr);
  return static_cast<const union_exprt &>(expr);
}
 
inline union_exprt &to_union_expr(exprt &expr)
{
  PRECONDITION(expr.id()==ID_union);
  union_exprt::check(expr);
  return static_cast<union_exprt &>(expr);
}
 
class empty_union_exprt : public nullary_exprt
{
public:
  explicit empty_union_exprt(typet _type)
    : nullary_exprt(ID_empty_union, std::move(_type))
  {
  }
};
 
template <>
inline bool can_cast_expr<empty_union_exprt>(const exprt &base)
{
  return base.id() == ID_empty_union;
}
 
inline void validate_expr(const empty_union_exprt &value)
{
  validate_operands(
    value, 0, "Empty-union constructor must not have any operand");
}
 
inline const empty_union_exprt &to_empty_union_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_empty_union);
  empty_union_exprt::check(expr);
  return static_cast<const empty_union_exprt &>(expr);
}
 
inline empty_union_exprt &to_empty_union_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_empty_union);
  empty_union_exprt::check(expr);
  return static_cast<empty_union_exprt &>(expr);
}
 
class struct_exprt : public multi_ary_exprt
{
public:
  struct_exprt(operandst _operands, typet _type)
    : multi_ary_exprt(ID_struct, std::move(_operands), std::move(_type))
  {
  }
 
  exprt &component(const irep_idt &name, const namespacet &ns);
  const exprt &component(const irep_idt &name, const namespacet &ns) const;
};
 
template <>
inline bool can_cast_expr<struct_exprt>(const exprt &base)
{
  return base.id() == ID_struct;
}
 
inline const struct_exprt &to_struct_expr(const exprt &expr)
{
  PRECONDITION(expr.id()==ID_struct);
  return static_cast<const struct_exprt &>(expr);
}
 
inline struct_exprt &to_struct_expr(exprt &expr)
{
  PRECONDITION(expr.id()==ID_struct);
  return static_cast<struct_exprt &>(expr);
}
 
 
class complex_exprt:public binary_exprt
{
public:
  complex_exprt(exprt _real, exprt _imag, complex_typet _type)
    : binary_exprt(
        std::move(_real),
        ID_complex,
        std::move(_imag),
        std::move(_type))
  {
  }
 
  exprt real()
  {
    return op0();
  }
 
  const exprt &real() const
  {
    return op0();
  }
 
  exprt imag()
  {
    return op1();
  }
 
  const exprt &imag() const
  {
    return op1();
  }
};
 
template <>
inline bool can_cast_expr<complex_exprt>(const exprt &base)
{
  return base.id() == ID_complex;
}
 
inline void validate_expr(const complex_exprt &value)
{
  validate_operands(value, 2, "Complex constructor must have two operands");
}
 
inline const complex_exprt &to_complex_expr(const exprt &expr)
{
  PRECONDITION(expr.id()==ID_complex);
  const complex_exprt &ret = static_cast<const complex_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
inline complex_exprt &to_complex_expr(exprt &expr)
{
  PRECONDITION(expr.id()==ID_complex);
  complex_exprt &ret = static_cast<complex_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
class complex_real_exprt : public unary_exprt
{
public:
  explicit complex_real_exprt(const exprt &op)
    : unary_exprt(ID_complex_real, op, to_complex_type(op.type()).subtype())
  {
  }
};
 
template <>
inline bool can_cast_expr<complex_real_exprt>(const exprt &base)
{
  return base.id() == ID_complex_real;
}
 
inline void validate_expr(const complex_real_exprt &expr)
{
  validate_operands(
    expr, 1, "real part retrieval operation must have one operand");
}
 
inline const complex_real_exprt &to_complex_real_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_complex_real);
  complex_real_exprt::check(expr);
  return static_cast<const complex_real_exprt &>(expr);
}
 
inline complex_real_exprt &to_complex_real_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_complex_real);
  complex_real_exprt::check(expr);
  return static_cast<complex_real_exprt &>(expr);
}
 
class complex_imag_exprt : public unary_exprt
{
public:
  explicit complex_imag_exprt(const exprt &op)
    : unary_exprt(ID_complex_imag, op, to_complex_type(op.type()).subtype())
  {
  }
};
 
template <>
inline bool can_cast_expr<complex_imag_exprt>(const exprt &base)
{
  return base.id() == ID_complex_imag;
}
 
inline void validate_expr(const complex_imag_exprt &expr)
{
  validate_operands(
    expr, 1, "imaginary part retrieval operation must have one operand");
}
 
inline const complex_imag_exprt &to_complex_imag_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_complex_imag);
  const complex_imag_exprt &ret = static_cast<const complex_imag_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
inline complex_imag_exprt &to_complex_imag_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_complex_imag);
  complex_imag_exprt &ret = static_cast<complex_imag_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
 
class typecast_exprt:public unary_exprt
{
public:
  typecast_exprt(exprt op, typet _type)
    : unary_exprt(ID_typecast, std::move(op), std::move(_type))
  {
  }
 
  // returns a typecast if the type doesn't already match
  static exprt conditional_cast(const exprt &expr, const typet &type)
  {
    if(expr.type() == type)
      return expr;
    else
      return typecast_exprt(expr, type);
  }
};
 
template <>
inline bool can_cast_expr<typecast_exprt>(const exprt &base)
{
  return base.id() == ID_typecast;
}
 
inline void validate_expr(const typecast_exprt &value)
{
  validate_operands(value, 1, "Typecast must have one operand");
}
 
inline const typecast_exprt &to_typecast_expr(const exprt &expr)
{
  PRECONDITION(expr.id()==ID_typecast);
  typecast_exprt::check(expr);
  return static_cast<const typecast_exprt &>(expr);
}
 
inline typecast_exprt &to_typecast_expr(exprt &expr)
{
  PRECONDITION(expr.id()==ID_typecast);
  typecast_exprt::check(expr);
  return static_cast<typecast_exprt &>(expr);
}
 
class and_exprt:public multi_ary_exprt
{
public:
  and_exprt(exprt op0, exprt op1)
    : multi_ary_exprt(std::move(op0), ID_and, std::move(op1), bool_typet())
  {
  }
 
  and_exprt(exprt op0, exprt op1, exprt op2)
    : multi_ary_exprt(
        ID_and,
        {std::move(op0), std::move(op1), std::move(op2)},
        bool_typet())
  {
  }
 
  and_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
    : multi_ary_exprt(
        ID_and,
        {std::move(op0), std::move(op1), std::move(op2), std::move(op3)},
        bool_typet())
  {
  }
 
  explicit and_exprt(exprt::operandst _operands)
    : multi_ary_exprt(ID_and, std::move(_operands), bool_typet())
  {
  }
};
 
 
exprt conjunction(const exprt::operandst &);
 
exprt conjunction(exprt a, exprt b);
 
template <>
inline bool can_cast_expr<and_exprt>(const exprt &base)
{
  return base.id() == ID_and;
}
 
inline const and_exprt &to_and_expr(const exprt &expr)
{
  PRECONDITION(expr.id()==ID_and);
  return static_cast<const and_exprt &>(expr);
}
 
inline and_exprt &to_and_expr(exprt &expr)
{
  PRECONDITION(expr.id()==ID_and);
  return static_cast<and_exprt &>(expr);
}
 
class nand_exprt : public multi_ary_exprt
{
public:
  nand_exprt(exprt op0, exprt op1)
    : multi_ary_exprt(std::move(op0), ID_nand, std::move(op1), bool_typet())
  {
  }
 
  explicit nand_exprt(exprt::operandst _operands)
    : multi_ary_exprt(ID_nand, std::move(_operands), bool_typet())
  {
  }
};
 
inline const nand_exprt &to_nand_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_nand);
  return static_cast<const nand_exprt &>(expr);
}
 
inline nand_exprt &to_nand_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_nand);
  return static_cast<nand_exprt &>(expr);
}
 
class implies_exprt:public binary_exprt
{
public:
  implies_exprt(exprt op0, exprt op1)
    : binary_exprt(std::move(op0), ID_implies, std::move(op1), bool_typet())
  {
  }
};
 
template <>
inline bool can_cast_expr<implies_exprt>(const exprt &base)
{
  return base.id() == ID_implies;
}
 
inline void validate_expr(const implies_exprt &value)
{
  validate_operands(value, 2, "Implies must have two operands");
}
 
inline const implies_exprt &to_implies_expr(const exprt &expr)
{
  PRECONDITION(expr.id()==ID_implies);
  const implies_exprt &ret = static_cast<const implies_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
inline implies_exprt &to_implies_expr(exprt &expr)
{
  PRECONDITION(expr.id()==ID_implies);
  implies_exprt &ret = static_cast<implies_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
class or_exprt:public multi_ary_exprt
{
public:
  or_exprt(exprt op0, exprt op1)
    : multi_ary_exprt(std::move(op0), ID_or, std::move(op1), bool_typet())
  {
  }
 
  or_exprt(exprt op0, exprt op1, exprt op2)
    : multi_ary_exprt(
        ID_or,
        {std::move(op0), std::move(op1), std::move(op2)},
        bool_typet())
  {
  }
 
  or_exprt(exprt op0, exprt op1, exprt op2, exprt op3)
    : multi_ary_exprt(
        ID_or,
        {std::move(op0), std::move(op1), std::move(op2), std::move(op3)},
        bool_typet())
  {
  }
 
  explicit or_exprt(exprt::operandst _operands)
    : multi_ary_exprt(ID_or, std::move(_operands), bool_typet())
  {
  }
};
 
 
exprt disjunction(const exprt::operandst &);
 
template <>
inline bool can_cast_expr<or_exprt>(const exprt &base)
{
  return base.id() == ID_or;
}
 
inline const or_exprt &to_or_expr(const exprt &expr)
{
  PRECONDITION(expr.id()==ID_or);
  return static_cast<const or_exprt &>(expr);
}
 
inline or_exprt &to_or_expr(exprt &expr)
{
  PRECONDITION(expr.id()==ID_or);
  return static_cast<or_exprt &>(expr);
}
 
class nor_exprt : public multi_ary_exprt
{
public:
  nor_exprt(exprt op0, exprt op1)
    : multi_ary_exprt(std::move(op0), ID_nor, std::move(op1), bool_typet())
  {
  }
 
  explicit nor_exprt(exprt::operandst _operands)
    : multi_ary_exprt(ID_nor, std::move(_operands), bool_typet())
  {
  }
};
 
inline const nor_exprt &to_nor_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_nor);
  return static_cast<const nor_exprt &>(expr);
}
 
inline nor_exprt &to_nor_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_nor);
  return static_cast<nor_exprt &>(expr);
}
 
class xor_exprt:public multi_ary_exprt
{
public:
  xor_exprt(exprt _op0, exprt _op1)
    : multi_ary_exprt(std::move(_op0), ID_xor, std::move(_op1), bool_typet())
  {
  }
 
  explicit xor_exprt(exprt::operandst _operands)
    : multi_ary_exprt(ID_xor, std::move(_operands), bool_typet())
  {
  }
};
 
template <>
inline bool can_cast_expr<xor_exprt>(const exprt &base)
{
  return base.id() == ID_xor;
}
 
inline const xor_exprt &to_xor_expr(const exprt &expr)
{
  PRECONDITION(expr.id()==ID_xor);
  return static_cast<const xor_exprt &>(expr);
}
 
inline xor_exprt &to_xor_expr(exprt &expr)
{
  PRECONDITION(expr.id()==ID_xor);
  return static_cast<xor_exprt &>(expr);
}
 
class xnor_exprt : public multi_ary_exprt
{
public:
  xnor_exprt(exprt _op0, exprt _op1)
    : multi_ary_exprt(std::move(_op0), ID_xnor, std::move(_op1), bool_typet())
  {
  }
 
  explicit xnor_exprt(exprt::operandst _operands)
    : multi_ary_exprt(ID_xnor, std::move(_operands), bool_typet())
  {
  }
};
 
template <>
inline bool can_cast_expr<xnor_exprt>(const exprt &base)
{
  return base.id() == ID_xnor;
}
 
inline const xnor_exprt &to_xnor_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_xnor);
  return static_cast<const xnor_exprt &>(expr);
}
 
inline xnor_exprt &to_xnor_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_xnor);
  return static_cast<xnor_exprt &>(expr);
}
 
class not_exprt:public unary_exprt
{
public:
  explicit not_exprt(exprt _op) : unary_exprt(ID_not, std::move(_op))
  {
    PRECONDITION(as_const(*this).op().is_boolean());
  }
};
 
template <>
inline bool can_cast_expr<not_exprt>(const exprt &base)
{
  return base.id() == ID_not;
}
 
inline void validate_expr(const not_exprt &value)
{
  validate_operands(value, 1, "Not must have one operand");
}
 
inline const not_exprt &to_not_expr(const exprt &expr)
{
  PRECONDITION(expr.id()==ID_not);
  not_exprt::check(expr);
  return static_cast<const not_exprt &>(expr);
}
 
inline not_exprt &to_not_expr(exprt &expr)
{
  PRECONDITION(expr.id()==ID_not);
  not_exprt::check(expr);
  return static_cast<not_exprt &>(expr);
}
 
 
class if_exprt : public ternary_exprt
{
public:
  if_exprt(exprt cond, const exprt &t, exprt f)
    : ternary_exprt(ID_if, std::move(cond), t, std::move(f), t.type())
  {
  }
 
  if_exprt(exprt cond, exprt t, exprt f, typet type)
    : ternary_exprt(
        ID_if,
        std::move(cond),
        std::move(t),
        std::move(f),
        std::move(type))
  {
  }
 
  exprt &cond()
  {
    return op0();
  }
 
  const exprt &cond() const
  {
    return op0();
  }
 
  exprt &true_case()
  {
    return op1();
  }
 
  const exprt &true_case() const
  {
    return op1();
  }
 
  exprt &false_case()
  {
    return op2();
  }
 
  const exprt &false_case() const
  {
    return op2();
  }
 
  static void check(
    const exprt &expr,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    ternary_exprt::check(expr, vm);
  }
 
  static void validate(
    const exprt &expr,
    const namespacet &ns,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    ternary_exprt::validate(expr, ns, vm);
  }
};
 
template <>
inline bool can_cast_expr<if_exprt>(const exprt &base)
{
  return base.id() == ID_if;
}
 
inline void validate_expr(const if_exprt &value)
{
  validate_operands(value, 3, "If-then-else must have three operands");
}
 
inline const if_exprt &to_if_expr(const exprt &expr)
{
  PRECONDITION(expr.id()==ID_if);
  const if_exprt &ret = static_cast<const if_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
inline if_exprt &to_if_expr(exprt &expr)
{
  PRECONDITION(expr.id()==ID_if);
  if_exprt &ret = static_cast<if_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
class with_exprt : public expr_protectedt
{
public:
  with_exprt(const exprt &_old, exprt _where, exprt _new_value)
    : expr_protectedt(
        ID_with,
        _old.type(),
        {_old, std::move(_where), std::move(_new_value)})
  {
  }
 
  exprt &old()
  {
    return op0();
  }
 
  const exprt &old() const
  {
    return op0();
  }
 
  exprt &where()
  {
    return op1();
  }
 
  const exprt &where() const
  {
    return op1();
  }
 
  exprt &new_value()
  {
    return op2();
  }
 
  const exprt &new_value() const
  {
    return op2();
  }
};
 
template <>
inline bool can_cast_expr<with_exprt>(const exprt &base)
{
  return base.id() == ID_with;
}
 
inline void validate_expr(const with_exprt &value)
{
  validate_operands(value, 3, "array/structure update must have 3 operands");
}
 
inline const with_exprt &to_with_expr(const exprt &expr)
{
  PRECONDITION(expr.id()==ID_with);
  const with_exprt &ret = static_cast<const with_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
inline with_exprt &to_with_expr(exprt &expr)
{
  PRECONDITION(expr.id()==ID_with);
  with_exprt &ret = static_cast<with_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
class index_designatort : public expr_protectedt
{
public:
  explicit index_designatort(exprt _index)
    : expr_protectedt(ID_index_designator, typet(), {std::move(_index)})
  {
  }
 
  const exprt &index() const
  {
    return op0();
  }
 
  exprt &index()
  {
    return op0();
  }
};
 
template <>
inline bool can_cast_expr<index_designatort>(const exprt &base)
{
  return base.id() == ID_index_designator;
}
 
inline void validate_expr(const index_designatort &value)
{
  validate_operands(value, 1, "Index designator must have one operand");
}
 
inline const index_designatort &to_index_designator(const exprt &expr)
{
  PRECONDITION(expr.id()==ID_index_designator);
  const index_designatort &ret = static_cast<const index_designatort &>(expr);
  validate_expr(ret);
  return ret;
}
 
inline index_designatort &to_index_designator(exprt &expr)
{
  PRECONDITION(expr.id()==ID_index_designator);
  index_designatort &ret = static_cast<index_designatort &>(expr);
  validate_expr(ret);
  return ret;
}
 
class member_designatort : public expr_protectedt
{
public:
  explicit member_designatort(const irep_idt &_component_name)
    : expr_protectedt(ID_member_designator, typet())
  {
    set(ID_component_name, _component_name);
  }
 
  irep_idt get_component_name() const
  {
    return get(ID_component_name);
  }
};
 
template <>
inline bool can_cast_expr<member_designatort>(const exprt &base)
{
  return base.id() == ID_member_designator;
}
 
inline void validate_expr(const member_designatort &value)
{
  validate_operands(value, 0, "Member designator must not have operands");
}
 
inline const member_designatort &to_member_designator(const exprt &expr)
{
  PRECONDITION(expr.id()==ID_member_designator);
  const member_designatort &ret = static_cast<const member_designatort &>(expr);
  validate_expr(ret);
  return ret;
}
 
inline member_designatort &to_member_designator(exprt &expr)
{
  PRECONDITION(expr.id()==ID_member_designator);
  member_designatort &ret = static_cast<member_designatort &>(expr);
  validate_expr(ret);
  return ret;
}
 
 
class update_exprt : public ternary_exprt
{
public:
  update_exprt(const exprt &_old, exprt _designator, exprt _new_value)
    : ternary_exprt(
        ID_update,
        _old,
        std::move(_designator),
        std::move(_new_value),
        _old.type())
  {
  }
 
  exprt &old()
  {
    return op0();
  }
 
  const exprt &old() const
  {
    return op0();
  }
 
  // the designator operands are either
  // 1) member_designator or
  // 2) index_designator
  // as defined above
  exprt::operandst &designator()
  {
    return op1().operands();
  }
 
  const exprt::operandst &designator() const
  {
    return op1().operands();
  }
 
  exprt &new_value()
  {
    return op2();
  }
 
  const exprt &new_value() const
  {
    return op2();
  }
 
  with_exprt make_with_expr() const;
 
  static void check(
    const exprt &expr,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    ternary_exprt::check(expr, vm);
  }
 
  static void validate(
    const exprt &expr,
    const namespacet &ns,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    ternary_exprt::validate(expr, ns, vm);
  }
};
 
template <>
inline bool can_cast_expr<update_exprt>(const exprt &base)
{
  return base.id() == ID_update;
}
 
inline void validate_expr(const update_exprt &value)
{
  validate_operands(
    value, 3, "Array/structure update must have three operands");
}
 
inline const update_exprt &to_update_expr(const exprt &expr)
{
  PRECONDITION(expr.id()==ID_update);
  const update_exprt &ret = static_cast<const update_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
inline update_exprt &to_update_expr(exprt &expr)
{
  PRECONDITION(expr.id()==ID_update);
  update_exprt &ret = static_cast<update_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
 
#if 0
class array_update_exprt:public expr_protectedt
{
public:
  array_update_exprt(
    const exprt &_array,
    const exprt &_index,
    const exprt &_new_value):
    exprt(ID_array_update, _array.type())
  {
    add_to_operands(_array, _index, _new_value);
  }
 
  array_update_exprt():expr_protectedt(ID_array_update)
  {
    operands().resize(3);
  }
 
  exprt &array()
  {
    return op0();
  }
 
  const exprt &array() const
  {
    return op0();
  }
 
  exprt &index()
  {
    return op1();
  }
 
  const exprt &index() const
  {
    return op1();
  }
 
  exprt &new_value()
  {
    return op2();
  }
 
  const exprt &new_value() const
  {
    return op2();
  }
};
 
template<> inline bool can_cast_expr<array_update_exprt>(const exprt &base)
{
  return base.id()==ID_array_update;
}
 
inline void validate_expr(const array_update_exprt &value)
{
  validate_operands(value, 3, "Array update must have three operands");
}
 
inline const array_update_exprt &to_array_update_expr(const exprt &expr)
{
  PRECONDITION(expr.id()==ID_array_update);
  const array_update_exprt &ret = static_cast<const array_update_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
inline array_update_exprt &to_array_update_expr(exprt &expr)
{
  PRECONDITION(expr.id()==ID_array_update);
  array_update_exprt &ret = static_cast<array_update_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
#endif
 
 
class member_exprt:public unary_exprt
{
public:
  member_exprt(exprt op, const irep_idt &component_name, typet _type)
    : unary_exprt(ID_member, std::move(op), std::move(_type))
  {
    const auto &compound_type_id = compound().type().id();
    PRECONDITION(
      compound_type_id == ID_struct_tag || compound_type_id == ID_union_tag ||
      compound_type_id == ID_struct || compound_type_id == ID_union);
    set_component_name(component_name);
  }
 
  member_exprt(exprt op, const struct_typet::componentt &c)
    : unary_exprt(ID_member, std::move(op), c.type())
  {
    const auto &compound_type_id = compound().type().id();
    PRECONDITION(
      compound_type_id == ID_struct_tag || compound_type_id == ID_union_tag ||
      compound_type_id == ID_struct || compound_type_id == ID_union);
    set_component_name(c.get_name());
  }
 
  irep_idt get_component_name() const
  {
    return get(ID_component_name);
  }
 
  void set_component_name(const irep_idt &component_name)
  {
    set(ID_component_name, component_name);
  }
 
  std::size_t get_component_number() const
  {
    return get_size_t(ID_component_number);
  }
 
  // will go away, use compound()
  const exprt &struct_op() const
  {
    return op0();
  }
 
  // will go away, use compound()
  exprt &struct_op()
  {
    return op0();
  }
 
  const exprt &compound() const
  {
    return op0();
  }
 
  exprt &compound()
  {
    return op0();
  }
 
  static void check(
    const exprt &expr,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    DATA_CHECK(
      vm,
      expr.operands().size() == 1,
      "member expression must have one operand");
  }
 
  static void validate(
    const exprt &expr,
    const namespacet &ns,
    const validation_modet vm = validation_modet::INVARIANT);
};
 
template <>
inline bool can_cast_expr<member_exprt>(const exprt &base)
{
  return base.id() == ID_member;
}
 
inline void validate_expr(const member_exprt &value)
{
  validate_operands(value, 1, "Extract member must have one operand");
}
 
inline const member_exprt &to_member_expr(const exprt &expr)
{
  PRECONDITION(expr.id()==ID_member);
  member_exprt::check(expr);
  return static_cast<const member_exprt &>(expr);
}
 
inline member_exprt &to_member_expr(exprt &expr)
{
  PRECONDITION(expr.id()==ID_member);
  member_exprt::check(expr);
  return static_cast<member_exprt &>(expr);
}
 
 
class type_exprt : public nullary_exprt
{
public:
  explicit type_exprt(typet type) : nullary_exprt(ID_type, std::move(type))
  {
  }
};
 
template <>
inline bool can_cast_expr<type_exprt>(const exprt &base)
{
  return base.id() == ID_type;
}
 
inline const type_exprt &to_type_expr(const exprt &expr)
{
  PRECONDITION(can_cast_expr<type_exprt>(expr));
  type_exprt::check(expr);
  return static_cast<const type_exprt &>(expr);
}
 
inline type_exprt &to_type_expr(exprt &expr)
{
  PRECONDITION(can_cast_expr<type_exprt>(expr));
  type_exprt::check(expr);
  return static_cast<type_exprt &>(expr);
}
 
class constant_exprt : public nullary_exprt
{
public:
  constant_exprt(const irep_idt &_value, typet _type)
    : nullary_exprt(ID_constant, std::move(_type))
  {
    set_value(_value);
  }
 
  const irep_idt &get_value() const
  {
    return get(ID_value);
  }
 
  void set_value(const irep_idt &value)
  {
    set(ID_value, value);
  }
 
  bool is_null_pointer() const;
 
  using irept::operator==;
  using irept::operator!=;
  bool operator==(bool rhs) const;
  bool operator!=(bool rhs) const;
  bool operator==(int rhs) const;
  bool operator!=(int rhs) const;
  bool operator==(std::nullptr_t) const;
  bool operator!=(std::nullptr_t) const;
 
  static void check(
    const exprt &expr,
    const validation_modet vm = validation_modet::INVARIANT);
 
  static void validate(
    const exprt &expr,
    const namespacet &,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    check(expr, vm);
  }
 
protected:
  bool value_is_zero_string() const;
};
 
template <>
inline bool can_cast_expr<constant_exprt>(const exprt &base)
{
  return base.is_constant();
}
 
inline void validate_expr(const constant_exprt &value)
{
  validate_operands(value, 0, "Constants must not have operands");
}
 
inline const constant_exprt &to_constant_expr(const exprt &expr)
{
  PRECONDITION(expr.is_constant());
  constant_exprt::check(expr);
  return static_cast<const constant_exprt &>(expr);
}
 
inline constant_exprt &to_constant_expr(exprt &expr)
{
  PRECONDITION(expr.is_constant());
  constant_exprt::check(expr);
  return static_cast<constant_exprt &>(expr);
}
 
bool operator==(const exprt &lhs, bool rhs);
 
bool operator!=(const exprt &lhs, bool rhs);
 
bool operator==(const exprt &lhs, int rhs);
 
bool operator!=(const exprt &lhs, int rhs);
 
bool operator==(const exprt &lhs, std::nullptr_t);
 
bool operator!=(const exprt &lhs, std::nullptr_t);
 
class true_exprt:public constant_exprt
{
public:
  true_exprt() : constant_exprt(ID_true, bool_typet())
  {
  }
};
 
class false_exprt:public constant_exprt
{
public:
  false_exprt() : constant_exprt(ID_false, bool_typet())
  {
  }
};
 
class nil_exprt : public nullary_exprt
{
public:
  nil_exprt()
    : nullary_exprt(static_cast<const nullary_exprt &>(get_nil_irep()))
  {
  }
};
 
template <>
inline bool can_cast_expr<nil_exprt>(const exprt &base)
{
  return base.id() == ID_nil;
}
 
class infinity_exprt : public nullary_exprt
{
public:
  explicit infinity_exprt(typet _type)
    : nullary_exprt(ID_infinity, std::move(_type))
  {
  }
};
 
class binding_exprt : public binary_exprt
{
public:
  using variablest = std::vector<symbol_exprt>;
 
  binding_exprt(
    irep_idt _id,
    const variablest &_variables,
    exprt _where,
    typet _type)
    : binary_exprt(
        multi_ary_exprt(
          ID_tuple,
          (const operandst &)_variables,
          typet(ID_tuple)),
        _id,
        std::move(_where),
        std::move(_type))
  {
  }
 
  variablest &variables()
  {
    return (variablest &)to_multi_ary_expr(op0()).operands();
  }
 
  const variablest &variables() const
  {
    return (variablest &)to_multi_ary_expr(op0()).operands();
  }
 
  exprt &where()
  {
    return op1();
  }
 
  const exprt &where() const
  {
    return op1();
  }
 
  exprt instantiate(const exprt::operandst &) const;
 
  exprt instantiate(const variablest &) const;
};
 
template <>
inline bool can_cast_expr<binding_exprt>(const exprt &base)
{
  return base.id() == ID_forall || base.id() == ID_exists ||
         base.id() == ID_lambda || base.id() == ID_array_comprehension;
}
 
inline void validate_expr(const binding_exprt &binding_expr)
{
  validate_operands(
    binding_expr, 2, "Binding expressions must have two operands");
}
 
inline const binding_exprt &to_binding_expr(const exprt &expr)
{
  PRECONDITION(
    expr.id() == ID_forall || expr.id() == ID_exists ||
    expr.id() == ID_lambda || expr.id() == ID_array_comprehension);
  const binding_exprt &ret = static_cast<const binding_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
inline binding_exprt &to_binding_expr(exprt &expr)
{
  PRECONDITION(
    expr.id() == ID_forall || expr.id() == ID_exists ||
    expr.id() == ID_lambda || expr.id() == ID_array_comprehension);
  binding_exprt &ret = static_cast<binding_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
class let_exprt : public binary_exprt
{
public:
  let_exprt(
    binding_exprt::variablest variables,
    operandst values,
    const exprt &where)
    : binary_exprt(
        binding_exprt(
          ID_let_binding,
          std::move(variables),
          where,
          where.type()),
        ID_let,
        multi_ary_exprt(irep_idt(), std::move(values), typet(ID_tuple)),
        where.type())
  {
    PRECONDITION(this->variables().size() == this->values().size());
  }
 
  let_exprt(symbol_exprt symbol, exprt value, const exprt &where)
    : let_exprt(
        binding_exprt::variablest{std::move(symbol)},
        operandst{std::move(value)},
        where)
  {
  }
 
  binding_exprt &binding()
  {
    return static_cast<binding_exprt &>(op0());
  }
 
  const binding_exprt &binding() const
  {
    return static_cast<const binding_exprt &>(op0());
  }
 
  symbol_exprt &symbol()
  {
    auto &variables = binding().variables();
    PRECONDITION(variables.size() == 1);
    return variables.front();
  }
 
  const symbol_exprt &symbol() const
  {
    const auto &variables = binding().variables();
    PRECONDITION(variables.size() == 1);
    return variables.front();
  }
 
  exprt &value()
  {
    auto &values = this->values();
    PRECONDITION(values.size() == 1);
    return values.front();
  }
 
  const exprt &value() const
  {
    const auto &values = this->values();
    PRECONDITION(values.size() == 1);
    return values.front();
  }
 
  operandst &values()
  {
    return static_cast<multi_ary_exprt &>(op1()).operands();
  }
 
  const operandst &values() const
  {
    return static_cast<const multi_ary_exprt &>(op1()).operands();
  }
 
  binding_exprt::variablest &variables()
  {
    return binding().variables();
  }
 
  const binding_exprt::variablest &variables() const
  {
    return binding().variables();
  }
 
  exprt &where()
  {
    return binding().where();
  }
 
  const exprt &where() const
  {
    return binding().where();
  }
 
  static void validate(const exprt &, validation_modet);
};
 
template <>
inline bool can_cast_expr<let_exprt>(const exprt &base)
{
  return base.id() == ID_let;
}
 
inline void validate_expr(const let_exprt &let_expr)
{
  validate_operands(let_expr, 2, "Let must have two operands");
}
 
inline const let_exprt &to_let_expr(const exprt &expr)
{
  PRECONDITION(expr.id()==ID_let);
  const let_exprt &ret = static_cast<const let_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
inline let_exprt &to_let_expr(exprt &expr)
{
  PRECONDITION(expr.id()==ID_let);
  let_exprt &ret = static_cast<let_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
 
class cond_exprt : public multi_ary_exprt
{
public:
  cond_exprt(operandst _operands, typet _type)
    : multi_ary_exprt(ID_cond, std::move(_operands), std::move(_type))
  {
  }
 
  void add_case(const exprt &condition, const exprt &value)
  {
    PRECONDITION(condition.is_boolean());
    operands().reserve(operands().size() + 2);
    operands().push_back(condition);
    operands().push_back(value);
  }
 
  // a lowering to nested if_exprt
  exprt lower() const;
};
 
template <>
inline bool can_cast_expr<cond_exprt>(const exprt &base)
{
  return base.id() == ID_cond;
}
 
inline void validate_expr(const cond_exprt &value)
{
  DATA_INVARIANT(
    value.operands().size() % 2 == 0, "cond must have even number of operands");
}
 
inline const cond_exprt &to_cond_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_cond);
  const cond_exprt &ret = static_cast<const cond_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
inline cond_exprt &to_cond_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_cond);
  cond_exprt &ret = static_cast<cond_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
class case_exprt : public multi_ary_exprt
{
public:
  case_exprt(operandst _operands, typet _type)
    : multi_ary_exprt(ID_case, std::move(_operands), std::move(_type))
  {
  }
 
  case_exprt(exprt _select_value, typet _type)
    : multi_ary_exprt(ID_case, {std::move(_select_value)}, std::move(_type))
  {
  }
 
  const exprt &select_value() const
  {
    PRECONDITION(!operands().empty());
    return operands()[0];
  }
 
  exprt &select_value()
  {
    PRECONDITION(!operands().empty());
    return operands()[0];
  }
 
  void add_case(const exprt &case_value, const exprt &result_value)
  {
    operands().reserve(operands().size() + 2);
    operands().push_back(case_value);
    operands().push_back(result_value);
  }
 
  std::size_t number_of_cases() const
  {
    PRECONDITION(operands().size() >= 1);
    return (operands().size() - 1) / 2;
  }
 
  const exprt &case_value(std::size_t i) const
  {
    PRECONDITION(i < number_of_cases());
    return operands()[1 + 2 * i];
  }
 
  exprt &case_value(std::size_t i)
  {
    PRECONDITION(i < number_of_cases());
    return operands()[1 + 2 * i];
  }
 
  const exprt &result_value(std::size_t i) const
  {
    PRECONDITION(i < number_of_cases());
    return operands()[1 + 2 * i + 1];
  }
 
  exprt &result_value(std::size_t i)
  {
    PRECONDITION(i < number_of_cases());
    return operands()[1 + 2 * i + 1];
  }
 
  static void validate_expr(const case_exprt &value)
  {
    DATA_INVARIANT(
      value.operands().size() >= 1,
      "case expression must have at least one operand");
    DATA_INVARIANT(
      value.operands().size() % 2 == 1,
      "case expression must have odd number of operands");
  }
};
 
template <>
inline bool can_cast_expr<case_exprt>(const exprt &base)
{
  return base.id() == ID_case;
}
 
inline const case_exprt &to_case_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_case);
  const case_exprt &ret = static_cast<const case_exprt &>(expr);
  case_exprt::validate_expr(ret);
  return ret;
}
 
inline case_exprt &to_case_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_case);
  case_exprt &ret = static_cast<case_exprt &>(expr);
  case_exprt::validate_expr(ret);
  return ret;
}
 
class array_comprehension_exprt : public binding_exprt
{
public:
  explicit array_comprehension_exprt(
    symbol_exprt arg,
    exprt body,
    array_typet _type)
    : binding_exprt(
        ID_array_comprehension,
        {std::move(arg)},
        std::move(body),
        std::move(_type))
  {
  }
 
  const array_typet &type() const
  {
    return static_cast<const array_typet &>(binary_exprt::type());
  }
 
  array_typet &type()
  {
    return static_cast<array_typet &>(binary_exprt::type());
  }
 
  const symbol_exprt &arg() const
  {
    auto &variables = this->variables();
    PRECONDITION(variables.size() == 1);
    return variables[0];
  }
 
  symbol_exprt &arg()
  {
    auto &variables = this->variables();
    PRECONDITION(variables.size() == 1);
    return variables[0];
  }
 
  const exprt &body() const
  {
    return where();
  }
 
  exprt &body()
  {
    return where();
  }
};
 
template <>
inline bool can_cast_expr<array_comprehension_exprt>(const exprt &base)
{
  return base.id() == ID_array_comprehension;
}
 
inline void validate_expr(const array_comprehension_exprt &value)
{
  validate_operands(value, 2, "'Array comprehension' must have two operands");
}
 
inline const array_comprehension_exprt &
to_array_comprehension_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_array_comprehension);
  const array_comprehension_exprt &ret =
    static_cast<const array_comprehension_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
inline array_comprehension_exprt &to_array_comprehension_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_array_comprehension);
  array_comprehension_exprt &ret =
    static_cast<array_comprehension_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
inline void validate_expr(const class class_method_descriptor_exprt &value);
 
class class_method_descriptor_exprt : public nullary_exprt
{
public:
  explicit class_method_descriptor_exprt(
    typet _type,
    irep_idt mangled_method_name,
    irep_idt class_id,
    irep_idt base_method_name)
    : nullary_exprt(ID_virtual_function, std::move(_type))
  {
    irep_idt id = id2string(class_id) + "." + id2string(mangled_method_name);
    set(ID_component_name, std::move(mangled_method_name));
    set(ID_C_class, std::move(class_id));
    set(ID_C_base_name, std::move(base_method_name));
    set(ID_identifier, std::move(id));
    validate_expr(*this);
  }
 
  const irep_idt &mangled_method_name() const
  {
    return get(ID_component_name);
  }
 
  const irep_idt &class_id() const
  {
    return get(ID_C_class);
  }
 
  const irep_idt &base_method_name() const
  {
    return get(ID_C_base_name);
  }
 
  const irep_idt &get_identifier() const
  {
    return get(ID_identifier);
  }
};
 
inline void validate_expr(const class class_method_descriptor_exprt &value)
{
  validate_operands(value, 0, "class method descriptor must not have operands");
  DATA_INVARIANT(
    !value.mangled_method_name().empty(),
    "class method descriptor must have a mangled method name.");
  DATA_INVARIANT(
    !value.class_id().empty(), "class method descriptor must have a class id.");
  DATA_INVARIANT(
    !value.base_method_name().empty(),
    "class method descriptor must have a base method name.");
  DATA_INVARIANT(
    value.get_identifier() == id2string(value.class_id()) + "." +
                                id2string(value.mangled_method_name()),
    "class method descriptor must have an identifier in the expected format.");
}
 
inline const class_method_descriptor_exprt &
to_class_method_descriptor_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_virtual_function);
  class_method_descriptor_exprt::check(expr);
  return static_cast<const class_method_descriptor_exprt &>(expr);
}
 
template <>
inline bool can_cast_expr<class_method_descriptor_exprt>(const exprt &base)
{
  return base.id() == ID_virtual_function;
}
 
class named_term_exprt : public binary_exprt
{
public:
  explicit named_term_exprt(symbol_exprt symbol, exprt value)
    : binary_exprt(
        std::move(symbol),
        ID_named_term,
        value, // not moved, for type
        value.type())
  {
    PRECONDITION(symbol.type() == type());
  }
 
  const symbol_exprt &symbol() const
  {
    return static_cast<const symbol_exprt &>(op0());
  }
 
  symbol_exprt &symbol()
  {
    return static_cast<symbol_exprt &>(op0());
  }
 
  const exprt &value() const
  {
    return op1();
  }
 
  exprt &value()
  {
    return op1();
  }
};
 
template <>
inline bool can_cast_expr<named_term_exprt>(const exprt &base)
{
  return base.id() == ID_named_term;
}
 
inline void validate_expr(const named_term_exprt &value)
{
  validate_operands(value, 2, "'named term' must have two operands");
}
 
inline const named_term_exprt &to_named_term_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_named_term);
  const named_term_exprt &ret = static_cast<const named_term_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
inline named_term_exprt &to_named_term_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_named_term);
  named_term_exprt &ret = static_cast<named_term_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
#endif // CPROVER_UTIL_STD_EXPR_H