cprover
Loading...
Searching...
No Matches
boolbv_onehot.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
12
literalt
boolbvt::convert_onehot
(
const
unary_exprt
&expr)
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
}
boolbv.h
boolbvt::convert_onehot
virtual literalt convert_onehot(const unary_exprt &expr)
Definition
boolbv_onehot.cpp:12
boolbvt::convert_bv
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
boolbvt::bv_utils
bv_utilst bv_utils
Definition
boolbv.h:118
irept::id
const irep_idt & id() const
Definition
irep.h:388
literalt
Definition
literal.h:26
prop_conv_solvert::prop
propt & prop
Definition
prop_conv_solver.h:130
unary_exprt
Generic base class for unary expressions.
Definition
std_expr.h:361
unary_exprt::op
const exprt & op() const
Definition
std_expr.h:391
bvt
std::vector< literalt > bvt
Definition
literal.h:201
const_literal
literalt const_literal(bool value)
Definition
literal.h:188
PRECONDITION
#define PRECONDITION(CONDITION)
Definition
invariant.h:463
solvers
flattening
boolbv_onehot.cpp
Generated by
1.13.2