Go to the documentation of this file.
3 #ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BIT_VECTOR_THEORY_H
4 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BIT_VECTOR_THEORY_H
11 #define SMT_BITVECTOR_THEORY_PREDICATE(the_identifier, the_name) \
13 struct the_name##t final \
15 static const char *identifier(); \
17 return_sort(const smt_termt &left, const smt_termt &right); \
18 static void validate(const smt_termt &left, const smt_termt &right); \
20 static const smt_function_application_termt::factoryt<the_name##t> the_name;
21 #include "smt_bit_vector_theory.def"
22 #undef SMT_BITVECTOR_THEORY_PREDICATE
25 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BIT_VECTOR_THEORY_H