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  PRECONDITION(expr.id() == ID_case);
16 
17  const std::vector<exprt> &operands=expr.operands();
18 
19  std::size_t width=boolbv_width(expr.type());
20 
21  if(width==0)
22  return conversion_failed(expr);
23 
24  bvt bv;
25  bv.resize(width);
26 
27  // make it free variables
28  Forall_literals(it, bv)
29  *it=prop.new_variable();
30 
32  operands.size() >= 3, "case should have at least three operands");
33 
35  operands.size() % 2 == 1, "number of case operands should be odd");
36 
37  enum { FIRST, COMPARE, VALUE } what=FIRST;
38  bvt compare_bv;
39  literalt previous_compare=const_literal(false);
40  literalt compare_literal=const_literal(false);
41 
42  forall_operands(it, expr)
43  {
44  bvt op=convert_bv(*it);
45 
46  switch(what)
47  {
48  case FIRST:
49  compare_bv.swap(op);
50  what=COMPARE;
51  break;
52 
53  case COMPARE:
55  compare_bv.size() == op.size(),
56  std::string("size of compare operand does not match:\n") +
57  "compare operand: " + std::to_string(compare_bv.size()) +
58  "\noperand: " + std::to_string(op.size()) + '\n' + it->pretty());
59 
60  compare_literal=bv_utils.equal(compare_bv, op);
61  compare_literal=prop.land(!previous_compare, compare_literal);
62 
63  previous_compare=prop.lor(previous_compare, compare_literal);
64 
65  what=VALUE;
66  break;
67 
68  case VALUE:
70  bv.size() == op.size(),
71  std::string("size of value operand does not match:\n") +
72  "result size: " + std::to_string(bv.size()) +
73  "\noperand: " + std::to_string(op.size()) + '\n' + it->pretty());
74 
75  {
76  literalt value_literal=bv_utils.equal(bv, op);
77 
79  prop.limplies(compare_literal, value_literal));
80  }
81 
82  what=COMPARE;
83  break;
84 
85  default:
87  }
88  }
89 
90  return bv;
91 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
bvt
std::vector< literalt > bvt
Definition: literal.h:201
invariant.h
propt::new_variable
virtual literalt new_variable()=0
exprt
Base class for all expressions.
Definition: expr.h:53
propt::lor
virtual literalt lor(literalt a, literalt b)=0
propt::l_set_to_true
void l_set_to_true(literalt a)
Definition: prop.h:52
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
boolbvt::convert_case
virtual bvt convert_case(const exprt &expr)
Definition: boolbv_case.cpp:13
propt::land
virtual literalt land(literalt a, literalt b)=0
Forall_literals
#define Forall_literals(it, bv)
Definition: literal.h:207
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
boolbvt::boolbv_width
boolbv_widtht boolbv_width
Definition: boolbv.h:95
boolbvt::conversion_failed
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:113
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
propt::limplies
virtual literalt limplies(literalt a, literalt b)=0
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
const_literal
literalt const_literal(bool value)
Definition: literal.h:188
irept::id
const irep_idt & id() const
Definition: irep.h:418
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
boolbvt::bv_utils
bv_utilst bv_utils
Definition: boolbv.h:98
literalt
Definition: literal.h:26
boolbv.h
exprt::operands
operandst & operands()
Definition: expr.h:95
bv_utilst::equal
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Definition: bv_utils.cpp:1113
prop_conv_solvert::prop
propt & prop
Definition: prop_conv_solver.h:131