================
@@ -575,6 +575,68 @@ ValueBoundsConstraintSet::computeConstantDelta(Value
value1, Value value2,
{{value1, dim1}, {value2, dim2}});
}
+void ValueBoundsConstraintSet::populateConstraints(Value value,
+ std::optional<int64_t> dim)
{
+ // `getExpr` pushes the value/dim onto the worklist (unless it was already
+ // analyzed).
+ (void)getExpr(value, dim);
+ // Process all values/dims on the worklist. This may traverse and analyze
+ // additional IR, depending the current stop function.
+ processWorklist();
+}
+
+bool ValueBoundsConstraintSet::compare(Value value1,
+ std::optional<int64_t> dim1,
+ ComparisonOperator cmp, Value value2,
+ std::optional<int64_t> dim2) {
+ // This function returns "true" if value1/dim1 CMP value2/dim2 is proved to
+ // hold.
+ //
+ // Example for ComparisonOperator::LE and index-typed values: We would like
to
+ // prove that value1 <= value2. Proof by contradiction: add the inverse
+ // relation (value1 > value2) to the constraint set and check if the
resulting
+ // constraint set is "empty" (i.e. has no solution). In that case,
+ // value1 > value2 must be incorrect and we can deduce that value1 <= value2
+ // holds.
+
+ // We cannot use prove anything if the constraint set is already empty.
----------------
dcaballe wrote:
typo: use prove?
https://github.com/llvm/llvm-project/pull/85895
_______________________________________________
llvm-branch-commits mailing list
llvm-branch-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-branch-commits
