bitvector_expr.h

Go to the documentation of this file.

/*******************************************************************\
 
Module: API to expression classes for bitvectors
 
Author: Daniel Kroening, kroening@kroening.com
 
\*******************************************************************/
 
#ifndef CPROVER_UTIL_BITVECTOR_EXPR_H
#define CPROVER_UTIL_BITVECTOR_EXPR_H

 
#include "bitvector_types.h"
#include "std_expr.h"

class bswap_exprt : public unary_exprt
{
public:
  bswap_exprt(exprt _op, std::size_t bits_per_byte, typet _type)
    : unary_exprt(ID_bswap, std::move(_op), std::move(_type))
  {
    set_bits_per_byte(bits_per_byte);
  }
 
  bswap_exprt(exprt _op, std::size_t bits_per_byte)
    : unary_exprt(ID_bswap, std::move(_op))
  {
    set_bits_per_byte(bits_per_byte);
  }
 
  std::size_t get_bits_per_byte() const
  {
    return get_size_t(ID_bits_per_byte);
  }
 
  void set_bits_per_byte(std::size_t bits_per_byte)
  {
    set_size_t(ID_bits_per_byte, bits_per_byte);
  }
};
 
template <>
inline bool can_cast_expr<bswap_exprt>(const exprt &base)
{
  return base.id() == ID_bswap;
}
 
inline void validate_expr(const bswap_exprt &value)
{
  validate_operands(value, 1, "bswap must have one operand");
  DATA_INVARIANT(
    value.op().type() == value.type(), "bswap type must match operand type");
}

inline const bswap_exprt &to_bswap_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_bswap);
  const bswap_exprt &ret = static_cast<const bswap_exprt &>(expr);
  validate_expr(ret);
  return ret;
}

inline bswap_exprt &to_bswap_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_bswap);
  bswap_exprt &ret = static_cast<bswap_exprt &>(expr);
  validate_expr(ret);
  return ret;
}

class bitnot_exprt : public unary_exprt
{
public:
  explicit bitnot_exprt(exprt op) : unary_exprt(ID_bitnot, std::move(op))
  {
  }
};
 
template <>
inline bool can_cast_expr<bitnot_exprt>(const exprt &base)
{
  return base.id() == ID_bitnot;
}
 
inline void validate_expr(const bitnot_exprt &value)
{
  validate_operands(value, 1, "Bit-wise not must have one operand");
}

inline const bitnot_exprt &to_bitnot_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_bitnot);
  const bitnot_exprt &ret = static_cast<const bitnot_exprt &>(expr);
  validate_expr(ret);
  return ret;
}

inline bitnot_exprt &to_bitnot_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_bitnot);
  bitnot_exprt &ret = static_cast<bitnot_exprt &>(expr);
  validate_expr(ret);
  return ret;
}

class bitor_exprt : public multi_ary_exprt
{
public:
  bitor_exprt(const exprt &_op0, exprt _op1)
    : multi_ary_exprt(_op0, ID_bitor, std::move(_op1), _op0.type())
  {
  }
 
  explicit bitor_exprt(exprt::operandst _operands)
    : multi_ary_exprt(ID_bitor, std::move(_operands))
  {
  }
 
  bitor_exprt(exprt::operandst _operands, typet _type)
    : multi_ary_exprt(ID_bitor, std::move(_operands), std::move(_type))
  {
  }
};
 
template <>
inline bool can_cast_expr<bitor_exprt>(const exprt &base)
{
  return base.id() == ID_bitor;
}

inline const bitor_exprt &to_bitor_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_bitor);
  return static_cast<const bitor_exprt &>(expr);
}

inline bitor_exprt &to_bitor_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_bitor);
  return static_cast<bitor_exprt &>(expr);
}

class bitnor_exprt : public multi_ary_exprt
{
public:
  bitnor_exprt(exprt _op0, exprt _op1)
    : multi_ary_exprt(std::move(_op0), ID_bitnor, std::move(_op1))
  {
  }
 
  explicit bitnor_exprt(exprt::operandst _operands)
    : multi_ary_exprt(ID_bitnor, std::move(_operands))
  {
  }
 
  bitnor_exprt(exprt::operandst _operands, typet _type)
    : multi_ary_exprt(ID_bitnor, std::move(_operands), std::move(_type))
  {
  }
};
 
template <>
inline bool can_cast_expr<bitnor_exprt>(const exprt &base)
{
  return base.id() == ID_bitnor;
}

inline const bitnor_exprt &to_bitnor_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_bitnor);
  return static_cast<const bitnor_exprt &>(expr);
}

inline bitnor_exprt &to_bitnor_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_bitnor);
  return static_cast<bitnor_exprt &>(expr);
}

class bitxor_exprt : public multi_ary_exprt
{
public:
  bitxor_exprt(exprt _op0, exprt _op1)
    : multi_ary_exprt(std::move(_op0), ID_bitxor, std::move(_op1))
  {
  }
 
  explicit bitxor_exprt(exprt::operandst _operands)
    : multi_ary_exprt(ID_bitxor, std::move(_operands))
  {
  }
 
  bitxor_exprt(exprt::operandst _operands, typet _type)
    : multi_ary_exprt(ID_bitxor, std::move(_operands), std::move(_type))
  {
  }
};
 
template <>
inline bool can_cast_expr<bitxor_exprt>(const exprt &base)
{
  return base.id() == ID_bitxor;
}

inline const bitxor_exprt &to_bitxor_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_bitxor);
  return static_cast<const bitxor_exprt &>(expr);
}

