[ConstraintSolver] Add isConditionImplied helper.

[fhahn]

Summary

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.

[fhahn]

Rebase

[fhahn]

rebase

[spatel]

LGTM

llvm/lib/Analysis/ConstraintSystem.cpp

149

Typo - existing

llvm/unittests/Analysis/ConstraintSystemTest.cpp

83

Typo: Slover -> Solver

[fhahn]

Address comments, rebase, will commit shortly.

llvm/include/llvm/Analysis/ConstraintSystem.h

 //===- ConstraintSystem.h -  A system of linear constraints. --------------===//
 //
 // 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
 //
 //===----------------------------------------------------------------------===//
 
 #ifndef LLVM_ANALYSIS_CONSTRAINTSOLVER_H
 #define LLVM_ANALYSIS_CONSTRAINTSOLVER_H
 
 #include "llvm/ADT/APInt.h"
 #include "llvm/ADT/ArrayRef.h"
 #include "llvm/ADT/SmallVector.h"
 #include <cstdlib>
 #include <string>
 
class ConstraintSystem {
   void dump();
 
   /// Retuns true if there may be a solution for the constraints in the system.
   bool mayHaveSolutionImpl();
 
 public:
   void addVariableRow(const SmallVector<int64_t, 8> &R) {
     assert(Constraints.empty() || R.size() == Constraints.back().size());
     for (auto &C : R) {
       auto A = std::abs(C);
       GCD = APIntOps::GreatestCommonDivisor({32, (uint32_t)A}, {32, GCD})
                 .getZExtValue();
     }
     Constraints.push_back(R);
     NumVariables = (uint32_t)std::max((size_t)NumVariables, R.size());
   }
 
   /// Retuns true if there may be a solution for the constraints in the system.
   bool mayHaveSolution();
+
+  static SmallVector<int64_t, 8> negate(SmallVector<int64_t, 8> R) {
+    // The negated constraint R is obtained by multiplying by -1 and adding 1 to
+    // the constant.
+    R[0] += 1;
+    for (unsigned i = 0; i < R.size(); i++)
+      R[i] *= -1;
+    return R;
+  }
+
+  bool isConditionImplied(SmallVector<int64_t, 8> R);
 };
 } // namespace llvm
 
 #endif

llvm/lib/Analysis/ConstraintSystem.cpp

