19 for(bvt::const_iterator it=op.begin(); it!=op.end(); it++)
23 one_seen=
prop.
lor(*it, one_seen);
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;
31 throw "unexpected onehot expression";
virtual literalt convert_onehot(const unary_exprt &expr)
virtual literalt lor(literalt a, literalt b)=0
virtual literalt land(literalt a, literalt b)=0
const irep_idt & id() const
virtual const bvt & convert_bv(const exprt &expr)
Generic base class for unary expressions.
literalt const_literal(bool value)
std::vector< literalt > bvt