CBMC
boolbv_reduction.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #include "boolbv.h"
10 
11 #include <util/bitvector_types.h>
12 
14 {
15  const bvt &op_bv=convert_bv(expr.op());
16 
17  INVARIANT(
18  !op_bv.empty(),
19  "reduction operand bitvector shall have width at least one");
20 
21  enum { O_OR, O_AND, O_XOR } op;
22 
23  const irep_idt id=expr.id();
24 
25  if(id==ID_reduction_or || id==ID_reduction_nor)
26  op=O_OR;
27  else if(id==ID_reduction_and || id==ID_reduction_nand)
28  op=O_AND;
29  else if(id==ID_reduction_xor || id==ID_reduction_xnor)
30  op=O_XOR;
31  else
33 
34  literalt l=op_bv[0];
35 
36  for(std::size_t i=1; i<op_bv.size(); i++)
37  {
38  switch(op)
39  {
40  case O_OR: l=prop.lor(l, op_bv[i]); break;
41  case O_AND: l=prop.land(l, op_bv[i]); break;
42  case O_XOR: l=prop.lxor(l, op_bv[i]); break;
43  }
44  }
45 
46  if(id==ID_reduction_nor ||
47  id==ID_reduction_nand ||
48  id==ID_reduction_xnor)
49  l=!l;
50 
51  return l;
52 }
53 
55 {
56  const bvt &op_bv=convert_bv(expr.op());
57 
58  INVARIANT(
59  !op_bv.empty(),
60  "reduction operand bitvector shall have width at least one");
61 
62  enum { O_OR, O_AND, O_XOR } op;
63 
64  const irep_idt id=expr.id();
65 
66  if(id==ID_reduction_or || id==ID_reduction_nor)
67  op=O_OR;
68  else if(id==ID_reduction_and || id==ID_reduction_nand)
69  op=O_AND;
70  else if(id==ID_reduction_xor || id==ID_reduction_xnor)
71  op=O_XOR;
72  else
74 
75  const typet &op_type=expr.op().type();
76 
77  if(op_type.id()!=ID_verilog_signedbv ||
78  op_type.id()!=ID_verilog_unsignedbv)
79  {
80  if(
81  (expr.type().id() == ID_verilog_signedbv ||
82  expr.type().id() == ID_verilog_unsignedbv) &&
83  to_bitvector_type(expr.type()).get_width() == 1)
84  {
85  bvt bv;
86  bv.resize(2);
87 
88  literalt l0=op_bv[0], l1=op_bv[1];
89 
90  for(std::size_t i=2; i<op_bv.size(); i+=2)
91  {
92  switch(op)
93  {
94  case O_OR:
95  l0=prop.lor(l0, op_bv[i]); l1=prop.lor(l1, op_bv[i+1]); break;
96  case O_AND:
97  l0=prop.land(l0, op_bv[i]); l1=prop.lor(l1, op_bv[i+1]); break;
98  case O_XOR:
99  l0=prop.lxor(l0, op_bv[i]); l1=prop.lor(l1, op_bv[i+1]); break;
100  }
101  }
102 
103  // Dominating values?
104  if(op==O_OR)
105  l1=prop.lselect(l0, const_literal(false), l1);
106  else if(op==O_AND)
107  l1=prop.lselect(l0, l1, const_literal(false));
108 
109  if(id==ID_reduction_nor ||
110  id==ID_reduction_nand ||
111  id==ID_reduction_xnor)
112  l0=!l0;
113 
114  // we give back 'x', which is 10, if we had seen a 'z'
115  l0=prop.lselect(l1, const_literal(false), l0);
116 
117  bv[0]=l0;
118  bv[1]=l1;
119 
120  return bv;
121  }
122  }
123 
124  return conversion_failed(expr);
125 }
Pre-defined bitvector types.
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
std::size_t get_width() const
Definition: std_types.h:920
virtual const bvt & convert_bv(const exprt &expr, const std::optional< std::size_t > expected_width={})
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition: boolbv.cpp:37
virtual literalt convert_reduction(const unary_exprt &expr)
virtual bvt convert_bv_reduction(const unary_exprt &expr)
bvt conversion_failed(const exprt &expr)
Print that the expression of x has failed conversion, then return a vector of x's width.
Definition: boolbv.cpp:83
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
typet & type()
Return the type of the expression.
Definition: expr.h:84
const irep_idt & id() const
Definition: irep.h:384
virtual literalt land(literalt a, literalt b)=0
virtual literalt lselect(literalt a, literalt b, literalt c)=0
virtual literalt lxor(literalt a, literalt b)=0
virtual literalt lor(literalt a, literalt b)=0
The type of an expression, extends irept.
Definition: type.h:29
Generic base class for unary expressions.
Definition: std_expr.h:361
const exprt & op() const
Definition: std_expr.h:391
std::vector< literalt > bvt
Definition: literal.h:201
literalt const_literal(bool value)
Definition: literal.h:188
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:525