Skip to content

Commit 525c23d

Browse files
tautschnigtautschnig
committed
Incremental SMT2 back-end: simplify encoded expressions
This is in preparation of moving to 3-operand with-expressions: without intervening use of the simplifier some generated expressions could become unnecessarily large.
1 parent e88ed5f commit 525c23d

File tree

3 files changed

+94
-43
lines changed

3 files changed

+94
-43
lines changed

‎src/util/simplify_expr.cpp

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1339,6 +1339,19 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
13391339
return changed(simplify_address_of(result)); // recursive call
13401340
}
13411341
}
1342+
else if(auto extractbits = expr_try_dynamic_cast<extractbits_exprt>(operand))
1343+
{
1344+
if(
1345+
can_cast_type<bitvector_typet>(expr_type) &&
1346+
can_cast_type<bitvector_typet>(operand.type()) &&
1347+
to_bitvector_type(expr_type).get_width() ==
1348+
to_bitvector_type(operand.type()).get_width())
1349+
{
1350+
extractbits_exprt result = *extractbits;
1351+
result.type() = expr_type;
1352+
return changed(simplify_extractbits(result));
1353+
}
1354+
}
13421355

13431356
return unchanged(expr);
13441357
}

‎src/util/simplify_expr_int.cpp

Lines changed: 8 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -992,10 +992,15 @@ simplify_exprt::simplify_concatenation(const concatenation_exprt &expr)
992992
}
993993

994994
// { x } = x
995-
if(
996-
new_expr.operands().size() == 1 && new_expr.op0().type() == new_expr.type())
995+
if(new_expr.operands().size() == 1)
997996
{
998-
return new_expr.op0();
997+
if(new_expr.op0().type() == new_expr.type())
998+
return new_expr.op0();
999+
else
1000+
{
1001+
return changed(
1002+
simplify_typecast(typecast_exprt{new_expr.op0(), new_expr.type()}));
1003+
}
9991004
}
10001005

10011006
if(no_change)

‎unit/solvers/smt2_incremental/encoding/struct_encoding.cpp

Lines changed: 73 additions & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@
66
#include <util/c_types.h>
77
#include <util/mathematical_types.h>
88
#include <util/namespace.h>
9+
#include <util/simplify_expr.h>
910
#include <util/symbol_table.h>
1011

