[all-commits] [llvm/llvm-project] 3eb141: [ConstraintSystem] Add helpers to deal with linear...

[Florian Hahn via All-commits]

  Branch: refs/heads/master
  Home:   https://github.com/llvm/llvm-project
  Commit: 3eb141e5078a0ce9d92eadc721bc49d214d23056
      https://github.com/llvm/llvm-project/commit/3eb141e5078a0ce9d92eadc721bc49d214d23056
  Author: Florian Hahn <flo at fhahn.com>
  Date:   2020-09-11 (Fri, 11 Sep 2020)

  Changed paths:
    A llvm/include/llvm/Analysis/ConstraintSystem.h
    M llvm/lib/Analysis/CMakeLists.txt
    A llvm/lib/Analysis/ConstraintSystem.cpp
    M llvm/unittests/Analysis/CMakeLists.txt
    A llvm/unittests/Analysis/ConstraintSystemTest.cpp
    A llvm/utils/convert-constraint-log-to-z3.py

  Log Message:
  -----------
  [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