cprover
Loading...
Searching...
No Matches
boolbv_onehot.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9
10#include "boolbv.h"
11
13{
14 PRECONDITION(expr.id() == ID_onehot || expr.id() == ID_onehot0);
15
16 bvt op=convert_bv(expr.op());
17
18 // onehot0 is the same as onehot with the input bits flipped
19 if(expr.id() == ID_onehot0)
20 op = bv_utils.inverted(op);
21
22 literalt one_seen=const_literal(false);
23 literalt more_than_one_seen=const_literal(false);
24
25 for(bvt::const_iterator it=op.begin(); it!=op.end(); it++)
26 {
27 more_than_one_seen=
28 prop.lor(more_than_one_seen, prop.land(*it, one_seen));
29 one_seen=prop.lor(*it, one_seen);
30 }
31
32 return prop.land(one_seen, !more_than_one_seen);
33}
virtual literalt convert_onehot(const unary_exprt &expr)
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:39
bv_utilst bv_utils
Definition boolbv.h:118
const irep_idt & id() const
Definition irep.h:388
Generic base class for unary expressions.
Definition std_expr.h:361
const exprt & op() const
Definition std_expr.h:391
std::vector< literalt > bvt
Definition literal.h:201
literalt const_literal(bool value)
Definition literal.h:188
#define PRECONDITION(CONDITION)
Definition invariant.h:463