[jira] [Commented] (CALCITE-3913) Test correctness using formal verification techniques

2020-10-29 Thread Qi Zhou (Jira)
[ https://issues.apache.org/jira/browse/CALCITE-3913?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel=17223278#comment-17223278 ] Qi Zhou commented on CALCITE-3913: -- The commit tree in the previous pull request becomes too

[jira] [Commented] (CALCITE-3913) Test correctness using formal verification techniques

2020-10-28 Thread Qi Zhou (Jira)
[ https://issues.apache.org/jira/browse/CALCITE-3913?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel=17222643#comment-17222643 ] Qi Zhou commented on CALCITE-3913: -- Add Symbolic Columns, and Convert Rex Node to Symbolic Columns. 

[jira] [Commented] (CALCITE-3913) Test correctness using formal verification techniques

2020-08-20 Thread Michael Mior (Jira)
[ https://issues.apache.org/jira/browse/CALCITE-3913?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel=17181352#comment-17181352 ] Michael Mior commented on CALCITE-3913: --- [~qzhou] A pull request certainly makes things easier

[jira] [Commented] (CALCITE-3913) Test correctness using formal verification techniques

2020-08-20 Thread Qi Zhou (Jira)
[ https://issues.apache.org/jira/browse/CALCITE-3913?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel=17181305#comment-17181305 ] Qi Zhou commented on CALCITE-3913: -- Hi Michael, Thanks for helping me. I am planning to push more code

[jira] [Commented] (CALCITE-3913) Test correctness using formal verification techniques

2020-08-20 Thread Michael Mior (Jira)
[ https://issues.apache.org/jira/browse/CALCITE-3913?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel=17181216#comment-17181216 ] Michael Mior commented on CALCITE-3913: --- [~qzhou] Thanks for starting a pull request! It's good

[jira] [Commented] (CALCITE-3913) Test correctness using formal verification techniques

2020-06-29 Thread Stamatis Zampetakis (Jira)
[ https://issues.apache.org/jira/browse/CALCITE-3913?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel=17148168#comment-17148168 ] Stamatis Zampetakis commented on CALCITE-3913: -- You can have as many commits as you like,

[jira] [Commented] (CALCITE-3913) Test correctness using formal verification techniques

2020-06-29 Thread Qi Zhou (Jira)
[ https://issues.apache.org/jira/browse/CALCITE-3913?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel=17148155#comment-17148155 ] Qi Zhou commented on CALCITE-3913: -- Hi,  Sorry for the late actions. I try to submit my first PR that

[jira] [Commented] (CALCITE-3913) Test correctness using formal verification techniques

2020-04-17 Thread Qi Zhou (Jira)
[ https://issues.apache.org/jira/browse/CALCITE-3913?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel=17086126#comment-17086126 ] Qi Zhou commented on CALCITE-3913: -- Yes, I believe the java binding library is on Maven central. Here

[jira] [Commented] (CALCITE-3913) Test correctness using formal verification techniques

2020-04-17 Thread Julian Hyde (Jira)
[ https://issues.apache.org/jira/browse/CALCITE-3913?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel=17086036#comment-17086036 ] Julian Hyde commented on CALCITE-3913: -- Is the java binding library on Maven central? If not, that

[jira] [Commented] (CALCITE-3913) Test correctness using formal verification techniques

2020-04-17 Thread Julian Hyde (Jira)
[ https://issues.apache.org/jira/browse/CALCITE-3913?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel=17086030#comment-17086030 ] Julian Hyde commented on CALCITE-3913: -- OK, we can make that work. The test would need to no-op if

[jira] [Commented] (CALCITE-3913) Test correctness using formal verification techniques

2020-04-16 Thread Qi Zhou (Jira)
[ https://issues.apache.org/jira/browse/CALCITE-3913?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel=17085361#comment-17085361 ] Qi Zhou commented on CALCITE-3913: -- Z3 is not write in java, it is written in c++, but it has a java

[jira] [Commented] (CALCITE-3913) Test correctness using formal verification techniques

2020-04-16 Thread Julian Hyde (Jira)
[ https://issues.apache.org/jira/browse/CALCITE-3913?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel=17085315#comment-17085315 ] Julian Hyde commented on CALCITE-3913: -- I assume that Z3 is java. What's the license? Is it on

[jira] [Commented] (CALCITE-3913) Test correctness using formal verification techniques

2020-04-16 Thread Qi Zhou (Jira)
[ https://issues.apache.org/jira/browse/CALCITE-3913?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel=17085257#comment-17085257 ] Qi Zhou commented on CALCITE-3913: -- Hi, I think the first step I can do is trying to add the code

[jira] [Commented] (CALCITE-3913) Test correctness using formal verification techniques

2020-04-10 Thread Chunwei Lei (Jira)
[ https://issues.apache.org/jira/browse/CALCITE-3913?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel=17081108#comment-17081108 ] Chunwei Lei commented on CALCITE-3913: -- Interesting work! I think checking the rule correctness is

[jira] [Commented] (CALCITE-3913) Test correctness using formal verification techniques

2020-04-10 Thread Qi Zhou (Jira)
[ https://issues.apache.org/jira/browse/CALCITE-3913?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel=17081040#comment-17081040 ] Qi Zhou commented on CALCITE-3913: -- The first thing we considering to do is to bring this tool to

[jira] [Commented] (CALCITE-3913) Test correctness using formal verification techniques

2020-04-10 Thread Haisheng Yuan (Jira)
[ https://issues.apache.org/jira/browse/CALCITE-3913?page=com.atlassian.jira.plugin.system.issuetabpanels:comment-tabpanel=17081011#comment-17081011 ] Haisheng Yuan commented on CALCITE-3913: I think one use case is that there are tens of