bool ConstraintSystem::eliminateUsingFM() {
   SmallVector<SmallVector<int64_t, 8>, 4> NewSystem;
 
   uint32_t NewGCD = 1;
   // FIXME do not use copy
   for (unsigned R1 = 0; R1 < Constraints.size(); R1++) {
     if (Constraints[R1][1] == 0) {
       SmallVector<int64_t, 8> NR;
       NR.push_back(Constraints[R1][0]);
       for (unsigned i = 2; i < Constraints[0].size(); i++) {
         NR.push_back(Constraints[R1][i]);
       }
       NewSystem.push_back(std::move(NR));
       continue;
     }
 
     // FIXME do not use copy
     bool EliminatedInRow = false;
for (unsigned R2 = R1 + 1; R2 < Constraints.size(); R2++) {
         continue;
 
       unsigned LowerR = R1;
       unsigned UpperR = R2;
       if (Constraints[UpperR][1] < 0)
         std::swap(LowerR, UpperR);
 
       SmallVector<int64_t, 8> NR;
       for (unsigned i = 0; i < NumVariables; i++) {
         if (i == 1)
           continue;
 
         int64_t M1, M2, N;
         if (__builtin_mul_overflow(Constraints[UpperR][i],
                                    ((-1) * Constraints[LowerR][1] / GCD), &M1))
           return false;
         if (__builtin_mul_overflow(Constraints[LowerR][i],

 }
 
 void ConstraintSystem::dump(ArrayRef<std::string> Names) {
   if (Constraints.empty())
     return;
 
   for (auto &Row : Constraints) {
     SmallVector<std::string, 16> Parts;
     for (unsigned i = 1; i < Row.size(); ++i) {
       if (Row[i] == 0)
         continue;
       std::string Coefficient = "";
       if (Row[i] != 1)
         Coefficient = std::to_string(Row[i]) + " * ";
       Parts.push_back(Coefficient + Names[i - 1]);
     }
     assert(!Parts.empty());
     LLVM_DEBUG(dbgs() << join(Parts, std::string(" + "))
                       << " <= " << std::to_string(Row[0]) << "\n");
   }
 }
 
 void ConstraintSystem::dump() {
   SmallVector<std::string, 16> Names;
   for (unsigned i = 1; i < Constraints.back().size(); ++i)
     Names.push_back("x" + std::to_string(i));
   LLVM_DEBUG(dbgs() << "---\n");
   dump(Names);
 }
 
 bool ConstraintSystem::mayHaveSolution() {
   dump();
   bool HasSolution = mayHaveSolutionImpl();
   LLVM_DEBUG(dbgs() << (HasSolution ? "sat" : "unsat") << "\n");
   return HasSolution;
 }
+
+bool ConstraintSystem::isConditionImplied(SmallVector<int64_t, 8> R) {
+  // If there is no solution with the negation of R added to the system, the
+  // condition must hold based on the exsisting constraints.
+  R = ConstraintSystem::negate(R);
+
+  auto NewSystem = *this;
+  NewSystem.addVariableRow(R);
+  return !NewSystem.mayHaveSolution();
+}

llvm/unittests/Analysis/ConstraintSystemTest.cpp

TEST(ConstraintSloverTest, TestSolutionChecks) {
 
     // 2x + y + 3z <= 10,  2x + y >= 10
     CS.addVariableRow({10, 2, 1, 3});
     CS.addVariableRow({-10, -2, -1, 0});
 
     EXPECT_TRUE(CS.mayHaveSolution());
   }
 }
+
+TEST(ConstraintSloverTest, IsConditionImplied) {
+  {
+    // For the test below, we assume we know
+    // x <= 5 && y <= 3
+    ConstraintSystem CS;
+    CS.addVariableRow({5, 1, 0});
+    CS.addVariableRow({3, 0, 1});
+
+    // x + y <= 6 does not hold.
+    EXPECT_FALSE(CS.isConditionImplied({6, 1, 1}));
+    // x + y <= 7 does not hold.
+    EXPECT_FALSE(CS.isConditionImplied({7, 1, 1}));
+    // x + y <= 8 does hold.
+    EXPECT_TRUE(CS.isConditionImplied({8, 1, 1}));
+
+    // 2 * x + y <= 12 does hold.
+    EXPECT_FALSE(CS.isConditionImplied({12, 2, 1}));
+    // 2 * x + y <= 13 does hold.
+    EXPECT_TRUE(CS.isConditionImplied({13, 2, 1}));
+
+    //  x + y <= 12 does hold.
+    EXPECT_FALSE(CS.isConditionImplied({12, 2, 1}));
+    // 2 * x + y <= 13 does hold.
+    EXPECT_TRUE(CS.isConditionImplied({13, 2, 1}));
+
+    // x <= y == x - y <= 0 does not hold.
+    EXPECT_FALSE(CS.isConditionImplied({0, 1, -1}));
+    // y <= x == -x + y <= 0 does not hold.
+    EXPECT_FALSE(CS.isConditionImplied({0, -1, 1}));
+  }
+
+  {
+    // For the test below, we assume we know
+    // x + 1 <= y + 1 == x - y <= 0
+    ConstraintSystem CS;
+    CS.addVariableRow({0, 1, -1});
+
+    // x <= y == x - y <= 0 does hold.
+    EXPECT_TRUE(CS.isConditionImplied({0, 1, -1}));
+    // y <= x == -x + y <= 0 does not hold.
+    EXPECT_FALSE(CS.isConditionImplied({0, -1, 1}));
+
+    // x <= y + 10 == x - y <= 10 does hold.
+    EXPECT_TRUE(CS.isConditionImplied({10, 1, -1}));
+    // x + 10 <= y == x - y <= -10 does NOT hold.
+    EXPECT_FALSE(CS.isConditionImplied({-10, 1, -1}));
+  }
+
+  {
+    // For the test below, we assume we know
+    // x <= y == x - y <= 0
+    // y <= z == y - x <= 0
+    ConstraintSystem CS;
+    CS.addVariableRow({0, 1, -1, 0});
+    CS.addVariableRow({0, 0, 1, -1});
+
+    // z <= y == -y + z <= 0 does not hold.
+    EXPECT_FALSE(CS.isConditionImplied({0, 0, -1, 1}));
+    // x <= z == x - z <= 0 does hold.
+    EXPECT_TRUE(CS.isConditionImplied({0, 1, 0, -1}));
+  }
+}
+
+TEST(ConstraintSloverTest, IsConditionImpliedOverflow) {
+  ConstraintSystem CS;
+  // Make sure isConditionImplied returns false when there is an overflow.
+  int64_t Limit = std::numeric_limits<int64_t>::max();
+  CS.addVariableRow({Limit - 1, Limit - 2, Limit - 3});
+  EXPECT_FALSE(CS.isConditionImplied({Limit - 1, Limit - 2, Limit - 3}));
+}
 } // namespace