inline bitxor_exprt &to_bitxor_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_bitxor);
  return static_cast<bitxor_exprt &>(expr);
}

class bitxnor_exprt : public multi_ary_exprt
{
public:
  bitxnor_exprt(exprt _op0, exprt _op1)
    : multi_ary_exprt(_op0, ID_bitxnor, _op1, _op0.type())
  {
  }
 
  explicit bitxnor_exprt(exprt::operandst _operands)
    : multi_ary_exprt(ID_bitxnor, std::move(_operands))
  {
  }
 
  bitxnor_exprt(exprt::operandst _operands, typet _type)
    : multi_ary_exprt(ID_bitxnor, std::move(_operands), std::move(_type))
  {
  }
};
 
template <>
inline bool can_cast_expr<bitxnor_exprt>(const exprt &base)
{
  return base.id() == ID_bitxnor;
}

inline const bitxnor_exprt &to_bitxnor_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_bitxnor);
  bitxnor_exprt::check(expr, validation_modet::INVARIANT);
  return static_cast<const bitxnor_exprt &>(expr);
}

inline bitxnor_exprt &to_bitxnor_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_bitxnor);
  bitxnor_exprt::check(expr, validation_modet::INVARIANT);
  return static_cast<bitxnor_exprt &>(expr);
}

class bitand_exprt : public multi_ary_exprt
{
public:
  bitand_exprt(const exprt &_op0, exprt _op1)
    : multi_ary_exprt(_op0, ID_bitand, std::move(_op1), _op0.type())
  {
  }
 
  explicit bitand_exprt(exprt::operandst _operands)
    : multi_ary_exprt(ID_bitand, std::move(_operands))
  {
  }
 
  bitand_exprt(exprt::operandst _operands, typet _type)
    : multi_ary_exprt(ID_bitand, std::move(_operands), std::move(_type))
  {
  }
};
 
template <>
inline bool can_cast_expr<bitand_exprt>(const exprt &base)
{
  return base.id() == ID_bitand;
}

inline const bitand_exprt &to_bitand_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_bitand);
  return static_cast<const bitand_exprt &>(expr);
}

inline bitand_exprt &to_bitand_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_bitand);
  return static_cast<bitand_exprt &>(expr);
}

class bitnand_exprt : public multi_ary_exprt
{
public:
  bitnand_exprt(exprt _op0, exprt _op1)
    : multi_ary_exprt(std::move(_op0), ID_bitnand, std::move(_op1))
  {
  }
 
  explicit bitnand_exprt(exprt::operandst _operands)
    : multi_ary_exprt(ID_bitnand, std::move(_operands))
  {
  }
 
  bitnand_exprt(exprt::operandst _operands, typet _type)
    : multi_ary_exprt(ID_bitnand, std::move(_operands), std::move(_type))
  {
  }
};
 
template <>
inline bool can_cast_expr<bitnand_exprt>(const exprt &base)
{
  return base.id() == ID_bitnand;
}

inline const bitnand_exprt &to_bitnand_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_bitnand);
  return static_cast<const bitnand_exprt &>(expr);
}

inline bitnand_exprt &to_bitnand_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_bitnand);
  return static_cast<bitnand_exprt &>(expr);
}

class shift_exprt : public binary_exprt
{
public:
  shift_exprt(exprt _src, const irep_idt &_id, exprt _distance)
    : binary_exprt(std::move(_src), _id, std::move(_distance))
  {
  }
 
  shift_exprt(exprt _src, const irep_idt &_id, const std::size_t _distance);
 
  exprt &op()
  {
    return op0();
  }
 
  const exprt &op() const
  {
    return op0();
  }
 
  exprt &distance()
  {
    return op1();
  }
 
  const exprt &distance() const
  {
    return op1();
  }
};
 
template <>
inline bool can_cast_expr<shift_exprt>(const exprt &base)
{
  return base.id() == ID_shl || base.id() == ID_ashr || base.id() == ID_lshr ||
         base.id() == ID_ror || base.id() == ID_rol;
}
 
inline void validate_expr(const shift_exprt &value)
{
  validate_operands(value, 2, "Shifts must have two operands");
}

inline const shift_exprt &to_shift_expr(const exprt &expr)
{
  const shift_exprt &ret = static_cast<const shift_exprt &>(expr);
  validate_expr(ret);
  return ret;
}

inline shift_exprt &to_shift_expr(exprt &expr)
{
  shift_exprt &ret = static_cast<shift_exprt &>(expr);
  validate_expr(ret);
  return ret;
}

class shl_exprt : public shift_exprt
{
public:
  shl_exprt(exprt _src, exprt _distance)
    : shift_exprt(std::move(_src), ID_shl, std::move(_distance))
  {
  }
 
  shl_exprt(exprt _src, const std::size_t _distance)
    : shift_exprt(std::move(_src), ID_shl, _distance)
  {
  }
};
 
template <>
inline bool can_cast_expr<shl_exprt>(const exprt &base)
{
  return base.id() == ID_shl;
}

inline const shl_exprt &to_shl_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_shl);
  const shl_exprt &ret = static_cast<const shl_exprt &>(expr);
  validate_expr(ret);
  return ret;
}

inline shl_exprt &to_shl_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_shl);
  shl_exprt &ret = static_cast<shl_exprt &>(expr);
  validate_expr(ret);
  return ret;
}

class ashr_exprt : public shift_exprt
{
public:
  ashr_exprt(exprt _src, exprt _distance)
    : shift_exprt(std::move(_src), ID_ashr, std::move(_distance))
  {
  }
 
  ashr_exprt(exprt _src, const std::size_t _distance)
    : shift_exprt(std::move(_src), ID_ashr, _distance)
  {
  }
};
 
