Go to the documentation of this file.
18 "reduction operand bitvector shall have width at least one");
20 enum { O_OR, O_AND, O_XOR } op;
24 if(
id==ID_reduction_or ||
id==ID_reduction_nor)
26 else if(
id==ID_reduction_and ||
id==ID_reduction_nand)
28 else if(
id==ID_reduction_xor ||
id==ID_reduction_xnor)
35 for(std::size_t i=1; i<op_bv.size(); i++)
39 case O_OR: l=
prop.
lor(l, op_bv[i]);
break;
40 case O_AND: l=
prop.
land(l, op_bv[i]);
break;
41 case O_XOR: l=
prop.
lxor(l, op_bv[i]);
break;
45 if(
id==ID_reduction_nor ||
46 id==ID_reduction_nand ||
47 id==ID_reduction_xnor)
59 "reduction operand bitvector shall have width at least one");
61 enum { O_OR, O_AND, O_XOR } op;
65 if(
id==ID_reduction_or ||
id==ID_reduction_nor)
67 else if(
id==ID_reduction_and ||
id==ID_reduction_nand)
69 else if(
id==ID_reduction_xor ||
id==ID_reduction_xnor)
76 if(op_type.
id()!=ID_verilog_signedbv ||
77 op_type.
id()!=ID_verilog_unsignedbv)
79 if((expr.
type().
id()==ID_verilog_signedbv ||
80 expr.
type().
id()==ID_verilog_unsignedbv) &&
88 for(std::size_t i=2; i<op_bv.size(); i+=2)
107 if(
id==ID_reduction_nor ||
108 id==ID_reduction_nand ||
109 id==ID_reduction_xnor)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
virtual literalt convert_reduction(const unary_exprt &expr)
The type of an expression, extends irept.
std::vector< literalt > bvt
Generic base class for unary expressions.
virtual literalt lor(literalt a, literalt b)=0
virtual literalt land(literalt a, literalt b)=0
#define UNREACHABLE
This should be used to mark dead code.
typet & type()
Return the type of the expression.
virtual literalt lxor(literalt a, literalt b)=0
void conversion_failed(const exprt &expr, bvt &bv)
literalt const_literal(bool value)
virtual bvt convert_bv_reduction(const unary_exprt &expr)
const irep_idt & id() const
virtual const bvt & convert_bv(const exprt &expr, const optionalt< std::size_t > expected_width=nullopt)
std::size_t get_size_t(const irep_namet &name) const
virtual literalt lselect(literalt a, literalt b, literalt c)=0