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 <util/invariant.h>
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:
53  compare_bv.size() == op.size(),
54  std::string("size of compare operand does not match:\n") +
55  "compare operand: " + std::to_string(compare_bv.size()) +
56  "\noperand: " + std::to_string(op.size()) + '\n' + it->pretty());
57 
58  compare_literal=bv_utils.equal(compare_bv, op);
59  compare_literal=prop.land(!previous_compare, compare_literal);
60 
61  previous_compare=prop.lor(previous_compare, compare_literal);
62 
63  what=VALUE;
64  break;
65 
66  case VALUE:
68  bv.size() == op.size(),
69  std::string("size of value operand does not match:\n") +
70  "result size: " + std::to_string(bv.size()) +
71  "\noperand: " + std::to_string(op.size()) + '\n' + it->pretty());
72 
73  {
74  literalt value_literal=bv_utils.equal(bv, op);
75 
77  prop.limplies(compare_literal, value_literal));
78  }
79 
80  what=COMPARE;
81  break;
82 
83  default:
84  assert(false);
85  }
86  }
87 
88  return bv;
89 }
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:1108
boolbv_widtht boolbv_width
Definition: boolbv.h:90
virtual literalt lor(literalt a, literalt b)=0
typet & type()
Definition: expr.h:56
#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:49
virtual literalt land(literalt a, literalt b)=0
virtual literalt new_variable()=0
#define Forall_literals(it, bv)
Definition: literal.h:206
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:116
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:42
std::string to_string(const string_constraintt &expr)
Used for debug printing.
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:278
operandst & operands()
Definition: expr.h:66
std::vector< literalt > bvt
Definition: literal.h:200