Skip to content

Commit c98aefd

Browse files
author
Daniel Kroening
committed
type simplify_inequality and auxiliary methods
This improves type safety.
1 parent b1e748a commit c98aefd

File tree

4 files changed

+64
-69
lines changed

4 files changed

+64
-69
lines changed

‎src/util/simplify_expr.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2225,7 +2225,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_node(exprt node)
22252225
expr.id()==ID_gt || expr.id()==ID_lt ||
22262226
expr.id()==ID_ge || expr.id()==ID_le)
22272227
{
2228-
r = simplify_inequality(expr);
2228+
r = simplify_inequality(to_binary_relation_expr(expr));
22292229
}
22302230
else if(expr.id()==ID_if)
22312231
{

‎src/util/simplify_expr_class.h

Lines changed: 11 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -154,7 +154,7 @@ class simplify_exprt
154154
NODISCARD resultt<> simplify_bitnot(const bitnot_exprt &);
155155
NODISCARD resultt<> simplify_not(const not_exprt &);
156156
NODISCARD resultt<> simplify_boolean(const exprt &);
157-
NODISCARD resultt<> simplify_inequality(const exprt &);
157+
NODISCARD resultt<> simplify_inequality(const binary_relation_exprt &);
158158
NODISCARD resultt<>
159159
simplify_ieee_float_relation(const binary_relation_exprt &);
160160
NODISCARD resultt<> simplify_lambda(const exprt &);
@@ -203,11 +203,16 @@ class simplify_exprt
203203
static tvt objects_equal(const exprt &a, const exprt &b);
204204
static tvt objects_equal_address_of(const exprt &a, const exprt &b);
205205
NODISCARD resultt<> simplify_address_of_arg(const exprt &);
206-
NODISCARD resultt<> simplify_inequality_both_constant(const exprt &);
207-
NODISCARD resultt<> simplify_inequality_no_constant(const exprt &);
208-
NODISCARD resultt<> simplify_inequality_rhs_is_constant(const exprt &);
209-
NODISCARD resultt<> simplify_inequality_address_of(const exprt &);
210-
NODISCARD resultt<> simplify_inequality_pointer_object(const exprt &);
206+
NODISCARD resultt<>
207+
simplify_inequality_both_constant(const binary_relation_exprt &);
208+
NODISCARD resultt<>
209+
simplify_inequality_no_constant(const binary_relation_exprt &);
210+
NODISCARD resultt<>
211+
simplify_inequality_rhs_is_constant(const binary_relation_exprt &);
212+
NODISCARD resultt<>
213+
simplify_inequality_address_of(const binary_relation_exprt &);
214+
NODISCARD resultt<>
215+
simplify_inequality_pointer_object(const binary_relation_exprt &);
211216

212217
// main recursion
213218
NODISCARD resultt<> simplify_node(exprt);

‎src/util/simplify_expr_int.cpp

Lines changed: 48 additions & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -1201,16 +1201,12 @@ simplify_exprt::simplify_bitnot(const bitnot_exprt &expr)
12011201
}
12021202

