4 Commits

Author SHA1 Message Date
Florian Hahn
9d31d1c214
[ConstraintElimination] Use logic from 3771310eed for queries only.
The logic added in 3771310eed was placed sub-optimally. Applying the
transform in ::getConstraint meant that it would also impact conditions
that are added to the system by the signed <-> unsigned transfer logic.

This meant we failed to add some signed facts to the signed system. To
make sure we still add as many useful facts to the signed/unsigned
systems, move the logic to the point where we query the system.
2022-10-08 11:03:45 +01:00
Florian Hahn
d227029ce4
[ConstraintElimination] Add test for regression after 3771310eede. 2022-10-07 20:42:16 +01:00
Florian Hahn
3771310eed
[ConstraintElimination] Convert to unsigned Pred if possible.
Convert SLE/SLT predicates to unsigned equivalents if both operands are
known to be signed-positive.

https://alive2.llvm.org/ce/z/tBeiZr
2022-10-07 12:27:36 +01:00
Florian Hahn
5b70db8f00
[ConstraintElimination] Add tests where unsigned system can be queried.
Add tests with a mix of signed and unsigned predicates. In some cases,
the unsigned system can be queried for signed predicates to improve
results.
2022-10-06 22:11:51 +01:00