cprover
smt_bit_vector_theory.cpp
Go to the documentation of this file.
1
// Author: Diffblue Ltd.
2
3
#include <
solvers/smt2_incremental/smt_bit_vector_theory.h
>
4
5
#include <
util/invariant.h
>
6
7
static
void
validate_bit_vector_predicate_arguments
(
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
solvers
smt2_incremental
smt_bit_vector_theory.cpp
Generated by
1.8.20