template <>
inline bool can_cast_expr<ashr_exprt>(const exprt &base)
{
  return base.id() == ID_ashr;
}

class lshr_exprt : public shift_exprt
{
public:
  lshr_exprt(exprt _src, exprt _distance)
    : shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
  {
  }
 
  lshr_exprt(exprt _src, const std::size_t _distance)
    : shift_exprt(std::move(_src), ID_lshr, std::move(_distance))
  {
  }
};
 
template <>
inline bool can_cast_expr<lshr_exprt>(const exprt &base)
{
  return base.id() == ID_lshr;
}

class extractbit_exprt : public binary_predicate_exprt
{
public:
  extractbit_exprt(exprt _src, exprt _index)
    : binary_predicate_exprt(std::move(_src), ID_extractbit, std::move(_index))
  {
  }
 
  extractbit_exprt(exprt _src, const std::size_t _index);
 
  exprt &src()
  {
    return op0();
  }
 
  exprt &index()
  {
    return op1();
  }
 
  const exprt &src() const
  {
    return op0();
  }
 
  const exprt &index() const
  {
    return op1();
  }
};
 
template <>
inline bool can_cast_expr<extractbit_exprt>(const exprt &base)
{
  return base.id() == ID_extractbit;
}
 
inline void validate_expr(const extractbit_exprt &value)
{
  validate_operands(value, 2, "Extract bit must have two operands");
}

inline const extractbit_exprt &to_extractbit_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_extractbit);
  const extractbit_exprt &ret = static_cast<const extractbit_exprt &>(expr);
  validate_expr(ret);
  return ret;
}

inline extractbit_exprt &to_extractbit_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_extractbit);
  extractbit_exprt &ret = static_cast<extractbit_exprt &>(expr);
  validate_expr(ret);
  return ret;
}

class extractbits_exprt : public expr_protectedt
{
public:
  extractbits_exprt(exprt _src, exprt _index, typet _type)
    : expr_protectedt(
        ID_extractbits,
        std::move(_type),
        {std::move(_src), std::move(_index)})
  {
  }
 
  extractbits_exprt(exprt _src, const std::size_t _index, typet _type);
 
  exprt &src()
  {
    return op0();
  }
 
  exprt &index()
  {
    return op1();
  }
 
  const exprt &src() const
  {
    return op0();
  }
 
  const exprt &index() const
  {
    return op1();
  }
};
 
template <>
inline bool can_cast_expr<extractbits_exprt>(const exprt &base)
{
  return base.id() == ID_extractbits;
}
 
inline void validate_expr(const extractbits_exprt &value)
{
  validate_operands(value, 2, "Extractbits must have two operands");
}

inline const extractbits_exprt &to_extractbits_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_extractbits);
  const extractbits_exprt &ret = static_cast<const extractbits_exprt &>(expr);
  validate_expr(ret);
  return ret;
}

inline extractbits_exprt &to_extractbits_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_extractbits);
  extractbits_exprt &ret = static_cast<extractbits_exprt &>(expr);
  validate_expr(ret);
  return ret;
}

class update_bit_exprt : public expr_protectedt
{
public:
  update_bit_exprt(exprt _src, exprt _index, exprt _new_value)
    : expr_protectedt(
        ID_update_bit,
        _src.type(),
        {_src, std::move(_index), std::move(_new_value)})
  {
    PRECONDITION(new_value().type().id() == ID_bool);
  }
 
  update_bit_exprt(exprt _src, const std::size_t _index, exprt _new_value);
 
  exprt &src()
  {
    return op0();
  }
 
  exprt &index()
  {
    return op1();
  }
 
  exprt &new_value()
  {
    return op2();
  }
 
  const exprt &src() const
  {
    return op0();
  }
 
  const exprt &index() const
  {
    return op1();
  }
 
  const exprt &new_value() const
  {
    return op2();
  }
 
  static void check(
    const exprt &expr,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    validate_operands(expr, 3, "update_bit must have three operands");
  }

  exprt lower() const;
};
 
template <>
inline bool can_cast_expr<update_bit_exprt>(const exprt &base)
{
  return base.id() == ID_update_bit;
}

inline const update_bit_exprt &to_update_bit_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_update_bit);
  update_bit_exprt::check(expr);
  return static_cast<const update_bit_exprt &>(expr);
}

inline update_bit_exprt &to_update_bit_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_update_bit);
  update_bit_exprt::check(expr);
  return static_cast<update_bit_exprt &>(expr);
}

class update_bits_exprt : public expr_protectedt
{
public:
  update_bits_exprt(exprt _src, exprt _index, exprt _new_value)
    : expr_protectedt(
        ID_update_bits,
        _src.type(),
        {_src, std::move(_index), std::move(_new_value)})
  {
  }
 
  update_bits_exprt(exprt _src, const std::size_t _index, exprt _new_value);
 
  exprt &src()
  {
    return op0();
  }
 
  exprt &index()
  {
    return op1();
  }
 
  exprt &new_value()
  {
    return op2();
  }
 
  const exprt &src() const
  {
    return op0();
  }
 
  const exprt &index() const
  {
    return op1();
  }
 
  const exprt &new_value() const
  {
    return op2();
  }
 
  static void check(
    const exprt &expr,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    validate_operands(expr, 3, "update_bits must have three operands");
  }

  exprt lower() const;
};
 
template <>
inline bool can_cast_expr<update_bits_exprt>(const exprt &base)
{
  return base.id() == ID_update_bits;
}

