[ 
https://issues.apache.org/jira/browse/CALCITE-7811?page=com.atlassian.jira.plugin.system.issuetabpanels:all-tabpanel
 ]

ASF GitHub Bot updated CALCITE-7811:
------------------------------------
    Labels: pull-request-available  (was: )

> 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
>            Priority: Major
>              Labels: pull-request-available
>
> 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)

Reply via email to