vlsi commented on PR #2236: URL: https://github.com/apache/calcite/pull/2236#issuecomment-6118417557
Thanks, @qizhou92, for the work on this, and sorry it sat without a decision for so long. I'm closing the PR: it no longer builds against `main`, and the approach needs changes large enough that a fresh PR is the better path. CALCITE-3913 stays open, and the notes below are for whoever picks it up. **Why it can't be merged as is** - The tests call `SqlToRelTestBase.createTester()`, which was removed when the tests moved to fluent fixtures (CALCITE-4885, Calcite 1.30). - `javasmt-solver-z3:z3-4.4.1-1558-gf96cfea` resolves to the Java bindings only: Gradle fetches no native library, and `libz3java` isn't published for that version at all. Unless the library is built by hand, `@BeforeAll` skips every test, so the tests would never run in CI. **What the verifier gets wrong** - `constantNotNullToExpr` turns every unsupported literal into `mkInt(0)`, so the verifier reports `'abc' = 'xyz'` as equivalent to `TRUE`. `INTEGER` and `BIGINT` literals go through `intValue()`, which truncates a `BIGINT` value. - `checkCondEq` compares only the rows where the condition is TRUE. That is right for a filter (`RexUnknownAs.FALSE`), but a simplification that turns NULL into FALSE under `NOT` passes, and `RexSimplify` bugs often involve three-valued logic. - Z3 integers are unbounded, so the verifier reports `a + 1 > a` as equivalent to `TRUE` and doesn't model `INTEGER` overflow. Z3 integer division also rounds differently from SQL when the dividend is negative: `-7 / 2` is -4 in Z3 and -3 in SQL. - `type2Sort` passes a `RelDataType` to `APPROX_TYPES.contains` and `BOOLEAN_TYPES.contains`, so `DOUBLE`, `BOOLEAN`, and `VARCHAR` columns get a `null` sort, and `mkConst` throws a `NullPointerException` for it. - `IN`, `CAST`, `CASE`, `SEARCH`, and other unsupported calls return `null`, which ends in a `NullPointerException` instead of an "unsupported" result. `SEARCH` matters most: `RexSimplify` turns ranges and `OR` chains into it, so most simplified expressions can't be checked without it (`RexUtil.expandSearch` would do). - `logicallyEquivalent` returns `false` both for "not equivalent" and for a solver `UNKNOWN`, so `rexNodeNotEq1` can't tell the two apart. **What a new attempt could look like** - Use the solver-independent JavaSMT API instead of `com.microsoft.z3`. SMTInterpol and Princess are pure Java and run in CI without native libraries; SMTInterpol has no bit-vectors, so Princess is the pure-Java option where they're needed. Recent `javasmt-solver-z3` releases publish the Z3 native libraries on Maven Central as separate classifier artifacts, so Z3 needs no manual build either. - Model `INTEGER` and `BIGINT` as 32-bit and 64-bit bit-vectors. They match the wrapping arithmetic of the default conformance; conformances with `checkedArithmetic()` throw on overflow instead. - Compare the two expressions under the `RexUnknownAs` mode the simplification ran in, as `RexSimplify.verify` does, and return one of three results: equivalent, different (with the counterexample from the model), or unsupported. - Build the expressions with the `RexProgramBuilderBase` helpers rather than through SQL, so the converter can't simplify them before the check. - Add a test where the verifier must report a known-wrong simplification as different. Every `checkSimplify` assertion expects "equivalent", so a verifier that always returns `true` passes them. - As discussed above, use the verifier as an oracle in `RexProgramFuzzyTest` with `RexFuzzer`, limited to integer and boolean expressions, and show at least one `RexSimplify` bug it catches that the existing paranoid check, `RexSimplify.verify`, misses. -- This is an automated message from the Apache Git Service. To respond to the message, please log on to GitHub and use the URL above to go to the specific comment. To unsubscribe, e-mail: [email protected] For queries about this service, please contact Infrastructure at: [email protected]
