cprover
Loading...
Searching...
No Matches
boolbv_case.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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;
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
58
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 {
73
76 }
77
78 what=COMPARE;
79 break;
80
81 default:
83 }
84 }
85
86 return bv;
87}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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
bv_utilst bv_utils
Definition boolbv.h:114
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
virtual std::size_t boolbv_width(const typet &type) const
Definition boolbv.h:99
virtual bvt convert_case(const exprt &expr)
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Base class for all expressions.
Definition expr.h:54
typet & type()
Return the type of the expression.
Definition expr.h:82
operandst & operands()
Definition expr.h:92
const irep_idt & id() const
Definition irep.h:396
void l_set_to_true(literalt a)
Definition prop.h:51
virtual literalt land(literalt a, literalt b)=0
virtual literalt limplies(literalt a, literalt b)=0
virtual bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
Definition prop.cpp:20
virtual literalt lor(literalt a, literalt b)=0
#define forall_operands(it, expr)
Definition expr.h:18
std::vector< literalt > bvt
Definition literal.h:201
literalt const_literal(bool value)
Definition literal.h:188
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:503
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:510
#define PRECONDITION(CONDITION)
Definition invariant.h:463