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  DATA_INVARIANT(operands.size() >= 2, "cond must have at least two operands");
26 
28  operands.size() % 2 == 0, "number of cond operands must be even");
29 
30  if(prop.has_set_to())
31  {
32  bool condition=true;
33  literalt previous_cond=const_literal(false);
34  literalt cond_literal=const_literal(false);
35 
36  // make it free variables
37  Forall_literals(it, bv)
38  *it=prop.new_variable();
39 
40  forall_operands(it, expr)
41  {
42  if(condition)
43  {
44  cond_literal=convert(*it);
45  cond_literal=prop.land(!previous_cond, cond_literal);
46 
47  previous_cond=prop.lor(previous_cond, cond_literal);
48  }
49  else
50  {
51  const bvt &op = convert_bv(*it, bv.size());
52 
53  literalt value_literal=bv_utils.equal(bv, op);
54 
55  prop.l_set_to_true(prop.limplies(cond_literal, value_literal));
56  }
57 
58  condition=!condition;
59  }
60  }
61  else
62  {
63  // functional version -- go backwards
64  for(std::size_t i=expr.operands().size(); i!=0; i-=2)
65  {
66  INVARIANT(
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 }
boolbvt::convert_cond
virtual bvt convert_cond(const cond_exprt &)
Definition: boolbv_cond.cpp:13
exprt::size
std::size_t size() const
Amount of nodes this expression tree contains.
Definition: expr.cpp:26
bvt
std::vector< literalt > bvt
Definition: literal.h:201
invariant.h
propt::new_variable
virtual literalt new_variable()=0
exprt
Base class for all expressions.
Definition: expr.h:53
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:52
propt::land
virtual literalt land(literalt a, literalt b)=0
Forall_literals
#define Forall_literals(it, bv)
Definition: literal.h:207
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
boolbvt::boolbv_width
boolbv_widtht boolbv_width
Definition: boolbv.h:95
boolbvt::conversion_failed
void conversion_failed(const exprt &expr, bvt &bv)
Definition: boolbv.h:113
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:511
propt::limplies
virtual literalt limplies(literalt a, literalt b)=0
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
const_literal
literalt const_literal(bool value)
Definition: literal.h:188
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
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:119
prop_conv_solvert::convert
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
Definition: prop_conv_solver.cpp:168
cond_exprt
this is a parametric version of an if-expression: it returns the value of the first case (using the o...
Definition: std_expr.h:4359
boolbvt::bv_utils
bv_utilst bv_utils
Definition: boolbv.h:98
literalt
Definition: literal.h:26
propt::has_set_to
virtual bool has_set_to() const
Definition: prop.h:81
boolbv.h
exprt::operands
operandst & operands()
Definition: expr.h:95
bv_utilst::equal
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Definition: bv_utils.cpp:1113
propt::lselect
virtual literalt lselect(literalt a, literalt b, literalt c)=0
validation_modet::INVARIANT
@ INVARIANT
prop_conv_solvert::prop
propt & prop
Definition: prop_conv_solver.h:131