cprover
smt_bit_vector_theory.h
Go to the documentation of this file.
1 // Author: Diffblue Ltd.
2 
3 #ifndef CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BIT_VECTOR_THEORY_H
4 #define CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BIT_VECTOR_THEORY_H
5 
7 
9 {
10 public:
11 #define SMT_BITVECTOR_THEORY_PREDICATE(the_identifier, the_name) \
12  /* NOLINTNEXTLINE(readability/identifiers) cpplint does not match the ## */ \
13  struct the_name##t final \
14  { \
15  static const char *identifier(); \
16  static smt_sortt \
17  return_sort(const smt_termt &left, const smt_termt &right); \
18  static void validate(const smt_termt &left, const smt_termt &right); \
19  }; \
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
23 };
24 
25 #endif // CPROVER_SOLVERS_SMT2_INCREMENTAL_SMT_BIT_VECTOR_THEORY_H