Skip to content

Commit b0e022b

Browse files
author
Daniel Kroening
committed
type simplify_inequality and auxiliary methods
This improves type safety.
1 parent 7ef8430 commit b0e022b

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,38 +1474,37 @@ 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
new_expr = boolean_negate(new_expr);
14851481
return changed(simplify_node(new_expr));
14861482
}
14871483
else if(expr.id()==ID_gt)
14881484
{
1489-
auto new_expr = expr;
1490-
new_expr.id(ID_ge);
1485+
auto new_rel_expr = expr;
1486+
new_rel_expr.id(ID_ge);
14911487
// swap operands
1492-
new_expr.op0().swap(new_expr.op1());
1493-
new_expr = simplify_inequality_no_constant(new_expr);
1488+
new_rel_expr.lhs().swap(new_rel_expr.rhs());
1489+
auto new_expr = simplify_inequality_no_constant(new_rel_expr);
14941490
new_expr = boolean_negate(new_expr);
14951491
return changed(simplify_node(new_expr));
14961492
}
14971493
else if(expr.id()==ID_lt)
14981494
{
1499-
auto new_expr = expr;
1500-
new_expr.id(ID_ge);
1501-
new_expr = simplify_inequality_no_constant(new_expr);
1495+
auto new_rel_expr = expr;
1496+
new_rel_expr.id(ID_ge);
1497+
auto new_expr = simplify_inequality_no_constant(new_rel_expr);
15021498
new_expr = boolean_negate(new_expr);
15031499
return changed(simplify_node(new_expr));
15041500
}
15051501
else if(expr.id()==ID_le)
15061502
{
1507-
auto new_expr = expr;
1508-
new_expr.id(ID_ge);
1503+
auto new_rel_expr = expr;
1504+
new_rel_expr.id(ID_ge);
15091505
// swap operands
1510-
new_expr.op0().swap(new_expr.op1());
1511-
new_expr = simplify_inequality_no_constant(new_expr);
1512-
return std::move(new_expr);
1506+
new_rel_expr.lhs().swap(new_rel_expr.rhs());
1507+
return changed(simplify_inequality_no_constant(new_rel_expr));
15131508
}
15141509

15151510
// now we only have >=, =
@@ -1577,12 +1572,12 @@ simplify_exprt::simplify_inequality_no_constant(const exprt &expr)
15771572
// On bit-vectors, this is only sound on '='.
15781573
if(expr.id()==ID_equal)
15791574
{
1580-
auto new_expr = expr;
1581-
if(!eliminate_common_addends(new_expr.op0(), new_expr.op1()))
1575+
auto new_expr = to_equal_expr(expr);
1576+
if(!eliminate_common_addends(new_expr.lhs(), new_expr.rhs()))
15821577
{
15831578
// remove zeros
1584-
new_expr.op0() = simplify_node(new_expr.op0());
1585-
new_expr.op1() = simplify_node(new_expr.op1());
1579+
new_expr.lhs() = simplify_node(new_expr.lhs());
1580+
new_expr.rhs() = simplify_node(new_expr.rhs());
15861581
return changed(simplify_inequality(new_expr)); // recursive call
15871582
}
15881583
}
@@ -1592,19 +1587,19 @@ simplify_exprt::simplify_inequality_no_constant(const exprt &expr)
15921587

15931588
/// \par expr: an inequality where the RHS is a constant
15941589
/// and the LHS is not
1595-
simplify_exprt::resultt<>
1596-
simplify_exprt::simplify_inequality_rhs_is_constant(const exprt &expr)
1590+
simplify_exprt::resultt<> simplify_exprt::simplify_inequality_rhs_is_constant(
1591+
const binary_relation_exprt &expr)
15971592
{
15981593
// the constant is always on the RHS
15991594
PRECONDITION(expr.op1().is_constant());
16001595

16011596
if(expr.op0().id()==ID_if && expr.op0().operands().size()==3)
16021597
{
16031598
if_exprt if_expr=lift_if(expr, 0);
1604-
if_expr.true_case() =
1605-
simplify_inequality_rhs_is_constant(if_expr.true_case());
1606-
if_expr.false_case() =
1607-
simplify_inequality_rhs_is_constant(if_expr.false_case());
1599+
if_expr.true_case() = simplify_inequality_rhs_is_constant(
1600+
to_binary_relation_expr(if_expr.true_case()));
1601+
if_expr.false_case() = simplify_inequality_rhs_is_constant(
1602+
to_binary_relation_expr(if_expr.false_case()));
16081603
return changed(simplify_if(if_expr));
16091604
}
16101605

@@ -1613,9 +1608,9 @@ simplify_exprt::simplify_inequality_rhs_is_constant(const exprt &expr)
16131608
{
16141609
if(expr.id()==ID_notequal)
16151610
{
1616-
auto new_expr = expr;
1617-
new_expr.id(ID_equal);
1618-
new_expr = simplify_inequality_rhs_is_constant(new_expr);
1611+
auto new_rel_expr = expr;
1612+
new_rel_expr.id(ID_equal);
1613+
auto new_expr = simplify_inequality_rhs_is_constant(new_rel_expr);
16191614
new_expr = boolean_negate(new_expr);
16201615
return changed(simplify_node(new_expr));
16211616
}
@@ -1826,9 +1821,9 @@ simplify_exprt::simplify_inequality_rhs_is_constant(const exprt &expr)
18261821

18271822
if(expr.id()==ID_notequal)
18281823
{
1829-
auto new_expr = expr;
1830-
new_expr.id(ID_equal);
1831-
new_expr = simplify_inequality_rhs_is_constant(new_expr);
1824+
auto new_rel_expr = expr;
1825+
new_rel_expr.id(ID_equal);
1826+
auto new_expr = simplify_inequality_rhs_is_constant(new_rel_expr);
18321827
new_expr = boolean_negate(new_expr);
18331828
return changed(simplify_node(new_expr));
18341829
}
@@ -1849,9 +1844,9 @@ simplify_exprt::simplify_inequality_rhs_is_constant(const exprt &expr)
18491844
}
18501845
else if(expr.id()==ID_lt)
18511846
{
1852-
auto new_expr = expr;
1853-
new_expr.id(ID_ge);
1854-
new_expr = simplify_inequality_rhs_is_constant(new_expr);
1847+
auto new_rel_expr = expr;
1848+
new_rel_expr.id(ID_ge);
1849+
auto new_expr = simplify_inequality_rhs_is_constant(new_rel_expr);
18551850
new_expr = boolean_negate(new_expr);
18561851
return changed(simplify_node(new_expr));
18571852
}
@@ -1864,11 +1859,11 @@ simplify_exprt::simplify_inequality_rhs_is_constant(const exprt &expr)
18641859
return true_exprt();
18651860
}
18661861

1867-
auto new_expr = expr;
1868-
new_expr.id(ID_ge);
1862+
auto new_rel_expr = expr;
1863+
new_rel_expr.id(ID_ge);
18691864
++i;
1870-
new_expr.op1() = from_integer(i, new_expr.op1().type());
1871-
new_expr = simplify_inequality_rhs_is_constant(new_expr);
1865+
new_rel_expr.rhs() = from_integer(i, new_rel_expr.rhs().type());
1866+
auto new_expr = simplify_inequality_rhs_is_constant(new_rel_expr);
18721867
new_expr = boolean_negate(new_expr);
18731868
return changed(simplify_node(new_expr));
18741869
}

‎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)