Dsl testing #21

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed

WKaiZ wants to merge 88 commits into qed-solver:main from WKaiZ:dsl-testing

.github/workflows/codegen-test.yml

-Original file line number
+Diff line change
@@ -0,0 +1,46 @@
+    name: Test Code Generation
+    on:
+      push:
+      pull_request:
+    jobs:
+      test-code-generation:
+        runs-on: ubuntu-latest
+        steps:
+          - uses: actions/checkout@v4
+          - name: Set up Java
+            uses: actions/setup-java@v4
+            with:
+              java-version: '23'
+              distribution: 'temurin'
+          - name: Cache Maven dependencies
+            uses: actions/cache@v3
+            with:
+              path: ~/.m2/repository
+              key: ${{ runner.os }}-maven-${{ hashFiles('**/pom.xml') }}
+              restore-keys: |
+                ${{ runner.os }}-maven-
+          - name: Build project
+            run: mvn -B compile --file pom.xml
+          - name: Run Calcite tests
+            run: |
+              chmod +x scripts/test-codegen.sh
+              ./scripts/test-codegen.sh
+          - name: Upload generated code
+            if: always()
+            uses: actions/upload-artifact@v4
+            with:
+              name: generated-code
+              path: |
+                src/main/java/org/qed/Generated/*.java
+                !src/main/java/org/qed/Generated/CalciteTester.java
+                !src/main/java/org/qed/Generated/CalciteGenerator.java
+                !src/main/java/org/qed/Generated/CalciteUtilities.java
+                !src/main/java/org/qed/Generated/EmptyConfig.java

.github/workflows/prover-test.yml

-Original file line number
+Diff line change
@@ -0,0 +1,58 @@
+    name: Test Provability
+    on:
+      push:
+      pull_request:
+    jobs:
+      test-provability:
+        runs-on: ubuntu-latest
+        steps:
+          - uses: actions/checkout@v4
+          - name: Set up Java
+            uses: actions/setup-java@v4
+            with:
+              java-version: '23'
+              distribution: 'temurin'
+          - name: Cache Maven dependencies
+            uses: actions/cache@v3
+            with:
+              path: ~/.m2/repository
+              key: ${{ runner.os }}-maven-${{ hashFiles('**/pom.xml') }}
+              restore-keys: |
+                ${{ runner.os }}-maven-
+          - name: Build project
+            run: mvn -B compile --file pom.xml
+          - name: Generate JSON for all rules
+            run: |
+              mkdir -p tmp-rules
+              mvn dependency:resolve
+              chmod +x scripts/generate-rule-json.sh
+              ./scripts/generate-rule-json.sh
+          - name: Install dependencies
+            run: |
+              chmod +x scripts/install-dependencies.sh
+              ./scripts/install-dependencies.sh
+          - name: Build qed-prover
+            run: |
+              chmod +x scripts/build-qed-prover.sh
+              ./scripts/build-qed-prover.sh
+          - name: Test all rules
+            run: |
+              chmod +x scripts/test-rules.sh
+              ./scripts/test-rules.sh
+          - name: Upload test artifacts
+            if: always()
+            uses: actions/upload-artifact@v4
+            with:
+              name: results
+              path: tmp-rules/

.gitignore

-Original file line number
+Diff line change
@@ Expand Up / @@ -5,3 +5,5 @@ @@
     target/
     *.iml
     .mvn/wrapper/maven-wrapper.jar
+    .vscode
+    .devcontainer

flake.lock

Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.