inline const update_bits_exprt &to_update_bits_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_update_bits);
  update_bits_exprt::check(expr);
  return static_cast<const update_bits_exprt &>(expr);
}

inline update_bits_exprt &to_update_bits_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_update_bits);
  update_bits_exprt::check(expr);
  return static_cast<update_bits_exprt &>(expr);
}

class replication_exprt : public binary_exprt
{
public:
  replication_exprt(constant_exprt _times, exprt _src, typet _type)
    : binary_exprt(
        std::move(_times),
        ID_replication,
        std::move(_src),
        std::move(_type))
  {
  }
 
  constant_exprt &times()
  {
    return static_cast<constant_exprt &>(op0());
  }
 
  const constant_exprt &times() const
  {
    return static_cast<const constant_exprt &>(op0());
  }
 
  exprt &op()
  {
    return op1();
  }
 
  const exprt &op() const
  {
    return op1();
  }
};
 
template <>
inline bool can_cast_expr<replication_exprt>(const exprt &base)
{
  return base.id() == ID_replication;
}
 
inline void validate_expr(const replication_exprt &value)
{
  validate_operands(value, 2, "Bit-wise replication must have two operands");
}

inline const replication_exprt &to_replication_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_replication);
  const replication_exprt &ret = static_cast<const replication_exprt &>(expr);
  validate_expr(ret);
  return ret;
}

inline replication_exprt &to_replication_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_replication);
  replication_exprt &ret = static_cast<replication_exprt &>(expr);
  validate_expr(ret);
  return ret;
}

class concatenation_exprt : public multi_ary_exprt
{
public:
  concatenation_exprt(operandst _operands, typet _type)
    : multi_ary_exprt(ID_concatenation, std::move(_operands), std::move(_type))
  {
  }
 
  concatenation_exprt(exprt _op0, exprt _op1, typet _type)
    : multi_ary_exprt(
        ID_concatenation,
        {std::move(_op0), std::move(_op1)},
        std::move(_type))
  {
  }
};
 
template <>
inline bool can_cast_expr<concatenation_exprt>(const exprt &base)
{
  return base.id() == ID_concatenation;
}

inline const concatenation_exprt &to_concatenation_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_concatenation);
  return static_cast<const concatenation_exprt &>(expr);
}

inline concatenation_exprt &to_concatenation_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_concatenation);
  return static_cast<concatenation_exprt &>(expr);
}

class popcount_exprt : public unary_exprt
{
public:
  popcount_exprt(exprt _op, typet _type)
    : unary_exprt(ID_popcount, std::move(_op), std::move(_type))
  {
  }
 
  explicit popcount_exprt(const exprt &_op)
    : unary_exprt(ID_popcount, _op, _op.type())
  {
  }

  exprt lower() const;
};
 
template <>
inline bool can_cast_expr<popcount_exprt>(const exprt &base)
{
  return base.id() == ID_popcount;
}
 
inline void validate_expr(const popcount_exprt &value)
{
  validate_operands(value, 1, "popcount must have one operand");
}

inline const popcount_exprt &to_popcount_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_popcount);
  const popcount_exprt &ret = static_cast<const popcount_exprt &>(expr);
  validate_expr(ret);
  return ret;
}

inline popcount_exprt &to_popcount_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_popcount);
  popcount_exprt &ret = static_cast<popcount_exprt &>(expr);
  validate_expr(ret);
  return ret;
}

class binary_overflow_exprt : public binary_predicate_exprt
{
public:
  binary_overflow_exprt(exprt _lhs, const irep_idt &kind, exprt _rhs)
    : binary_predicate_exprt(std::move(_lhs), make_id(kind), std::move(_rhs))
  {
    INVARIANT(
      valid_id(id()),
      "The kind used to construct binary_overflow_exprt should be in the set "
      "of expected valid kinds.");
  }
 
  static void check(
    const exprt &expr,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    binary_exprt::check(expr, vm);
 
    if(expr.id() != ID_overflow_shl)
    {
      const binary_exprt &binary_expr = to_binary_expr(expr);
      DATA_CHECK(
        vm,
        binary_expr.lhs().type() == binary_expr.rhs().type(),
        "operand types must match");
    }
  }
 
  static void validate(
    const exprt &expr,
    const namespacet &,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    check(expr, vm);
  }

  static bool valid_id(const irep_idt &id)
  {
    return id == ID_overflow_plus || id == ID_overflow_mult ||
           id == ID_overflow_minus || id == ID_overflow_shl;
  }
 
private:
  static irep_idt make_id(const irep_idt &kind)
  {
    if(valid_id(kind))
      return kind;
    else
      return "overflow-" + id2string(kind);
  }
};
 
template <>
inline bool can_cast_expr<binary_overflow_exprt>(const exprt &base)
{
  return binary_overflow_exprt::valid_id(base.id());
}
 
inline void validate_expr(const binary_overflow_exprt &value)
{
  validate_operands(
    value, 2, "binary overflow expression must have two operands");
}

inline const binary_overflow_exprt &to_binary_overflow_expr(const exprt &expr)
{
  PRECONDITION(
    expr.id() == ID_overflow_plus || expr.id() == ID_overflow_mult ||
    expr.id() == ID_overflow_minus || expr.id() == ID_overflow_shl);
  const binary_overflow_exprt &ret =
    static_cast<const binary_overflow_exprt &>(expr);
  validate_expr(ret);
  return ret;
}

inline binary_overflow_exprt &to_binary_overflow_expr(exprt &expr)
{
  PRECONDITION(
    expr.id() == ID_overflow_plus || expr.id() == ID_overflow_mult ||
    expr.id() == ID_overflow_minus || expr.id() == ID_overflow_shl);
  binary_overflow_exprt &ret = static_cast<binary_overflow_exprt &>(expr);
  validate_expr(ret);
  return ret;
}
 
