cprover
smt_bit_vector_theory.cpp File Reference
#include <solvers/smt2_incremental/smt_bit_vector_theory.h>
#include <util/invariant.h>
#include "smt_bit_vector_theory.def"
+ Include dependency graph for smt_bit_vector_theory.cpp:

Go to the source code of this file.

Macros

#define SMT_BITVECTOR_THEORY_PREDICATE(the_identifier, the_name)
 

Functions

static void validate_bit_vector_predicate_arguments (const smt_termt &left, const smt_termt &right)
 

Macro Definition Documentation

◆ SMT_BITVECTOR_THEORY_PREDICATE

#define SMT_BITVECTOR_THEORY_PREDICATE (   the_identifier,
  the_name 
)
Value:
void smt_bit_vector_theoryt::the_name##t::validate( \
const smt_termt &left, const smt_termt &right) \
{ \
validate_bit_vector_predicate_arguments(left, right); \
} \
\
smt_sortt smt_bit_vector_theoryt::the_name##t::return_sort( \
const smt_termt &, const smt_termt &) \
{ \
return smt_bool_sortt{}; \
} \
\
const char *smt_bit_vector_theoryt::the_name##t::identifier() \
{ \
return #the_identifier; \
} \
\
smt_bit_vector_theoryt::the_name##t> \
smt_bit_vector_theoryt::the_name{};

Definition at line 22 of file smt_bit_vector_theory.cpp.

Function Documentation

◆ validate_bit_vector_predicate_arguments()

static void validate_bit_vector_predicate_arguments ( const smt_termt left,
const smt_termt right 
)
static

Definition at line 7 of file smt_bit_vector_theory.cpp.

smt_termt
Definition: smt_terms.h:16
validate
static bool validate(const string_refinementt::infot &info)
Definition: string_refinement.cpp:150
smt_bool_sortt
Definition: smt_sorts.h:78
smt_function_application_termt::factoryt
Definition: smt_terms.h:130