@@ -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)
@@ -65,94 +65,94 @@ bool operator!=(const exprt &lhs, int rhs)
65
65
return true ;
66
66
}
67
67
68
- bool operator ==(const constant_exprt &lhs, int rhs)
68
+ bool constant_exprt:: operator ==(int rhs) const
69
69
{
70
70
if (rhs == 0 )
71
71
{
72
- const irep_idt &type_id = lhs. type ().id ();
72
+ const irep_idt &type_id = type ().id ();
73
73
74
74
if (type_id == ID_integer)
75
75
{
76
- return integer_typet{}.zero_expr () == lhs ;
76
+ return integer_typet{}.zero_expr () == * this ;
77
77
}
78
78
else if (type_id == ID_natural)
79
79
{
80
- return natural_typet{}.zero_expr () == lhs ;
80
+ return natural_typet{}.zero_expr () == * this ;
81
81
}
82
82
else if (type_id == ID_real)
83
83
{
84
- return real_typet{}.zero_expr () == lhs ;
84
+ return real_typet{}.zero_expr () == * this ;
85
85
}
86
86
else if (type_id == ID_rational)
87
87
{
88
88
rationalt rat_value;
89
- if (to_rational (lhs , rat_value))
89
+ if (to_rational (* this , rat_value))
90
90
CHECK_RETURN (false );
91
91
return rat_value.is_zero ();
92
92
}
93
93
else if (
94
94
type_id == ID_unsignedbv || type_id == ID_signedbv ||
95
95
type_id == ID_c_bool || type_id == ID_c_bit_field)
96
96
{
97
- return lhs. value_is_zero_string ();
97
+ return value_is_zero_string ();
98
98
}
99
99
else if (type_id == ID_fixedbv)
100
100
{
101
- return fixedbvt (lhs ).is_zero ();
101
+ return fixedbvt (* this ).is_zero ();
102
102
}
103
103
else if (type_id == ID_floatbv)
104
104
{
105
- return ieee_float_valuet (lhs ).is_zero ();
105
+ return ieee_float_valuet (* this ).is_zero ();
106
106
}
107
107
else if (type_id == ID_pointer)
108
108
{
109
- return lhs == nullptr ;
109
+ return * this == nullptr ;
110
110
}
111
111
else
112
112
return false ;
113
113
}
114
114
else if (rhs == 1 )
115
115
{
116
- const irep_idt &type_id = lhs. type ().id ();
116
+ const irep_idt &type_id = type ().id ();
117
117
118
118
if (type_id == ID_integer)
119
119
{
120
- return integer_typet{}.one_expr () == lhs ;
120
+ return integer_typet{}.one_expr () == * this ;
121
121
}
122
122
else if (type_id == ID_natural)
123
123
{
124
- return natural_typet{}.one_expr () == lhs ;
124
+ return natural_typet{}.one_expr () == * this ;
125
125
}
126
126
else if (type_id == ID_real)
127
127
{
128
- return real_typet{}.one_expr () == lhs ;
128
+ return real_typet{}.one_expr () == * this ;
129
129
}
130
130
else if (type_id == ID_rational)
131
131
{
132
132
rationalt rat_value;
133
- if (to_rational (lhs , rat_value))
133
+ if (to_rational (* this , rat_value))
134
134
CHECK_RETURN (false );
135
135
return rat_value.is_one ();
136
136
}
137
137
else if (
138
138
type_id == ID_unsignedbv || type_id == ID_signedbv ||
139
139
type_id == ID_c_bool || type_id == ID_c_bit_field)
140
140
{
141
- const auto width = to_bitvector_type (lhs. type ()).get_width ();
141
+ const auto width = to_bitvector_type (type ()).get_width ();
142
142
mp_integer int_value =
143
- bvrep2integer (id2string (lhs. get_value ()), width, false );
143
+ bvrep2integer (id2string (get_value ()), width, false );
144
144
return int_value == 1 ;
145
145
}
146
146
else if (type_id == ID_fixedbv)
147
147
{
148
- fixedbv_spect spec{to_fixedbv_type (lhs. type ())};
148
+ fixedbv_spect spec{to_fixedbv_type (type ())};
149
149
fixedbvt one{spec};
150
150
one.from_integer (1 );
151
- return one == fixedbvt{lhs };
151
+ return one == fixedbvt{* this };
152
152
}
153
153
else if (type_id == ID_floatbv)
154
154
{
155
- return ieee_float_valuet (lhs ) == 1 ;
155
+ return ieee_float_valuet (* this ) == 1 ;
156
156
}
157
157
else
158
158
return false ;
@@ -161,10 +161,10 @@ bool operator==(const constant_exprt &lhs, int rhs)
161
161
PRECONDITION (false );
162
162
}
163
163
164
- bool operator !=(const constant_exprt &lhs, int rhs) const
164
+ bool constant_exprt:: operator !=(int rhs) const
165
165
{
166
166
PRECONDITION (rhs == 0 || rhs == 1 );
167
- return !(lhs == rhs);
167
+ return !(* this == rhs);
168
168
}
169
169
170
170
bool constant_exprt::is_null_pointer () const
@@ -195,16 +195,16 @@ bool operator!=(const exprt &lhs, std::nullptr_t rhs)
195
195
return !lhs.is_constant () || !to_constant_expr (lhs).is_null_pointer ();
196
196
}
197
197
198
- bool operator ==(const constant_exprt &lhs, std::nullptr_t rhs)
198
+ bool constant_exprt:: operator ==(std::nullptr_t rhs) const
199
199
{
200
200
(void )rhs; // unused parameter
201
- return lhs. is_null_pointer ();
201
+ return is_null_pointer ();
202
202
}
203
203
204
- bool operator !=(const constant_exprt &lhs, std::nullptr_t rhs) const
204
+ bool constant_exprt:: operator !=(std::nullptr_t rhs) const
205
205
{
206
206
(void )rhs; // unused parameter
207
- return !lhs. is_null_pointer ();
207
+ return !is_null_pointer ();
208
208
}
209
209
210
210
void constant_exprt::check (const exprt &expr, const validation_modet vm)
0 commit comments