Skip to content

Commit 04b28e5

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 48490fb commit 04b28e5

File tree

4 files changed

+180
-83
lines changed

4 files changed

+180
-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, [email protected]
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, [email protected]
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: 143 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,10 +8,17 @@ Author: Daniel Kroening, [email protected]
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,130 @@ 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 constant_exprt &lhs, int rhs)
61+
{
62+
if(rhs == 0)
63+
{
64+
const irep_idt &type_id = lhs.type().id();
65+
66+
if(type_id == ID_integer)
67+
{
68+
return integer_typet{}.zero_expr() == lhs;
69+
}
70+
else if(type_id == ID_natural)
71+
{
72+
return natural_typet{}.zero_expr() == lhs;
73+
}
74+
else if(type_id == ID_real)
75+
{
76+
return real_typet{}.zero_expr() == lhs;
77+
}
78+
else if(type_id == ID_rational)
79+
{
80+
rationalt rat_value;
81+
if(to_rational(lhs, rat_value))
82+
CHECK_RETURN(false);
83+
return rat_value.is_zero();
84+
}
85+
else if(
86+
type_id == ID_unsignedbv || type_id == ID_signedbv ||
87+
type_id == ID_c_bool || type_id == ID_c_bit_field)
88+
{
89+
return lhs.value_is_zero_string();
90+
}
91+
else if(type_id == ID_fixedbv)
92+
{
93+
return fixedbvt(lhs).is_zero();
94+
}
95+
else if(type_id == ID_floatbv)
96+
{
97+
return ieee_float_valuet(lhs).is_zero();
98+
}
99+
else if(type_id == ID_pointer)
100+
{
101+
return lhs == nullptr;
102+
}
103+
else
104+
return false;
105+
}
106+
else if(rhs == 1)
107+
{
108+
const irep_idt &type_id = lhs.type().id();
109+
110+
if(type_id == ID_integer)
111+
{
112+
return integer_typet{}.one_expr() == lhs;
113+
}
114+
else if(type_id == ID_natural)
115+
{
116+
return natural_typet{}.one_expr() == lhs;
117+
}
118+
else if(type_id == ID_real)
119+
{
120+
return real_typet{}.one_expr() == lhs;
121+
}
122+
else if(type_id == ID_rational)
123+
{
124+
rationalt rat_value;
125+
if(to_rational(lhs, rat_value))
126+
CHECK_RETURN(false);
127+
return rat_value.is_one();
128+
}
129+
else if(
130+
type_id == ID_unsignedbv || type_id == ID_signedbv ||
131+
type_id == ID_c_bool || type_id == ID_c_bit_field)
132+
{
133+
const auto width = to_bitvector_type(lhs.type()).get_width();
134+
mp_integer int_value =
135+
bvrep2integer(id2string(lhs.get_value()), width, false);
136+
return int_value == 1;
137+
}
138+
else if(type_id == ID_fixedbv)
139+
{
140+
fixedbv_spect spec{to_fixedbv_type(lhs.type())};
141+
fixedbvt one{spec};
142+
one.from_integer(1);
143+
return one == fixedbvt{lhs};
144+
}
145+
else if(type_id == ID_floatbv)
146+
{
147+
return ieee_float_valuet(lhs) == 1;
148+
}
149+
else
150+
return false;
151+
}
152+
else
153+
PRECONDITION(false);
154+
}
155+
25156
bool constant_exprt::is_null_pointer() const
26157
{
27158
if(type().id() != ID_pointer)
@@ -38,6 +169,18 @@ bool constant_exprt::is_null_pointer() const
38169
return false;
39170
}
40171

172+
bool operator==(const exprt &lhs, std::nullptr_t rhs)
173+
{
174+
(void)rhs; // unused parameter
175+
return lhs.is_constant() && to_constant_expr(lhs).is_null_pointer();
176+
}
177+
178+
bool operator==(const constant_exprt &lhs, std::nullptr_t rhs)
179+
{
180+
(void)rhs; // unused parameter
181+
return lhs.is_null_pointer();
182+
}
183+
41184
void constant_exprt::check(const exprt &expr, const validation_modet vm)
42185
{
43186
nullary_exprt::check(expr, vm);

‎src/util/std_expr.h

Lines changed: 28 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3189,6 +3189,34 @@ 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+
bool operator!=(const exprt &lhs, bool rhs);
3196+
/// \copydoc operator==(const constant_exprt &, bool)
3197+
bool operator==(const constant_exprt &lhs, bool rhs);
3198+
bool operator!=(const constant_exprt &lhs, bool rhs);
3199+
3200+
/// Return whether the expression \p lhs is a constant representing the numeric
3201+
/// value \p rhs; only values 0 and 1 are supported for \p rhs.
3202+
/// For value 0 we consider the following types: ID_integer, ID_natural,
3203+
/// ID_rational, ID_unsignedbv, ID_signedbv, ID_c_bool, ID_c_bit_field,
3204+
/// ID_fixedbv, ID_floatbv, ID_pointer.<br>
3205+
/// For ID_pointer, returns true iff the value is a zero string or a null
3206+
/// pointer.<br>
3207+
/// For value 1 we consider the following types: ID_integer, ID_natural,
3208+
/// ID_rational, ID_unsignedbv, ID_signedbv, ID_c_bool, ID_c_bit_field,
3209+
/// ID_fixedbv, ID_floatbv.<br>
3210+
/// For all other types, return false.
3211+
bool operator==(const exprt &lhs, int rhs);
3212+
/// \copydoc operator==(const constant_exprt &, int)
3213+
bool operator==(const constant_exprt &lhs, int rhs);
3214+
3215+
/// Return whether the expression \p lhs is a constant representing the NULL
3216+
/// pointer.
3217+
bool operator==(const exprt &lhs, std::nullptr_t);
3218+
/// \copydoc operator==(const constant_exprt &, std::nullptr_t)
3219+
bool operator==(const constant_exprt &lhs, std::nullptr_t);
31923220

31933221
/// \brief The Boolean constant true
31943222
class true_exprt:public constant_exprt

0 commit comments

Comments
 (0)