Skip to content

Commit 0900508

Browse files
tautschnigtautschnig
committed
operator== for exprt and bool, int, nullptr_t
Introduces comparison operators for more concise code, and deprecates `exprt::is_{true,false,zero,one}` in favour of these.
1 parent e88ed5f commit 0900508

File tree

4 files changed

+220
-83
lines changed

4 files changed

+220
-83
lines changed

‎src/util/expr.cpp‎

Lines changed: 4 additions & 83 deletions
Original file line numberDiff line numberDiff line change
@@ -26,14 +26,14 @@ Author: Daniel Kroening, kroening@kroening.com
2626
/// \return True if is a Boolean constant representing `true`, false otherwise.
2727
bool exprt::is_true() const
2828
{
29-
return is_constant() && is_boolean() && get(ID_value) != ID_false;
29+
return *this == true;
3030
}
3131

3232
/// Return whether the expression is a constant representing `false`.
3333
/// \return True if is a Boolean constant representing `false`, false otherwise.
3434
bool exprt::is_false() const
3535
{
36-
return is_constant() && is_boolean() && get(ID_value) == ID_false;
36+
return *this == false;
3737
}
3838

3939
/// Return whether the expression is a constant representing 0.
@@ -46,45 +46,7 @@ bool exprt::is_false() const
4646
/// \return True if has value 0, false otherwise.
4747
bool exprt::is_zero() const
4848
{
49-
if(is_constant())
50-
{
51-
const constant_exprt &constant=to_constant_expr(*this);
52-
const irep_idt &type_id=type().id_string();
53-
54-
if(type_id==ID_integer || type_id==ID_natural)
55-
{
56-
return constant.value_is_zero_string();
57-
}
58-
else if(type_id==ID_rational)
59-
{
60-
rationalt rat_value;
61-
if(to_rational(*this, rat_value))
62-
CHECK_RETURN(false);
63-
return rat_value.is_zero();
64-
}
65-
else if(
66-
type_id == ID_unsignedbv || type_id == ID_signedbv ||
67-
type_id == ID_c_bool || type_id == ID_c_bit_field)
68-
{
69-
return constant.value_is_zero_string();
70-
}
71-
else if(type_id==ID_fixedbv)
72-
{
73-
if(fixedbvt(constant)==0)
74-
return true;
75-
}
76-
else if(type_id==ID_floatbv)
77-
{
78-
if(ieee_float_valuet(constant) == 0)
79-
return true;
80-
}
81-
else if(type_id==ID_pointer)
82-
{
83-
return constant.is_null_pointer();
84-
}
85-
}
86-
87-
return false;
49+
return *this == 0;
8850
}
8951

9052
/// Return whether the expression is a constant representing 1.
@@ -95,48 +57,7 @@ bool exprt::is_zero() const
9557
/// \return True if has value 1, false otherwise.
9658
bool exprt::is_one() const
9759
{
98-
if(is_constant())
99-
{
100-
const auto &constant_expr = to_constant_expr(*this);
101-
const irep_idt &type_id = type().id();
102-
103-
if(type_id==ID_integer || type_id==ID_natural)
104-
{
105-
mp_integer int_value =
106-
string2integer(id2string(constant_expr.get_value()));
107-
if(int_value==1)
108-
return true;
109-
}
110-
else if(type_id==ID_rational)
111-
{
112-
rationalt rat_value;
113-
if(to_rational(*this, rat_value))
114-
CHECK_RETURN(false);
115-
return rat_value.is_one();
116-
}
117-
else if(
118-
type_id == ID_unsignedbv || type_id == ID_signedbv ||
119-
type_id == ID_c_bool || type_id == ID_c_bit_field)
120-
{
121-
const auto width = to_bitvector_type(type()).get_width();
122-
mp_integer int_value =
123-
bvrep2integer(id2string(constant_expr.get_value()), width, false);
124-
if(int_value==1)
125-
return true;
126-
}
127-
else if(type_id==ID_fixedbv)
128-
{
129-
if(fixedbvt(constant_expr) == 1)
130-
return true;
131-
}
132-
else if(type_id==ID_floatbv)
133-
{
134-
if(ieee_float_valuet(constant_expr) == 1)
135-
return true;
136-
}
137-
}
138-
139-
return false;
60+
return *this == 1;
14061
}
14162

14263
/// Get a \ref source_locationt from the expression or from its operands

‎src/util/expr.h‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
1010
#define CPROVER_UTIL_EXPR_H
1111

1212
#include "as_const.h"
13+
#include "deprecate.h"
1314
#include "type.h"
1415
#include "validate_expressions.h"
1516
#include "validate_types.h"
@@ -214,9 +215,13 @@ class exprt:public irept
214215
return id() == ID_constant;
215216
}
216217

