CBMC
boolbv_if.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module:
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
9
10
#include "
boolbv.h
"
11
12
bvt
boolbvt::convert_if
(
const
if_exprt
&expr)
13
{
14
std::size_t width=
boolbv_width
(expr.
type
());
15
16
if
(width==0)
17
return
bvt
();
// An empty bit-vector if.
18
19
literalt
cond=
convert
(expr.
cond
());
20
21
const
bvt
&true_case_bv =
convert_bv
(expr.
true_case
(), width);
22
const
bvt
&false_case_bv =
convert_bv
(expr.
false_case
(), width);
23
24
return
bv_utils
.
select
(cond, true_case_bv, false_case_bv);
25
}
bvt
std::vector< literalt > bvt
Definition:
literal.h:201
if_exprt
The trinary if-then-else operator.
Definition:
std_expr.h:2322
bv_utilst::select
bvt select(literalt s, const bvt &a, const bvt &b)
If s is true, selects a otherwise selects b.
Definition:
bv_utils.cpp:92
if_exprt::false_case
exprt & false_case()
Definition:
std_expr.h:2360
exprt::type
typet & type()
Return the type of the expression.
Definition:
expr.h:84
boolbvt::boolbv_width
virtual std::size_t boolbv_width(const typet &type) const
Definition:
boolbv.h:102
boolbvt::convert_bv
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width={})
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition:
boolbv.cpp:39
boolbvt::convert_if
virtual bvt convert_if(const if_exprt &expr)
Definition:
boolbv_if.cpp:12
prop_conv_solvert::convert
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
Definition:
prop_conv_solver.cpp:156
if_exprt::true_case
exprt & true_case()
Definition:
std_expr.h:2350
boolbvt::bv_utils
bv_utilst bv_utils
Definition:
boolbv.h:117
if_exprt::cond
exprt & cond()
Definition:
std_expr.h:2340
literalt
Definition:
literal.h:25
boolbv.h
src
solvers
flattening
boolbv_if.cpp
Generated by
1.8.17