Skip to content

Commit b3c456f

Browse files
kroeningkroening
authored
Merge pull request #6543 from tautschnig/is_boolean
Consistently use exprt::is_boolean()
2 parents abd5181 + 882b295 commit b3c456f

37 files changed

+114
-128
lines changed

‎jbmc/src/java_bytecode/expr2java.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -175,7 +175,7 @@ std::string expr2javat::convert_constant(
175175
else
176176
return "false";
177177
}
178-
else if(src.type().id()==ID_bool)
178+
else if(src.is_boolean())
179179
{
180180
if(src.is_true())
181181
return "true";

‎src/analyses/guard_expr.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,7 @@ exprt guard_exprt::guard_expr(exprt expr) const
3737

3838
void guard_exprt::add(const exprt &expr)
3939
{
40-
PRECONDITION(expr.type().id() == ID_bool);
40+
PRECONDITION(expr.is_boolean());
4141

4242
if(is_false() || expr.is_true())
4343
return;

‎src/analyses/invariant_set.cpp

+3-3
Original file line numberDiff line numberDiff line change
@@ -381,7 +381,7 @@ void invariant_sett::strengthen(const exprt &expr)
381381

382382
void invariant_sett::strengthen_rec(const exprt &expr)
383383
{
384-
if(expr.type().id()!=ID_bool)
384+
if(!expr.is_boolean())
385385
throw "non-Boolean argument to strengthen()";
386386

387387
#if 0
@@ -584,7 +584,7 @@ tvt invariant_sett::implies(const exprt &expr) const
584584

585585
tvt invariant_sett::implies_rec(const exprt &expr) const
586586
{
587-
if(expr.type().id()!=ID_bool)
587+
if(!expr.is_boolean())
588588
throw "implies: non-Boolean expression";
589589

590590
#if 0
@@ -696,7 +696,7 @@ void invariant_sett::get_bounds(unsigned a, boundst &bounds) const
696696

697697
void invariant_sett::nnf(exprt &expr, bool negate)
698698
{
699-
if(expr.type().id()!=ID_bool)
699+
if(!expr.is_boolean())
700700
throw "nnf: non-Boolean expression";
701701

702702
if(expr.is_true())

‎src/analyses/variable-sensitivity/abstract_environment.cpp

+2-3
Original file line numberDiff line numberDiff line change
@@ -262,16 +262,15 @@ bool abstract_environmentt::assume(const exprt &expr, const namespacet &ns)
262262
// We should only attempt to assume Boolean things
263263
// This should be enforced by the well-structured-ness of the
264264
// goto-program and the way assume is used.
265-
PRECONDITION(expr.type().id() == ID_bool);
265+
PRECONDITION(expr.is_boolean());
266266

267267
auto simplified = simplify_expr(expr, ns);
268268
auto assumption = do_assume(simplified, ns);
269269

270270
if(assumption.id() != ID_nil) // I.E. actually a value
271271
{
272272
// Should be of the right type
273-
INVARIANT(
274-
assumption.type().id() == ID_bool, "simplification preserves type");
273+
INVARIANT(assumption.is_boolean(), "simplification preserves type");
275274

276275
if(assumption.is_false())
277276
{

‎src/ansi-c/c_typecheck_expr.cpp

+17-15
Original file line numberDiff line numberDiff line change
@@ -431,7 +431,7 @@ void c_typecheck_baset::typecheck_expr_main(exprt &expr)
431431
// This is one of the few places where it's detectable
432432
// that we are using "bool" for boolean operators instead
433433
// of "int". We convert for this reason.
434-
if(op.type().id() == ID_bool)
434+
if(op.is_boolean())
435435
op = typecast_exprt(op, signed_int_type());
436436

437437
irept::subt &generic_associations=
@@ -960,7 +960,7 @@ void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr)
960960
// This is one of the few places where it's detectable
961961
// that we are using "bool" for boolean operators instead
962962
// of "int". We convert for this reason.
963-
if(op.type().id() == ID_bool)
963+
if(op.is_boolean())
964964
type = signed_int_type();
965965
else
966966
type = op.type();
@@ -1102,7 +1102,7 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr)
11021102
// This is one of the few places where it's detectable
11031103
// that we are using "bool" for boolean operators instead
11041104
// of "int". We convert for this reason.
1105-
if(op.type().id() == ID_bool)
1105+
if(op.is_boolean())
11061106
op = typecast_exprt(op, signed_int_type());
11071107

11081108
// we need to find a member with the right type
@@ -1718,7 +1718,7 @@ void c_typecheck_baset::typecheck_expr_address_of(exprt &expr)
17181718
throw 0;
17191719
}
17201720

1721-
if(op.type().id() == ID_bool)
1721+
if(op.is_boolean())
17221722
{
17231723
error().source_location = expr.source_location();
17241724
error() << "cannot take address of a single bit" << eom;
@@ -4387,7 +4387,7 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
43874387
{
43884388
implicit_typecast_arithmetic(op0, op1);
43894389
if(
4390-
op1.type().id() == ID_bool || op1.type().id() == ID_c_bool ||
4390+
op1.is_boolean() || op1.type().id() == ID_c_bool ||
43914391
op1.type().id() == ID_c_enum_tag || op1.type().id() == ID_unsignedbv ||
43924392
op1.type().id() == ID_signedbv || op1.type().id() == ID_c_bit_field)
43934393
{
@@ -4453,7 +4453,7 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
44534453
implicit_typecast_arithmetic(op1);
44544454

44554455
if(
4456-
is_number(op1.type()) || op1.type().id() == ID_bool ||
4456+
is_number(op1.type()) || op1.is_boolean() ||
44574457
op1.type().id() == ID_c_bool || op1.type().id() == ID_c_enum_tag)
44584458
{
44594459
op1 = typecast_exprt(op1, o_type0);
@@ -4464,22 +4464,24 @@ void c_typecheck_baset::typecheck_side_effect_assignment(
44644464
o_type0.id()==ID_c_bool)
44654465
{
44664466
implicit_typecast_arithmetic(op0, op1);
4467-
if(op1.type().id()==ID_bool ||
4468-
op1.type().id()==ID_c_bool ||
4469-
op1.type().id()==ID_c_enum_tag ||
4470-
op1.type().id()==ID_unsignedbv ||
4471-
op1.type().id()==ID_signedbv)
4467+
if(
4468+
op1.is_boolean() || op1.type().id() == ID_c_bool ||
4469+
op1.type().id() == ID_c_enum_tag || op1.type().id() == ID_unsignedbv ||
4470+
op1.type().id() == ID_signedbv)
4471+
{
44724472
return;
4473+
}
44734474
}
44744475
else
44754476
{
44764477
implicit_typecast_arithmetic(op0, op1);
44774478

4478-
if(is_number(op1.type()) ||
4479-
op1.type().id()==ID_bool ||
4480-
op1.type().id()==ID_c_bool ||
4481-
op1.type().id()==ID_c_enum_tag)
4479+
if(
4480+
is_number(op1.type()) || op1.is_boolean() ||
4481+
op1.type().id() == ID_c_bool || op1.type().id() == ID_c_enum_tag)
4482+
{
44824483
return;
4484+
}
44834485
}
44844486
}
44854487

‎src/ansi-c/padding.cpp

+3-4
Original file line numberDiff line numberDiff line change
@@ -193,8 +193,7 @@ static void add_padding_msvc(struct_typet &type, const namespacet &ns)
193193
const auto width = to_c_bit_field_type(it->type()).get_width();
194194
bit_field_bits += width;
195195
}
196-
else if(
197-
it->type().id() == ID_bool && underlying_bits == config.ansi_c.char_width)
196+
else if(it->is_boolean() && underlying_bits == config.ansi_c.char_width)
198197
{
199198
++bit_field_bits;
200199
}
@@ -242,7 +241,7 @@ static void add_padding_msvc(struct_typet &type, const namespacet &ns)
242241
const auto width = to_c_bit_field_type(it->type()).get_width();
243242
bit_field_bits += width;
244243
}
245-
else if(it->type().id() == ID_bool)
244+
else if(it->is_boolean())
246245
{
247246
underlying_bits = config.ansi_c.char_width;
248247
++bit_field_bits;
@@ -304,7 +303,7 @@ static void add_padding_gcc(struct_typet &type, const namespacet &ns)
304303
const std::size_t width = to_c_bit_field_type(it->type()).get_width();
305304
bit_field_bits+=width;
306305
}
307-
else if(it->type().id() == ID_bool)
306+
else if(it->is_boolean())
308307
{
309308
++bit_field_bits;
310309
}

‎src/cpp/cpp_typecheck_conversions.cpp

+4-4
Original file line numberDiff line numberDiff line change
@@ -221,7 +221,7 @@ bool cpp_typecheckt::standard_conversion_integral_promotion(
221221
return true;
222222
}
223223

224-
if(expr.type().id() == ID_bool || expr.type().id() == ID_c_bool)
224+
if(expr.is_boolean() || expr.type().id() == ID_c_bool)
225225
{
226226
new_expr = typecast_exprt(expr, int_type);
227227
return true;
@@ -308,7 +308,7 @@ bool cpp_typecheckt::standard_conversion_integral_conversion(
308308

309309
if(
310310
expr.type().id() != ID_signedbv && expr.type().id() != ID_unsignedbv &&
311-
expr.type().id() != ID_c_bool && expr.type().id() != ID_bool &&
311+
expr.type().id() != ID_c_bool && !expr.is_boolean() &&
312312
expr.type().id() != ID_c_enum_tag)
313313
{
314314
return false;
@@ -640,7 +640,7 @@ bool cpp_typecheckt::standard_conversion_boolean(
640640

641641
if(
642642
expr.type().id() != ID_signedbv && expr.type().id() != ID_unsignedbv &&
643-
expr.type().id() != ID_pointer && expr.type().id() != ID_bool &&
643+
expr.type().id() != ID_pointer && !expr.is_boolean() &&
644644
expr.type().id() != ID_c_enum_tag)
645645
{
646646
return false;
@@ -1838,7 +1838,7 @@ bool cpp_typecheckt::reinterpret_typecast(
18381838

18391839
if(
18401840
(e.type().id() == ID_unsignedbv || e.type().id() == ID_signedbv ||
1841-
e.type().id() == ID_c_bool || e.type().id() == ID_bool) &&
1841+
e.type().id() == ID_c_bool || e.is_boolean()) &&
18421842
type.id() == ID_pointer && !is_reference(type))
18431843
{
18441844
// integer to pointer

‎src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -88,7 +88,7 @@ bool disjunctive_polynomial_accelerationt::accelerate(
8888
polynomialt poly;
8989
exprt target=*it;
9090

91-
if(it->type().id()==ID_bool)
91+
if(it->is_boolean())
9292
{
9393
// Hack: don't try to accelerate booleans.
9494
continue;
@@ -150,7 +150,7 @@ bool disjunctive_polynomial_accelerationt::accelerate(
150150
std::cout << "Trying to accelerate " << format(*it) << '\n';
151151
#endif
152152

153-
if(it->type().id()==ID_bool)
153+
if(it->is_boolean())
154154
{
155155
// Hack: don't try to accelerate booleans.
156156
accelerator.dirty_vars.insert(*it);

‎src/goto-instrument/cover_util.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,7 @@ Author: Daniel Kroening
1313

1414
bool is_condition(const exprt &src)
1515
{
16-
if(src.type().id() != ID_bool)
16+
if(!src.is_boolean())
1717
return false;
1818

1919
// conditions are 'atomic predicates'
@@ -73,7 +73,7 @@ void collect_decisions_rec(const exprt &src, std::set<exprt> &dest)
7373
return;
7474
}
7575

76-
if(src.type().id() == ID_bool)
76+
if(src.is_boolean())
7777
{
7878
if(src.is_constant())
7979
{

‎src/goto-programs/goto_program.h

+1-1
Original file line numberDiff line numberDiff line change
@@ -1011,7 +1011,7 @@ class goto_programt
10111011
const exprt &_cond,
10121012
const source_locationt &l = source_locationt::nil())
10131013
{
1014-
PRECONDITION(_cond.type().id() == ID_bool);
1014+
PRECONDITION(_cond.is_boolean());
10151015
return instructiont(
10161016
static_cast<const goto_instruction_codet &>(get_nil_irep()),
10171017
l,

‎src/goto-programs/interpreter_evaluate.cpp

+2-2
Original file line numberDiff line numberDiff line change
@@ -380,7 +380,7 @@ interpretert::mp_vectort interpretert::evaluate(const exprt &expr)
380380
const auto width = to_c_bool_type(expr.type()).get_width();
381381
return {bvrep2integer(value, width, false)};
382382
}
383-
else if(expr.type().id()==ID_bool)
383+
else if(expr.is_boolean())
384384
{
385385
return {expr.is_true()};
386386
}
@@ -910,7 +910,7 @@ interpretert::mp_vectort interpretert::evaluate(const exprt &expr)
910910
const auto s = integer2bvrep(value, width);
911911
return {bvrep2integer(s, width, false)};
912912
}
913-
else if((expr.type().id()==ID_bool) || (expr.type().id()==ID_c_bool))
913+
else if(expr.is_boolean() || expr.type().id() == ID_c_bool)
914914
return {value != 0};
915915
}
916916
}

‎src/solvers/flattening/boolbv.cpp

+3-3
Original file line numberDiff line numberDiff line change
@@ -95,7 +95,7 @@ bvt boolbvt::conversion_failed(const exprt &expr)
9595
/// circuit
9696
bvt boolbvt::convert_bitvector(const exprt &expr)
9797
{
98-
if(expr.type().id()==ID_bool)
98+
if(expr.is_boolean())
9999
return {convert(expr)};
100100

101101
if(expr.id()==ID_index)
@@ -317,7 +317,7 @@ bvt boolbvt::convert_function_application(
317317

318318
literalt boolbvt::convert_rest(const exprt &expr)
319319
{
320-
PRECONDITION(expr.type().id() == ID_bool);
320+
PRECONDITION(expr.is_boolean());
321321

322322
if(expr.id()==ID_typecast)
323323
return convert_typecast(to_typecast_expr(expr));
@@ -506,7 +506,7 @@ bool boolbvt::boolbv_set_equality_to_true(const equal_exprt &expr)
506506

507507
void boolbvt::set_to(const exprt &expr, bool value)
508508
{
509-
PRECONDITION(expr.type().id() == ID_bool);
509+
PRECONDITION(expr.is_boolean());
510510

511511
const auto equal_expr = expr_try_dynamic_cast<equal_exprt>(expr);
512512
if(value && equal_expr && !boolbv_set_equality_to_true(*equal_expr))

‎src/solvers/flattening/boolbv_get.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -278,7 +278,7 @@ exprt boolbvt::bv_get(const bvt &bv, const typet &type) const
278278

279279
exprt boolbvt::bv_get_cache(const exprt &expr) const
280280
{
281-
if(expr.type().id()==ID_bool) // boolean?
281+
if(expr.is_boolean())
282282
return get(expr);
283283

284284
// look up literals in cache

‎src/solvers/flattening/boolbv_let.cpp

+1-2
Original file line numberDiff line numberDiff line change
@@ -51,11 +51,10 @@ bvt boolbvt::convert_let(const let_exprt &expr)
5151
// Now assign
5252
for(const auto &binding : make_range(fresh_variables).zip(converted_values))
5353
{
54-
bool is_boolean = binding.first.type().id() == ID_bool;
5554
const auto &identifier = binding.first.get_identifier();
5655

5756
// make the symbol visible
58-
if(is_boolean)
57+
if(binding.first.is_boolean())
5958
{
6059
DATA_INVARIANT(binding.second.size() == 1, "boolean values have one bit");
6160
symbols[identifier] = binding.second[0];

‎src/solvers/flattening/bv_pointers.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -121,7 +121,7 @@ bvt bv_pointerst::object_offset_encoding(const bvt &object, const bvt &offset)
121121

122122
literalt bv_pointerst::convert_rest(const exprt &expr)
123123
{
124-
PRECONDITION(expr.type().id() == ID_bool);
124+
PRECONDITION(expr.is_boolean());
125125

126126
const exprt::operandst &operands=expr.operands();
127127

‎src/solvers/floatbv/float_bv.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -73,7 +73,7 @@ exprt float_bvt::convert(const exprt &expr) const
7373
return nil_exprt();
7474
}
7575
else if(
76-
expr.id() == ID_typecast && expr.type().id() == ID_bool &&
76+
expr.id() == ID_typecast && expr.is_boolean() &&
7777
to_typecast_expr(expr).op().type().id() == ID_floatbv) // float -> bool
7878
{
7979
return not_exprt(is_zero(to_typecast_expr(expr).op()));

‎src/solvers/prop/bdd_expr.cpp

+2-3
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,7 @@ Author: Michael Tautschnig, [email protected]
1818

1919
bddt bdd_exprt::from_expr_rec(const exprt &expr)
2020
{
21-
PRECONDITION(expr.type().id() == ID_bool);
21+
PRECONDITION(expr.is_boolean());
2222

2323
if(expr.is_constant())
2424
return expr.is_false() ? bdd_mgr.bdd_false() : bdd_mgr.bdd_true();
@@ -49,8 +49,7 @@ bddt bdd_exprt::from_expr_rec(const exprt &expr)
4949

5050
return n_lhs.bdd_or(rhs);
5151
}
52-
else if(
53-
expr.id() == ID_equal && to_equal_expr(expr).lhs().type().id() == ID_bool)
52+
else if(expr.id() == ID_equal && to_equal_expr(expr).lhs().is_boolean())
5453
{
5554
const equal_exprt &eq_expr=to_equal_expr(expr);
5655

0 commit comments

Comments
 (0)