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((expr.type().id()==ID_verilog_signedbv ||
80  expr.type().id()==ID_verilog_unsignedbv) &&
81  expr.type().get_size_t(ID_width) == 1)
82  {
83  bvt bv;
84  bv.resize(2);
85 
86  literalt l0=op_bv[0], l1=op_bv[1];
87 
88  for(std::size_t i=2; i<op_bv.size(); i+=2)
89  {
90  switch(op)
91  {
92  case O_OR:
93  l0=prop.lor(l0, op_bv[i]); l1=prop.lor(l1, op_bv[i+1]); break;
94  case O_AND:
95  l0=prop.land(l0, op_bv[i]); l1=prop.lor(l1, op_bv[i+1]); break;
96  case O_XOR:
97  l0=prop.lxor(l0, op_bv[i]); l1=prop.lor(l1, op_bv[i+1]); break;
98  }
99  }
100 
101  // Dominating values?
102  if(op==O_OR)
103  l1=prop.lselect(l0, const_literal(false), l1);
104  else if(op==O_AND)
105  l1=prop.lselect(l0, l1, const_literal(false));
106 
107  if(id==ID_reduction_nor ||
108  id==ID_reduction_nand ||
109  id==ID_reduction_xnor)
110  l0=!l0;
111 
112  // we give back 'x', which is 10, if we had seen a 'z'
113  l0=prop.lselect(l1, const_literal(false), l0);
114 
115  bv[0]=l0;
116  bv[1]=l1;
117 
118  return bv;
119  }
120  }
121 
122  return conversion_failed(expr);
123 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
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:27
bvt
std::vector< literalt > bvt
Definition: literal.h:200
unary_exprt
Generic base class for unary expressions.
Definition: std_expr.h:331
propt::lor
virtual literalt lor(literalt a, literalt b)=0
propt::land
virtual literalt land(literalt a, literalt b)=0
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
propt::lxor
virtual literalt lxor(literalt a, literalt b)=0
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
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: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
literalt
Definition: literal.h:24
boolbv.h
propt::lselect
virtual literalt lselect(literalt a, literalt b, literalt c)=0
validation_modet::INVARIANT
@ INVARIANT
prop_conv_solvert::prop
propt & prop
Definition: prop_conv.h:152