12 INVARIANT(left_sort,
"Left operand must have bitvector sort.");
14 INVARIANT(right_sort,
"Right operand must have bitvector sort.");
18 left_sort->bit_width() == right_sort->bit_width(),
19 "Left and right operands must have the same bit width.");
382 INVARIANT(operand_sort,
"The operand is expected to have a bit-vector sort.");
static const smt_function_application_termt::factoryt< unsigned_less_than_or_equalt > unsigned_less_than_or_equal
static const smt_function_application_termt::factoryt< signed_less_than_or_equalt > signed_less_than_or_equal
static const smt_function_application_termt::factoryt< addt > add
static const smt_function_application_termt::factoryt< signed_greater_than_or_equalt > signed_greater_than_or_equal
static const smt_function_application_termt::factoryt< unsigned_greater_thant > unsigned_greater_than
static const smt_function_application_termt::factoryt< unsigned_remaindert > unsigned_remainder
static const smt_function_application_termt::factoryt< unsigned_greater_than_or_equalt > unsigned_greater_than_or_equal
static const smt_function_application_termt::factoryt< multiplyt > multiply
static const smt_function_application_termt::factoryt< signed_less_thant > signed_less_than
static const smt_function_application_termt::factoryt< signed_greater_thant > signed_greater_than
static const smt_function_application_termt::factoryt< negatet > negate
static const smt_function_application_termt::factoryt< unsigned_dividet > unsigned_divide
static const smt_function_application_termt::factoryt< unsigned_less_thant > unsigned_less_than
static const smt_function_application_termt::factoryt< signed_dividet > signed_divide
static const smt_function_application_termt::factoryt< signed_remaindert > signed_remainder
static const smt_function_application_termt::factoryt< subtractt > subtract
const sub_classt * cast() const &
const smt_sortt & get_sort() const
static void validate_bit_vector_operator_arguments(const smt_termt &left, const smt_termt &right)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static const char * identifier()
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static const char * identifier()
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static const char * identifier()
static void validate(const smt_termt &operand)
static smt_sortt return_sort(const smt_termt &operand)
static const char * identifier()
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static const char * identifier()
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static const char * identifier()
static const char * identifier()
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static const char * identifier()
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static const char * identifier()
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static const char * identifier()
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static const char * identifier()
static const char * identifier()
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static const char * identifier()
static const char * identifier()
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static const char * identifier()
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)
static const char * identifier()
static void validate(const smt_termt &lhs, const smt_termt &rhs)
static smt_sortt return_sort(const smt_termt &lhs, const smt_termt &rhs)