class plus_overflow_exprt : public binary_overflow_exprt
{
public:
  plus_overflow_exprt(exprt _lhs, exprt _rhs)
    : binary_overflow_exprt(std::move(_lhs), ID_overflow_plus, std::move(_rhs))
  {
  }

  exprt lower() const;
};
 
template <>
inline bool can_cast_expr<plus_overflow_exprt>(const exprt &base)
{
  return base.id() == ID_overflow_plus;
}
 
class minus_overflow_exprt : public binary_overflow_exprt
{
public:
  minus_overflow_exprt(exprt _lhs, exprt _rhs)
    : binary_overflow_exprt(std::move(_lhs), ID_overflow_minus, std::move(_rhs))
  {
  }

  exprt lower() const;
};
 
template <>
inline bool can_cast_expr<minus_overflow_exprt>(const exprt &base)
{
  return base.id() == ID_overflow_minus;
}
 
class mult_overflow_exprt : public binary_overflow_exprt
{
public:
  mult_overflow_exprt(exprt _lhs, exprt _rhs)
    : binary_overflow_exprt(std::move(_lhs), ID_overflow_mult, std::move(_rhs))
  {
  }

  exprt lower() const;
};
 
template <>
inline bool can_cast_expr<mult_overflow_exprt>(const exprt &base)
{
  return base.id() == ID_overflow_mult;
}
 
class shl_overflow_exprt : public binary_overflow_exprt
{
public:
  shl_overflow_exprt(exprt _lhs, exprt _rhs)
    : binary_overflow_exprt(std::move(_lhs), ID_overflow_shl, std::move(_rhs))
  {
  }
};
 
template <>
inline bool can_cast_expr<shl_overflow_exprt>(const exprt &base)
{
  return base.id() == ID_overflow_shl;
}

class unary_overflow_exprt : public unary_predicate_exprt
{
public:
  unary_overflow_exprt(const irep_idt &kind, exprt _op)
    : unary_predicate_exprt("overflow-" + id2string(kind), std::move(_op))
  {
  }
 
  static void check(
    const exprt &expr,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    unary_exprt::check(expr, vm);
  }
 
  static void validate(
    const exprt &expr,
    const namespacet &,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    check(expr, vm);
  }
};
 
template <>
inline bool can_cast_expr<unary_overflow_exprt>(const exprt &base)
{
  return base.id() == ID_overflow_unary_minus;
}
 
inline void validate_expr(const unary_overflow_exprt &value)
{
  validate_operands(
    value, 1, "unary overflow expression must have one operand");
}

class unary_minus_overflow_exprt : public unary_overflow_exprt
{
public:
  explicit unary_minus_overflow_exprt(exprt _op)
    : unary_overflow_exprt(ID_unary_minus, std::move(_op))
  {
  }
 
  static void check(
    const exprt &expr,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    unary_exprt::check(expr, vm);
  }
 
  static void validate(
    const exprt &expr,
    const namespacet &,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    check(expr, vm);
  }
};
 
template <>
inline bool can_cast_expr<unary_minus_overflow_exprt>(const exprt &base)
{
  return base.id() == ID_overflow_unary_minus;
}
 
inline void validate_expr(const unary_minus_overflow_exprt &value)
{
  validate_operands(
    value, 1, "unary minus overflow expression must have one operand");
}

inline const unary_overflow_exprt &to_unary_overflow_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_overflow_unary_minus);
  const unary_overflow_exprt &ret =
    static_cast<const unary_overflow_exprt &>(expr);
  validate_expr(ret);
  return ret;
}

inline unary_overflow_exprt &to_unary_overflow_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_overflow_unary_minus);
  unary_overflow_exprt &ret = static_cast<unary_overflow_exprt &>(expr);
  validate_expr(ret);
  return ret;
}

class count_leading_zeros_exprt : public unary_exprt
{
public:
  count_leading_zeros_exprt(exprt _op, bool _zero_permitted, typet _type)
    : unary_exprt(ID_count_leading_zeros, std::move(_op), std::move(_type))
  {
    zero_permitted(_zero_permitted);
  }
 
  explicit count_leading_zeros_exprt(const exprt &_op)
    : count_leading_zeros_exprt(_op, true, _op.type())
  {
  }
 
  bool zero_permitted() const
  {
    return !get_bool(ID_C_bounds_check);
  }
 
  void zero_permitted(bool value)
  {
    set(ID_C_bounds_check, !value);
  }
 
  static void check(
    const exprt &expr,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    DATA_CHECK(
      vm,
      expr.operands().size() == 1,
      "unary expression must have a single operand");
    DATA_CHECK(
      vm,
      can_cast_type<bitvector_typet>(to_unary_expr(expr).op().type()),
      "operand must be of bitvector type");
  }
 
  static void validate(
    const exprt &expr,
    const namespacet &,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    check(expr, vm);
  }

  exprt lower() const;
};
 
template <>
inline bool can_cast_expr<count_leading_zeros_exprt>(const exprt &base)
{
  return base.id() == ID_count_leading_zeros;
}
 
inline void validate_expr(const count_leading_zeros_exprt &value)
{
  validate_operands(value, 1, "count_leading_zeros must have one operand");
}

inline const count_leading_zeros_exprt &
to_count_leading_zeros_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_count_leading_zeros);
  const count_leading_zeros_exprt &ret =
    static_cast<const count_leading_zeros_exprt &>(expr);
  validate_expr(ret);
  return ret;
}

