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 literalt one_seen=const_literal(false);
19 literalt more_than_one_seen=const_literal(false);
20
21 for(bvt::const_iterator it=op.begin(); it!=op.end(); it++)
22 {
23 more_than_one_seen=
24 prop.lor(more_than_one_seen, prop.land(*it, one_seen));
25 one_seen=prop.lor(*it, one_seen);
26 }
27
28 if(expr.id()==ID_onehot)
29 return prop.land(one_seen, !more_than_one_seen);
30 else
31 {
33 expr.id() == ID_onehot0,
34 "should be a onehot0 expression as other onehot expression kind has been "
35 "handled in other branch");
36 return !more_than_one_seen;
37 }
38}
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
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
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423