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  if(op_bv.empty())
17  throw "reduction operators take one non-empty operand";
18 
19  enum { O_OR, O_AND, O_XOR } op;
20 
21  const irep_idt id=expr.id();
22 
23  if(id==ID_reduction_or || id==ID_reduction_nor)
24  op=O_OR;
25  else if(id==ID_reduction_and || id==ID_reduction_nand)
26  op=O_AND;
27  else if(id==ID_reduction_xor || id==ID_reduction_xnor)
28  op=O_XOR;
29  else
30  throw "unexpected reduction operator";
31 
32  literalt l=op_bv[0];
33 
34  for(std::size_t i=1; i<op_bv.size(); i++)
35  {
36  switch(op)
37  {
38  case O_OR: l=prop.lor(l, op_bv[i]); break;
39  case O_AND: l=prop.land(l, op_bv[i]); break;
40  case O_XOR: l=prop.lxor(l, op_bv[i]); break;
41  }
42  }
43 
44  if(id==ID_reduction_nor ||
45  id==ID_reduction_nand ||
46  id==ID_reduction_xnor)
47  l=!l;
48 
49  return l;
50 }
51 
53 {
54  const bvt &op_bv=convert_bv(expr.op());
55 
56  if(op_bv.empty())
57  throw "reduction operators take one non-empty operand";
58 
59  enum { O_OR, O_AND, O_XOR } op;
60 
61  const irep_idt id=expr.id();
62 
63  if(id==ID_reduction_or || id==ID_reduction_nor)
64  op=O_OR;
65  else if(id==ID_reduction_and || id==ID_reduction_nand)
66  op=O_AND;
67  else if(id==ID_reduction_xor || id==ID_reduction_xnor)
68  op=O_XOR;
69  else
70  throw "unexpected reduction operator";
71 
72  const typet &op_type=expr.op().type();
73 
74  if(op_type.id()!=ID_verilog_signedbv ||
75  op_type.id()!=ID_verilog_unsignedbv)
76  {
77  if((expr.type().id()==ID_verilog_signedbv ||
78  expr.type().id()==ID_verilog_unsignedbv) &&
79  expr.type().get_int(ID_width)==1)
80  {
81  bvt bv;
82  bv.resize(2);
83 
84  literalt l0=op_bv[0], l1=op_bv[1];
85 
86  for(std::size_t i=2; i<op_bv.size(); i+=2)
87  {
88  switch(op)
89  {
90  case O_OR:
91  l0=prop.lor(l0, op_bv[i]); l1=prop.lor(l1, op_bv[i+1]); break;
92  case O_AND:
93  l0=prop.land(l0, op_bv[i]); l1=prop.lor(l1, op_bv[i+1]); break;
94  case O_XOR:
95  l0=prop.lxor(l0, op_bv[i]); l1=prop.lor(l1, op_bv[i+1]); break;
96  }
97  }
98 
99  // Dominating values?
100  if(op==O_OR)
101  l1=prop.lselect(l0, const_literal(false), l1);
102  else if(op==O_AND)
103  l1=prop.lselect(l0, l1, const_literal(false));
104 
105  if(id==ID_reduction_nor ||
106  id==ID_reduction_nand ||
107  id==ID_reduction_xnor)
108  l0=!l0;
109 
110  // we give back 'x', which is 10, if we had seen a 'z'
111  l0=prop.lselect(l1, const_literal(false), l0);
112 
113  bv[0]=l0;
114  bv[1]=l1;
115 
116  return bv;
117  }
118  }
119 
120  return conversion_failed(expr);
121 }
The type of an expression.
Definition: type.h:22
virtual bvt convert_bv_reduction(const unary_exprt &expr)
const exprt & op() const
Definition: std_expr.h:340
signed int get_int(const irep_namet &name) const
Definition: irep.cpp:245
virtual literalt lor(literalt a, literalt b)=0
typet & type()
Definition: expr.h:56
virtual literalt land(literalt a, literalt b)=0
const irep_idt & id() const
Definition: irep.h:189
virtual literalt convert_reduction(const unary_exprt &expr)
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:116
virtual literalt lxor(literalt a, literalt b)=0
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:108
Generic base class for unary expressions.
Definition: std_expr.h:303
literalt const_literal(bool value)
Definition: literal.h:187
virtual literalt lselect(literalt a, literalt b, literalt c)=0
std::vector< literalt > bvt
Definition: literal.h:200