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(
23  (expr.type().id() == ID_verilog_signedbv ||
24  expr.type().id() == ID_verilog_unsignedbv) &&
25  to_bitvector_type(expr.type()).get_width() == 1)
26  {
27  literalt has_x_or_z=bv_utils.verilog_bv_has_x_or_z(op_bv);
28  literalt normal_bits_zero=
30 
31  bvt bv;
32  bv.resize(2);
33 
34  // this returns 'x' for 'z'
35  bv[0]=prop.lselect(has_x_or_z, const_literal(false), normal_bits_zero);
36  bv[1]=has_x_or_z;
37 
38  return bv;
39  }
40  }
41 
42 
43  return conversion_failed(expr);
44 }
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:29
bvt
std::vector< literalt > bvt
Definition: literal.h:201
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
boolbvt::conversion_failed
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:113
const_literal
literalt const_literal(bool value)
Definition: literal.h:188
irept::id
const irep_idt & id() const
Definition: irep.h:418
unary_exprt::op
const exprt & op() const
Definition: std_expr.h:281
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
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1041
boolbvt::bv_utils
bv_utilst bv_utils
Definition: boolbv.h:98
literalt
Definition: literal.h:26
boolbv.h
bv_utilst::verilog_bv_normal_bits
bvt verilog_bv_normal_bits(const bvt &)
Definition: bv_utils.cpp:1359
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:1344
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1089
prop_conv_solvert::prop
propt & prop
Definition: prop_conv_solver.h:131
not_exprt
Boolean negation.
Definition: std_expr.h:2843