cprover
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 
13 {
14  bvt op=convert_bv(expr.op());
15 
16  literalt one_seen=const_literal(false);
17  literalt more_than_one_seen=const_literal(false);
18 
19  for(bvt::const_iterator it=op.begin(); it!=op.end(); it++)
20  {
21  more_than_one_seen=
22  prop.lor(more_than_one_seen, prop.land(*it, one_seen));
23  one_seen=prop.lor(*it, one_seen);
24  }
25 
26  if(expr.id()==ID_onehot)
27  return prop.land(one_seen, !more_than_one_seen);
28  else if(expr.id()==ID_onehot0)
29  return !more_than_one_seen;
30  else
31  throw "unexpected onehot expression";
32 }
virtual literalt convert_onehot(const unary_exprt &expr)
const exprt & op() const
Definition: std_expr.h:340
virtual literalt lor(literalt a, literalt b)=0
virtual literalt land(literalt a, literalt b)=0
const irep_idt & id() const
Definition: irep.h:259
virtual const bvt & convert_bv(const exprt &expr)
Definition: boolbv.cpp:116
Generic base class for unary expressions.
Definition: std_expr.h:303
literalt const_literal(bool value)
Definition: literal.h:187
std::vector< literalt > bvt
Definition: literal.h:200