cprover
boolbv_not.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  const bvt &op_bv=convert_bv(expr.op());
15  CHECK_RETURN(!op_bv.empty());
16 
17  const typet &op_type=expr.op().type();
18 
19  if(op_type.id()!=ID_verilog_signedbv ||
20  op_type.id()!=ID_verilog_unsignedbv)
21  {
22  if((expr.type().id()==ID_verilog_signedbv ||
23  expr.type().id()==ID_verilog_unsignedbv) &&
24  expr.type().get_size_t(ID_width) == 1)
25  {
26  literalt has_x_or_z=bv_utils.verilog_bv_has_x_or_z(op_bv);
27  literalt normal_bits_zero=
29 
30  bvt bv;
31  bv.resize(2);
32 
33  // this returns 'x' for 'z'
34  bv[0]=prop.lselect(has_x_or_z, const_literal(false), normal_bits_zero);
35  bv[1]=has_x_or_z;
36 
37  return bv;
38  }
39  }
40 
41 
42  return conversion_failed(expr);
43 }
typet
The type of an expression, extends irept.
Definition: type.h:27
bvt
std::vector< literalt > bvt
Definition: literal.h:200
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
boolbvt::conversion_failed
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:110
const_literal
literalt const_literal(bool value)
Definition: literal.h:187
irept::id
const irep_idt & id() const
Definition: irep.h:259
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:371
boolbvt::convert_bv
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
Definition: boolbv.cpp:112
irept::get_size_t
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:254
boolbvt::bv_utils
bv_utilst bv_utils
Definition: boolbv.h:95
literalt
Definition: literal.h:24
boolbv.h
bv_utilst::verilog_bv_normal_bits
bvt verilog_bv_normal_bits(const bvt &)
Definition: bv_utils.cpp:1362
boolbvt::convert_not
virtual bvt convert_not(const not_exprt &expr)
Definition: boolbv_not.cpp:12
bv_utilst::is_zero
literalt is_zero(const bvt &op)
Definition: bv_utils.h:141
propt::lselect
virtual literalt lselect(literalt a, literalt b, literalt c)=0
bv_utilst::verilog_bv_has_x_or_z
literalt verilog_bv_has_x_or_z(const bvt &)
Definition: bv_utils.cpp:1347
prop_conv_solvert::prop
propt & prop
Definition: prop_conv.h:152
not_exprt
Boolean negation.
Definition: std_expr.h:3308
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470