inline count_leading_zeros_exprt &to_count_leading_zeros_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_count_leading_zeros);
  count_leading_zeros_exprt &ret =
    static_cast<count_leading_zeros_exprt &>(expr);
  validate_expr(ret);
  return ret;
}

class count_trailing_zeros_exprt : public unary_exprt
{
public:
  count_trailing_zeros_exprt(exprt _op, bool _zero_permitted, typet _type)
    : unary_exprt(ID_count_trailing_zeros, std::move(_op), std::move(_type))
  {
    zero_permitted(_zero_permitted);
  }
 
  explicit count_trailing_zeros_exprt(const exprt &_op)
    : count_trailing_zeros_exprt(_op, true, _op.type())
  {
  }
 
  bool zero_permitted() const
  {
    return !get_bool(ID_C_bounds_check);
  }
 
  void zero_permitted(bool value)
  {
    set(ID_C_bounds_check, !value);
  }
 
  static void check(
    const exprt &expr,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    DATA_CHECK(
      vm,
      expr.operands().size() == 1,
      "unary expression must have a single operand");
    DATA_CHECK(
      vm,
      can_cast_type<bitvector_typet>(to_unary_expr(expr).op().type()),
      "operand must be of bitvector type");
  }
 
  static void validate(
    const exprt &expr,
    const namespacet &,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    check(expr, vm);
  }

  exprt lower() const;
};
 
template <>
inline bool can_cast_expr<count_trailing_zeros_exprt>(const exprt &base)
{
  return base.id() == ID_count_trailing_zeros;
}
 
inline void validate_expr(const count_trailing_zeros_exprt &value)
{
  validate_operands(value, 1, "count_trailing_zeros must have one operand");
}

inline const count_trailing_zeros_exprt &
to_count_trailing_zeros_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_count_trailing_zeros);
  const count_trailing_zeros_exprt &ret =
    static_cast<const count_trailing_zeros_exprt &>(expr);
  validate_expr(ret);
  return ret;
}

inline count_trailing_zeros_exprt &to_count_trailing_zeros_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_count_trailing_zeros);
  count_trailing_zeros_exprt &ret =
    static_cast<count_trailing_zeros_exprt &>(expr);
  validate_expr(ret);
  return ret;
}

class bitreverse_exprt : public unary_exprt
{
public:
  explicit bitreverse_exprt(exprt op)
    : unary_exprt(ID_bitreverse, std::move(op))
  {
  }

  exprt lower() const;
};
 
template <>
inline bool can_cast_expr<bitreverse_exprt>(const exprt &base)
{
  return base.id() == ID_bitreverse;
}
 
inline void validate_expr(const bitreverse_exprt &value)
{
  validate_operands(value, 1, "Bit-wise reverse must have one operand");
}

inline const bitreverse_exprt &to_bitreverse_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_bitreverse);
  const bitreverse_exprt &ret = static_cast<const bitreverse_exprt &>(expr);
  validate_expr(ret);
  return ret;
}

inline bitreverse_exprt &to_bitreverse_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_bitreverse);
  bitreverse_exprt &ret = static_cast<bitreverse_exprt &>(expr);
  validate_expr(ret);
  return ret;
}

class saturating_plus_exprt : public binary_exprt
{
public:
  saturating_plus_exprt(exprt _lhs, exprt _rhs)
    : binary_exprt(std::move(_lhs), ID_saturating_plus, std::move(_rhs))
  {
  }
 
  saturating_plus_exprt(exprt _lhs, exprt _rhs, typet _type)
    : binary_exprt(
        std::move(_lhs),
        ID_saturating_plus,
        std::move(_rhs),
        std::move(_type))
  {
  }
};
 
template <>
inline bool can_cast_expr<saturating_plus_exprt>(const exprt &base)
{
  return base.id() == ID_saturating_plus;
}
 
inline void validate_expr(const saturating_plus_exprt &value)
{
  validate_operands(value, 2, "saturating plus must have two operands");
}

inline const saturating_plus_exprt &to_saturating_plus_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_saturating_plus);
  const saturating_plus_exprt &ret =
    static_cast<const saturating_plus_exprt &>(expr);
  validate_expr(ret);
  return ret;
}

inline saturating_plus_exprt &to_saturating_plus_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_saturating_plus);
  saturating_plus_exprt &ret = static_cast<saturating_plus_exprt &>(expr);
  validate_expr(ret);
  return ret;
}

class saturating_minus_exprt : public binary_exprt
{
public:
  saturating_minus_exprt(exprt _lhs, exprt _rhs)
    : binary_exprt(std::move(_lhs), ID_saturating_minus, std::move(_rhs))
  {
  }
};
 
template <>
inline bool can_cast_expr<saturating_minus_exprt>(const exprt &base)
{
  return base.id() == ID_saturating_minus;
}
 
inline void validate_expr(const saturating_minus_exprt &value)
{
  validate_operands(value, 2, "saturating minus must have two operands");
}

inline const saturating_minus_exprt &to_saturating_minus_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_saturating_minus);
  const saturating_minus_exprt &ret =
    static_cast<const saturating_minus_exprt &>(expr);
  validate_expr(ret);
  return ret;
}

inline saturating_minus_exprt &to_saturating_minus_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_saturating_minus);
  saturating_minus_exprt &ret = static_cast<saturating_minus_exprt &>(expr);
  validate_expr(ret);
  return ret;
}