flake.nix

            
                      Original file line number
                      Diff line number
                      Diff line change
                  
    @@ -2,35 +2,57 @@
  
      inputs = {

        nixpkgs.url = "github:NixOS/nixpkgs/nixpkgs-unstable";

        flake-utils.url = "github:numtide/flake-utils";

        parser-release = {

        cvc5-src = {

          flake = false;

          url = "https://github.com/qed-solver/parser/releases/download/latest/qed-parser-1.0-SNAPSHOT-jar-with-dependencies.jar";

          url = "github:cvc5/cvc5";

        };

      };

      outputs = { self, nixpkgs, flake-utils, parser-release }:

      outputs = { self, nixpkgs, flake-utils, cvc5-src }:

        flake-utils.lib.eachDefaultSystem (system:

          let

            pkgs = nixpkgs.legacyPackages.${system};

            parser = pkgs.stdenv.mkDerivation {

              name = "qed-parser";

              src = parser-release;

              buildInputs = with pkgs; [ jre ];

              nativeBuildInputs = with pkgs; [ makeWrapper ];

              buildCommand = ''

                jar=$out/share/java/qed-parser.jar

                install -Dm444 $src $jar

                makeWrapper ${pkgs.jre}/bin/java $out/bin/qed-parser --add-flags "--enable-preview --add-opens=java.base/java.lang.reflect=ALL-UNNAMED -jar $jar"

            cvc5-pname = "cvc5-1.0.5";

            cvc5-java = pkgs.stdenv.mkDerivation {

              name = cvc5-pname;

              src = cvc5-src;

              nativeBuildInputs = with pkgs; [ pkg-config cmake flex ];

              buildInputs = with pkgs; [

                cadical.dev

                symfpu

                gmp

                gtest

                libantlr3c

                antlr3_4

                boost

                jdk21

                (python3.withPackages (ps: with ps; [ pyparsing toml ]))

              ];

              cmakeFlags = [

                "-DBUILD_BINDINGS_JAVA=ON"

                "-DBUILD_SHARED_LIBS=1"

                "-DCMAKE_BUILD_TYPE=Production"

                "-DANTLR3_JAR=${pkgs.antlr3_4}/lib/antlr/antlr-3.4-complete.jar"

              ];

              preConfigure = ''

                patchShebangs ./src/

              '';

            };

          in

          {

            packages.default = parser;

            devShells.default = pkgs.mkShell {

              packages = with pkgs; [

                jdk

                cvc5-java

                jdk21

                jetbrains.idea-community

              ];

              CVC5_JAVA = "${cvc5-java}/share/java/cvc5.jar";

              LD_LIBRARY_PATH = pkgs.lib.strings.makeLibraryPath [ cvc5-java ];

            };

          });

    }

pom.xml

-Original file line number
+Diff line change
@@ Expand Up / @@ -21,7 +21,6 @@ @@
                             <argument>-classpath</argument>
                             <classpath/>
                             <argument>org.qed.Main</argument>
-                            <argument>${args}</argument>
                         </arguments>
                     </configuration>
                 </plugin>
@@ Expand Down Expand Up / @@ -52,9 +51,11 @@ @@
                     <groupId>org.apache.maven.plugins</groupId>
                     <artifactId>maven-compiler-plugin</artifactId>
                     <configuration>
-                        <source>19</source>
-                        <target>19</target>
-                        <compilerArgs>--enable-preview</compilerArgs>
+                        <source>23</source>
+                        <target>23</target>
+                        <compilerArgs>
+                            <arg>--enable-preview</arg>
+                        </compilerArgs>
                     </configuration>
                 </plugin>
             </plugins>
@@ Expand Down Expand Up / @@ -88,13 +89,28 @@ @@
             </dependency>
             <dependency>
                 <groupId>org.slf4j</groupId>
-                <artifactId>slf4j-nop</artifactId>
-                <version>2.0.5</version>
+                <artifactId>slf4j-api</artifactId>
+                <version>2.0.12</version>
+            </dependency>
+            <dependency>
+                <groupId>org.slf4j</groupId>
+                <artifactId>slf4j-simple</artifactId>
+                <version>2.0.12</version>
             </dependency>
             <dependency>
                 <groupId>org.glavo.kala</groupId>
                 <artifactId>kala-common</artifactId>
                 <version>0.67.0</version>
             </dependency>
+            <dependency>
+                <groupId>io.github.p-org.solvers</groupId>
+                <artifactId>cvc5</artifactId>
+                <version>0.0.7-v5</version>
+            </dependency>
+            <dependency>
+                <groupId>org.reflections</groupId>
+                <artifactId>reflections</artifactId>
+                <version>0.10.2</version>
+            </dependency>
         </dependencies>
-    </project>
+    </project>

rules/JoinCommute-.json

-Original file line number
+Diff line change
@@ -0,0 +1,72 @@
+    {
+      "help" : [ "LogicalJoin(condition=[pred($0, $1)], joinType=[inner])\n  LogicalTableScan(table=[[Left]])\n  LogicalTableScan(table=[[Right]])\n", "LogicalProject(col-Left=[$1], col-Right=[$0])\n  LogicalJoin(condition=[pred($1, $0)], joinType=[inner])\n    LogicalTableScan(table=[[Right]])\n    LogicalTableScan(table=[[Left]])\n" ],
+      "schemas" : [ {
+        "types" : [ "INTEGER" ],
+        "nullable" : [ true ],
+        "name" : "Left",
+        "guaranteed" : [ ],
+        "fields" : [ "col-Left" ],
+        "key" : [ ]
+      }, {
+        "types" : [ "INTEGER" ],
+        "nullable" : [ true ],
+        "name" : "Right",
+        "guaranteed" : [ ],
+        "fields" : [ "col-Right" ],
+        "key" : [ ]
+      } ],
+      "queries" : [ {
+        "join" : {
+          "condition" : {
+            "type" : "BOOLEAN",
+            "operand" : [ {
+              "column" : 0,
+              "type" : "INTEGER"
+            }, {
+              "column" : 1,
+              "type" : "INTEGER"
+            } ],
+            "operator" : "pred"
+          },
+          "left" : {
+            "scan" : 0
+          },
+          "kind" : "INNER",
+          "right" : {
+            "scan" : 1
+          }
+        }
+      }, {
+        "project" : {
+          "source" : {
+            "join" : {
+              "condition" : {
+                "type" : "BOOLEAN",
+                "operand" : [ {
+                  "column" : 1,
+                  "type" : "INTEGER"
+                }, {
+                  "column" : 0,
+                  "type" : "INTEGER"
+                } ],
+                "operator" : "pred"
+              },
+              "left" : {
+                "scan" : 1
+              },
+              "kind" : "INNER",
+              "right" : {
+                "scan" : 0
+              }
+            }
+          },
+          "target" : [ {
+            "column" : 1,
+            "type" : "INTEGER"
+          }, {
+            "column" : 0,
+            "type" : "INTEGER"
+          } ]
+        }
+      } ]
+    }

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Dsl testing #21

Uh oh!

Diff view

Diff view

There are no files selected for viewing

Uh oh!

Uh oh!

Uh oh!