cprover
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 
10 #include "boolbv.h"
11 
13 {
14  const bvt &op_bv=convert_bv(expr.op());
15 
16  INVARIANT(
17  !op_bv.empty(),
18  "reduction operand bitvector shall have width at least one");
19 
20  enum { O_OR, O_AND, O_XOR } op;
21 
22  const irep_idt id=expr.id();
23 
24  if(id==ID_reduction_or || id==ID_reduction_nor)
25  op=O_OR;
26  else if(id==ID_reduction_and || id==ID_reduction_nand)
27  op=O_AND;
28  else if(id==ID_reduction_xor || id==ID_reduction_xnor)
29  op=O_XOR;
30  else
32 
33  literalt l=op_bv[0];
34 
35  for(std::size_t i=1; i<op_bv.size(); i++)
36  {
37  switch(op)
38  {
39  case O_OR: l=prop.lor(l, op_bv[i]); break;
40  case O_AND: l=prop.land(l, op_bv[i]); break;
41  case O_XOR: l=prop.lxor(l, op_bv[i]); break;
42  }
43  }
44 
45  if(id==ID_reduction_nor ||
46  id==ID_reduction_nand ||
47  id==ID_reduction_xnor)
48  l=!l;
49 
50  return l;
51 }
52 
54 {
55  const bvt &op_bv=convert_bv(expr.op());
56 
57  INVARIANT(
58  !op_bv.empty(),
59  "reduction operand bitvector shall have width at least one");
60 
61  enum { O_OR, O_AND, O_XOR } op;
62 
63  const irep_idt id=expr.id();
64 
65  if(id==ID_reduction_or || id==ID_reduction_nor)
66  op=O_OR;
67  else if(id==ID_reduction_and || id==ID_reduction_nand)
68  op=O_AND;
69  else if(id==ID_reduction_xor || id==ID_reduction_xnor)
70  op=O_XOR;
71  else
73 
74  const typet &op_type=expr.op().type();
75 
76  if(op_type.id()!=ID_verilog_signedbv ||
77  op_type.id()!=ID_verilog_unsignedbv)
78  {
79  if(
80  (expr.type().id() == ID_verilog_signedbv ||
81  expr.type().id() == ID_verilog_unsignedbv) &&
82  to_bitvector_type(expr.type()).get_width() == 1)
83  {
84  bvt bv;
85  bv.resize(2);
86 
87  literalt l0=op_bv[0], l1=op_bv[1];
88 
89  for(std::size_t i=2; i<op_bv.size(); i+=2)
90  {
91  switch(op)
92  {
93  case O_OR:
94  l0=prop.lor(l0, op_bv[i]); l1=prop.lor(l1, op_bv[i+1]); break;
95  case O_AND:
96  l0=prop.land(l0, op_bv[i]); l1=prop.lor(l1, op_bv[i+1]); break;
97  case O_XOR:
98  l0=prop.lxor(l0, op_bv[i]); l1=prop.lor(l1, op_bv[i+1]); break;
99  }
100  }
101 
102  // Dominating values?
103  if(op==O_OR)
104  l1=prop.lselect(l0, const_literal(false), l1);
105  else if(op==O_AND)
106  l1=prop.lselect(l0, l1, const_literal(false));
107 
108  if(id==ID_reduction_nor ||
109  id==ID_reduction_nand ||
110  id==ID_reduction_xnor)
111  l0=!l0;
112 
113  // we give back 'x', which is 10, if we had seen a 'z'
114  l0=prop.lselect(l1, const_literal(false), l0);
115 
116  bv[0]=l0;
117  bv[1]=l1;
118 
119  return bv;
120  }
121  }
122 
123  return conversion_failed(expr);
124 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
boolbvt::convert_reduction
virtual literalt convert_reduction(const unary_exprt &expr)
Definition: boolbv_reduction.cpp:12
typet
The type of an expression, extends irept.
Definition: type.h:29
bvt
std::vector< literalt > bvt
Definition: literal.h:201
unary_exprt
Generic base class for unary expressions.
Definition: std_expr.h:269
propt::lor
virtual literalt lor(literalt a, literalt b)=0
propt::land
virtual literalt land(literalt a, literalt b)=0
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
propt::lxor
virtual literalt lxor(literalt a, literalt b)=0
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
boolbvt::convert_bv_reduction
virtual bvt convert_bv_reduction(const unary_exprt &expr)
Definition: boolbv_reduction.cpp:53
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
literalt
Definition: literal.h:26
boolbv.h
propt::lselect
virtual literalt lselect(literalt a, literalt b, literalt c)=0
validation_modet::INVARIANT
@ INVARIANT
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