llvm-project

Commit Graph

Author	SHA1	Message	Date
Florian Hahn	0bcfd4cbac	[ConstraintElimination] Rewrite tests to reduce verification complexity. This patch reduces the bitwidth of types certain tests operate and gets rid of a number of @use(i1) calls and xor's the conditions together instead, which eliminates all timeouts when verifying the tests. See https://github.com/AliveToolkit/alive2/issues/744 for more details.	2021-08-26 16:41:40 +01:00
Florian Hahn	ca268ed285	[ConstraintElimination] Decompose zext for unsigned compares. For unsigned compares, zext should be a no-op and we can add the extended value to the constraint system.	2021-02-07 20:53:06 +00:00
Florian Hahn	a14a59f2f2	[ConstraintElimination] Add additional tests. Adds additional test cases with zexts, conditions that require temporary indices.	2021-02-07 18:00:17 +00:00

Author

SHA1

Message

Date

Florian Hahn

0bcfd4cbac

[ConstraintElimination] Rewrite tests to reduce verification complexity.

This patch reduces the bitwidth of types certain tests operate and gets
rid of a number of @use(i1) calls and xor's the conditions together
instead, which eliminates all timeouts when verifying the tests.
See https://github.com/AliveToolkit/alive2/issues/744 for more details.

2021-08-26 16:41:40 +01:00

Florian Hahn

ca268ed285

[ConstraintElimination] Decompose zext for unsigned compares.

For unsigned compares, zext should be a no-op and we can add the
extended value to the constraint system.

2021-02-07 20:53:06 +00:00

Florian Hahn

a14a59f2f2

[ConstraintElimination] Add additional tests.

Adds additional test cases with zexts, conditions that require temporary
indices.

2021-02-07 18:00:17 +00:00

3 Commits