[GitHub] [calcite] vlsi commented on pull request #2236: [CALCITE-3913] Test correctness using formal verification (Qi Zhou)

vlsi commented on pull request #2236: URL: https://github.com/apache/calcite/pull/2236#issuecomment-726680603 >but what is the time requirement in general for checking RexNode implication, like ~10 milliseconds? ~1 milliseconds? ~0.1 milliseconds? Just want to get a sense. The

[GitHub] [calcite] vlsi commented on pull request #2236: [CALCITE-3913] Test correctness using formal verification (Qi Zhou)

vlsi commented on pull request #2236: URL: https://github.com/apache/calcite/pull/2236#issuecomment-726355820 I guess we want to keep RexImplicationChecker, so we don't want to use slow approaches like z3 there. On the other hand, z3 might be helpful for testing RexImplicationChecker.

[GitHub] [calcite] vlsi commented on pull request #2236: [CALCITE-3913] Test correctness using formal verification (Qi Zhou)

vlsi commented on pull request #2236: URL: https://github.com/apache/calcite/pull/2236#issuecomment-720787197 @qizhou92 , this looks nice. Have you seen `RexFuzzer`, `RexProgramFuzzyTest`, `org.apache.calcite.rex.RexSimplify#verify` ? I wonder if `z3` verifications could be

[GitHub] [calcite] vlsi commented on pull request #2236: [CALCITE-3913] Test correctness using formal verification (Qi Zhou)

vlsi commented on pull request #2236: URL: https://github.com/apache/calcite/pull/2236#issuecomment-719457908 @qizhou92 , thanks for the PR. > I am not quite sure how much code I should push in commit to reviewing That differs on a case-by-case basis. For z3