class overflow_result_exprt : public expr_protectedt
{
public:
  overflow_result_exprt(exprt _lhs, const irep_idt &kind, exprt _rhs)
    : expr_protectedt(
        make_id(kind),
        struct_typet{
          {{ID_value, _lhs.type()},
           {"overflow-" + id2string(kind), bool_typet{}}}},
        {_lhs, std::move(_rhs)})
  {
    INVARIANT(
      valid_id(id()),
      "The kind used to construct overflow_result_exprt should be in the set "
      "of expected valid kinds.");
  }
 
  overflow_result_exprt(exprt _op, const irep_idt &kind)
    : expr_protectedt(
        make_id(kind),
        struct_typet{
          {{ID_value, _op.type()},
           {"overflow-" + id2string(kind), bool_typet{}}}},
        {_op})
  {
    INVARIANT(
      valid_id(id()),
      "The kind used to construct overflow_result_exprt should be in the set "
      "of expected valid kinds.");
  }
 
  // 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;
 
  static void check(
    const exprt &expr,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    if(expr.id() != ID_overflow_result_unary_minus)
      binary_exprt::check(expr, vm);
 
    if(
      expr.id() != ID_overflow_result_unary_minus &&
      expr.id() != ID_overflow_result_shl)
    {
      const binary_exprt &binary_expr = to_binary_expr(expr);
      DATA_CHECK(
        vm,
        binary_expr.lhs().type() == binary_expr.rhs().type(),
        "operand types must match");
    }
  }
 
  static void validate(
    const exprt &expr,
    const namespacet &,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    check(expr, vm);
  }

  static bool valid_id(const irep_idt &id)
  {
    return id == ID_overflow_result_plus || id == ID_overflow_result_mult ||
           id == ID_overflow_result_minus || id == ID_overflow_result_shl ||
           id == ID_overflow_result_unary_minus;
  }
 
private:
  static irep_idt make_id(const irep_idt &kind)
  {
    return "overflow_result-" + id2string(kind);
  }
};
 
template <>
inline bool can_cast_expr<overflow_result_exprt>(const exprt &base)
{
  return overflow_result_exprt::valid_id(base.id());
}
 
inline void validate_expr(const overflow_result_exprt &value)
{
  if(value.id() == ID_overflow_result_unary_minus)
  {
    validate_operands(
      value, 1, "unary overflow expression must have two operands");
  }
  else
  {
    validate_operands(
      value, 2, "binary overflow expression must have two operands");
  }
}

inline const overflow_result_exprt &to_overflow_result_expr(const exprt &expr)
{
  PRECONDITION(overflow_result_exprt::valid_id(expr.id()));
  const overflow_result_exprt &ret =
    static_cast<const overflow_result_exprt &>(expr);
  validate_expr(ret);
  return ret;
}

inline overflow_result_exprt &to_overflow_result_expr(exprt &expr)
{
  PRECONDITION(overflow_result_exprt::valid_id(expr.id()));
  overflow_result_exprt &ret = static_cast<overflow_result_exprt &>(expr);
  validate_expr(ret);
  return ret;
}

class find_first_set_exprt : public unary_exprt
{
public:
  find_first_set_exprt(exprt _op, typet _type)
    : unary_exprt(ID_find_first_set, std::move(_op), std::move(_type))
  {
  }
 
  explicit find_first_set_exprt(const exprt &_op)
    : find_first_set_exprt(_op, _op.type())
  {
  }
 
  static void check(
    const exprt &expr,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    DATA_CHECK(
      vm,
      expr.operands().size() == 1,
      "unary expression must have a single operand");
    DATA_CHECK(
      vm,
      can_cast_type<bitvector_typet>(to_unary_expr(expr).op().type()),
      "operand must be of bitvector type");
  }
 
  static void validate(
    const exprt &expr,
    const namespacet &,
    const validation_modet vm = validation_modet::INVARIANT)
  {
    check(expr, vm);
  }

  exprt lower() const;
};
 
template <>
inline bool can_cast_expr<find_first_set_exprt>(const exprt &base)
{
  return base.id() == ID_find_first_set;
}
 
inline void validate_expr(const find_first_set_exprt &value)
{
  validate_operands(value, 1, "find_first_set must have one operand");
}

inline const find_first_set_exprt &to_find_first_set_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_find_first_set);
  const find_first_set_exprt &ret =
    static_cast<const find_first_set_exprt &>(expr);
  validate_expr(ret);
  return ret;
}

inline find_first_set_exprt &to_find_first_set_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_find_first_set);
  find_first_set_exprt &ret = static_cast<find_first_set_exprt &>(expr);
  validate_expr(ret);
  return ret;
}

class zero_extend_exprt : public unary_exprt
{
public:
  zero_extend_exprt(exprt _op, typet _type)
    : unary_exprt(ID_zero_extend, std::move(_op), std::move(_type))
  {
  }
 
  // a lowering to extraction or concatenation
  exprt lower() const;
};
 
template <>
inline bool can_cast_expr<zero_extend_exprt>(const exprt &base)
{
  return base.id() == ID_zero_extend;
}

inline const zero_extend_exprt &to_zero_extend_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_zero_extend);
  zero_extend_exprt::check(expr);
  return static_cast<const zero_extend_exprt &>(expr);
}

inline zero_extend_exprt &to_zero_extend_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_zero_extend);
  zero_extend_exprt::check(expr);
  return static_cast<zero_extend_exprt &>(expr);
}

class onehot_exprt : public unary_predicate_exprt
{
public:
  explicit onehot_exprt(exprt _op)
    : unary_predicate_exprt(ID_onehot, std::move(_op))
  {
  }

  exprt lower() const;
};

inline const onehot_exprt &to_onehot_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_onehot);
  onehot_exprt::check(expr);
  return static_cast<const onehot_exprt &>(expr);
}

