22 if(operands.size()==2)
33 if(bv0.size()==bv1.size() && !bv0.empty() &&
51 else if((op0.
type().
id()==ID_range &&
93 bvt extract0, extract1;
95 extract0.resize(bv0.size()/2);
96 extract1.resize(bv1.size()/2);
98 for(std::size_t i=0; i<extract0.size(); i++)
101 for(std::size_t i=0; i<extract1.size(); i++)
102 extract1[i]=bv1[i*2];
virtual literalt limplies(literalt a, literalt b)=0
void l_set_to_true(literalt a)
const irep_idt & id() const
virtual literalt convert_bv_rel(const exprt &expr)
virtual const bvt & convert_bv(const exprt &expr)
literalt rel(const bvt &bv0, irep_idt id, const bvt &bv1, representationt rep)
virtual bool literal(const exprt &expr, std::size_t bit, literalt &literal) const
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
bvtypet get_bvtype(const typet &type)
std::vector< exprt > operandst
virtual literalt equality(const exprt &e1, const exprt &e2)
const floatbv_typet & to_floatbv_type(const typet &type)
Cast a generic typet to a floatbv_typet.
Base class for all expressions.
virtual bool has_set_to() const
virtual literalt convert_rest(const exprt &expr)
std::vector< literalt > bvt
literalt relation(const bvt &src1, relt rel, const bvt &src2)