cprover
boolbv_case.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 <iostream>
12 
14 {
15  const std::vector<exprt> &operands=expr.operands();
16 
17  std::size_t width=boolbv_width(expr.type());
18 
19  if(width==0)
20  return conversion_failed(expr);
21 
22  bvt bv;
23  bv.resize(width);
24 
25  // make it free variables
26  Forall_literals(it, bv)
27  *it=prop.new_variable();
28 
29  if(operands.size()<3)
30  throw "case takes at least three operands";
31 
32  if((operands.size()%2)!=1)
33  throw "number of case operands must be odd";
34 
35  enum { FIRST, COMPARE, VALUE } what=FIRST;
36  bvt compare_bv;
37  literalt previous_compare=const_literal(false);
38  literalt compare_literal=const_literal(false);
39 
40  forall_operands(it, expr)
41  {
42  bvt op=convert_bv(*it);
43 
44  switch(what)
45  {
46  case FIRST:
47  compare_bv.swap(op);
48  what=COMPARE;
49  break;
50 
51  case COMPARE:
52  if(compare_bv.size()!=op.size())
53  {
54  std::cerr << "compare operand: " << compare_bv.size()
55  << "\noperand: " << op.size() << '\n'
56  << it->pretty()
57  << '\n';
58 
59  throw "size of compare operand does not match";
60  }
61 
62  compare_literal=bv_utils.equal(compare_bv, op);
63  compare_literal=prop.land(!previous_compare, compare_literal);
64 
65  previous_compare=prop.lor(previous_compare, compare_literal);
66 
67  what=VALUE;
68  break;
69 
70  case VALUE:
71  if(bv.size()!=op.size())
72  {
73  std::cerr << "result size: " << bv.size()
74  << "\noperand: " << op.size() << '\n'
75  << it->pretty()
76  << '\n';
77 
78  throw "size of value operand does not match";
79  }
80 
81  {
82  literalt value_literal=bv_utils.equal(bv, op);
83 
85  prop.limplies(compare_literal, value_literal));
86  }
87 
88  what=COMPARE;
89  break;
90 
91  default:
92  assert(false);
93  }
94  }
95 
96  return bv;
97 }
virtual bvt convert_case(const exprt &expr)
Definition: boolbv_case.cpp:13
bv_utilst bv_utils
Definition: boolbv.h:93
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Definition: bv_utils.cpp:1089
boolbv_widtht boolbv_width
Definition: boolbv.h:90
virtual literalt lor(literalt a, literalt b)=0
typet & type()
Definition: expr.h:60
#define VALUE
Definition: xml_y.tab.cpp:151
virtual literalt limplies(literalt a, literalt b)=0
void l_set_to_true(literalt a)
Definition: prop.h:47
virtual literalt land(literalt a, literalt b)=0
virtual literalt new_variable()=0
#define Forall_literals(it, bv)
Definition: literal.h:203
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:115
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:108
#define forall_operands(it, expr)
Definition: expr.h:17
literalt const_literal(bool value)
Definition: literal.h:187
Base class for all expressions.
Definition: expr.h:46
operandst & operands()
Definition: expr.h:70
std::vector< literalt > bvt
Definition: literal.h:197