[
https://issues.apache.org/jira/browse/CALCITE-7811?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel&focusedCommentId=18118080#comment-18118080
]
Jasmin Trada edited comment on CALCITE-7811 at 9/23/26 10:22 PM:
-----------------------------------------------------------------
Here's the failing test PR:
[https://github.com/apache/calcite/pull/5285/changes]
was (Author: JIRAUSER297048):
Here's the failing test PR:
[https://github.com/apache/calcite/pull/5285/changes]
Root cause:
In RexImplicationChecker.InputUsageFinder (the visitor that extracts "column op
literal" facts from an expression for the substitution-based implication check),
visitCall's switch statement has no case for NOT:
{code:java}
@Override public Void visitCall(RexCall call) {
switch (call.getOperator().getKind()) {
case GREATER_THAN:
case GREATER_THAN_OR_EQUAL:
case LESS_THAN:
case LESS_THAN_OR_EQUAL:
case EQUALS:
case NOT_EQUALS:
updateBinaryOpUsage(call);
break;
case IS_NULL:
case IS_NOT_NULL:
updateUnaryOpUsage(call);
break;
default:
}
return super.visitCall(call); // unconditionally recurses into NOT's operand
}
{code}
Because NOT isn't a handled case, the switch is a no-op for it, but the trailing
"return super.visitCall(call)" still recurses into the NOT's child
unconditionally.
For NOT(x = 'a'), that child is EQUALS(x, 'a'), which IS a handled kind, so the
visitor records "x is compared with EQUALS to 'a'" -- with no memory that this
equality was actually negated. RexUtil.toDnf doesn't rewrite NOT(=(...)) into
<>(...) either (its NOT case only special-cases NOT(NOT(x)), NOT(OR(...)),
NOT(AND(...))), so this misclassification survives unmasked into
RexImplicationChecker's substitution logic, which then "verifies" implication by
plugging x = 'a' into the right-hand side instead of the true fact x <> 'a'.
Proposed fix:
Add a NOT case to InputUsageFinder.visitCall that, when the operand is a
comparison
(=, <>, <, <=, >, >=), rewrites it to the equivalent negated comparison using
the
existing (already null-safe, per SqlKind.negateNullSafe())
RexUtil.negate(RexBuilder,
RexCall) helper, and records that instead of recursing into the un-negated
operand.
For anything else NOT might wrap (AND, OR, another NOT, IS NULL, a boolean
column),
it deliberately does not descend into the operand -- leaving that usage
unrecorded
causes checkSupport() to conservatively bail out (return false / "not implied")
rather than reasoning from an incorrect fact, which matches the class's
documented
contract ("if it says implies, it's definitely true; it cannot prove first does
not
imply second").
> RexImplicationChecker incorrectly proves NOT(x = a) implies (x = a OR x = b)
> ----------------------------------------------------------------------------
>
> Key: CALCITE-7811
> URL: https://issues.apache.org/jira/browse/CALCITE-7811
> Project: Calcite
> Issue Type: Bug
> Reporter: Jasmin Trada
> Assignee: Jasmin Trada
> Priority: Major
> Labels: pull-request-available
> Fix For: 1.43.0
>
>
> RexImplicationChecker.implies() can return true for an implication that does
> not
> actually hold, when the premise contains NOT wrapped directly around a
> comparison
> (e.g. NOT(x = a)).
> Repro:
> {code:java}
> final Fixture f = new Fixture();
> final RexNode sEqA = f.eq(f.str, f.charLiteral("a"));
> final RexNode sEqB = f.eq(f.str, f.charLiteral("b"));
> final RexNode sNeA = f.ne(f.str, f.charLiteral("a"));
> final RexNode sNotEqA = f.rexBuilder.makeCall(SqlStdOperatorTable.NOT, sEqA);
> final RexNode sEqAOrEqB = f.or(sEqA, sEqB);
> // Correct: the checker soundly declines to prove this (x = 'c' is a
> counterexample).
> assertFalse(f.checker.implies(sNeA, sEqAOrEqB));
> // Bug: the logically identical NOT(x = 'a') is wrongly reported as implying
> the OR.
> assertTrue(f.checker.implies(sNotEqA, sEqAOrEqB)); // should be false
> {code}
> "x <> 'a'" and "NOT(x = 'a')" are logically identical, but the checker treats
> them
> differently: only the syntactic NOT_EQUALS form is handled soundly. NOT(x =
> 'a')
> is silently misrecorded internally as a plain x = 'a' usage, so the checker
> "proves"
> NOT(x = 'a') implies (x = 'a' OR x = 'b') by testing x = 'a' against the
> right-hand
> side, instead of testing x <> 'a'.
--
This message was sent by Atlassian Jira
(v8.20.10#820010)
