[llvm] [ConstraintSys] Solve sub-system with variables needed for query (NFC) (PR #210432)

Nikita Popov via llvm-commits llvm-commits at lists.llvm.org
Sat Jul 18 07:45:53 PDT 2026


================
@@ -221,6 +227,67 @@ bool ConstraintSystem::mayHaveSolution() {
   return HasSolution;
 }
 
+std::pair<ConstraintSystem, SmallVector<int64_t, 8>>
+ConstraintSystem::getSubSystem(ArrayRef<int64_t> R) const {
+  // Only constraints that share a variable (transitively) with a query R can
+  // affect whether system + !R has a solution.
+  //
+  // Mark variables in the query and collect to the transitive closure over
+  // variables that co-occur in a constraint row.
+  ConstraintSystem SubSystem;
+  SmallBitVector InSystem(NumVariables + 1, false);
+  for (unsigned Id = 1, E = R.size(); Id < E; ++Id)
+    if (R[Id] != 0)
+      InSystem[Id] = true;
+  bool Changed = true;
+  while (Changed) {
+    Changed = false;
+    for (const auto &Row : Constraints) {
+      // No common variables, skip.
+      if (none_of(Row,
+                  [&](const Entry &E) { return E.Id != 0 && InSystem[E.Id]; }))
+        continue;
+      for (const Entry &E : Row)
+        if (E.Id != 0 && !InSystem[E.Id]) {
+          InSystem[E.Id] = true;
+          Changed = true;
+        }
+    }
+  }
+
+  // Assign compact indices to the variables of the sub-system.
+  SmallVector<unsigned, 16> OldToNew;
+  OldToNew.assign(NumVariables + 1, 0);
+  unsigned NextIdx = 1;
+  for (unsigned Id = 1; Id <= NumVariables; ++Id)
+    if (InSystem[Id])
+      OldToNew[Id] = NextIdx++;
+
+  // Build new compact set of rows.
+  SubSystem.NumVariables = NextIdx;
+  for (const auto &Row : Constraints) {
+    if (none_of(Row,
+                [&](const Entry &E) { return E.Id != 0 && InSystem[E.Id]; }))
+      continue;
----------------
nikic wrote:

Wonder whether it would be faster to also have a bit vector for included rows or not.

https://github.com/llvm/llvm-project/pull/210432


More information about the llvm-commits mailing list