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 &op1_bv=convert_bv(expr.true_case());
22  const bvt &op2_bv=convert_bv(expr.false_case());
23 
24  if(op1_bv.size()!=width || op2_bv.size()!=width)
25  throw "operand size mismatch for if "+expr.pretty();
26 
27  return bv_utils.select(cond, op1_bv, op2_bv);
28 }
exprt & true_case()
Definition: std_expr.h:3395
bv_utilst bv_utils
Definition: boolbv.h:93
literalt convert(const exprt &expr) override
Definition: prop_conv.cpp:162
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
Definition: irep.cpp:641
boolbv_widtht boolbv_width
Definition: boolbv.h:90
The trinary if-then-else operator.
Definition: std_expr.h:3361
exprt & cond()
Definition: std_expr.h:3385
typet & type()
Definition: expr.h:56
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:116
bvt select(literalt s, const bvt &a, const bvt &b)
If s is true, selects a otherwise selects b.
Definition: bv_utils.cpp:96
exprt & false_case()
Definition: std_expr.h:3405
virtual bvt convert_if(const if_exprt &expr)
Definition: boolbv_if.cpp:12
std::vector< literalt > bvt
Definition: literal.h:200