@@ -39,14 +39,14 @@ bool operator!=(const exprt &lhs, bool rhs)
39
39
return !lhs.is_constant () || to_constant_expr (lhs) != rhs;
40
40
}
41
41
42
- bool operator ==(const constant_exprt &lhs, bool rhs)
42
+ bool constant_exprt:: operator ==(bool rhs) const
43
43
{
44
- return lhs. is_boolean () && (lhs. get_value () != ID_false) == rhs;
44
+ return is_boolean () && (get_value () != ID_false) == rhs;
45
45
}
46
46
47
- bool operator !=(const constant_exprt &lhs, bool rhs)
47
+ bool constant_exprt:: operator !=(bool rhs) const
48
48
{
49
- return !lhs. is_boolean () || (lhs. get_value () != ID_false) != rhs;
49
+ return !is_boolean () || (get_value () != ID_false) != rhs;
50
50
}
51
51
52
52
bool operator ==(const exprt &lhs, int rhs)
@@ -57,94 +57,94 @@ bool operator==(const exprt &lhs, int rhs)
57
57
return false ;
58
58
}
59
59
60
- bool operator ==(const constant_exprt &lhs, int rhs)
60
+ bool constant_exprt:: operator ==(int rhs) const
61
61
{
62
62
if (rhs == 0 )
63
63
{
64
- const irep_idt &type_id = lhs. type ().id ();
64
+ const irep_idt &type_id = type ().id ();
65
65
66
66
if (type_id == ID_integer)
67
67
{
68
- return integer_typet{}.zero_expr () == lhs ;
68
+ return integer_typet{}.zero_expr () == * this ;
69
69
}
70
70
else if (type_id == ID_natural)
71
71
{
72
- return natural_typet{}.zero_expr () == lhs ;
72
+ return natural_typet{}.zero_expr () == * this ;
73
73
}
74
74
else if (type_id == ID_real)
75
75
{
76
- return real_typet{}.zero_expr () == lhs ;
76
+ return real_typet{}.zero_expr () == * this ;
77
77
}
78
78
else if (type_id == ID_rational)
79
79
{
80
80
rationalt rat_value;
81
- if (to_rational (lhs , rat_value))
81
+ if (to_rational (* this , rat_value))
82
82
CHECK_RETURN (false );
83
83
return rat_value.is_zero ();
84
84
}
85
85
else if (
86
86
type_id == ID_unsignedbv || type_id == ID_signedbv ||
87
87
type_id == ID_c_bool || type_id == ID_c_bit_field)
88
88
{
89
- return lhs. value_is_zero_string ();
89
+ return value_is_zero_string ();
90
90
}
91
91
else if (type_id == ID_fixedbv)
92
92
{
93
- return fixedbvt (lhs ).is_zero ();
93
+ return fixedbvt (* this ).is_zero ();
94
94
}
95
95
else if (type_id == ID_floatbv)
96
96
{
97
- return ieee_float_valuet (lhs ).is_zero ();
97
+ return ieee_float_valuet (* this ).is_zero ();
98
98
}
99
99
else if (type_id == ID_pointer)
100
100
{
101
- return lhs == nullptr ;
101
+ return * this == nullptr ;
102
102
}
103
103
else
104
104
return false ;
105
105
}
106
106
else if (rhs == 1 )
107
107
{
108
- const irep_idt &type_id = lhs. type ().id ();
108
+ const irep_idt &type_id = type ().id ();
109
109
110
110
if (type_id == ID_integer)
111
111
{
112
- return integer_typet{}.one_expr () == lhs ;
112
+ return integer_typet{}.one_expr () == * this ;
113
113
}
114
114
else if (type_id == ID_natural)
115
115
{
116
- return natural_typet{}.one_expr () == lhs ;
116
+ return natural_typet{}.one_expr () == * this ;
117
117
}
118
118
else if (type_id == ID_real)
119
119
{
120
- return real_typet{}.one_expr () == lhs ;
120
+ return real_typet{}.one_expr () == * this ;
121
121
}
122
122
else if (type_id == ID_rational)
123
123
{
124
124
rationalt rat_value;
125
- if (to_rational (lhs , rat_value))
125
+ if (to_rational (* this , rat_value))
126
126
CHECK_RETURN (false );
127
127
return rat_value.is_one ();
128
128
}
129
129
else if (
130
130
type_id == ID_unsignedbv || type_id == ID_signedbv ||
131
131
type_id == ID_c_bool || type_id == ID_c_bit_field)
132
132
{
133
- const auto width = to_bitvector_type (lhs. type ()).get_width ();
133
+ const auto width = to_bitvector_type (type ()).get_width ();
134
134
mp_integer int_value =
135
- bvrep2integer (id2string (lhs. get_value ()), width, false );
135
+ bvrep2integer (id2string (get_value ()), width, false );
136
136
return int_value == 1 ;
137
137
}
138
138
else if (type_id == ID_fixedbv)
139
139
{
140
- fixedbv_spect spec{to_fixedbv_type (lhs. type ())};
140
+ fixedbv_spect spec{to_fixedbv_type (type ())};
141
141
fixedbvt one{spec};
142
142
one.from_integer (1 );
143
- return one == fixedbvt{lhs };
143
+ return one == fixedbvt{* this };
144
144
}
145
145
else if (type_id == ID_floatbv)
146
146
{
147
- return ieee_float_valuet (lhs ) == 1 ;
147
+ return ieee_float_valuet (* this ) == 1 ;
148
148
}
149
149
else
150
150
return false ;
@@ -175,10 +175,10 @@ bool operator==(const exprt &lhs, std::nullptr_t rhs)
175
175
return lhs.is_constant () && to_constant_expr (lhs).is_null_pointer ();
176
176
}
177
177
178
- bool operator ==(const constant_exprt &lhs, std::nullptr_t rhs)
178
+ bool constant_exprt:: operator ==(std::nullptr_t rhs) const
179
179
{
180
180
(void )rhs; // unused parameter
181
- return lhs. is_null_pointer ();
181
+ return is_null_pointer ();
182
182
}
183
183
184
184
void constant_exprt::check (const exprt &expr, const validation_modet vm)
0 commit comments