3eb141e507
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
83 lines
2.0 KiB
C++
83 lines
2.0 KiB
C++
//===--- ConstraintSystemTests.cpp ----------------------------------------===//
|
|
//
|
|
// Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
|
|
// See https://llvm.org/LICENSE.txt for license information.
|
|
// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
|
|
//
|
|
//===----------------------------------------------------------------------===//
|
|
|
|
#include "llvm/Analysis/ConstraintSystem.h"
|
|
#include "gtest/gtest.h"
|
|
|
|
using namespace llvm;
|
|
|
|
namespace {
|
|
|
|
TEST(ConstraintSloverTest, TestSolutionChecks) {
|
|
{
|
|
ConstraintSystem CS;
|
|
// x + y <= 10, x >= 5, y >= 6, x <= 10, y <= 10
|
|
CS.addVariableRow({10, 1, 1});
|
|
CS.addVariableRow({-5, -1, 0});
|
|
CS.addVariableRow({-6, 0, -1});
|
|
CS.addVariableRow({10, 1, 0});
|
|
CS.addVariableRow({10, 0, 1});
|
|
|
|
EXPECT_FALSE(CS.mayHaveSolution());
|
|
}
|
|
|
|
{
|
|
ConstraintSystem CS;
|
|
// x + y <= 10, x >= 2, y >= 3, x <= 10, y <= 10
|
|
CS.addVariableRow({10, 1, 1});
|
|
CS.addVariableRow({-2, -1, 0});
|
|
CS.addVariableRow({-3, 0, -1});
|
|
CS.addVariableRow({10, 1, 0});
|
|
CS.addVariableRow({10, 0, 1});
|
|
|
|
EXPECT_TRUE(CS.mayHaveSolution());
|
|
}
|
|
|
|
{
|
|
ConstraintSystem CS;
|
|
// x + y <= 10, 10 >= x, 10 >= y; does not have a solution.
|
|
CS.addVariableRow({10, 1, 1});
|
|
CS.addVariableRow({-10, -1, 0});
|
|
CS.addVariableRow({-10, 0, -1});
|
|
|
|
EXPECT_FALSE(CS.mayHaveSolution());
|
|
}
|
|
|
|
{
|
|
ConstraintSystem CS;
|
|
// x + y >= 20, 10 >= x, 10 >= y; does HAVE a solution.
|
|
CS.addVariableRow({-20, -1, -1});
|
|
CS.addVariableRow({-10, -1, 0});
|
|
CS.addVariableRow({-10, 0, -1});
|
|
|
|
EXPECT_TRUE(CS.mayHaveSolution());
|
|
}
|
|
|
|
{
|
|
ConstraintSystem CS;
|
|
|
|
// 2x + y + 3z <= 10, 2x + y >= 10, y >= 1
|
|
CS.addVariableRow({10, 2, 1, 3});
|
|
CS.addVariableRow({-10, -2, -1, 0});
|
|
CS.addVariableRow({-1, 0, 0, -1});
|
|
|
|
EXPECT_FALSE(CS.mayHaveSolution());
|
|
}
|
|
|
|
{
|
|
ConstraintSystem CS;
|
|
|
|
// 2x + y + 3z <= 10, 2x + y >= 10
|
|
CS.addVariableRow({10, 2, 1, 3});
|
|
CS.addVariableRow({-10, -2, -1, 0});
|
|
|
|
EXPECT_TRUE(CS.mayHaveSolution());
|
|
}
|
|
}
|
|
} // namespace
|