12031203
/// simplifies inequalities !=, <=, <, >=, >, and also ==
1204-
simplify_exprt::resultt<> simplify_exprt::simplify_inequality(const exprt &expr)
1204+
simplify_exprt::resultt<>
1205+
simplify_exprt::simplify_inequality(const binary_relation_exprt &expr)
12051206
{
1206-
const exprt::operandst &operands = expr.operands();
1207-
12081207
if(expr.type().id()!=ID_bool)
12091208
return unchanged(expr);
12101209

1211-
if(operands.size()!=2)
1212-
return unchanged(expr);
1213-
12141210
exprt tmp0=expr.op0();
12151211
exprt tmp1=expr.op1();
12161212

@@ -1231,8 +1227,10 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality(const exprt &expr)
12311227
if(tmp0.id()==ID_if && tmp0.operands().size()==3)
12321228
{
12331229
if_exprt if_expr=lift_if(expr, 0);
1234-
if_expr.true_case() = simplify_inequality(if_expr.true_case());
1235-
if_expr.false_case() = simplify_inequality(if_expr.false_case());
1230+
if_expr.true_case() =
1231+
simplify_inequality(to_binary_relation_expr(if_expr.true_case()));
1232+
if_expr.false_case() =
1233+
simplify_inequality(to_binary_relation_expr(if_expr.false_case()));
12361234
return changed(simplify_if(if_expr));
12371235
}
12381236

@@ -1271,7 +1269,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality(const exprt &expr)
12711269
{
12721270
// we want the constant on the RHS
12731271

1274-
exprt new_expr = expr;
1272+
binary_relation_exprt new_expr = expr;
12751273

12761274
if(expr.id()==ID_ge)
12771275
new_expr.id(ID_le);
@@ -1301,11 +1299,9 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality(const exprt &expr)
13011299

13021300
/// simplifies inequalities for the case in which both sides
13031301
/// of the inequality are constants
1304-
simplify_exprt::resultt<>
1305-
simplify_exprt::simplify_inequality_both_constant(const exprt &expr)
1302+
simplify_exprt::resultt<> simplify_exprt::simplify_inequality_both_constant(
1303+
const binary_relation_exprt &expr)
13061304
{
1307-
PRECONDITION(expr.operands().size() == 2);
1308-
13091305
exprt tmp0 = expr.op0();
13101306
exprt tmp1 = expr.op1();
13111307

@@ -1466,8 +1462,8 @@ bool simplify_exprt::eliminate_common_addends(
14661462
return true;
14671463
}
14681464

1469-
simplify_exprt::resultt<>
1470-
simplify_exprt::simplify_inequality_no_constant(const exprt &expr)
1465+
simplify_exprt::resultt<> simplify_exprt::simplify_inequality_no_constant(
1466+
const binary_relation_exprt &expr)
14711467
{
14721468
// pretty much all of the simplifications below are unsound
14731469
// for IEEE float because of NaN!
@@ -1478,35 +1474,34 @@ simplify_exprt::simplify_inequality_no_constant(const exprt &expr)
14781474
// eliminate strict inequalities
14791475
if(expr.id()==ID_notequal)
14801476
{
1481-
auto new_expr = expr;
1482-
new_expr.id(ID_equal);
1483-
new_expr = simplify_inequality_no_constant(new_expr);
1477+
auto new_rel_expr = expr;
1478+
new_rel_expr.id(ID_equal);
1479+
auto new_expr = simplify_inequality_no_constant(new_rel_expr);
14841480
return changed(simplify_not(not_exprt(new_expr)));
14851481
}
14861482
else if(expr.id()==ID_gt)
14871483
{
1488-
auto new_expr = expr;
1489-
new_expr.id(ID_ge);
1484+
auto new_rel_expr = expr;
1485+
new_rel_expr.id(ID_ge);
14901486
// swap operands
1491-
new_expr.op0().swap(new_expr.op1());
1492-
new_expr = simplify_inequality_no_constant(new_expr);
1487+
new_rel_expr.lhs().swap(new_rel_expr.rhs());
1488+
auto new_expr = simplify_inequality_no_constant(new_rel_expr);
14931489
return changed(simplify_not(not_exprt(new_expr)));
14941490
}
14951491
else if(expr.id()==ID_lt)
14961492
{
1497-
auto new_expr = expr;
1498-
new_expr.id(ID_ge);
1499-
new_expr = simplify_inequality_no_constant(new_expr);
1493+
auto new_rel_expr = expr;
1494+
new_rel_expr.id(ID_ge);
1495+
auto new_expr = simplify_inequality_no_constant(new_rel_expr);
15001496
return changed(simplify_not(not_exprt(new_expr)));
15011497
}
15021498
else if(expr.id()==ID_le)
15031499
{
1504-
auto new_expr = expr;
1505-
new_expr.id(ID_ge);
1500+
auto new_rel_expr = expr;
1501+
new_rel_expr.id(ID_ge);
15061502
// swap operands
1507-
new_expr.op0().swap(new_expr.op1());
1508-
new_expr = simplify_inequality_no_constant(new_expr);
1509-
return std::move(new_expr);
1503+
new_rel_expr.lhs().swap(new_rel_expr.rhs());
1504+
return changed(simplify_inequality_no_constant(new_rel_expr));
15101505
}
15111506

15121507
// now we only have >=, =
@@ -1574,12 +1569,12 @@ simplify_exprt::simplify_inequality_no_constant(const exprt &expr)
15741569
// On bit-vectors, this is only sound on '='.
15751570
if(expr.id()==ID_equal)
15761571
{
1577-
auto new_expr = expr;
1578-
if(!eliminate_common_addends(new_expr.op0(), new_expr.op1()))
1572+
auto new_expr = to_equal_expr(expr);
1573+
if(!eliminate_common_addends(new_expr.lhs(), new_expr.rhs()))
15791574
{
15801575
// remove zeros
1581-
new_expr.op0() = simplify_node(new_expr.op0());
1582-
new_expr.op1() = simplify_node(new_expr.op1());
1576+
new_expr.lhs() = simplify_node(new_expr.lhs());
1577+
new_expr.rhs() = simplify_node(new_expr.rhs());
15831578
return changed(simplify_inequality(new_expr)); // recursive call
15841579
}
15851580
}
@@ -1589,19 +1584,19 @@ simplify_exprt::simplify_inequality_no_constant(const exprt &expr)
15891584

15901585
/// \par expr: an inequality where the RHS is a constant
15911586
/// and the LHS is not
1592-
simplify_exprt::resultt<>
1593-
simplify_exprt::simplify_inequality_rhs_is_constant(const exprt &expr)
1587+
simplify_exprt::resultt<> simplify_exprt::simplify_inequality_rhs_is_constant(
1588+
const binary_relation_exprt &expr)
15941589
{
15951590
// the constant is always on the RHS
15961591
PRECONDITION(expr.op1().is_constant());
15971592

15981593
if(expr.op0().id()==ID_if && expr.op0().operands().size()==3)
15991594
{
16001595
if_exprt if_expr=lift_if(expr, 0);
1601-
if_expr.true_case() =
1602-
simplify_inequality_rhs_is_constant(if_expr.true_case());
1603-
if_expr.false_case() =
1604-
simplify_inequality_rhs_is_constant(if_expr.false_case());
1596+
if_expr.true_case() = simplify_inequality_rhs_is_constant(
1597+
to_binary_relation_expr(if_expr.true_case()));
1598+
if_expr.false_case() = simplify_inequality_rhs_is_constant(
1599+
to_binary_relation_expr(if_expr.false_case()));
16051600
return changed(simplify_if(if_expr));
16061601
}
16071602

@@ -1610,9 +1605,9 @@ simplify_exprt::simplify_inequality_rhs_is_constant(const exprt &expr)
16101605
{
16111606
if(expr.id()==ID_notequal)
16121607
{
1613-
auto new_expr = expr;
1614-
new_expr.id(ID_equal);
1615-
new_expr = simplify_inequality_rhs_is_constant(new_expr);
1608+
auto new_rel_expr = expr;
1609+
new_rel_expr.id(ID_equal);
1610+
auto new_expr = simplify_inequality_rhs_is_constant(new_rel_expr);
16161611
return changed(simplify_not(not_exprt(new_expr)));
16171612
}
16181613

@@ -1822,9 +1817,9 @@ simplify_exprt::simplify_inequality_rhs_is_constant(const exprt &expr)
18221817

18231818
if(expr.id()==ID_notequal)
18241819
{
1825-
auto new_expr = expr;
1826-
new_expr.id(ID_equal);
1827-
new_expr = simplify_inequality_rhs_is_constant(new_expr);
1820+
auto new_rel_expr = expr;
1821+
new_rel_expr.id(ID_equal);
1822+
auto new_expr = simplify_inequality_rhs_is_constant(new_rel_expr);
18281823
return changed(simplify_not(not_exprt(new_expr)));
18291824
}
18301825
else if(expr.id()==ID_gt)
@@ -1844,9 +1839,9 @@ simplify_exprt::simplify_inequality_rhs_is_constant(const exprt &expr)
18441839
}
18451840
else if(expr.id()==ID_lt)
18461841
{
1847-
auto new_expr = expr;
1848-
new_expr.id(ID_ge);
1849-
new_expr = simplify_inequality_rhs_is_constant(new_expr);
1842+
auto new_rel_expr = expr;
1843+
new_rel_expr.id(ID_ge);
1844+
auto new_expr = simplify_inequality_rhs_is_constant(new_rel_expr);
18501845
return changed(simplify_not(not_exprt(new_expr)));
18511846
}
18521847
else if(expr.id()==ID_le)
@@ -1858,11 +1853,11 @@ simplify_exprt::simplify_inequality_rhs_is_constant(const exprt &expr)
18581853
return true_exprt();
18591854
}
18601855

1861-
auto new_expr = expr;
1862-
new_expr.id(ID_ge);
1856+
auto new_rel_expr = expr;
1857+
new_rel_expr.id(ID_ge);
18631858
++i;
1864-
new_expr.op1() = from_integer(i, new_expr.op1().type());
1865-
new_expr = simplify_inequality_rhs_is_constant(new_expr);
1859+
new_rel_expr.op1() = from_integer(i, new_rel_expr.op1().type());
1860+
auto new_expr = simplify_inequality_rhs_is_constant(new_rel_expr);
18661861
return changed(simplify_not(not_exprt(new_expr)));
18671862
}
18681863
}

‎src/util/simplify_expr_pointer.cpp

Lines changed: 4 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -418,13 +418,10 @@ simplify_exprt::simplify_pointer_offset(const unary_exprt &expr)
418418
return unchanged(expr);
419419
}
420420

421-
simplify_exprt::resultt<>
422-
simplify_exprt::simplify_inequality_address_of(const exprt &expr)
421+
simplify_exprt::resultt<> simplify_exprt::simplify_inequality_address_of(
422+
const binary_relation_exprt &expr)
423423
{
424424
PRECONDITION(expr.id() == ID_equal || expr.id() == ID_notequal);
425-
PRECONDITION(expr.type().id() == ID_bool);
426-
DATA_INVARIANT(
427-
expr.operands().size() == 2, "(in)equalities have two operands");
428425

429426
exprt tmp0=expr.op0();
430427
if(tmp0.id()==ID_typecast)
@@ -473,13 +470,11 @@ simplify_exprt::simplify_inequality_address_of(const exprt &expr)
473470
return unchanged(expr);
474471
}
475472

476-
simplify_exprt::resultt<>
477-
simplify_exprt::simplify_inequality_pointer_object(const exprt &expr)
473+
simplify_exprt::resultt<> simplify_exprt::simplify_inequality_pointer_object(
474+
const binary_relation_exprt &expr)
478475
{
479476
PRECONDITION(expr.id() == ID_equal || expr.id() == ID_notequal);
480477
PRECONDITION(expr.type().id() == ID_bool);
481-
DATA_INVARIANT(
482-
expr.operands().size() == 2, "(in)equalities have two operands");
483478

484479
exprt::operandst new_inequality_ops;
485480
forall_operands(it, expr)

0 commit comments

Comments
 (0)