cprover
Loading...
Searching...
No Matches
boolbv_cond.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 const exprt::operandst &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
24 DATA_INVARIANT(operands.size() >= 2, "cond must have at least two operands");
25
27 operands.size() % 2 == 0, "number of cond operands must be even");
28
29 if(prop.has_set_to())
30 {
31 bool condition=true;
32 literalt previous_cond=const_literal(false);
33 literalt cond_literal=const_literal(false);
34
35 // make it free variables
36 bv = prop.new_variables(width);
37
38 forall_operands(it, expr)
39 {
40 if(condition)
41 {
42 cond_literal=convert(*it);
43 cond_literal=prop.land(!previous_cond, cond_literal);
44
45 previous_cond=prop.lor(previous_cond, cond_literal);
46 }
47 else
48 {
49 const bvt &op = convert_bv(*it, bv.size());
50
51 literalt value_literal=bv_utils.equal(bv, op);
52
53 prop.l_set_to_true(prop.limplies(cond_literal, value_literal));
54 }
55
56 condition=!condition;
57 }
58 }
59 else
60 {
61 bv.resize(width);
62
63 // functional version -- go backwards
64 for(std::size_t i=expr.operands().size(); i!=0; i-=2)
65 {
67 i >= 2,
68 "since the number of operands is even if i is nonzero it must be "
69 "greater than two");
70 const exprt &cond=expr.operands()[i-2];
71 const exprt &value=expr.operands()[i-1];
72
73 literalt cond_literal=convert(cond);
74
75 const bvt &op = convert_bv(value, bv.size());
76
77 for(std::size_t j = 0; j < bv.size(); j++)
78 bv[j] = prop.lselect(cond_literal, op[j], bv[j]);
79 }
80 }
81
82 return bv;
83}
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
virtual bvt convert_cond(const cond_exprt &)
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
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
this is a parametric version of an if-expression: it returns the value of the first case (using the o...
Definition std_expr.h:3119
Base class for all expressions.
Definition expr.h:54
std::vector< exprt > operandst
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:82
operandst & operands()
Definition expr.h:92
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
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 literalt lselect(literalt a, literalt b, literalt c)=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
virtual bool has_set_to() const
Definition prop.h:80
#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 DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:510
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423