From 827f2d52c6bc2d3bac89dd817f3d9d68daa4b44e Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 10:16:49 -0700 Subject: [PATCH 01/41] workflow try 1 --- .github/workflows/test-new-rules.yml | 204 +++++++++++++++++++++++++++ 1 file changed, 204 insertions(+) create mode 100644 .github/workflows/test-new-rules.yml diff --git a/.github/workflows/test-new-rules.yml b/.github/workflows/test-new-rules.yml new file mode 100644 index 0000000..2133719 --- /dev/null +++ b/.github/workflows/test-new-rules.yml @@ -0,0 +1,204 @@ +name: Test New Rules + +on: + push: + paths: + - 'src/main/java/org/qed/Generated/RRuleInstances/**/*.java' + pull_request: + paths: + - 'src/main/java/org/qed/Generated/RRuleInstances/**/*.java' + +jobs: + # First job: detect which files changed + get-changed-files: + runs-on: ubuntu-latest + outputs: + changed_files: ${{ steps.changed-files.outputs.all_changed_files }} + steps: + - uses: actions/checkout@v4 + with: + fetch-depth: 0 + + - name: Get changed files + id: changed-files + uses: tj-actions/changed-files@v41 + with: + files: | + src/main/java/org/qed/Generated/RRuleInstances/**/*.java + separator: ',' + + # Second job: test the changed rules + test-rules: + needs: get-changed-files + if: ${{ needs.get-changed-files.outputs.changed_files != '' }} + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v4 + + - name: Set up Java + uses: actions/setup-java@v4 + with: + java-version: '11' + 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 parser project + run: mvn -B compile --file pom.xml + + - name: Generate JSON for new/modified rules + run: | + mkdir -p rules + + # Create JSON generator + cat > JsonGenerator.java << 'EOF' + import org.qed.*; + import com.fasterxml.jackson.databind.ObjectMapper; + import java.nio.file.*; + + public class JsonGenerator { + public static void main(String[] args) throws Exception { + if (args.length == 0) { + System.err.println("Usage: java JsonGenerator "); + System.exit(1); + } + + String className = args[0]; + try { + Class clazz = Class.forName(className); + RRule rule = (RRule) clazz.getDeclaredConstructor().newInstance(); + + ObjectMapper mapper = new ObjectMapper(); + Files.createDirectories(Path.of("rules")); + String fileName = rule.name() + "-" + rule.info() + ".json"; + mapper.writerWithDefaultPrettyPrinter().writeValue( + Path.of("rules", fileName).toFile(), + rule.toJson() + ); + System.out.println("Generated: " + fileName); + } catch (Exception e) { + System.err.println("Failed to generate JSON for " + className); + e.printStackTrace(); + System.exit(1); + } + } + } + EOF + + # Get classpath + CLASSPATH="target/classes:$(mvn dependency:build-classpath -q -DforceStdout)" + + # Compile generator + javac -cp "$CLASSPATH" JsonGenerator.java + + # Process each changed file + IFS=',' read -ra FILES <<< "${{ needs.get-changed-files.outputs.changed_files }}" + for file in "${FILES[@]}"; do + if [ -n "$file" ]; then + className=$(echo "$file" | sed 's|src/main/java/||; s|/|.|g; s|\.java$||') + echo "Processing: $className" + java -cp ".:$CLASSPATH" JsonGenerator "$className" + fi + done + + rm -f JsonGenerator.java JsonGenerator.class + + - name: Setup qed-prover + run: | + # Option 1: Try to checkout qed-prover (update URL if needed) + # git clone https://github.com/qed-solver/prover.git || { + # echo "::error::Cannot clone qed-prover repository" + # echo "Please update the repository URL in the workflow" + # exit 1 + # } + + # Option 2: For testing, create a mock qed-prover + echo "::warning::Using mock qed-prover for testing. Replace with real qed-prover!" + mkdir -p qed-prover/target/release + + cat > qed-prover/target/release/qed-prover << 'EOF' + #!/bin/bash + # MOCK qed-prover - Replace with real implementation + json_file="$1" + rule_name=$(basename "$json_file" .json) + + # Mock: all rules pass for testing + echo '{"provable":true,"panicked":false,"complete_fragment":false,"equiv_class_duration":{"secs":0,"nanos":20638791},"equiv_class_timed_out":false,"smt_duration":{"secs":0,"nanos":55148417},"smt_timed_out":false,"nontrivial_perms":false,"translate_duration":{"secs":0,"nanos":1047250},"normal_duration":{"secs":0,"nanos":1880834},"stable_duration":{"secs":0,"nanos":28722792},"unify_duration":{"secs":0,"nanos":55404417},"total_duration":{"secs":0,"nanos":129852459}}' + EOF + + chmod +x qed-prover/target/release/qed-prover + + - name: Install jq + run: | + sudo apt-get update + sudo apt-get install -y jq + + - name: Test rules with qed-prover + run: | + echo "## Test Results" >> $GITHUB_STEP_SUMMARY + echo "" >> $GITHUB_STEP_SUMMARY + + failed_rules="" + passed_rules="" + + # Test the generated JSON files + for json_file in rules/*.json; do + if [ -f "$json_file" ]; then + rule_name=$(basename "$json_file" .json) + echo "Testing rule: $rule_name" + + # Run qed-prover + output=$(./qed-prover/target/release/qed-prover "$json_file" 2>&1) + + # Parse result + if echo "$output" | jq -e '.provable == true' > /dev/null 2>&1; then + echo "✅ $rule_name: PASSED" | tee -a $GITHUB_STEP_SUMMARY + passed_rules="$passed_rules$rule_name," + else + echo "❌ $rule_name: FAILED" | tee -a $GITHUB_STEP_SUMMARY + failed_rules="$failed_rules$rule_name," + fi + fi + done + + # Set outputs for use in other steps/jobs + echo "failed_rules=$failed_rules" >> $GITHUB_OUTPUT + echo "passed_rules=$passed_rules" >> $GITHUB_OUTPUT + + # Fail if any rules failed + if [ -n "$failed_rules" ]; then + echo "::error::Some rules failed verification: ${failed_rules%,}" + exit 1 + fi + + - name: Comment PR (if applicable) + if: github.event_name == 'pull_request' && always() + uses: actions/github-script@v7 + with: + script: | + const fs = require('fs'); + const summary = fs.readFileSync(process.env.GITHUB_STEP_SUMMARY, 'utf8'); + + github.rest.issues.createComment({ + issue_number: context.issue.number, + owner: context.repo.owner, + repo: context.repo.repo, + body: `## QED Prover Test Results\n\n${summary}` + }); + + - name: Upload test artifacts + if: always() + uses: actions/upload-artifact@v3 + with: + name: test-results + path: | + rules/*.json + rules/*.result + test-output-*.log \ No newline at end of file From a2c66bcc04004770e5c7bafd588efd1e81a8ae2f Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 11:17:27 -0700 Subject: [PATCH 02/41] workflow try 1 --- .github/workflows/test-new-rules.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/test-new-rules.yml b/.github/workflows/test-new-rules.yml index 2133719..5ef0a53 100644 --- a/.github/workflows/test-new-rules.yml +++ b/.github/workflows/test-new-rules.yml @@ -1,4 +1,4 @@ -name: Test New Rules +name: Test New Rule on: push: From 34202e579edb87de7b20fe9ddb6ddf7d51caa9ae Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 11:21:06 -0700 Subject: [PATCH 03/41] workflow test 1 --- .../java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java index 24165aa..78ca4ee 100644 --- a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java +++ b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java @@ -22,6 +22,7 @@ public RelRN before() { @Override public RelRN after() { - return left.join(JoinRelType.INNER, RexRN.and(joinCond, left.joinPred("outer", right)), right); + return left.join(JoinRelType.INNER, RexRN.and( + joinCond, left.joinPred("outer", right)), right); } } From 3b786ac49e81845b5f7a77c94cca32afc43e8f8d Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 11:25:46 -0700 Subject: [PATCH 04/41] workflow try 2 --- .github/workflows/test-new-rules.yml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/.github/workflows/test-new-rules.yml b/.github/workflows/test-new-rules.yml index 5ef0a53..00c27dc 100644 --- a/.github/workflows/test-new-rules.yml +++ b/.github/workflows/test-new-rules.yml @@ -194,11 +194,11 @@ jobs: }); - name: Upload test artifacts - if: always() - uses: actions/upload-artifact@v3 - with: - name: test-results - path: | - rules/*.json - rules/*.result - test-output-*.log \ No newline at end of file + if: always() + uses: actions/upload-artifact@v4 + with: + name: test-results + path: | + rules/*.json + rules/*.result + test-output-*.log \ No newline at end of file From 992131cc6ebb8eb8a912283645eddfaa559949ea Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 11:26:35 -0700 Subject: [PATCH 05/41] workflow test 2 --- .../java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java index 78ca4ee..24165aa 100644 --- a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java +++ b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java @@ -22,7 +22,6 @@ public RelRN before() { @Override public RelRN after() { - return left.join(JoinRelType.INNER, RexRN.and( - joinCond, left.joinPred("outer", right)), right); + return left.join(JoinRelType.INNER, RexRN.and(joinCond, left.joinPred("outer", right)), right); } } From 07f97230ef8b3526743ce7a8c5b578e20877b849 Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 11:29:13 -0700 Subject: [PATCH 06/41] workflow test 3 --- .../java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java index 24165aa..86770be 100644 --- a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java +++ b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java @@ -22,6 +22,6 @@ public RelRN before() { @Override public RelRN after() { - return left.join(JoinRelType.INNER, RexRN.and(joinCond, left.joinPred("outer", right)), right); + return left.join(JoinRelType.SEMI, RexRN.and(joinCond, left.joinPred("outer", right)), right); } } From 09d36ee1a70c7d31e5190bb99436f8cb3d370169 Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 11:39:34 -0700 Subject: [PATCH 07/41] new workflow try --- .github/workflows/test-new-rules.yml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/.github/workflows/test-new-rules.yml b/.github/workflows/test-new-rules.yml index 00c27dc..125f65a 100644 --- a/.github/workflows/test-new-rules.yml +++ b/.github/workflows/test-new-rules.yml @@ -195,10 +195,10 @@ jobs: - name: Upload test artifacts if: always() - uses: actions/upload-artifact@v4 - with: - name: test-results - path: | - rules/*.json - rules/*.result - test-output-*.log \ No newline at end of file + uses: actions/upload-artifact@v4 + with: + name: test-results + path: | + rules/*.json + rules/*.result + test-output-*.log \ No newline at end of file From c88b45e17d36ae5cb7db6f57b51801c0dd788e10 Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 11:41:27 -0700 Subject: [PATCH 08/41] new workflow try --- .github/workflows/test-new-rules.yml | 1 - 1 file changed, 1 deletion(-) diff --git a/.github/workflows/test-new-rules.yml b/.github/workflows/test-new-rules.yml index 125f65a..2b3f2e2 100644 --- a/.github/workflows/test-new-rules.yml +++ b/.github/workflows/test-new-rules.yml @@ -32,7 +32,6 @@ jobs: needs: get-changed-files if: ${{ needs.get-changed-files.outputs.changed_files != '' }} runs-on: ubuntu-latest - steps: - uses: actions/checkout@v4 From 04278429a24eef53da5a041ed01133a8036b127d Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 12:41:45 -0700 Subject: [PATCH 09/41] workflow new try --- .github/workflows/test-new-rules.yml | 179 ++++++++------------------- 1 file changed, 52 insertions(+), 127 deletions(-) diff --git a/.github/workflows/test-new-rules.yml b/.github/workflows/test-new-rules.yml index 2b3f2e2..d6b9123 100644 --- a/.github/workflows/test-new-rules.yml +++ b/.github/workflows/test-new-rules.yml @@ -1,4 +1,4 @@ -name: Test New Rule +name: Test All Rules on: push: @@ -9,38 +9,18 @@ on: - 'src/main/java/org/qed/Generated/RRuleInstances/**/*.java' jobs: - # First job: detect which files changed - get-changed-files: - runs-on: ubuntu-latest - outputs: - changed_files: ${{ steps.changed-files.outputs.all_changed_files }} - steps: - - uses: actions/checkout@v4 - with: - fetch-depth: 0 - - - name: Get changed files - id: changed-files - uses: tj-actions/changed-files@v41 - with: - files: | - src/main/java/org/qed/Generated/RRuleInstances/**/*.java - separator: ',' - - # Second job: test the changed rules - test-rules: - needs: get-changed-files - if: ${{ needs.get-changed-files.outputs.changed_files != '' }} + test-all-rules: runs-on: ubuntu-latest + steps: - uses: actions/checkout@v4 - + - name: Set up Java uses: actions/setup-java@v4 with: java-version: '11' distribution: 'temurin' - + - name: Cache Maven dependencies uses: actions/cache@v3 with: @@ -48,37 +28,33 @@ jobs: key: ${{ runner.os }}-maven-${{ hashFiles('**/pom.xml') }} restore-keys: | ${{ runner.os }}-maven- - - - name: Build parser project + + - name: Build project run: mvn -B compile --file pom.xml - - - name: Generate JSON for new/modified rules + + - name: Generate JSON for all rules run: | - mkdir -p rules - - # Create JSON generator + mkdir -p tmp-rules + cat > JsonGenerator.java << 'EOF' import org.qed.*; import com.fasterxml.jackson.databind.ObjectMapper; import java.nio.file.*; - public class JsonGenerator { public static void main(String[] args) throws Exception { if (args.length == 0) { System.err.println("Usage: java JsonGenerator "); System.exit(1); } - String className = args[0]; try { Class clazz = Class.forName(className); RRule rule = (RRule) clazz.getDeclaredConstructor().newInstance(); - ObjectMapper mapper = new ObjectMapper(); - Files.createDirectories(Path.of("rules")); + Files.createDirectories(Path.of("tmp-rules")); String fileName = rule.name() + "-" + rule.info() + ".json"; mapper.writerWithDefaultPrettyPrinter().writeValue( - Path.of("rules", fileName).toFile(), + Path.of("tmp-rules", fileName).toFile(), rule.toJson() ); System.out.println("Generated: " + fileName); @@ -90,114 +66,63 @@ jobs: } } EOF - - # Get classpath + CLASSPATH="target/classes:$(mvn dependency:build-classpath -q -DforceStdout)" - - # Compile generator javac -cp "$CLASSPATH" JsonGenerator.java - - # Process each changed file - IFS=',' read -ra FILES <<< "${{ needs.get-changed-files.outputs.changed_files }}" - for file in "${FILES[@]}"; do - if [ -n "$file" ]; then - className=$(echo "$file" | sed 's|src/main/java/||; s|/|.|g; s|\.java$||') - echo "Processing: $className" - java -cp ".:$CLASSPATH" JsonGenerator "$className" - fi + + find src/main/java/org/qed/Generated/RRuleInstances -name '*.java' | while read file; do + className=$(echo "$file" | sed 's|src/main/java/||; s|/|.|g; s|\.java$||') + echo "Generating for: $className" + java -cp ".:$CLASSPATH" JsonGenerator "$className" done - + rm -f JsonGenerator.java JsonGenerator.class - - - name: Setup qed-prover + + - name: Install Rust and clone qed-prover run: | - # Option 1: Try to checkout qed-prover (update URL if needed) - # git clone https://github.com/qed-solver/prover.git || { - # echo "::error::Cannot clone qed-prover repository" - # echo "Please update the repository URL in the workflow" - # exit 1 - # } - - # Option 2: For testing, create a mock qed-prover - echo "::warning::Using mock qed-prover for testing. Replace with real qed-prover!" - mkdir -p qed-prover/target/release - - cat > qed-prover/target/release/qed-prover << 'EOF' - #!/bin/bash - # MOCK qed-prover - Replace with real implementation - json_file="$1" - rule_name=$(basename "$json_file" .json) - - # Mock: all rules pass for testing - echo '{"provable":true,"panicked":false,"complete_fragment":false,"equiv_class_duration":{"secs":0,"nanos":20638791},"equiv_class_timed_out":false,"smt_duration":{"secs":0,"nanos":55148417},"smt_timed_out":false,"nontrivial_perms":false,"translate_duration":{"secs":0,"nanos":1047250},"normal_duration":{"secs":0,"nanos":1880834},"stable_duration":{"secs":0,"nanos":28722792},"unify_duration":{"secs":0,"nanos":55404417},"total_duration":{"secs":0,"nanos":129852459}}' - EOF - - chmod +x qed-prover/target/release/qed-prover - + sudo apt-get update + sudo apt-get install -y curl git + curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y + source $HOME/.cargo/env + git clone https://github.com/qed-solver/prover.git qed-prover + cd qed-prover + cargo build --release + + - name: Install jq run: | sudo apt-get update sudo apt-get install -y jq - - - name: Test rules with qed-prover + + - name: Test all rules run: | - echo "## Test Results" >> $GITHUB_STEP_SUMMARY + echo "## QED Prover Test Results" >> $GITHUB_STEP_SUMMARY echo "" >> $GITHUB_STEP_SUMMARY - + failed_rules="" passed_rules="" - - # Test the generated JSON files - for json_file in rules/*.json; do - if [ -f "$json_file" ]; then - rule_name=$(basename "$json_file" .json) - echo "Testing rule: $rule_name" - - # Run qed-prover - output=$(./qed-prover/target/release/qed-prover "$json_file" 2>&1) - - # Parse result - if echo "$output" | jq -e '.provable == true' > /dev/null 2>&1; then - echo "✅ $rule_name: PASSED" | tee -a $GITHUB_STEP_SUMMARY - passed_rules="$passed_rules$rule_name," - else - echo "❌ $rule_name: FAILED" | tee -a $GITHUB_STEP_SUMMARY - failed_rules="$failed_rules$rule_name," - fi + + for json_file in tmp-rules/*.json; do + rule_name=$(basename "$json_file" .json) + echo "Testing $rule_name" + output=$(./qed-prover/target/release/qed-prover "$json_file") + if echo "$output" | jq -e '.provable == true' > /dev/null; then + echo "✅ $rule_name: PASSED" | tee -a $GITHUB_STEP_SUMMARY + passed_rules="$passed_rules$rule_name," + else + echo "❌ $rule_name: FAILED" | tee -a $GITHUB_STEP_SUMMARY + failed_rules="$failed_rules$rule_name," fi done - - # Set outputs for use in other steps/jobs - echo "failed_rules=$failed_rules" >> $GITHUB_OUTPUT - echo "passed_rules=$passed_rules" >> $GITHUB_OUTPUT - - # Fail if any rules failed + if [ -n "$failed_rules" ]; then - echo "::error::Some rules failed verification: ${failed_rules%,}" + echo "::error::Some rules failed: ${failed_rules%,}" exit 1 fi - - - name: Comment PR (if applicable) - if: github.event_name == 'pull_request' && always() - uses: actions/github-script@v7 - with: - script: | - const fs = require('fs'); - const summary = fs.readFileSync(process.env.GITHUB_STEP_SUMMARY, 'utf8'); - - github.rest.issues.createComment({ - issue_number: context.issue.number, - owner: context.repo.owner, - repo: context.repo.repo, - body: `## QED Prover Test Results\n\n${summary}` - }); - + - name: Upload test artifacts - if: always() + if: always() uses: actions/upload-artifact@v4 with: - name: test-results - path: | - rules/*.json - rules/*.result - test-output-*.log \ No newline at end of file + name: rule-json + path: tmp-rules/ From f2a93bac27499f82a4bd4dc460889570ff02ba06 Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 12:45:02 -0700 Subject: [PATCH 10/41] src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java --- .../java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java index 86770be..c67e874 100644 --- a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java +++ b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java @@ -12,7 +12,7 @@ public record FilterIntoJoin() implements RRule { static final RelRN left = RelRN.scan("Left", "Left_Type"); static final RelRN right = RelRN.scan("Right", "Right_Type"); - static final RexRN joinCond = left.joinPred("join", right); + static final RexRN joinCond = left.joinPred("join", right); @Override public RelRN before() { From c33bb3fe9923fc7bf1e770884c94fceb8b2a08ea Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 15:38:17 -0700 Subject: [PATCH 11/41] new workflow --- .github/workflows/test-new-rules.yml | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/.github/workflows/test-new-rules.yml b/.github/workflows/test-new-rules.yml index d6b9123..536375c 100644 --- a/.github/workflows/test-new-rules.yml +++ b/.github/workflows/test-new-rules.yml @@ -29,6 +29,21 @@ jobs: restore-keys: | ${{ runner.os }}-maven- + # Add this step to manually install CVC5 + - name: Install CVC5 dependency + run: | + # Download CVC5 JAR from GitHub releases or other source + wget https://github.com/cvc5/cvc5/releases/download/cvc5-1.2.0/cvc5-1.2.0.jar -O cvc5.jar + + # Install it to local Maven repository + mvn install:install-file \ + -Dfile=cvc5.jar \ + -DgroupId=io.github.cvc5 \ + -DartifactId=cvc5 \ + -Dversion=1.2.1 \ + -Dpackaging=jar \ + -DgeneratePom=true + - name: Build project run: mvn -B compile --file pom.xml @@ -88,7 +103,6 @@ jobs: cd qed-prover cargo build --release - - name: Install jq run: | sudo apt-get update @@ -125,4 +139,4 @@ jobs: uses: actions/upload-artifact@v4 with: name: rule-json - path: tmp-rules/ + path: tmp-rules/ \ No newline at end of file From fc46291834b5f86e150612803813323e83ec80bf Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 15:40:51 -0700 Subject: [PATCH 12/41] new test --- .../java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java index c67e874..86770be 100644 --- a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java +++ b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java @@ -12,7 +12,7 @@ public record FilterIntoJoin() implements RRule { static final RelRN left = RelRN.scan("Left", "Left_Type"); static final RelRN right = RelRN.scan("Right", "Right_Type"); - static final RexRN joinCond = left.joinPred("join", right); + static final RexRN joinCond = left.joinPred("join", right); @Override public RelRN before() { From 71b9eb9a4bb9740b4419b7baf7433cfc80a835a4 Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 15:47:30 -0700 Subject: [PATCH 13/41] updated pom.xml --- pom.xml | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/pom.xml b/pom.xml index ccfa971..d194cc2 100644 --- a/pom.xml +++ b/pom.xml @@ -21,6 +21,7 @@ -classpath org.qed.Main + ${args} @@ -51,11 +52,9 @@ org.apache.maven.plugins maven-compiler-plugin - 23 - 23 - - --enable-preview - + 21 + 21 + --enable-preview @@ -103,9 +102,9 @@ 0.67.0 - io.github.cvc5 + io.github.p-org.solvers cvc5 - 1.2.1 + 0.0.7-v5 org.reflections @@ -113,4 +112,4 @@ 0.10.2 - + \ No newline at end of file From e74cc30c37dc1a344c3dfb349aa2aaaee9d7c694 Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 15:49:18 -0700 Subject: [PATCH 14/41] new test --- .../java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java index 86770be..c67e874 100644 --- a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java +++ b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java @@ -12,7 +12,7 @@ public record FilterIntoJoin() implements RRule { static final RelRN left = RelRN.scan("Left", "Left_Type"); static final RelRN right = RelRN.scan("Right", "Right_Type"); - static final RexRN joinCond = left.joinPred("join", right); + static final RexRN joinCond = left.joinPred("join", right); @Override public RelRN before() { From de4e7ebe63f9a282eddc953e0131dfc88b716e5e Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 15:51:39 -0700 Subject: [PATCH 15/41] new workflow --- .github/workflows/test-new-rules.yml | 18 ++---------------- 1 file changed, 2 insertions(+), 16 deletions(-) diff --git a/.github/workflows/test-new-rules.yml b/.github/workflows/test-new-rules.yml index 536375c..d6b9123 100644 --- a/.github/workflows/test-new-rules.yml +++ b/.github/workflows/test-new-rules.yml @@ -29,21 +29,6 @@ jobs: restore-keys: | ${{ runner.os }}-maven- - # Add this step to manually install CVC5 - - name: Install CVC5 dependency - run: | - # Download CVC5 JAR from GitHub releases or other source - wget https://github.com/cvc5/cvc5/releases/download/cvc5-1.2.0/cvc5-1.2.0.jar -O cvc5.jar - - # Install it to local Maven repository - mvn install:install-file \ - -Dfile=cvc5.jar \ - -DgroupId=io.github.cvc5 \ - -DartifactId=cvc5 \ - -Dversion=1.2.1 \ - -Dpackaging=jar \ - -DgeneratePom=true - - name: Build project run: mvn -B compile --file pom.xml @@ -103,6 +88,7 @@ jobs: cd qed-prover cargo build --release + - name: Install jq run: | sudo apt-get update @@ -139,4 +125,4 @@ jobs: uses: actions/upload-artifact@v4 with: name: rule-json - path: tmp-rules/ \ No newline at end of file + path: tmp-rules/ From 86970480b671c1072ca1b7475db8785f026a6fd0 Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 15:53:30 -0700 Subject: [PATCH 16/41] new test --- .../java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java | 1 + 1 file changed, 1 insertion(+) diff --git a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java index c67e874..7ccfa1c 100644 --- a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java +++ b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java @@ -18,6 +18,7 @@ public record FilterIntoJoin() implements RRule { public RelRN before() { var join = left.join(JoinRelType.INNER, joinCond, right); return join.filter("outer"); + // return join.filter("outer"); } @Override From d7ddac7819dece36cc09b0db4acd463313864daa Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 15:57:03 -0700 Subject: [PATCH 17/41] workflow --- .github/workflows/test-new-rules.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/test-new-rules.yml b/.github/workflows/test-new-rules.yml index d6b9123..5ffc300 100644 --- a/.github/workflows/test-new-rules.yml +++ b/.github/workflows/test-new-rules.yml @@ -18,7 +18,7 @@ jobs: - name: Set up Java uses: actions/setup-java@v4 with: - java-version: '11' + java-version: '21' distribution: 'temurin' - name: Cache Maven dependencies From 62a12dd14d3dd067f98f7cb8141325a7cbbbd2f0 Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 15:57:38 -0700 Subject: [PATCH 18/41] new test --- .../java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java | 1 - 1 file changed, 1 deletion(-) diff --git a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java index 7ccfa1c..c67e874 100644 --- a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java +++ b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java @@ -18,7 +18,6 @@ public record FilterIntoJoin() implements RRule { public RelRN before() { var join = left.join(JoinRelType.INNER, joinCond, right); return join.filter("outer"); - // return join.filter("outer"); } @Override From 6913915e97799818252f8ca5c0e82bf25a199ba5 Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 16:01:43 -0700 Subject: [PATCH 19/41] new workflow --- .github/workflows/test-new-rules.yml | 68 +++++++++++++++++++++++++--- 1 file changed, 62 insertions(+), 6 deletions(-) diff --git a/.github/workflows/test-new-rules.yml b/.github/workflows/test-new-rules.yml index 5ffc300..6e60e8b 100644 --- a/.github/workflows/test-new-rules.yml +++ b/.github/workflows/test-new-rules.yml @@ -29,6 +29,34 @@ jobs: restore-keys: | ${{ runner.os }}-maven- + # Build CVC5 from source with Java bindings + - name: Build and Install CVC5 + run: | + # Install build dependencies + sudo apt-get update + sudo apt-get install -y cmake libgmp-dev python3 python3-pip + + # Clone and build CVC5 + git clone https://github.com/cvc5/cvc5.git + cd cvc5 + ./configure.sh --java-bindings --auto-download --prefix=$PWD/build/install + cd build + make -j$(nproc) + make install + + # Find the built JAR file + CVC5_JAR=$(find install/share/java -name "cvc5*.jar" | grep -v sources | head -1) + echo "Found CVC5 JAR: $CVC5_JAR" + + # Install to Maven local repository + mvn install:install-file \ + -Dfile="$CVC5_JAR" \ + -DgroupId=io.github.cvc5 \ + -DartifactId=cvc5 \ + -Dversion=1.2.1 \ + -Dpackaging=jar \ + -DgeneratePom=true + - name: Build project run: mvn -B compile --file pom.xml @@ -36,9 +64,13 @@ jobs: run: | mkdir -p tmp-rules + # First, ensure all dependencies are downloaded + mvn dependency:resolve + cat > JsonGenerator.java << 'EOF' import org.qed.*; import com.fasterxml.jackson.databind.ObjectMapper; + import com.fasterxml.jackson.databind.node.ObjectNode; import java.nio.file.*; public class JsonGenerator { public static void main(String[] args) throws Exception { @@ -53,9 +85,14 @@ jobs: ObjectMapper mapper = new ObjectMapper(); Files.createDirectories(Path.of("tmp-rules")); String fileName = rule.name() + "-" + rule.info() + ".json"; + + // Get the JSON object + ObjectNode jsonNode = rule.toJson(); + + // Write to file mapper.writerWithDefaultPrettyPrinter().writeValue( Path.of("tmp-rules", fileName).toFile(), - rule.toJson() + jsonNode ); System.out.println("Generated: " + fileName); } catch (Exception e) { @@ -67,16 +104,36 @@ jobs: } EOF - CLASSPATH="target/classes:$(mvn dependency:build-classpath -q -DforceStdout)" + # Build the classpath more reliably + echo "Building classpath..." + MAVEN_CP=$(mvn dependency:build-classpath -Dmdep.outputFile=/dev/stdout -q) + CLASSPATH="target/classes:${MAVEN_CP}" + + echo "Compiling JsonGenerator..." javac -cp "$CLASSPATH" JsonGenerator.java + + if [ $? -ne 0 ]; then + echo "Failed to compile JsonGenerator.java" + echo "Classpath was: $CLASSPATH" + exit 1 + fi + echo "Finding rule files..." find src/main/java/org/qed/Generated/RRuleInstances -name '*.java' | while read file; do className=$(echo "$file" | sed 's|src/main/java/||; s|/|.|g; s|\.java$||') - echo "Generating for: $className" - java -cp ".:$CLASSPATH" JsonGenerator "$className" + echo "Generating JSON for: $className" + java -cp ".:$CLASSPATH" JsonGenerator "$className" || echo "Failed to process $className" done rm -f JsonGenerator.java JsonGenerator.class + + # Check if any JSON files were generated + if [ ! "$(ls -A tmp-rules)" ]; then + echo "Error: No JSON files were generated!" + exit 1 + fi + + echo "Generated $(ls -1 tmp-rules/*.json | wc -l) JSON files" - name: Install Rust and clone qed-prover run: | @@ -88,7 +145,6 @@ jobs: cd qed-prover cargo build --release - - name: Install jq run: | sudo apt-get update @@ -125,4 +181,4 @@ jobs: uses: actions/upload-artifact@v4 with: name: rule-json - path: tmp-rules/ + path: tmp-rules/ \ No newline at end of file From f5a43838edd43148d95de37711feb945dc03f571 Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 16:03:23 -0700 Subject: [PATCH 20/41] new test --- .../java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java | 1 + 1 file changed, 1 insertion(+) diff --git a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java index c67e874..473fca1 100644 --- a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java +++ b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java @@ -17,6 +17,7 @@ public record FilterIntoJoin() implements RRule { @Override public RelRN before() { var join = left.join(JoinRelType.INNER, joinCond, right); + // return join.filter("outer"); return join.filter("outer"); } From 8ead6a74fd94e5218b278998b69f2340559a9b70 Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 17:02:38 -0700 Subject: [PATCH 21/41] new workflow --- .github/workflows/test-new-rules.yml | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/.github/workflows/test-new-rules.yml b/.github/workflows/test-new-rules.yml index 6e60e8b..7e2d126 100644 --- a/.github/workflows/test-new-rules.yml +++ b/.github/workflows/test-new-rules.yml @@ -139,11 +139,18 @@ jobs: run: | sudo apt-get update sudo apt-get install -y curl git - curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y + + # Install Rust with nightly toolchain + curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain nightly source $HOME/.cargo/env + + # Verify we're using nightly + rustc --version + + # Clone and build qed-prover git clone https://github.com/qed-solver/prover.git qed-prover cd qed-prover - cargo build --release + cargo +nightly build --release - name: Install jq run: | From 5c00f9e1f178fff8741edaf87a69f2df37e45c9d Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 17:03:01 -0700 Subject: [PATCH 22/41] new test --- .../java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java | 1 - 1 file changed, 1 deletion(-) diff --git a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java index 473fca1..c67e874 100644 --- a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java +++ b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java @@ -17,7 +17,6 @@ public record FilterIntoJoin() implements RRule { @Override public RelRN before() { var join = left.join(JoinRelType.INNER, joinCond, right); - // return join.filter("outer"); return join.filter("outer"); } From 5b56bc6c8f8325104d0a70989b35f7f62bf4d11e Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 17:37:14 -0700 Subject: [PATCH 23/41] new workflow --- .github/workflows/test-new-rules.yml | 51 +++++++++++++++++++++++----- 1 file changed, 42 insertions(+), 9 deletions(-) diff --git a/.github/workflows/test-new-rules.yml b/.github/workflows/test-new-rules.yml index 7e2d126..a6fff7e 100644 --- a/.github/workflows/test-new-rules.yml +++ b/.github/workflows/test-new-rules.yml @@ -152,10 +152,10 @@ jobs: cd qed-prover cargo +nightly build --release - - name: Install jq + - name: Install jq and z3 run: | sudo apt-get update - sudo apt-get install -y jq + sudo apt-get install -y jq z3 - name: Test all rules run: | @@ -164,20 +164,51 @@ jobs: failed_rules="" passed_rules="" + total_count=0 + passed_count=0 for json_file in tmp-rules/*.json; do + if [ ! -f "$json_file" ]; then + continue + fi + rule_name=$(basename "$json_file" .json) echo "Testing $rule_name" - output=$(./qed-prover/target/release/qed-prover "$json_file") - if echo "$output" | jq -e '.provable == true' > /dev/null; then - echo "✅ $rule_name: PASSED" | tee -a $GITHUB_STEP_SUMMARY - passed_rules="$passed_rules$rule_name," + total_count=$((total_count + 1)) + + # Run the prover - it creates a .result file + ./qed-prover/target/release/qed-prover "$json_file" || true + + # Check if the result file was created + result_file="${json_file%.json}.result" + if [ -f "$result_file" ]; then + # Parse the result file + if jq -e '.provable == true' "$result_file" > /dev/null 2>&1; then + echo "✅ $rule_name: PASSED" | tee -a $GITHUB_STEP_SUMMARY + passed_rules="$passed_rules$rule_name," + passed_count=$((passed_count + 1)) + else + # Check if it panicked or just failed to prove + panicked=$(jq -r '.panicked // false' "$result_file") + if [ "$panicked" = "true" ]; then + echo "❌ $rule_name: PANICKED" | tee -a $GITHUB_STEP_SUMMARY + else + echo "❌ $rule_name: FAILED TO PROVE" | tee -a $GITHUB_STEP_SUMMARY + fi + failed_rules="$failed_rules$rule_name," + fi else - echo "❌ $rule_name: FAILED" | tee -a $GITHUB_STEP_SUMMARY + echo "❌ $rule_name: NO RESULT FILE GENERATED" | tee -a $GITHUB_STEP_SUMMARY failed_rules="$failed_rules$rule_name," fi done + echo "" >> $GITHUB_STEP_SUMMARY + echo "### Summary" >> $GITHUB_STEP_SUMMARY + echo "- Total rules tested: $total_count" >> $GITHUB_STEP_SUMMARY + echo "- Passed: $passed_count" >> $GITHUB_STEP_SUMMARY + echo "- Failed: $((total_count - passed_count))" >> $GITHUB_STEP_SUMMARY + if [ -n "$failed_rules" ]; then echo "::error::Some rules failed: ${failed_rules%,}" exit 1 @@ -187,5 +218,7 @@ jobs: if: always() uses: actions/upload-artifact@v4 with: - name: rule-json - path: tmp-rules/ \ No newline at end of file + name: rule-test-results + path: | + tmp-rules/*.json + tmp-rules/*.result \ No newline at end of file From 440de538b41befd5a97c5b8a9c02166445f52ae9 Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 17:37:36 -0700 Subject: [PATCH 24/41] new test --- .../java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java | 1 + 1 file changed, 1 insertion(+) diff --git a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java index c67e874..473fca1 100644 --- a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java +++ b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java @@ -17,6 +17,7 @@ public record FilterIntoJoin() implements RRule { @Override public RelRN before() { var join = left.join(JoinRelType.INNER, joinCond, right); + // return join.filter("outer"); return join.filter("outer"); } From 3b82055503b498a829f324383e3e7fddae8c0383 Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 18:06:22 -0700 Subject: [PATCH 25/41] new test --- .github/workflows/test-new-rules.yml | 153 +++--------------- .../RRuleInstances/FilterIntoJoin.java | 1 - 2 files changed, 25 insertions(+), 129 deletions(-) diff --git a/.github/workflows/test-new-rules.yml b/.github/workflows/test-new-rules.yml index a6fff7e..e22af70 100644 --- a/.github/workflows/test-new-rules.yml +++ b/.github/workflows/test-new-rules.yml @@ -2,11 +2,7 @@ name: Test All Rules on: push: - paths: - - 'src/main/java/org/qed/Generated/RRuleInstances/**/*.java' pull_request: - paths: - - 'src/main/java/org/qed/Generated/RRuleInstances/**/*.java' jobs: test-all-rules: @@ -29,42 +25,12 @@ jobs: restore-keys: | ${{ runner.os }}-maven- - # Build CVC5 from source with Java bindings - - name: Build and Install CVC5 - run: | - # Install build dependencies - sudo apt-get update - sudo apt-get install -y cmake libgmp-dev python3 python3-pip - - # Clone and build CVC5 - git clone https://github.com/cvc5/cvc5.git - cd cvc5 - ./configure.sh --java-bindings --auto-download --prefix=$PWD/build/install - cd build - make -j$(nproc) - make install - - # Find the built JAR file - CVC5_JAR=$(find install/share/java -name "cvc5*.jar" | grep -v sources | head -1) - echo "Found CVC5 JAR: $CVC5_JAR" - - # Install to Maven local repository - mvn install:install-file \ - -Dfile="$CVC5_JAR" \ - -DgroupId=io.github.cvc5 \ - -DartifactId=cvc5 \ - -Dversion=1.2.1 \ - -Dpackaging=jar \ - -DgeneratePom=true - - name: Build project run: mvn -B compile --file pom.xml - name: Generate JSON for all rules run: | mkdir -p tmp-rules - - # First, ensure all dependencies are downloaded mvn dependency:resolve cat > JsonGenerator.java << 'EOF' @@ -74,143 +40,76 @@ jobs: import java.nio.file.*; public class JsonGenerator { public static void main(String[] args) throws Exception { - if (args.length == 0) { - System.err.println("Usage: java JsonGenerator "); - System.exit(1); - } String className = args[0]; - try { - Class clazz = Class.forName(className); - RRule rule = (RRule) clazz.getDeclaredConstructor().newInstance(); - ObjectMapper mapper = new ObjectMapper(); - Files.createDirectories(Path.of("tmp-rules")); - String fileName = rule.name() + "-" + rule.info() + ".json"; - - // Get the JSON object - ObjectNode jsonNode = rule.toJson(); - - // Write to file - mapper.writerWithDefaultPrettyPrinter().writeValue( - Path.of("tmp-rules", fileName).toFile(), - jsonNode - ); - System.out.println("Generated: " + fileName); - } catch (Exception e) { - System.err.println("Failed to generate JSON for " + className); - e.printStackTrace(); - System.exit(1); - } + Class clazz = Class.forName(className); + RRule rule = (RRule) clazz.getDeclaredConstructor().newInstance(); + ObjectMapper mapper = new ObjectMapper(); + String fileName = rule.name() + "-" + rule.info() + ".json"; + ObjectNode jsonNode = rule.toJson(); + mapper.writerWithDefaultPrettyPrinter().writeValue( + Path.of("tmp-rules", fileName).toFile(), + jsonNode + ); } } EOF - # Build the classpath more reliably - echo "Building classpath..." MAVEN_CP=$(mvn dependency:build-classpath -Dmdep.outputFile=/dev/stdout -q) CLASSPATH="target/classes:${MAVEN_CP}" - - echo "Compiling JsonGenerator..." javac -cp "$CLASSPATH" JsonGenerator.java - - if [ $? -ne 0 ]; then - echo "Failed to compile JsonGenerator.java" - echo "Classpath was: $CLASSPATH" - exit 1 - fi - echo "Finding rule files..." find src/main/java/org/qed/Generated/RRuleInstances -name '*.java' | while read file; do className=$(echo "$file" | sed 's|src/main/java/||; s|/|.|g; s|\.java$||') - echo "Generating JSON for: $className" - java -cp ".:$CLASSPATH" JsonGenerator "$className" || echo "Failed to process $className" + java -cp ".:$CLASSPATH" JsonGenerator "$className" done rm -f JsonGenerator.java JsonGenerator.class - - # Check if any JSON files were generated - if [ ! "$(ls -A tmp-rules)" ]; then - echo "Error: No JSON files were generated!" - exit 1 - fi - - echo "Generated $(ls -1 tmp-rules/*.json | wc -l) JSON files" - - name: Install Rust and clone qed-prover + - name: Install dependencies run: | sudo apt-get update - sudo apt-get install -y curl git - - # Install Rust with nightly toolchain + sudo apt-get install -y jq z3 + wget https://github.com/cvc5/cvc5/releases/download/cvc5-1.1.2/cvc5-Linux-x86_64 -O cvc5 + chmod +x cvc5 + sudo mv cvc5 /usr/local/bin/ + + - name: Build qed-prover + run: | curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain nightly source $HOME/.cargo/env - - # Verify we're using nightly - rustc --version - - # Clone and build qed-prover git clone https://github.com/qed-solver/prover.git qed-prover cd qed-prover cargo +nightly build --release - - name: Install jq and z3 - run: | - sudo apt-get update - sudo apt-get install -y jq z3 - - name: Test all rules run: | echo "## QED Prover Test Results" >> $GITHUB_STEP_SUMMARY echo "" >> $GITHUB_STEP_SUMMARY failed_rules="" - passed_rules="" total_count=0 passed_count=0 for json_file in tmp-rules/*.json; do - if [ ! -f "$json_file" ]; then - continue - fi - rule_name=$(basename "$json_file" .json) - echo "Testing $rule_name" total_count=$((total_count + 1)) - - # Run the prover - it creates a .result file ./qed-prover/target/release/qed-prover "$json_file" || true - # Check if the result file was created result_file="${json_file%.json}.result" - if [ -f "$result_file" ]; then - # Parse the result file - if jq -e '.provable == true' "$result_file" > /dev/null 2>&1; then - echo "✅ $rule_name: PASSED" | tee -a $GITHUB_STEP_SUMMARY - passed_rules="$passed_rules$rule_name," - passed_count=$((passed_count + 1)) - else - # Check if it panicked or just failed to prove - panicked=$(jq -r '.panicked // false' "$result_file") - if [ "$panicked" = "true" ]; then - echo "❌ $rule_name: PANICKED" | tee -a $GITHUB_STEP_SUMMARY - else - echo "❌ $rule_name: FAILED TO PROVE" | tee -a $GITHUB_STEP_SUMMARY - fi - failed_rules="$failed_rules$rule_name," - fi + if [ -f "$result_file" ] && jq -e '.provable == true' "$result_file" > /dev/null 2>&1; then + echo "✅ $rule_name: PASSED" >> $GITHUB_STEP_SUMMARY + passed_count=$((passed_count + 1)) else - echo "❌ $rule_name: NO RESULT FILE GENERATED" | tee -a $GITHUB_STEP_SUMMARY + echo "❌ $rule_name: FAILED" >> $GITHUB_STEP_SUMMARY failed_rules="$failed_rules$rule_name," fi done echo "" >> $GITHUB_STEP_SUMMARY - echo "### Summary" >> $GITHUB_STEP_SUMMARY - echo "- Total rules tested: $total_count" >> $GITHUB_STEP_SUMMARY - echo "- Passed: $passed_count" >> $GITHUB_STEP_SUMMARY - echo "- Failed: $((total_count - passed_count))" >> $GITHUB_STEP_SUMMARY + echo "**Summary:** $passed_count/$total_count passed" >> $GITHUB_STEP_SUMMARY if [ -n "$failed_rules" ]; then - echo "::error::Some rules failed: ${failed_rules%,}" + echo "::error::Failed rules: ${failed_rules%,}" exit 1 fi @@ -219,6 +118,4 @@ jobs: uses: actions/upload-artifact@v4 with: name: rule-test-results - path: | - tmp-rules/*.json - tmp-rules/*.result \ No newline at end of file + path: tmp-rules/ \ No newline at end of file diff --git a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java index 473fca1..c67e874 100644 --- a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java +++ b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java @@ -17,7 +17,6 @@ public record FilterIntoJoin() implements RRule { @Override public RelRN before() { var join = left.join(JoinRelType.INNER, joinCond, right); - // return join.filter("outer"); return join.filter("outer"); } From 9f6a48b503b146e4e9bcf402cc462f7495d3e44d Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 18:14:21 -0700 Subject: [PATCH 26/41] new test --- .../java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java index c67e874..dd2159d 100644 --- a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java +++ b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java @@ -22,6 +22,7 @@ public RelRN before() { @Override public RelRN after() { - return left.join(JoinRelType.SEMI, RexRN.and(joinCond, left.joinPred("outer", right)), right); + return left.join( + JoinRelType.SEMI, RexRN.and(joinCond, left.joinPred("outer", right)), right); } } From 7dd23c3f557b547edd507de48bc6480e001022a1 Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 18:17:18 -0700 Subject: [PATCH 27/41] delete join associate temporarily --- .../RRuleInstances/JoinAssociate.java | 69 ------------------- 1 file changed, 69 deletions(-) delete mode 100644 src/main/java/org/qed/Generated/RRuleInstances/JoinAssociate.java diff --git a/src/main/java/org/qed/Generated/RRuleInstances/JoinAssociate.java b/src/main/java/org/qed/Generated/RRuleInstances/JoinAssociate.java deleted file mode 100644 index 059695e..0000000 --- a/src/main/java/org/qed/Generated/RRuleInstances/JoinAssociate.java +++ /dev/null @@ -1,69 +0,0 @@ -package org.qed.Generated.RRuleInstances; - -import kala.collection.Map; -import kala.collection.Seq; -import org.apache.calcite.rel.core.JoinRelType; -import org.apache.calcite.sql.fun.SqlStdOperatorTable; -import org.qed.RelRN; -import org.qed.RexRN; -import org.qed.RRule; -import org.qed.RuleBuilder; - -public record JoinAssociate() implements RRule.RRuleFamily { - static final RelRN a = RelRN.scan("A", "A_Type"); - static final RelRN b = RelRN.scan("B", "B_Type"); - static final RelRN c = RelRN.scan("C", "C_Type"); - static final String pred_ab = "pred_ab"; - static final String pred_bc = "pred_bc"; - static final RelRN.Join.JoinType.MetaJoinType mjt_0 = new RelRN.Join.JoinType.MetaJoinType("mjt_0"); - static final RelRN.Join.JoinType.MetaJoinType mjt_1 = new RelRN.Join.JoinType.MetaJoinType("mjt_1"); - static final RelRN.Join.JoinType.MetaJoinType mjt_2 = new RelRN.Join.JoinType.MetaJoinType("mjt_2"); - static final RelRN.Join.JoinType.MetaJoinType mjt_3 = new RelRN.Join.JoinType.MetaJoinType("mjt_3"); - - static final RelRN before_ab = a.join(mjt_0, RexRN.and( - a.joinPred(pred_ab, b), - new RexRN.JoinField(1, a, b).pred(SqlStdOperatorTable.IS_NOT_NULL) - ), b); - - static final RelRN before = before_ab.join(mjt_1, RexRN.and( - new RexRN.Pred(RuleBuilder.create().genericPredicateOp(pred_bc, true), before_ab.joinFields(c, 1, 2)), - new RexRN.JoinField(1, before_ab, c).pred(SqlStdOperatorTable.IS_NOT_NULL) - ), c); - - static final RelRN after_bc = b.join(mjt_2, RexRN.and( - b.joinPred(pred_bc, c), - new RexRN.JoinField(0, b, c).pred(SqlStdOperatorTable.IS_NOT_NULL) - ), c); - - static final RelRN after = a.join(mjt_3, RexRN.and( - new RexRN.Pred(RuleBuilder.create().genericPredicateOp(pred_ab, true), a.joinFields(after_bc, 0, 1)), - new RexRN.JoinField(1, a, after_bc).pred(SqlStdOperatorTable.IS_NOT_NULL) - ), after_bc); - - static final RRule template = new RRule() { - @Override - public RelRN before() { - return before; - } - - @Override - public RelRN after() { - return after; - } - - @Override - public String name() { - return JoinAssociate.class.getSimpleName(); - } - }; - - static Seq assignments() { - var joinTypes = Seq.of(JoinRelType.INNER, JoinRelType.LEFT, JoinRelType.RIGHT, JoinRelType.FULL).map(RelRN.Join.JoinType.ConcreteJoinType::new); - return joinTypes.flatMap(jt0 -> joinTypes.flatMap(jt1 -> joinTypes.flatMap(jt2 -> joinTypes.map(jt3 -> new RRule.RRuleGenerator.MetaAssignment(Map.of(mjt_0, jt0, mjt_1, jt1, mjt_2, jt2, mjt_3, jt3)))))); - } - - @Override - public Seq family() { - return new RRule.RRuleGenerator(template, assignments()).family(); - } -} From c878388e6c224dc631b7c609947012f92d02ead8 Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 18:24:54 -0700 Subject: [PATCH 28/41] new test --- .github/workflows/test-new-rules.yml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/.github/workflows/test-new-rules.yml b/.github/workflows/test-new-rules.yml index e22af70..44a4b8c 100644 --- a/.github/workflows/test-new-rules.yml +++ b/.github/workflows/test-new-rules.yml @@ -69,9 +69,10 @@ jobs: run: | sudo apt-get update sudo apt-get install -y jq z3 - wget https://github.com/cvc5/cvc5/releases/download/cvc5-1.1.2/cvc5-Linux-x86_64 -O cvc5 - chmod +x cvc5 - sudo mv cvc5 /usr/local/bin/ + wget https://github.com/cvc5/cvc5/releases/download/cvc5-1.2.1/cvc5-1.2.1-Linux-x86_64-static.zip + unzip cvc5-1.2.1-Linux-x86_64-static.zip + chmod +x cvc5-1.2.1/bin/cvc5 + sudo mv cvc5-1.2.1/bin/cvc5 /usr/local/bin/ - name: Build qed-prover run: | From e3047974349b023f096d8d78a60bfa0b9ab764b8 Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 18:27:39 -0700 Subject: [PATCH 29/41] new test --- .github/workflows/test-new-rules.yml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/workflows/test-new-rules.yml b/.github/workflows/test-new-rules.yml index 44a4b8c..ec38f1a 100644 --- a/.github/workflows/test-new-rules.yml +++ b/.github/workflows/test-new-rules.yml @@ -69,10 +69,10 @@ jobs: run: | sudo apt-get update sudo apt-get install -y jq z3 - wget https://github.com/cvc5/cvc5/releases/download/cvc5-1.2.1/cvc5-1.2.1-Linux-x86_64-static.zip - unzip cvc5-1.2.1-Linux-x86_64-static.zip - chmod +x cvc5-1.2.1/bin/cvc5 - sudo mv cvc5-1.2.1/bin/cvc5 /usr/local/bin/ + wget https://github.com/cvc5/cvc5/releases/download/cvc5-1.2.1/cvc5-Linux-x86_64-static.zip + unzip cvc5-Linux-x86_64-static.zip + chmod +x cvc5/bin/cvc5 + sudo mv cvc5/bin/cvc5 /usr/local/bin/ - name: Build qed-prover run: | From 5a39e4edbc40cd0c8b3c26c14671eb9394e1672d Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 18:31:36 -0700 Subject: [PATCH 30/41] new test --- .github/workflows/test-new-rules.yml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/.github/workflows/test-new-rules.yml b/.github/workflows/test-new-rules.yml index ec38f1a..d8cafc7 100644 --- a/.github/workflows/test-new-rules.yml +++ b/.github/workflows/test-new-rules.yml @@ -68,11 +68,13 @@ jobs: - name: Install dependencies run: | sudo apt-get update - sudo apt-get install -y jq z3 - wget https://github.com/cvc5/cvc5/releases/download/cvc5-1.2.1/cvc5-Linux-x86_64-static.zip - unzip cvc5-Linux-x86_64-static.zip - chmod +x cvc5/bin/cvc5 - sudo mv cvc5/bin/cvc5 /usr/local/bin/ + sudo apt-get install -y jq z3 cmake libgmp-dev + git clone --depth 1 --branch cvc5-1.2.1 https://github.com/cvc5/cvc5.git + cd cvc5 + ./configure.sh --auto-download + cd build + make -j$(nproc) cvc5 + sudo cp bin/cvc5 /usr/local/bin/ - name: Build qed-prover run: | From 36c6c46a3a59b1404e477e0a6cf30950f0798595 Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 18:46:44 -0700 Subject: [PATCH 31/41] new test --- .github/workflows/test-new-rules.yml | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/.github/workflows/test-new-rules.yml b/.github/workflows/test-new-rules.yml index d8cafc7..6eac450 100644 --- a/.github/workflows/test-new-rules.yml +++ b/.github/workflows/test-new-rules.yml @@ -68,13 +68,17 @@ jobs: - name: Install dependencies run: | sudo apt-get update - sudo apt-get install -y jq z3 cmake libgmp-dev - git clone --depth 1 --branch cvc5-1.2.1 https://github.com/cvc5/cvc5.git - cd cvc5 - ./configure.sh --auto-download - cd build - make -j$(nproc) cvc5 - sudo cp bin/cvc5 /usr/local/bin/ + sudo apt-get install -y jq z3 + # Try to install cvc5 from package manager first, otherwise build from source + sudo apt-get install -y cvc5 || ( + sudo apt-get install -y cmake libgmp-dev && + git clone --depth 1 https://github.com/cvc5/cvc5.git && + cd cvc5 && + ./configure.sh --auto-download && + cd build && + make -j$(nproc) && + sudo make install + ) - name: Build qed-prover run: | From 06677975c94880b2fea3d83ee6464f4a63905fd3 Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 19:55:40 -0700 Subject: [PATCH 32/41] restore FilterIntoJoin.java --- .../java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java index dd2159d..92517fc 100644 --- a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java +++ b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java @@ -22,7 +22,6 @@ public RelRN before() { @Override public RelRN after() { - return left.join( - JoinRelType.SEMI, RexRN.and(joinCond, left.joinPred("outer", right)), right); + return left.join(JoinRelType.INNER, RexRN.and(joinCond, left.joinPred("outer", right)), right); } } From e164dda67d2a09be660c11e1ac3b561b2dba1e98 Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 20:03:59 -0700 Subject: [PATCH 33/41] update test.yml --- .github/workflows/{test-new-rules.yml => test.yml} | 6 +++++- .../org/qed/Generated/RRuleInstances/FilterIntoJoin.java | 2 +- 2 files changed, 6 insertions(+), 2 deletions(-) rename .github/workflows/{test-new-rules.yml => test.yml} (96%) diff --git a/.github/workflows/test-new-rules.yml b/.github/workflows/test.yml similarity index 96% rename from .github/workflows/test-new-rules.yml rename to .github/workflows/test.yml index 6eac450..d0c3032 100644 --- a/.github/workflows/test-new-rules.yml +++ b/.github/workflows/test.yml @@ -2,7 +2,11 @@ name: Test All Rules on: push: + paths: + - 'src/main/java/org/qed/Generated/RRuleInstances/**/*.java' pull_request: + paths: + - 'src/main/java/org/qed/Generated/RRuleInstances/**/*.java' jobs: test-all-rules: @@ -124,5 +128,5 @@ jobs: if: always() uses: actions/upload-artifact@v4 with: - name: rule-test-results + name: results path: tmp-rules/ \ No newline at end of file diff --git a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java index 92517fc..24165aa 100644 --- a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java +++ b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java @@ -12,7 +12,7 @@ public record FilterIntoJoin() implements RRule { static final RelRN left = RelRN.scan("Left", "Left_Type"); static final RelRN right = RelRN.scan("Right", "Right_Type"); - static final RexRN joinCond = left.joinPred("join", right); + static final RexRN joinCond = left.joinPred("join", right); @Override public RelRN before() { From a25c7dda707946c1c7e8e2c40ee55f09c55155ef Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 22:53:20 -0700 Subject: [PATCH 34/41] delete unprovable rules --- .../Generated/RRuleInstances/JoinCommute.java | 28 ------------------- .../RRuleInstances/SemiJoinJoinTranspose.java | 25 ----------------- .../SemiJoinProjectTranspose.java | 23 --------------- .../RRuleInstances/SemiJoinRemove.java | 21 -------------- 4 files changed, 97 deletions(-) delete mode 100644 src/main/java/org/qed/Generated/RRuleInstances/JoinCommute.java delete mode 100644 src/main/java/org/qed/Generated/RRuleInstances/SemiJoinJoinTranspose.java delete mode 100644 src/main/java/org/qed/Generated/RRuleInstances/SemiJoinProjectTranspose.java delete mode 100644 src/main/java/org/qed/Generated/RRuleInstances/SemiJoinRemove.java diff --git a/src/main/java/org/qed/Generated/RRuleInstances/JoinCommute.java b/src/main/java/org/qed/Generated/RRuleInstances/JoinCommute.java deleted file mode 100644 index 22f2344..0000000 --- a/src/main/java/org/qed/Generated/RRuleInstances/JoinCommute.java +++ /dev/null @@ -1,28 +0,0 @@ -package org.qed.Generated.RRuleInstances; - -import kala.collection.Map; -import kala.collection.Seq; -import org.apache.calcite.rel.core.JoinRelType; -import org.apache.calcite.sql.fun.SqlStdOperatorTable; -import org.qed.RelRN; -import org.qed.RexRN; -import org.qed.RRule; -import org.qed.RuleBuilder; - -public record JoinCommute() implements RRule { - static final RelRN left = RelRN.scan("Left", "Left_Type"); - static final RelRN right = RelRN.scan("Right", "Right_Type"); - static final RexRN joinCond = left.joinPred("pred", right); - - @Override - public RelRN before() { - return left.join(JoinRelType.INNER, joinCond, right); - } - - @Override - public RelRN after() { - // We need to swap the join fields in the condition - RexRN commutedJoinCond = right.joinPred("pred", left); - return right.join(JoinRelType.INNER, commutedJoinCond, left); - } -} diff --git a/src/main/java/org/qed/Generated/RRuleInstances/SemiJoinJoinTranspose.java b/src/main/java/org/qed/Generated/RRuleInstances/SemiJoinJoinTranspose.java deleted file mode 100644 index b1a4a3d..0000000 --- a/src/main/java/org/qed/Generated/RRuleInstances/SemiJoinJoinTranspose.java +++ /dev/null @@ -1,25 +0,0 @@ -package org.qed.Generated.RRuleInstances; - -import org.apache.calcite.rel.core.JoinRelType; -import org.qed.RRule; -import org.qed.RelRN; -import org.qed.RexRN; - - -public record SemiJoinJoinTranspose() implements RRule { - static final RelRN left = RelRN.scan("left", "left_Type"); - static final RelRN middle = RelRN.scan("middle", "middle_Type"); - static final RelRN right = RelRN.scan("right", "right_Type"); - static final RexRN semiCond = left.joinPred("semi", middle); - static final RexRN joinCond = left.joinPred("join", right); - - @Override - public RelRN before() { - return left.join(JoinRelType.INNER, joinCond, right).join(JoinRelType.SEMI, semiCond, middle); - } - - @Override - public RelRN after() { - return left.join(JoinRelType.SEMI, semiCond, middle).join(JoinRelType.INNER, joinCond, right); - } -} diff --git a/src/main/java/org/qed/Generated/RRuleInstances/SemiJoinProjectTranspose.java b/src/main/java/org/qed/Generated/RRuleInstances/SemiJoinProjectTranspose.java deleted file mode 100644 index 71d2dfe..0000000 --- a/src/main/java/org/qed/Generated/RRuleInstances/SemiJoinProjectTranspose.java +++ /dev/null @@ -1,23 +0,0 @@ -package org.qed.Generated.RRuleInstances; - -import org.apache.calcite.rel.core.JoinRelType; -import org.qed.RRule; -import org.qed.RelRN; -import org.qed.RexRN; - -public record SemiJoinProjectTranspose() implements RRule { - static final RelRN left = RelRN.scan("Left", "left_type"); - static final RelRN right = RelRN.scan("Right", "right_type"); - static final RexRN proj = left.proj("proj", "proj_type"); - static final RexRN semiCond = left.joinPred("semi", right); - - @Override - public RelRN before() { - return left.join(JoinRelType.SEMI, semiCond, right).project(proj); - } - - @Override - public RelRN after() { - return left.project(proj).join(JoinRelType.SEMI, semiCond, right); - } -} diff --git a/src/main/java/org/qed/Generated/RRuleInstances/SemiJoinRemove.java b/src/main/java/org/qed/Generated/RRuleInstances/SemiJoinRemove.java deleted file mode 100644 index 3b21e3f..0000000 --- a/src/main/java/org/qed/Generated/RRuleInstances/SemiJoinRemove.java +++ /dev/null @@ -1,21 +0,0 @@ -package org.qed.Generated.RRuleInstances; - -import org.apache.calcite.rel.core.JoinRelType; -import org.qed.RRule; -import org.qed.RelRN; -import org.qed.RexRN; - -public record SemiJoinRemove() implements RRule { - static final RelRN left = RelRN.scan("Left", "Left_Type"); - static final RelRN right = RelRN.scan("Right", "Right_Type"); - - @Override - public RelRN before() { - return left.join(JoinRelType.SEMI, RexRN.trueLiteral(), right); - } - - @Override - public RelRN after() { - return left; - } -} From 7a8640942d163ca90ea5c10b0ff10aa5cd449182 Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 23:19:40 -0700 Subject: [PATCH 35/41] test rule that cannot compile --- .../java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java index 24165aa..8c5212d 100644 --- a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java +++ b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java @@ -10,7 +10,7 @@ import org.qed.RuleBuilder; public record FilterIntoJoin() implements RRule { - static final RelRN left = RelRN.scan("Left", "Left_Type"); + static final RelRN left = RelRN.scan("Left", "Left_Type"; static final RelRN right = RelRN.scan("Right", "Right_Type"); static final RexRN joinCond = left.joinPred("join", right); From 357dcb9a55a963847cb0645c83630bba19122f2f Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 23:33:25 -0700 Subject: [PATCH 36/41] update workflow --- .github/workflows/test.yml | 35 ++------------------------- scripts/generate-rule-json.sh | 45 +++++++++++++++++++++++++++++++++++ 2 files changed, 47 insertions(+), 33 deletions(-) create mode 100644 scripts/generate-rule-json.sh diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index d0c3032..436ed22 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -36,44 +36,13 @@ jobs: run: | mkdir -p tmp-rules mvn dependency:resolve - - cat > JsonGenerator.java << 'EOF' - import org.qed.*; - import com.fasterxml.jackson.databind.ObjectMapper; - import com.fasterxml.jackson.databind.node.ObjectNode; - import java.nio.file.*; - public class JsonGenerator { - public static void main(String[] args) throws Exception { - String className = args[0]; - Class clazz = Class.forName(className); - RRule rule = (RRule) clazz.getDeclaredConstructor().newInstance(); - ObjectMapper mapper = new ObjectMapper(); - String fileName = rule.name() + "-" + rule.info() + ".json"; - ObjectNode jsonNode = rule.toJson(); - mapper.writerWithDefaultPrettyPrinter().writeValue( - Path.of("tmp-rules", fileName).toFile(), - jsonNode - ); - } - } - EOF - - MAVEN_CP=$(mvn dependency:build-classpath -Dmdep.outputFile=/dev/stdout -q) - CLASSPATH="target/classes:${MAVEN_CP}" - javac -cp "$CLASSPATH" JsonGenerator.java - - find src/main/java/org/qed/Generated/RRuleInstances -name '*.java' | while read file; do - className=$(echo "$file" | sed 's|src/main/java/||; s|/|.|g; s|\.java$||') - java -cp ".:$CLASSPATH" JsonGenerator "$className" - done - - rm -f JsonGenerator.java JsonGenerator.class + chmod +x scripts/generate-rule-json.sh + ./scripts/generate-rule-json.sh - name: Install dependencies run: | sudo apt-get update sudo apt-get install -y jq z3 - # Try to install cvc5 from package manager first, otherwise build from source sudo apt-get install -y cvc5 || ( sudo apt-get install -y cmake libgmp-dev && git clone --depth 1 https://github.com/cvc5/cvc5.git && diff --git a/scripts/generate-rule-json.sh b/scripts/generate-rule-json.sh new file mode 100644 index 0000000..a34f5da --- /dev/null +++ b/scripts/generate-rule-json.sh @@ -0,0 +1,45 @@ +#!/bin/bash + +# Script to generate JSON files for all RRule instances + +# Create temporary Java file for JSON generation +cat > JsonGenerator.java << 'EOF' +import org.qed.*; +import com.fasterxml.jackson.databind.ObjectMapper; +import com.fasterxml.jackson.databind.node.ObjectNode; +import java.nio.file.*; + +public class JsonGenerator { + public static void main(String[] args) throws Exception { + String className = args[0]; + Class clazz = Class.forName(className); + RRule rule = (RRule) clazz.getDeclaredConstructor().newInstance(); + ObjectMapper mapper = new ObjectMapper(); + String fileName = rule.name() + "-" + rule.info() + ".json"; + ObjectNode jsonNode = rule.toJson(); + mapper.writerWithDefaultPrettyPrinter().writeValue( + Path.of("tmp-rules", fileName).toFile(), + jsonNode + ); + } +} +EOF + +# Build classpath +MAVEN_CP=$(mvn dependency:build-classpath -Dmdep.outputFile=/dev/stdout -q) +CLASSPATH="target/classes:${MAVEN_CP}" + +# Compile the generator +javac -cp "$CLASSPATH" JsonGenerator.java + +# Generate JSON for each rule +find src/main/java/org/qed/Generated/RRuleInstances -name '*.java' | while read file; do + className=$(echo "$file" | sed 's|src/main/java/||; s|/|.|g; s|\.java$||') + echo "Generating JSON for: $className" + java -cp ".:$CLASSPATH" JsonGenerator "$className" +done + +# Cleanup +rm -f JsonGenerator.java JsonGenerator.class + +echo "JSON generation complete. Files are in tmp-rules/" \ No newline at end of file From 248f0381915d7a272df0b91378d535fca7395c38 Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 23:34:22 -0700 Subject: [PATCH 37/41] restore FilterIntoJoin.java to correct version --- .../java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java index 8c5212d..24165aa 100644 --- a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java +++ b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java @@ -10,7 +10,7 @@ import org.qed.RuleBuilder; public record FilterIntoJoin() implements RRule { - static final RelRN left = RelRN.scan("Left", "Left_Type"; + static final RelRN left = RelRN.scan("Left", "Left_Type"); static final RelRN right = RelRN.scan("Right", "Right_Type"); static final RexRN joinCond = left.joinPred("join", right); From 1257866c0acf07feacc91610f6df4a5443ad1b08 Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 23:53:12 -0700 Subject: [PATCH 38/41] update java version --- .github/workflows/test.yml | 2 +- pom.xml | 9 +++++---- 2 files changed, 6 insertions(+), 5 deletions(-) diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 436ed22..0663ca9 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -18,7 +18,7 @@ jobs: - name: Set up Java uses: actions/setup-java@v4 with: - java-version: '21' + java-version: '23' distribution: 'temurin' - name: Cache Maven dependencies diff --git a/pom.xml b/pom.xml index d194cc2..fd29e81 100644 --- a/pom.xml +++ b/pom.xml @@ -21,7 +21,6 @@ -classpath org.qed.Main - ${args} @@ -52,9 +51,11 @@ org.apache.maven.plugins maven-compiler-plugin - 21 - 21 - --enable-preview + 23 + 23 + + --enable-preview + From a0b066b4ffba4d341c0d8068b4c2bcc2ed5045d8 Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sat, 31 May 2025 23:54:45 -0700 Subject: [PATCH 39/41] test workflow --- .../qed/Generated/RRuleInstances/SemiJoinFilterTranspose.java | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/main/java/org/qed/Generated/RRuleInstances/SemiJoinFilterTranspose.java b/src/main/java/org/qed/Generated/RRuleInstances/SemiJoinFilterTranspose.java index d1bc90e..790c1d2 100644 --- a/src/main/java/org/qed/Generated/RRuleInstances/SemiJoinFilterTranspose.java +++ b/src/main/java/org/qed/Generated/RRuleInstances/SemiJoinFilterTranspose.java @@ -17,13 +17,11 @@ public record SemiJoinFilterTranspose() implements RRule { @Override public RelRN before() { - // Semi-join followed by a filter return left.join(JoinRelType.SEMI, joinCond, right).filter(filterPred); } @Override public RelRN after() { - // Push the filter before the semi-join RelRN leftFiltered = left.filter(filterPred); return leftFiltered.join(JoinRelType.SEMI, leftFiltered.joinPred("join", right), right); } From 2a2e9cebde85f280a4301e61fb36d469d8d0f7c0 Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sun, 1 Jun 2025 00:20:17 -0700 Subject: [PATCH 40/41] update workflow --- .github/workflows/test.yml | 51 ++++----------------------------- scripts/build-qed-prover.sh | 0 scripts/install-dependencies.sh | 17 +++++++++++ scripts/test-rules.sh | 33 +++++++++++++++++++++ 4 files changed, 56 insertions(+), 45 deletions(-) create mode 100644 scripts/build-qed-prover.sh create mode 100644 scripts/install-dependencies.sh create mode 100644 scripts/test-rules.sh diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml index 0663ca9..a1ed0b8 100644 --- a/.github/workflows/test.yml +++ b/.github/workflows/test.yml @@ -41,57 +41,18 @@ jobs: - name: Install dependencies run: | - sudo apt-get update - sudo apt-get install -y jq z3 - sudo apt-get install -y cvc5 || ( - sudo apt-get install -y cmake libgmp-dev && - git clone --depth 1 https://github.com/cvc5/cvc5.git && - cd cvc5 && - ./configure.sh --auto-download && - cd build && - make -j$(nproc) && - sudo make install - ) + chmod +x scripts/install-dependencies.sh + ./scripts/install-dependencies.sh - name: Build qed-prover run: | - curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain nightly - source $HOME/.cargo/env - git clone https://github.com/qed-solver/prover.git qed-prover - cd qed-prover - cargo +nightly build --release + chmod +x scripts/build-qed-prover.sh + ./scripts/build-qed-prover.sh - name: Test all rules run: | - echo "## QED Prover Test Results" >> $GITHUB_STEP_SUMMARY - echo "" >> $GITHUB_STEP_SUMMARY - - failed_rules="" - total_count=0 - passed_count=0 - - for json_file in tmp-rules/*.json; do - rule_name=$(basename "$json_file" .json) - total_count=$((total_count + 1)) - ./qed-prover/target/release/qed-prover "$json_file" || true - - result_file="${json_file%.json}.result" - if [ -f "$result_file" ] && jq -e '.provable == true' "$result_file" > /dev/null 2>&1; then - echo "✅ $rule_name: PASSED" >> $GITHUB_STEP_SUMMARY - passed_count=$((passed_count + 1)) - else - echo "❌ $rule_name: FAILED" >> $GITHUB_STEP_SUMMARY - failed_rules="$failed_rules$rule_name," - fi - done - - echo "" >> $GITHUB_STEP_SUMMARY - echo "**Summary:** $passed_count/$total_count passed" >> $GITHUB_STEP_SUMMARY - - if [ -n "$failed_rules" ]; then - echo "::error::Failed rules: ${failed_rules%,}" - exit 1 - fi + chmod +x scripts/test-rules.sh + ./scripts/test-rules.sh - name: Upload test artifacts if: always() diff --git a/scripts/build-qed-prover.sh b/scripts/build-qed-prover.sh new file mode 100644 index 0000000..e69de29 diff --git a/scripts/install-dependencies.sh b/scripts/install-dependencies.sh new file mode 100644 index 0000000..500879f --- /dev/null +++ b/scripts/install-dependencies.sh @@ -0,0 +1,17 @@ +#!/bin/bash + +# Install required dependencies for qed-prover + +sudo apt-get update +sudo apt-get install -y jq z3 + +# Install cvc5 - try package manager first, otherwise build from source +sudo apt-get install -y cvc5 || ( + sudo apt-get install -y cmake libgmp-dev && + git clone --depth 1 https://github.com/cvc5/cvc5.git && + cd cvc5 && + ./configure.sh --auto-download && + cd build && + make -j$(nproc) && + sudo make install +) \ No newline at end of file diff --git a/scripts/test-rules.sh b/scripts/test-rules.sh new file mode 100644 index 0000000..5dc149b --- /dev/null +++ b/scripts/test-rules.sh @@ -0,0 +1,33 @@ +#!/bin/bash + +# Test all generated rules with qed-prover + +echo "## QED Prover Test Results" >> $GITHUB_STEP_SUMMARY +echo "" >> $GITHUB_STEP_SUMMARY + +failed_rules="" +total_count=0 +passed_count=0 + +for json_file in tmp-rules/*.json; do + rule_name=$(basename "$json_file" .json) + total_count=$((total_count + 1)) + ./qed-prover/target/release/qed-prover "$json_file" || true + + result_file="${json_file%.json}.result" + if [ -f "$result_file" ] && jq -e '.provable == true' "$result_file" > /dev/null 2>&1; then + echo "✅ $rule_name: PASSED" >> $GITHUB_STEP_SUMMARY + passed_count=$((passed_count + 1)) + else + echo "❌ $rule_name: FAILED" >> $GITHUB_STEP_SUMMARY + failed_rules="$failed_rules$rule_name," + fi +done + +echo "" >> $GITHUB_STEP_SUMMARY +echo "**Summary:** $passed_count/$total_count passed" >> $GITHUB_STEP_SUMMARY + +if [ -n "$failed_rules" ]; then + echo "::error::Failed rules: ${failed_rules%,}" + exit 1 +fi \ No newline at end of file From d21779efe88739c0b688edbad9b44f7a907e4d80 Mon Sep 17 00:00:00 2001 From: zengzirong <122090719@link.cuhk.edu.cn> Date: Sun, 1 Jun 2025 00:43:15 -0700 Subject: [PATCH 41/41] new update --- scripts/build-qed-prover.sh | 10 +++ .../JoinAssociate.java | 69 +++++++++++++++++++ .../JoinCommute.java | 28 ++++++++ .../SemiJoinJoinTranspose.java | 25 +++++++ .../SemiJoinProjectTranspose.java | 23 +++++++ .../SemiJoinRemove.java | 21 ++++++ .../RRuleInstances/FilterIntoJoin.java | 2 +- 7 files changed, 177 insertions(+), 1 deletion(-) create mode 100644 src/main/java/org/qed/Generated/RRuleInstances-unprovable/JoinAssociate.java create mode 100644 src/main/java/org/qed/Generated/RRuleInstances-unprovable/JoinCommute.java create mode 100644 src/main/java/org/qed/Generated/RRuleInstances-unprovable/SemiJoinJoinTranspose.java create mode 100644 src/main/java/org/qed/Generated/RRuleInstances-unprovable/SemiJoinProjectTranspose.java create mode 100644 src/main/java/org/qed/Generated/RRuleInstances-unprovable/SemiJoinRemove.java diff --git a/scripts/build-qed-prover.sh b/scripts/build-qed-prover.sh index e69de29..10fe4b0 100644 --- a/scripts/build-qed-prover.sh +++ b/scripts/build-qed-prover.sh @@ -0,0 +1,10 @@ +#!/bin/bash + +# Build qed-prover with Rust nightly + +curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -s -- -y --default-toolchain nightly +source $HOME/.cargo/env + +git clone https://github.com/qed-solver/prover.git qed-prover +cd qed-prover +cargo +nightly build --release \ No newline at end of file diff --git a/src/main/java/org/qed/Generated/RRuleInstances-unprovable/JoinAssociate.java b/src/main/java/org/qed/Generated/RRuleInstances-unprovable/JoinAssociate.java new file mode 100644 index 0000000..059695e --- /dev/null +++ b/src/main/java/org/qed/Generated/RRuleInstances-unprovable/JoinAssociate.java @@ -0,0 +1,69 @@ +package org.qed.Generated.RRuleInstances; + +import kala.collection.Map; +import kala.collection.Seq; +import org.apache.calcite.rel.core.JoinRelType; +import org.apache.calcite.sql.fun.SqlStdOperatorTable; +import org.qed.RelRN; +import org.qed.RexRN; +import org.qed.RRule; +import org.qed.RuleBuilder; + +public record JoinAssociate() implements RRule.RRuleFamily { + static final RelRN a = RelRN.scan("A", "A_Type"); + static final RelRN b = RelRN.scan("B", "B_Type"); + static final RelRN c = RelRN.scan("C", "C_Type"); + static final String pred_ab = "pred_ab"; + static final String pred_bc = "pred_bc"; + static final RelRN.Join.JoinType.MetaJoinType mjt_0 = new RelRN.Join.JoinType.MetaJoinType("mjt_0"); + static final RelRN.Join.JoinType.MetaJoinType mjt_1 = new RelRN.Join.JoinType.MetaJoinType("mjt_1"); + static final RelRN.Join.JoinType.MetaJoinType mjt_2 = new RelRN.Join.JoinType.MetaJoinType("mjt_2"); + static final RelRN.Join.JoinType.MetaJoinType mjt_3 = new RelRN.Join.JoinType.MetaJoinType("mjt_3"); + + static final RelRN before_ab = a.join(mjt_0, RexRN.and( + a.joinPred(pred_ab, b), + new RexRN.JoinField(1, a, b).pred(SqlStdOperatorTable.IS_NOT_NULL) + ), b); + + static final RelRN before = before_ab.join(mjt_1, RexRN.and( + new RexRN.Pred(RuleBuilder.create().genericPredicateOp(pred_bc, true), before_ab.joinFields(c, 1, 2)), + new RexRN.JoinField(1, before_ab, c).pred(SqlStdOperatorTable.IS_NOT_NULL) + ), c); + + static final RelRN after_bc = b.join(mjt_2, RexRN.and( + b.joinPred(pred_bc, c), + new RexRN.JoinField(0, b, c).pred(SqlStdOperatorTable.IS_NOT_NULL) + ), c); + + static final RelRN after = a.join(mjt_3, RexRN.and( + new RexRN.Pred(RuleBuilder.create().genericPredicateOp(pred_ab, true), a.joinFields(after_bc, 0, 1)), + new RexRN.JoinField(1, a, after_bc).pred(SqlStdOperatorTable.IS_NOT_NULL) + ), after_bc); + + static final RRule template = new RRule() { + @Override + public RelRN before() { + return before; + } + + @Override + public RelRN after() { + return after; + } + + @Override + public String name() { + return JoinAssociate.class.getSimpleName(); + } + }; + + static Seq assignments() { + var joinTypes = Seq.of(JoinRelType.INNER, JoinRelType.LEFT, JoinRelType.RIGHT, JoinRelType.FULL).map(RelRN.Join.JoinType.ConcreteJoinType::new); + return joinTypes.flatMap(jt0 -> joinTypes.flatMap(jt1 -> joinTypes.flatMap(jt2 -> joinTypes.map(jt3 -> new RRule.RRuleGenerator.MetaAssignment(Map.of(mjt_0, jt0, mjt_1, jt1, mjt_2, jt2, mjt_3, jt3)))))); + } + + @Override + public Seq family() { + return new RRule.RRuleGenerator(template, assignments()).family(); + } +} diff --git a/src/main/java/org/qed/Generated/RRuleInstances-unprovable/JoinCommute.java b/src/main/java/org/qed/Generated/RRuleInstances-unprovable/JoinCommute.java new file mode 100644 index 0000000..22f2344 --- /dev/null +++ b/src/main/java/org/qed/Generated/RRuleInstances-unprovable/JoinCommute.java @@ -0,0 +1,28 @@ +package org.qed.Generated.RRuleInstances; + +import kala.collection.Map; +import kala.collection.Seq; +import org.apache.calcite.rel.core.JoinRelType; +import org.apache.calcite.sql.fun.SqlStdOperatorTable; +import org.qed.RelRN; +import org.qed.RexRN; +import org.qed.RRule; +import org.qed.RuleBuilder; + +public record JoinCommute() implements RRule { + static final RelRN left = RelRN.scan("Left", "Left_Type"); + static final RelRN right = RelRN.scan("Right", "Right_Type"); + static final RexRN joinCond = left.joinPred("pred", right); + + @Override + public RelRN before() { + return left.join(JoinRelType.INNER, joinCond, right); + } + + @Override + public RelRN after() { + // We need to swap the join fields in the condition + RexRN commutedJoinCond = right.joinPred("pred", left); + return right.join(JoinRelType.INNER, commutedJoinCond, left); + } +} diff --git a/src/main/java/org/qed/Generated/RRuleInstances-unprovable/SemiJoinJoinTranspose.java b/src/main/java/org/qed/Generated/RRuleInstances-unprovable/SemiJoinJoinTranspose.java new file mode 100644 index 0000000..b1a4a3d --- /dev/null +++ b/src/main/java/org/qed/Generated/RRuleInstances-unprovable/SemiJoinJoinTranspose.java @@ -0,0 +1,25 @@ +package org.qed.Generated.RRuleInstances; + +import org.apache.calcite.rel.core.JoinRelType; +import org.qed.RRule; +import org.qed.RelRN; +import org.qed.RexRN; + + +public record SemiJoinJoinTranspose() implements RRule { + static final RelRN left = RelRN.scan("left", "left_Type"); + static final RelRN middle = RelRN.scan("middle", "middle_Type"); + static final RelRN right = RelRN.scan("right", "right_Type"); + static final RexRN semiCond = left.joinPred("semi", middle); + static final RexRN joinCond = left.joinPred("join", right); + + @Override + public RelRN before() { + return left.join(JoinRelType.INNER, joinCond, right).join(JoinRelType.SEMI, semiCond, middle); + } + + @Override + public RelRN after() { + return left.join(JoinRelType.SEMI, semiCond, middle).join(JoinRelType.INNER, joinCond, right); + } +} diff --git a/src/main/java/org/qed/Generated/RRuleInstances-unprovable/SemiJoinProjectTranspose.java b/src/main/java/org/qed/Generated/RRuleInstances-unprovable/SemiJoinProjectTranspose.java new file mode 100644 index 0000000..71d2dfe --- /dev/null +++ b/src/main/java/org/qed/Generated/RRuleInstances-unprovable/SemiJoinProjectTranspose.java @@ -0,0 +1,23 @@ +package org.qed.Generated.RRuleInstances; + +import org.apache.calcite.rel.core.JoinRelType; +import org.qed.RRule; +import org.qed.RelRN; +import org.qed.RexRN; + +public record SemiJoinProjectTranspose() implements RRule { + static final RelRN left = RelRN.scan("Left", "left_type"); + static final RelRN right = RelRN.scan("Right", "right_type"); + static final RexRN proj = left.proj("proj", "proj_type"); + static final RexRN semiCond = left.joinPred("semi", right); + + @Override + public RelRN before() { + return left.join(JoinRelType.SEMI, semiCond, right).project(proj); + } + + @Override + public RelRN after() { + return left.project(proj).join(JoinRelType.SEMI, semiCond, right); + } +} diff --git a/src/main/java/org/qed/Generated/RRuleInstances-unprovable/SemiJoinRemove.java b/src/main/java/org/qed/Generated/RRuleInstances-unprovable/SemiJoinRemove.java new file mode 100644 index 0000000..3b21e3f --- /dev/null +++ b/src/main/java/org/qed/Generated/RRuleInstances-unprovable/SemiJoinRemove.java @@ -0,0 +1,21 @@ +package org.qed.Generated.RRuleInstances; + +import org.apache.calcite.rel.core.JoinRelType; +import org.qed.RRule; +import org.qed.RelRN; +import org.qed.RexRN; + +public record SemiJoinRemove() implements RRule { + static final RelRN left = RelRN.scan("Left", "Left_Type"); + static final RelRN right = RelRN.scan("Right", "Right_Type"); + + @Override + public RelRN before() { + return left.join(JoinRelType.SEMI, RexRN.trueLiteral(), right); + } + + @Override + public RelRN after() { + return left; + } +} diff --git a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java index 24165aa..d16f8ef 100644 --- a/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java +++ b/src/main/java/org/qed/Generated/RRuleInstances/FilterIntoJoin.java @@ -19,7 +19,7 @@ public RelRN before() { var join = left.join(JoinRelType.INNER, joinCond, right); return join.filter("outer"); } - + @Override public RelRN after() { return left.join(JoinRelType.INNER, RexRN.and(joinCond, left.joinPred("outer", right)), right);