cprover
smt_bit_vector_theory.h File Reference
#include <solvers/smt2_incremental/smt_terms.h>
#include "smt_bit_vector_theory.def"
+ Include dependency graph for smt_bit_vector_theory.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

class  smt_bit_vector_theoryt
 

Macros

#define SMT_BITVECTOR_THEORY_PREDICATE(the_identifier, the_name)
 

Macro Definition Documentation

◆ SMT_BITVECTOR_THEORY_PREDICATE

#define SMT_BITVECTOR_THEORY_PREDICATE (   the_identifier,
  the_name 
)
Value:
/* NOLINTNEXTLINE(readability/identifiers) cpplint does not match the ## */ \
struct the_name##t final \
{ \
static const char *identifier(); \
static smt_sortt \
return_sort(const smt_termt &left, const smt_termt &right); \
static void validate(const smt_termt &left, const smt_termt &right); \
}; \
static bool validate(const string_refinementt::infot &info)

Definition at line 11 of file smt_bit_vector_theory.h.