Skip to content

Commit ba0d94c

Browse files
committed
Reduce variable equivalences unnecessarily generated by set_literals
There is no need to call set_literals for `A == A`, and if we end up in set_literals via another code path we can still avoid generating the trivially-true equality of `l == l`.
1 parent ffa00d7 commit ba0d94c

File tree

2 files changed

+10
-4
lines changed

2 files changed

+10
-4
lines changed

src/solvers/flattening/boolbv.cpp

Lines changed: 5 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -489,10 +489,12 @@ bool boolbvt::boolbv_set_equality_to_true(const equal_exprt &expr)
489489

490490
const bvt &bv1=convert_bv(expr.rhs());
491491

492-
const irep_idt &identifier=
493-
to_symbol_expr(expr.lhs()).get_identifier();
492+
if(expr.rhs() != expr.lhs())
493+
{
494+
const irep_idt &identifier = to_symbol_expr(expr.lhs()).get_identifier();
494495

495-
map.set_literals(identifier, type, bv1);
496+
map.set_literals(identifier, type, bv1);
497+
}
496498

497499
if(freeze_all)
498500
set_frozen(bv1);

src/solvers/flattening/boolbv_map.cpp

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -110,7 +110,11 @@ void boolbv_mapt::set_literals(
110110
INVARIANT(
111111
bit < map_entry.literal_map.size(), "bit index shall be within bounds");
112112

113-
prop.set_equal(map_entry.literal_map[bit], literal);
113+
if(map_entry.literal_map[bit] != literal)
114+
{
115+
// this branch should be avoided wherever possible
116+
prop.set_equal(map_entry.literal_map[bit], literal);
117+
}
114118
}
115119
}
116120
}

0 commit comments

Comments
 (0)