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 <iostream>
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 
54  if(bv.size()!=op.size())
55  {
56  std::cerr << "result size: " << bv.size()
57  << "\noperand: " << op.size() << '\n'
58  << it->pretty()
59  << '\n';
60 
61  throw "size of value operand does not match";
62  }
63 
64  literalt value_literal=bv_utils.equal(bv, op);
65 
66  prop.l_set_to_true(prop.limplies(cond_literal, value_literal));
67  }
68 
69  condition=!condition;
70  }
71  }
72  else
73  {
74  // functional version -- go backwards
75  for(std::size_t i=expr.operands().size(); i!=0; i-=2)
76  {
77  assert(i>=2);
78  const exprt &cond=expr.operands()[i-2];
79  const exprt &value=expr.operands()[i-1];
80 
81  literalt cond_literal=convert(cond);
82 
83  const bvt &op=convert_bv(value);
84 
85  if(bv.size()!=op.size())
86  throw "unexpected operand size in convert_cond";
87 
88  for(std::size_t i=0; i<bv.size(); i++)
89  bv[i]=prop.lselect(cond_literal, op[i], bv[i]);
90  }
91  }
92 
93  return bv;
94 }
bv_utilst bv_utils
Definition: boolbv.h:93
virtual literalt convert(const exprt &expr) override
Definition: prop_conv.cpp:175
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Definition: bv_utils.cpp:1089
boolbv_widtht boolbv_width
Definition: boolbv.h:90
virtual literalt lor(literalt a, literalt b)=0
typet & type()
Definition: expr.h:60
virtual literalt limplies(literalt a, literalt b)=0
void l_set_to_true(literalt a)
Definition: prop.h:47
virtual literalt land(literalt a, literalt b)=0
virtual literalt new_variable()=0
#define Forall_literals(it, bv)
Definition: literal.h:203
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:115
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:49
literalt const_literal(bool value)
Definition: literal.h:187
Base class for all expressions.
Definition: expr.h:46
virtual bool has_set_to() const
Definition: prop.h:76
virtual literalt lselect(literalt a, literalt b, literalt c)=0
operandst & operands()
Definition: expr.h:70
std::vector< literalt > bvt
Definition: literal.h:197