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 
16  if(op_bv.empty())
17  throw "not operator takes one non-empty operand";
18 
19  const typet &op_type=expr.op().type();
20 
21  if(op_type.id()!=ID_verilog_signedbv ||
22  op_type.id()!=ID_verilog_unsignedbv)
23  {
24  if((expr.type().id()==ID_verilog_signedbv ||
25  expr.type().id()==ID_verilog_unsignedbv) &&
26  expr.type().get_size_t(ID_width) == 1)
27  {
28  literalt has_x_or_z=bv_utils.verilog_bv_has_x_or_z(op_bv);
29  literalt normal_bits_zero=
31 
32  bvt bv;
33  bv.resize(2);
34 
35  // this returns 'x' for 'z'
36  bv[0]=prop.lselect(has_x_or_z, const_literal(false), normal_bits_zero);
37  bv[1]=has_x_or_z;
38 
39  return bv;
40  }
41  }
42 
43 
44  return conversion_failed(expr);
45 }
The type of an expression.
Definition: type.h:22
Boolean negation.
Definition: std_expr.h:3228
bv_utilst bv_utils
Definition: boolbv.h:93
const exprt & op() const
Definition: std_expr.h:340
typet & type()
Definition: expr.h:56
literalt is_zero(const bvt &op)
Definition: bv_utils.h:141
const irep_idt & id() const
Definition: irep.h:259
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:116
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:108
literalt verilog_bv_has_x_or_z(const bvt &)
Definition: bv_utils.cpp:1335
bvt verilog_bv_normal_bits(const bvt &)
Definition: bv_utils.cpp:1350
virtual bvt convert_not(const not_exprt &expr)
Definition: boolbv_not.cpp:12
literalt const_literal(bool value)
Definition: literal.h:187
virtual literalt lselect(literalt a, literalt b, literalt c)=0
std::size_t get_size_t(const irep_namet &name) const
Definition: irep.cpp:255
std::vector< literalt > bvt
Definition: literal.h:200