cprover
boolbv_cond.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 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  bv.resize(width);
24 
25  if(operands.size()<2)
26  throw "cond takes at least two operands";
27 
28  if((operands.size()%2)!=0)
29  throw "number of cond operands must be even";
30 
31  if(prop.has_set_to())
32  {
33  bool condition=true;
34  literalt previous_cond=const_literal(false);
35  literalt cond_literal=const_literal(false);
36 
37  // make it free variables
38  Forall_literals(it, bv)
39  *it=prop.new_variable();
40 
41  forall_operands(it, expr)
42  {
43  if(condition)
44  {
45  cond_literal=convert(*it);
46  cond_literal=prop.land(!previous_cond, cond_literal);
47 
48  previous_cond=prop.lor(previous_cond, cond_literal);
49  }
50  else
51  {
52  const bvt &op=convert_bv(*it);
53 
55  bv.size() == op.size(),
56  std::string("size of value operand does not match:\n") +
57  "result size: " + std::to_string(bv.size()) +
58  "\noperand: " + std::to_string(op.size()) + '\n' + it->pretty());
59 
60  literalt value_literal=bv_utils.equal(bv, op);
61 
62  prop.l_set_to_true(prop.limplies(cond_literal, value_literal));
63  }
64 
65  condition=!condition;
66  }
67  }
68  else
69  {
70  // functional version -- go backwards
71  for(std::size_t i=expr.operands().size(); i!=0; i-=2)
72  {
73  assert(i>=2);
74  const exprt &cond=expr.operands()[i-2];
75  const exprt &value=expr.operands()[i-1];
76 
77  literalt cond_literal=convert(cond);
78 
79  const bvt &op=convert_bv(value);
80 
81  if(bv.size()!=op.size())
82  throw "unexpected operand size in convert_cond";
83 
84  for(std::size_t i=0; i<bv.size(); i++)
85  bv[i]=prop.lselect(cond_literal, op[i], bv[i]);
86  }
87  }
88 
89  return bv;
90 }
bv_utilst bv_utils
Definition: boolbv.h:93
literalt convert(const exprt &expr) override
Definition: prop_conv.cpp:162
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
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
virtual bvt convert_cond(const exprt &expr)
Definition: boolbv_cond.cpp:13
std::vector< exprt > operandst
Definition: expr.h:45
literalt const_literal(bool value)
Definition: literal.h:187
Base class for all expressions.
Definition: expr.h:42
virtual bool has_set_to() const
Definition: prop.h:78
std::string to_string(const string_constraintt &expr)
Used for debug printing.
virtual literalt lselect(literalt a, literalt b, literalt c)=0
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:257
operandst & operands()
Definition: expr.h:66
std::vector< literalt > bvt
Definition: literal.h:200