218+
DEPRECATED(SINCE(2025, 7, 5, "use expr == true instead"))
217219
bool is_true() const;
220+
DEPRECATED(SINCE(2025, 7, 5, "use expr == false instead"))
218221
bool is_false() const;
222+
DEPRECATED(SINCE(2025, 7, 5, "use expr == 0 instead"))
219223
bool is_zero() const;
224+
DEPRECATED(SINCE(2025, 7, 5, "use expr == 1 instead"))
220225
bool is_one() const;
221226

222227
/// Return whether the expression represents a Boolean.

‎src/util/std_expr.cpp‎

Lines changed: 169 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,10 +8,17 @@ Author: Daniel Kroening, kroening@kroening.com
88

99
#include "std_expr.h"
1010

11+
#include "arith_tools.h"
1112
#include "config.h"
13+
#include "expr_util.h"
14+
#include "fixedbv.h"
15+
#include "ieee_float.h"
16+
#include "mathematical_types.h"
1217
#include "namespace.h"
1318
#include "pointer_expr.h"
1419
#include "range.h"
20+
#include "rational.h"
21+
#include "rational_tools.h"
1522
#include "substitute_symbols.h"
1623

1724
#include <map>
@@ -22,6 +29,144 @@ bool constant_exprt::value_is_zero_string() const
2229
return val.find_first_not_of('0')==std::string::npos;
2330
}
2431

32+
bool operator==(const exprt &lhs, bool rhs)
33+
{
34+
return lhs.is_constant() && to_constant_expr(lhs) == rhs;
35+
}
36+
37+
bool operator!=(const exprt &lhs, bool rhs)
38+
{
39+
return !lhs.is_constant() || to_constant_expr(lhs) != rhs;
40+
}
41+
42+
bool operator==(const constant_exprt &lhs, bool rhs)
43+
{
44+
return lhs.is_boolean() && (lhs.get_value() != ID_false) == rhs;
45+
}
46+
47+
bool operator!=(const constant_exprt &lhs, bool rhs)
48+
{
49+
return !lhs.is_boolean() || (lhs.get_value() != ID_false) != rhs;
50+
}
51+
52+
bool operator==(const exprt &lhs, int rhs)
53+
{
54+
if(lhs.is_constant())
55+
return to_constant_expr(lhs) == rhs;
56+
else
57+
return false;
58+
}
59+
60+
bool operator!=(const exprt &lhs, int rhs)
61+
{
62+
if(lhs.is_constant())
63+
return to_constant_expr(lhs) != rhs;
64+
else
65+
return true;
66+
}
67+
68+
bool operator==(const constant_exprt &lhs, int rhs)
69+
{
70+
if(rhs == 0)
71+
{
72+
const irep_idt &type_id = lhs.type().id();
73+
74+
if(type_id == ID_integer)
75+
{
76+
return integer_typet{}.zero_expr() == lhs;
77+
}
78+
else if(type_id == ID_natural)
79+
{
80+
return natural_typet{}.zero_expr() == lhs;
81+
}
82+
else if(type_id == ID_real)
83+
{
84+
return real_typet{}.zero_expr() == lhs;
85+
}
86+
else if(type_id == ID_rational)
87+
{
88+
rationalt rat_value;
89+
if(to_rational(lhs, rat_value))
90+
CHECK_RETURN(false);
91+
return rat_value.is_zero();
92+
}
93+
else if(
94+
type_id == ID_unsignedbv || type_id == ID_signedbv ||
95+
type_id == ID_c_bool || type_id == ID_c_bit_field)
96+
{
97+
return lhs.value_is_zero_string();
98+
}
99+
else if(type_id == ID_fixedbv)
100+
{
101+
return fixedbvt(lhs).is_zero();
102+
}
103+
else if(type_id == ID_floatbv)
104+
{
105+
return ieee_float_valuet(lhs).is_zero();
106+
}
107+
else if(type_id == ID_pointer)
108+
{
109+
return lhs == nullptr;
110+
}
111+
else
112+
return false;
113+
}
114+
else if(rhs == 1)
115+
{
116+
const irep_idt &type_id = lhs.type().id();
117+
118+
if(type_id == ID_integer)
119+
{
120+
return integer_typet{}.one_expr() == lhs;
121+
}
122+
else if(type_id == ID_natural)
123+
{
124+
return natural_typet{}.one_expr() == lhs;
125+
}
126+
else if(type_id == ID_real)
127+
{
128+
return real_typet{}.one_expr() == lhs;
129+
}
130+
else if(type_id == ID_rational)
131+
{
132+
rationalt rat_value;
133+
if(to_rational(lhs, rat_value))
134+
CHECK_RETURN(false);
135+
return rat_value.is_one();
136+
}
137+
else if(
138+
type_id == ID_unsignedbv || type_id == ID_signedbv ||
139+
type_id == ID_c_bool || type_id == ID_c_bit_field)
140+
{
141+
const auto width = to_bitvector_type(lhs.type()).get_width();
142+
mp_integer int_value =
143+
bvrep2integer(id2string(lhs.get_value()), width, false);
144+
return int_value == 1;
145+
}
146+
else if(type_id == ID_fixedbv)
147+
{
148+
fixedbv_spect spec{to_fixedbv_type(lhs.type())};
149+
fixedbvt one{spec};
150+
one.from_integer(1);
151+
return one == fixedbvt{lhs};
152+
}
153+
else if(type_id == ID_floatbv)
154+
{
155+
return ieee_float_valuet(lhs) == 1;
156+
}
157+
else
158+
return false;
159+
}
160+
else
161+
PRECONDITION(false);
162+
}
163+
164+
bool operator!=(const constant_exprt &lhs, int rhs) const
165+
{
166+
PRECONDITION(rhs == 0 || rhs == 1);
167+
return !(lhs == rhs);
168+
}
169+
25170
bool constant_exprt::is_null_pointer() const
26171
{
27172
if(type().id() != ID_pointer)
@@ -38,6 +183,30 @@ bool constant_exprt::is_null_pointer() const
38183
return false;
39184
}
40185

