cprover
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 
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:2964
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:96
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:3001
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
boolbvt::boolbv_width
boolbv_widtht boolbv_width
Definition: boolbv.h:95
boolbvt::convert_if
virtual bvt convert_if(const if_exprt &expr)
Definition: boolbv_if.cpp:12
boolbvt::convert_bv
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition: boolbv.cpp:119
prop_conv_solvert::convert
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
Definition: prop_conv_solver.cpp:168
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:2991
boolbvt::bv_utils
bv_utilst bv_utils
Definition: boolbv.h:98
if_exprt::cond
exprt & cond()
Definition: std_expr.h:2981
literalt
Definition: literal.h:26
boolbv.h