CBMC
boolbv_constraint_select_one.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 
10 #include "boolbv.h"
11 
13 {
14  const exprt::operandst &operands=expr.operands();
15 
16  if(expr.id()!=ID_constraint_select_one)
17  throw "expected constraint_select_one expression";
18 
19  if(operands.empty())
20  throw "constraint_select_one takes at least one operand";
21 
22  if(expr.type() != to_multi_ary_expr(expr).op0().type())
23  throw "constraint_select_one expects matching types";
24 
25  bvt bv;
26 
27  if(prop.has_set_to())
28  {
29  std::size_t width=boolbv_width(expr.type());
30  bv=prop.new_variables(width);
31 
32  bvt b;
33  b.reserve(expr.operands().size());
34 
35  // add constraints
36  for(const auto &op : expr.operands())
37  {
38  bvt it_bv = convert_bv(op);
39 
40  if(it_bv.size()!=bv.size())
41  throw "constraint_select_one expects matching width";
42 
43  b.push_back(bv_utils.equal(bv, it_bv));
44  }
45 
46  prop.lcnf(b);
47  }
48  else
49  {
50  std::size_t op_nr=0;
51  for(const auto &op : expr.operands())
52  {
53  const bvt &op_bv = convert_bv(op);
54 
55  if(op_nr==0)
56  bv=op_bv;
57  else
58  {
59  if(op_bv.size()!=bv.size())
60  return conversion_failed(expr);
61 
62  for(std::size_t i=0; i<op_bv.size(); i++)
63  bv[i]=prop.lselect(prop.new_variable(), bv[i], op_bv[i]);
64  }
65 
66  op_nr++;
67  }
68  }
69 
70  return bv;
71 }
virtual const bvt & convert_bv(const exprt &expr, const std::optional< std::size_t > expected_width={})
Convert expression to vector of literalts, using an internal cache to speed up conversion if availabl...
Definition: boolbv.cpp:37
virtual bvt convert_constraint_select_one(const exprt &expr)
bv_utilst bv_utils
Definition: boolbv.h:116
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:83
virtual std::size_t boolbv_width(const typet &type) const
Definition: boolbv.h:101
literalt equal(const bvt &op0, const bvt &op1)
Bit-blasting ID_equal and use in other encodings.
Definition: bv_utils.cpp:1364
Base class for all expressions.
Definition: expr.h:56
std::vector< exprt > operandst
Definition: expr.h:58
typet & type()
Return the type of the expression.
Definition: expr.h:84
operandst & operands()
Definition: expr.h:94
const irep_idt & id() const
Definition: irep.h:384
virtual literalt lselect(literalt a, literalt b, literalt c)=0
void lcnf(literalt l0, literalt l1)
Definition: prop.h:58
virtual bvt new_variables(std::size_t width)
generates a bitvector of given width with new variables
Definition: prop.cpp:30
virtual literalt new_variable()=0
virtual bool has_set_to() const
Definition: prop.h:81
std::vector< literalt > bvt
Definition: literal.h:201
const multi_ary_exprt & to_multi_ary_expr(const exprt &expr)
Cast an exprt to a multi_ary_exprt.
Definition: std_expr.h:987