186+
bool operator==(const exprt &lhs, std::nullptr_t rhs)
187+
{
188+
(void)rhs; // unused parameter
189+
return lhs.is_constant() && to_constant_expr(lhs).is_null_pointer();
190+
}
191+
192+
bool operator!=(const exprt &lhs, std::nullptr_t rhs)
193+
{
194+
(void)rhs; // unused parameter
195+
return !lhs.is_constant() || !to_constant_expr(lhs).is_null_pointer();
196+
}
197+
198+
bool operator==(const constant_exprt &lhs, std::nullptr_t rhs)
199+
{
200+
(void)rhs; // unused parameter
201+
return lhs.is_null_pointer();
202+
}
203+
204+
bool operator!=(const constant_exprt &lhs, std::nullptr_t rhs) const
205+
{
206+
(void)rhs; // unused parameter
207+
return !lhs.is_null_pointer();
208+
}
209+
41210
void constant_exprt::check(const exprt &expr, const validation_modet vm)
42211
{
43212
nullary_exprt::check(expr, vm);

‎src/util/std_expr.h‎

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3189,6 +3189,48 @@ inline constant_exprt &to_constant_expr(exprt &expr)
31893189
return static_cast<constant_exprt &>(expr);
31903190
}
31913191

3192+
/// Return whether the expression \p lhs is a constant of Boolean type that is
3193+
/// representing the Boolean value \p rhs.
3194+
bool operator==(const exprt &lhs, bool rhs);
3195+
/// \copydoc operator==(const exprt &, bool)
3196+
bool operator==(const constant_exprt &lhs, bool rhs);
3197+
3198+
/// Return whether the expression \p lhs is not a constant of Boolean type or is
3199+
/// not representing the Boolean value \p rhs.
3200+
bool operator!=(const exprt &lhs, bool rhs);
3201+
/// \copydoc operator!=(const exprt &, bool)
3202+
bool operator!=(const constant_exprt &lhs, bool rhs);
3203+
3204+
/// Return whether the expression \p lhs is a constant representing the numeric
3205+
/// value \p rhs; only values 0 and 1 are supported for \p rhs.
3206+
/// For value 0 we consider the following types: ID_integer, ID_natural,
3207+
/// ID_rational, ID_unsignedbv, ID_signedbv, ID_c_bool, ID_c_bit_field,
3208+
/// ID_fixedbv, ID_floatbv, ID_pointer.<br>
3209+
/// For ID_pointer, returns true iff the value is a zero string or a null
3210+
/// pointer.<br>
3211+
/// For value 1 we consider the following types: ID_integer, ID_natural,
3212+
/// ID_rational, ID_unsignedbv, ID_signedbv, ID_c_bool, ID_c_bit_field,
3213+
/// ID_fixedbv, ID_floatbv.<br>
3214+
/// For all other types, return false.
3215+
bool operator==(const exprt &lhs, int rhs);
3216+
/// \copydoc operator==(const exprt &, int)
3217+
bool operator==(const constant_exprt &lhs, int rhs);
3218+
3219+
/// Returns the negation of \ref operator==(const exprt &, int).
3220+
bool operator!=(const exprt &lhs, int rhs);
3221+
/// \copydoc operator!=(const exprt &, int)
3222+
bool operator!=(const constant_exprt &lhs, int rhs);
3223+
3224+
/// Return whether the expression \p lhs is a constant representing the NULL
3225+
/// pointer.
3226+
bool operator==(const exprt &lhs, std::nullptr_t);
3227+
/// \copydoc operator==(const exprt &, std::nullptr_t)
3228+
bool operator==(const constant_exprt &lhs, std::nullptr_t);
3229+
3230+
/// Returns the negation of \ref operator==(const exprt &, std::nullptr_t).
3231+
bool operator!=(const exprt &lhs, std::nullptr_t);
3232+
/// \copydoc operator!=(const exprt &, std::nullptr_t)
3233+
bool operator!=(const constant_exprt &lhs, std::nullptr_t);
31923234

31933235
/// \brief The Boolean constant true
31943236
class true_exprt:public constant_exprt

0 commit comments

Comments
 (0)