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.");
22 #define SMT_BITVECTOR_THEORY_PREDICATE(the_identifier, the_name) \
23 void smt_bit_vector_theoryt::the_name##t::validate( \
24 const smt_termt &left, const smt_termt &right) \
26 validate_bit_vector_predicate_arguments(left, right); \
29 smt_sortt smt_bit_vector_theoryt::the_name##t::return_sort( \
30 const smt_termt &, const smt_termt &) \
32 return smt_bool_sortt{}; \
35 const char *smt_bit_vector_theoryt::the_name##t::identifier() \
37 return #the_identifier; \
40 const smt_function_application_termt::factoryt< \
41 smt_bit_vector_theoryt::the_name##t> \
42 smt_bit_vector_theoryt::the_name{};
43 #include "smt_bit_vector_theory.def"
44 #undef SMT_BITVECTOR_THEORY_PREDICATE
const sub_classt * cast() const &
const smt_sortt & get_sort() const
static void validate_bit_vector_predicate_arguments(const smt_termt &left, const smt_termt &right)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.