Add GitHub Actions workflow to verify rule provability on push/PR

.github/workflows/test.yml

@@ -0,0 +1,62 @@
+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:
+    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/

pom.xml

@@ -103,14 +103,14 @@
             <version>0.67.0</version>
         </dependency>
         <dependency>
-            <groupId>io.github.cvc5</groupId>
+            <groupId>io.github.p-org.solvers</groupId>
             <artifactId>cvc5</artifactId>
-            <version>1.2.1</version>
+            <version>0.0.7-v5</version>
         </dependency>
         <dependency>
             <groupId>org.reflections</groupId>
             <artifactId>reflections</artifactId>
             <version>0.10.2</version>
         </dependency>
     </dependencies>
-</project>
+</project>

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

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/"

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
+)

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

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);

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);
     }