cprover
smt_bit_vector_theory.cpp
Go to the documentation of this file.
1 // Author: Diffblue Ltd.
2 
4 
5 #include <util/invariant.h>
6 
8  const smt_termt &left,
9  const smt_termt &right)
10 {
11  const auto left_sort = left.get_sort().cast<smt_bit_vector_sortt>();
12  INVARIANT(left_sort, "Left operand must have bitvector sort.");
13  const auto right_sort = right.get_sort().cast<smt_bit_vector_sortt>();
14  INVARIANT(right_sort, "Right operand must have bitvector sort.");
15  // The below invariant is based on the smtlib standard.
16  // See http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV
17  INVARIANT(
18  left_sort->bit_width() == right_sort->bit_width(),
19  "Left and right operands must have the same bit width.");
20 }
21 
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) \
25  { \
26  validate_bit_vector_predicate_arguments(left, right); \
27  } \
28  \
29  smt_sortt smt_bit_vector_theoryt::the_name##t::return_sort( \
30  const smt_termt &, const smt_termt &) \
31  { \
32  return smt_bool_sortt{}; \
33  } \
34  \
35  const char *smt_bit_vector_theoryt::the_name##t::identifier() \
36  { \
37  return #the_identifier; \
38  } \
39  \
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
smt_bit_vector_theory.h
smt_termt
Definition: smt_terms.h:16
invariant.h
smt_bit_vector_sortt
Definition: smt_sorts.h:84
smt_sortt::cast
const sub_classt * cast() const &
validate_bit_vector_predicate_arguments
static void validate_bit_vector_predicate_arguments(const smt_termt &left, const smt_termt &right)
Definition: smt_bit_vector_theory.cpp:7
smt_termt::get_sort
const smt_sortt & get_sort() const
Definition: smt_terms.cpp:35
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423