Commit Graph

4 Commits

Author SHA1 Message Date
Florian Hahn db22e70d01 [ConstraintSolver] Add isConditionImplied helper.
This patch adds a isConditionImplied function that
takes a constraint and returns true if the constraint
is implied by the current constraints in the system.

Reviewed By: spatel

Differential Revision: https://reviews.llvm.org/D84545
2020-09-15 13:50:11 +01:00
Florian Hahn cd4edf94cd Recommit "[ConstraintSystem] Add helpers to deal with linear constraints."
This patch recommits "[ConstraintSystem] Add helpers to deal with linear constraints."
(it reverts the revert commit 8da6ae4ce1).

The reason for the revert was using __builtin_multiply_overflow, which
is not available for all compilers. The patch has been updated to use
MulOverflow from MathExtras.h
2020-09-15 12:07:26 +01:00
Florian Hahn 8da6ae4ce1 Revert "[ConstraintSystem] Add helpers to deal with linear constraints."
This reverts commit 3eb141e507.

This uses __builtin_mul_overflow which is not available everywhere.
2020-09-11 14:49:04 +01:00
Florian Hahn 3eb141e507 [ConstraintSystem] Add helpers to deal with linear constraints.
This patch introduces a new ConstraintSystem class, that maintains a set
of linear constraints and uses Fourier–Motzkin elimination to eliminate
constraints to check if there are solutions for the system.

It also adds a convert-constraint-log-to-z3.py script, which can parse
the debug output of the constraint system and convert it to a python
script that feeds the constraints into Z3 and checks if it produces the
same result as the LLVM implementation. This is for verification
purposes.

Reviewed By: spatel

Differential Revision: https://reviews.llvm.org/D84544
2020-09-11 14:43:22 +01:00