1112
#include <solvers/smt2_incremental/encoding/nondet_padding.h>
@@ -242,12 +243,16 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]")
242243
symbol_expr,
243244
make_member_name_expression("green"),
244245
from_integer(0, signedbv_typet{32})};
245-
const concatenation_exprt expected{
246-
{from_integer(0, signedbv_typet{32}),
247-
extractbits_exprt{symbol_expr_as_bv, 24, unsignedbv_typet{16}},
248-
extractbits_exprt{symbol_expr_as_bv, 0, signedbv_typet{24}}},
249-
bv_typet{72}};
250-
REQUIRE(test.struct_encoding.encode(with) == expected);
246+
const exprt expected = simplify_expr(
247+
concatenation_exprt{
248+
{from_integer(0, signedbv_typet{32}),
249+
extractbits_exprt{symbol_expr_as_bv, 24, unsignedbv_typet{16}},
250+
extractbits_exprt{symbol_expr_as_bv, 0, signedbv_typet{24}}},
251+
bv_typet{72}},
252+
test.ns);
253+
const exprt encoded =
254+
simplify_expr(test.struct_encoding.encode(with), test.ns);
255+
REQUIRE(encoded == expected);
251256
}
252257
SECTION("Second member")
253258
{
@@ -268,20 +273,26 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]")
268273
symbol_expr,
269274
make_member_name_expression("ham"),
270275
from_integer(0, signedbv_typet{24})};
271-
const concatenation_exprt expected{
272-
{extractbits_exprt{symbol_expr_as_bv, 40, signedbv_typet{32}},
273-
extractbits_exprt{symbol_expr_as_bv, 24, unsignedbv_typet{16}},
274-
from_integer(0, signedbv_typet{24})},
275-
bv_typet{72}};
276-
REQUIRE(test.struct_encoding.encode(with) == expected);
276+
const exprt expected = simplify_expr(
277+
concatenation_exprt{
278+
{extractbits_exprt{symbol_expr_as_bv, 40, signedbv_typet{32}},
279+
extractbits_exprt{symbol_expr_as_bv, 24, unsignedbv_typet{16}},
280+
from_integer(0, signedbv_typet{24})},
281+
bv_typet{72}},
282+
test.ns);
283+
const exprt encoded =
284+
simplify_expr(test.struct_encoding.encode(with), test.ns);
285+
REQUIRE(encoded == expected);
277286
}
278287
SECTION("First and second members")
279288
{
280-
const concatenation_exprt expected{
281-
{from_integer(0, signedbv_typet{32}),
282-
from_integer(1, unsignedbv_typet{16}),
283-
extractbits_exprt{symbol_expr_as_bv, 0, signedbv_typet{24}}},
284-
bv_typet{72}};
289+
const exprt expected = simplify_expr(
290+
concatenation_exprt{
291+
{from_integer(0, signedbv_typet{32}),
292+
from_integer(1, unsignedbv_typet{16}),
293+
extractbits_exprt{symbol_expr_as_bv, 0, signedbv_typet{24}}},
294+
bv_typet{72}},
295+
test.ns);
285296
SECTION("Operands in field order")
286297
{
287298
with_exprt with_in_order{
@@ -291,7 +302,9 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]")
291302
with_in_order.operands().push_back(make_member_name_expression("eggs"));
292303
with_in_order.operands().push_back(
293304
from_integer(1, unsignedbv_typet{16}));
294-
REQUIRE(test.struct_encoding.encode(with_in_order) == expected);
305+
const exprt encoded =
306+
simplify_expr(test.struct_encoding.encode(with_in_order), test.ns);
307+
REQUIRE(encoded == expected);
295308
}
296309
SECTION("Operands in reverse order vs fields")
297310
{
@@ -302,16 +315,20 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]")
302315
with_reversed.operands().push_back(
303316
make_member_name_expression("green"));
304317
with_reversed.operands().push_back(from_integer(0, signedbv_typet{32}));
305-
REQUIRE(test.struct_encoding.encode(with_reversed) == expected);
318+
const exprt encoded =
319+
simplify_expr(test.struct_encoding.encode(with_reversed), test.ns);
320+
REQUIRE(encoded == expected);
306321
}
307322
}
308323
SECTION("First and third members")
309324
{
310-
const concatenation_exprt expected{
311-
{from_integer(0, signedbv_typet{32}),
312-
extractbits_exprt{symbol_expr_as_bv, 24, unsignedbv_typet{16}},
313-
from_integer(1, signedbv_typet{24})},
314-
bv_typet{72}};
325+
const exprt expected = simplify_expr(
326+
concatenation_exprt{
327+
{from_integer(0, signedbv_typet{32}),
328+
extractbits_exprt{symbol_expr_as_bv, 24, unsignedbv_typet{16}},
329+
from_integer(1, signedbv_typet{24})},
330+
bv_typet{72}},
331+
test.ns);
315332
SECTION("Operands in field order")
316333
{
317334
with_exprt with_in_order{
@@ -320,7 +337,9 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]")
320337
from_integer(0, signedbv_typet{32})};
321338
with_in_order.operands().push_back(make_member_name_expression("ham"));
322339
with_in_order.operands().push_back(from_integer(1, signedbv_typet{24}));
323-
REQUIRE(test.struct_encoding.encode(with_in_order) == expected);
340+
const exprt encoded =
341+
simplify_expr(test.struct_encoding.encode(with_in_order), test.ns);
342+
REQUIRE(encoded == expected);
324343
}
325344
SECTION("Operands in reverse order vs fields")
326345
{
@@ -331,16 +350,20 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]")
331350
with_reversed.operands().push_back(
332351
make_member_name_expression("green"));
333352
with_reversed.operands().push_back(from_integer(0, signedbv_typet{32}));
334-
REQUIRE(test.struct_encoding.encode(with_reversed) == expected);
353+
const exprt encoded =
354+
simplify_expr(test.struct_encoding.encode(with_reversed), test.ns);
355+
REQUIRE(encoded == expected);
335356
}
336357
}
337358
SECTION("Second and third members")
338359
{
339-
const concatenation_exprt expected{
340-
{extractbits_exprt{symbol_expr_as_bv, 40, signedbv_typet{32}},
341-
from_integer(0, unsignedbv_typet{16}),
342-
from_integer(1, signedbv_typet{24})},
343-
bv_typet{72}};
360+
const exprt expected = simplify_expr(
361+
concatenation_exprt{
362+
{extractbits_exprt{symbol_expr_as_bv, 40, signedbv_typet{32}},
363+
from_integer(0, unsignedbv_typet{16}),
364+
from_integer(1, signedbv_typet{24})},
365+
bv_typet{72}},
366+
test.ns);
344367
SECTION("Operands in field order")
345368
{
346369
with_exprt with_in_order{
@@ -349,7 +372,9 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]")
349372
from_integer(0, unsignedbv_typet{16})};
350373
with_in_order.operands().push_back(make_member_name_expression("ham"));
351374
with_in_order.operands().push_back(from_integer(1, signedbv_typet{24}));
352-
REQUIRE(test.struct_encoding.encode(with_in_order) == expected);
375+
const exprt encoded =
376+
simplify_expr(test.struct_encoding.encode(with_in_order), test.ns);
377+
REQUIRE(encoded == expected);
353378
}
354379
SECTION("Operands in reverse order vs fields")
355380
{
@@ -360,16 +385,20 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]")
360385
with_reversed.operands().push_back(make_member_name_expression("eggs"));
361386
with_reversed.operands().push_back(
362387
from_integer(0, unsignedbv_typet{16}));
363-
REQUIRE(test.struct_encoding.encode(with_reversed) == expected);
388+
const exprt encoded =
389+
simplify_expr(test.struct_encoding.encode(with_reversed), test.ns);
390+
REQUIRE(encoded == expected);
364391
}
365392
}
366393
SECTION("All members")
367394
{
368-
const concatenation_exprt expected{
369-
{from_integer(1, signedbv_typet{32}),
370-
from_integer(2, unsignedbv_typet{16}),
371-
from_integer(3, signedbv_typet{24})},
372-
bv_typet{72}};
395+
const exprt expected = simplify_expr(
396+
concatenation_exprt{
397+
{from_integer(1, signedbv_typet{32}),
398+
from_integer(2, unsignedbv_typet{16}),
399+
from_integer(3, signedbv_typet{24})},
400+
bv_typet{72}},
401+
test.ns);
373402
SECTION("Operands in field order")
374403
{
375404
with_exprt with{
@@ -380,7 +409,9 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]")
380409
with.operands().push_back(from_integer(2, unsignedbv_typet{16}));
381410
with.operands().push_back(make_member_name_expression("ham"));
382411
with.operands().push_back(from_integer(3, signedbv_typet{24}));
383-
REQUIRE(test.struct_encoding.encode(with) == expected);
412+
const exprt encoded =
413+
simplify_expr(test.struct_encoding.encode(with), test.ns);
414+
REQUIRE(encoded == expected);
384415
}
385416
SECTION("Operands out of order vs fields")
386417
{
@@ -392,7 +423,9 @@ TEST_CASE("struct encoding of expressions", "[core][smt2_incremental]")
392423
with.operands().push_back(from_integer(3, signedbv_typet{24}));
393424
with.operands().push_back(make_member_name_expression("green"));
394425
with.operands().push_back(from_integer(1, signedbv_typet{32}));
395-
REQUIRE(test.struct_encoding.encode(with) == expected);
426+
const exprt encoded =
427+
simplify_expr(test.struct_encoding.encode(with), test.ns);
428+
REQUIRE(encoded == expected);
396429
}
397430
}
398431
}

0 commit comments

Comments
 (0)