inline onehot_exprt &to_onehot_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_onehot);
  onehot_exprt::check(expr);
  return static_cast<onehot_exprt &>(expr);
}

class onehot0_exprt : public unary_predicate_exprt
{
public:
  explicit onehot0_exprt(exprt _op)
    : unary_predicate_exprt(ID_onehot0, std::move(_op))
  {
  }

  exprt lower() const;
};

inline const onehot0_exprt &to_onehot0_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_onehot0);
  onehot0_exprt::check(expr);
  return static_cast<const onehot0_exprt &>(expr);
}

inline onehot0_exprt &to_onehot0_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_onehot0);
  onehot0_exprt::check(expr);
  return static_cast<onehot0_exprt &>(expr);
}

class reduction_and_exprt : public unary_predicate_exprt
{
public:
  explicit reduction_and_exprt(exprt _op)
    : unary_predicate_exprt(ID_reduction_and, std::move(_op))
  {
  }
};
 
template <>
inline bool can_cast_expr<reduction_and_exprt>(const exprt &expr)
{
  return expr.id() == ID_reduction_and;
}

inline const reduction_and_exprt &to_reduction_and_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_reduction_and);
  reduction_and_exprt::check(expr);
  return static_cast<const reduction_and_exprt &>(expr);
}

inline reduction_and_exprt &to_reduction_and_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_reduction_and);
  reduction_and_exprt::check(expr);
  return static_cast<reduction_and_exprt &>(expr);
}

class reduction_or_exprt : public unary_predicate_exprt
{
public:
  explicit reduction_or_exprt(exprt _op)
    : unary_predicate_exprt(ID_reduction_or, std::move(_op))
  {
  }
};
 
template <>
inline bool can_cast_expr<reduction_or_exprt>(const exprt &expr)
{
  return expr.id() == ID_reduction_or;
}

inline const reduction_or_exprt &to_reduction_or_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_reduction_or);
  reduction_or_exprt::check(expr);
  return static_cast<const reduction_or_exprt &>(expr);
}

inline reduction_or_exprt &to_reduction_or_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_reduction_or);
  reduction_or_exprt::check(expr);
  return static_cast<reduction_or_exprt &>(expr);
}

class reduction_nor_exprt : public unary_predicate_exprt
{
public:
  explicit reduction_nor_exprt(exprt _op)
    : unary_predicate_exprt(ID_reduction_nor, std::move(_op))
  {
  }
};
 
template <>
inline bool can_cast_expr<reduction_nor_exprt>(const exprt &expr)
{
  return expr.id() == ID_reduction_nor;
}

inline const reduction_nor_exprt &to_reduction_nor_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_reduction_nor);
  reduction_nor_exprt::check(expr);
  return static_cast<const reduction_nor_exprt &>(expr);
}

inline reduction_nor_exprt &to_reduction_nor_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_reduction_nor);
  reduction_nor_exprt::check(expr);
  return static_cast<reduction_nor_exprt &>(expr);
}

class reduction_nand_exprt : public unary_predicate_exprt
{
public:
  explicit reduction_nand_exprt(exprt _op)
    : unary_predicate_exprt(ID_reduction_nand, std::move(_op))
  {
  }
};
 
template <>
inline bool can_cast_expr<reduction_nand_exprt>(const exprt &expr)
{
  return expr.id() == ID_reduction_nand;
}

inline const reduction_nand_exprt &to_reduction_nand_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_reduction_nand);
  reduction_nand_exprt::check(expr);
  return static_cast<const reduction_nand_exprt &>(expr);
}

inline reduction_nand_exprt &to_reduction_nand_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_reduction_nand);
  reduction_nand_exprt::check(expr);
  return static_cast<reduction_nand_exprt &>(expr);
}

class reduction_xor_exprt : public unary_predicate_exprt
{
public:
  explicit reduction_xor_exprt(exprt _op)
    : unary_predicate_exprt(ID_reduction_xor, std::move(_op))
  {
  }
};
 
template <>
inline bool can_cast_expr<reduction_xor_exprt>(const exprt &expr)
{
  return expr.id() == ID_reduction_xor;
}

inline const reduction_xor_exprt &to_reduction_xor_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_reduction_xor);
  reduction_xor_exprt::check(expr);
  return static_cast<const reduction_xor_exprt &>(expr);
}

inline reduction_xor_exprt &to_reduction_xor_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_reduction_xor);
  reduction_xor_exprt::check(expr);
  return static_cast<reduction_xor_exprt &>(expr);
}

class reduction_xnor_exprt : public unary_predicate_exprt
{
public:
  explicit reduction_xnor_exprt(exprt _op)
    : unary_predicate_exprt(ID_reduction_xnor, std::move(_op))
  {
  }
};
 
template <>
inline bool can_cast_expr<reduction_xnor_exprt>(const exprt &expr)
{
  return expr.id() == ID_reduction_xnor;
}

inline const reduction_xnor_exprt &to_reduction_xnor_expr(const exprt &expr)
{
  PRECONDITION(expr.id() == ID_reduction_xnor);
  reduction_xnor_exprt::check(expr);
  return static_cast<const reduction_xnor_exprt &>(expr);
}

inline reduction_xnor_exprt &to_reduction_xnor_expr(exprt &expr)
{
  PRECONDITION(expr.id() == ID_reduction_xnor);
  reduction_xnor_exprt::check(expr);
  return static_cast<reduction_xnor_exprt &>(expr);
}
 
#endif // CPROVER_UTIL_BITVECTOR_EXPR_H