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  // make it free variables
25  bvt bv = prop.new_variables(width);
26 
28  operands.size() >= 3, "case should have at least three operands");
29 
31  operands.size() % 2 == 1, "number of case operands should be odd");
32 
33  enum { FIRST, COMPARE, VALUE } what=FIRST;
34  bvt compare_bv;
35  literalt previous_compare=const_literal(false);
36  literalt compare_literal=const_literal(false);
37 
38  forall_operands(it, expr)
39  {
40  bvt op=convert_bv(*it);
41 
42  switch(what)
43  {
44  case FIRST:
45  compare_bv.swap(op);
46  what=COMPARE;
47  break;
48 
49  case COMPARE:
51  compare_bv.size() == op.size(),
52  std::string("size of compare operand does not match:\n") +
53  "compare operand: " + std::to_string(compare_bv.size()) +
54  "\noperand: " + std::to_string(op.size()) + '\n' + it->pretty());
55 
56  compare_literal=bv_utils.equal(compare_bv, op);
57  compare_literal=prop.land(!previous_compare, compare_literal);
58 
59  previous_compare=prop.lor(previous_compare, compare_literal);
60 
61  what=VALUE;
62  break;
63 
64  case VALUE:
66  bv.size() == op.size(),
67  std::string("size of value operand does not match:\n") +
68  "result size: " + std::to_string(bv.size()) +
69  "\noperand: " + std::to_string(op.size()) + '\n' + it->pretty());
70 
71  {
72  literalt value_literal=bv_utils.equal(bv, op);
73 
75  prop.limplies(compare_literal, value_literal));
76  }
77 
78  what=COMPARE;
79  break;
80 
81  default:
83  }
84  }
85 
86  return bv;
87 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
propt::new_variables
virtual bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
Definition: prop.cpp:20
bvt
std::vector< literalt > bvt
Definition: literal.h:201
invariant.h
exprt
Base class for all expressions.
Definition: expr.h:54
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:50
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:57
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
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
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:510
propt::limplies
virtual literalt limplies(literalt a, literalt b)=0
boolbvt::boolbv_width
virtual std::size_t boolbv_width(const typet &type) const
Definition: boolbv.h:97
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
const_literal
literalt const_literal(bool value)
Definition: literal.h:188
irept::id
const irep_idt & id() const
Definition: irep.h:407
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:40
boolbvt::bv_utils
bv_utilst bv_utils
Definition: boolbv.h:112
literalt
Definition: literal.h:26
boolbvt::conversion_failed
bvt conversion_failed(const exprt &expr)
Print that the expression of x has failed conversion, then return a vector of x's width.
Definition: boolbv.cpp:84
boolbv.h
exprt::operands
operandst & operands()
Definition: expr.h:92
bv_utilst::equal
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Definition: bv_utils.cpp:1103
prop_conv_solvert::prop
propt & prop
Definition: prop_conv_solver.h:126