Move CI around and run parser on log files

.github/workflows/continuous_integration.yml

@@ -1,24 +1,124 @@
 name: Continuous integration
-on: [push, pull_request]
+on: [push, pull_request, workflow_dispatch]
 
 jobs:
-  test:
+  format:
     runs-on: ubuntu-latest
 
     steps:
-    - uses: actions/checkout@v2
-    - run: cargo test --all
+    - uses: actions/checkout@v4
+    - run: cargo fmt --all -- --check
 
-  format:
+  clippy:
     runs-on: ubuntu-latest
 
     steps:
-    - uses: actions/checkout@v2
-    - run: cargo fmt --all -- --check
+    - uses: actions/checkout@v4
+    - run: cargo clippy --all -- -D warnings
 
-  clippy:
+  test:
+    # will wait for new cache on push to main branch, otherwise will run straight away with existing cache
+    needs: generate_log
+    strategy:
+      matrix:
+        z3version: ['4.8.7', '4.12.2']
+    runs-on: ubuntu-latest
+
+    steps:
+    - uses: actions/checkout@v4
+    - id: configure-z3-id
+      run: echo "z3_v_clean=$(echo "${{ matrix.z3version }}" | sed 's/\./_/g')" >> $GITHUB_OUTPUT
+    - uses: actions/cache/restore@v3
+      with:
+        path: logs_z3_v${{ steps.configure-z3-id.outputs.z3_v_clean }}.tar.bz2
+        key: logs-${{ steps.configure-z3-id.outputs.z3_v_clean }}-${{ github.sha }}
+    - id: extract-cache
+      run: tar -xf "logs_z3_v${{ steps.configure-z3-id.outputs.z3_v_clean }}.tar.bz2"
+    - run: cargo test --all
+
+  generate_log:
+    # only run this job on push to main branch
+    if: (github.event_name == 'push' && github.ref == 'refs/heads/main') || github.event_name == 'workflow_dispatch'
+    strategy: 
+      matrix:
+        z3version: ['4.8.7', '4.12.2']
+
+    # for versions of Z3 at least 4.9.0 we need v1.3 of the GitHub action, for older versions of Z3, 1.2.2
     runs-on: ubuntu-latest
 
     steps:
-    - uses: actions/checkout@v2
-    - run: cargo clippy --all -- -D warnings
+      - uses: actions/checkout@v3 # this copies the whole repository
+        with:
+          fetch-depth: 0 # needed, see GitHub Action "Changed Files"
+
+      - name: Install Z3 for older version 
+        uses: pavpanchekha/[email protected] # see GitHub Action "Install Z3"
+        if: ${{ matrix.z3version == '4.8.7' || matrix.z3version == '4.8.8' || matrix.z3version == '4.8.9' }}
+        with:
+          version: ${{ matrix.z3version }} 
+
+      - name: Install Z3 for newer version 
+        uses: pavpanchekha/[email protected] # see GitHub Action "Install Z3"
+        if: ${{ !(matrix.z3version == '4.8.7' || matrix.z3version == '4.8.8' || matrix.z3version == '4.8.9') }}
+        with:
+          version: ${{ matrix.z3version }} 
+
+      - name: Configure Z3 version environment variable
+        id: configure-z3-id
+        run:
+          echo "z3_v_clean=$(echo "${{ matrix.z3version }}" | sed 's/\./_/g')" >> $GITHUB_OUTPUT
+
+      - name: Cache log files
+        id: cache-log
+        uses: actions/cache@v3
+        with:
+          path: logs_z3_v${{ steps.configure-z3-id.outputs.z3_v_clean }}.tar.bz2
+          key: logs-${{ steps.configure-z3-id.outputs.z3_v_clean }}-${{ github.sha }}
+          restore-keys: |
+            logs-${{ steps.configure-z3-id.outputs.z3_v_clean }}-
+
+      - name: Run Z3 solver on changed smt2 files and compress 
+        id: run_z3_and_upload
+        env:
+          CACHE_FILE: logs_z3_v${{ steps.configure-z3-id.outputs.z3_v_clean }}.tar.bz2
+        run: |
+          # Create the 'logs' directory
+          mkdir logs
+          test -f "${CACHE_FILE}" && tar -xf "${CACHE_FILE}" || echo "No cache"
+
+          # Loop through all files and check that log exists
+          for file in smt-problems/**/*.smt2; do
+              test -f "$file" || break
+              # Get the file hash
+              file_hash=$(shasum -a 256 "$file" | cut -d' ' -f1)
+              # Get the filename without extension
+              base_name=$(basename "${file%.*}")
+              # Log file name
+              log_file_name="logs/${base_name}_fHash_${file_hash}.log"
+              test -f "${log_file_name}" && continue
+
+              rm -f "logs/${base_name}_fHash_*.log"
+              echo "Processing $file to $log_file_name"
+              # Run Z3 solver for the file and save the log in the 'logs' directory, TODO: `proof=true`?
+              z3 trace=true proof=true trace-file-name=${log_file_name} ./$file > /dev/null || echo "!!! Error processing $file"
+          done
+
+          # Compress the 'logs' directory using bzip2
+          echo "Compressing to ${CACHE_FILE}"
+          tar -cjf "${CACHE_FILE}" logs/
+
+      # TODO: not enough permission for this.
+      # - name: Delete old cache
+      #   run: |
+      #     echo "Fetching list of cache key"
+      #     cacheKeys=$(gh cache list -R $REPO | cut -f 1)
+
+      #     ## Setting this to not fail the workflow while deleting cache keys. 
+      #     set +e
+      #     for cacheKey in $cacheKeys; do
+      #         echo "Deleting $cacheKey"
+      #         gh cache delete $cacheKey -R $REPO
+      #     done
+      #   env:
+      #     GH_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+      #     REPO: ${{ github.repository }}

smt-log-parser/src/lib.rs

@@ -6,3 +6,6 @@ pub mod parsers;
 
 /// Pretty printing for items.
 pub mod display_with;
+
+pub use parsers::LogParser;
+pub use parsers::z3::z3parser::Z3Parser;

smt-log-parser/src/parsers/z3/mod.rs

@@ -17,7 +17,7 @@ impl<T: Z3LogParser + Default> LogParser for T {
         first_byte == b'['
     }
 
-    fn process_line(&mut self, line: &str, _line_no: usize) -> bool {
+    fn process_line(&mut self, line: &str, line_no: usize) -> bool {
         // Much faster than `split_whitespace` or `split(' ')` since it works on
         // [u8] instead of [char] and so doesn't need to convert to UTF-8.
         let mut split = line.split_ascii_whitespace();
@@ -52,7 +52,11 @@ impl<T: Z3LogParser + Default> LogParser for T {
             "[conflict]" => self.conflict(split),
             _ => None,
         };
-        parse.unwrap_or_else(|| eprintln!("Error parsing line: {line:?}"));
+        parse.unwrap_or_else(|| if std::env::var("SLP_TEST_MODE").is_ok() {
+            panic!("Error parsing line {line_no}: {line:?}");
+        } else {
+            eprintln!("Error parsing line {line_no}: {line:?}")
+        });
         true
     }
 

smt-log-parser/tests/parse_logs.rs

@@ -0,0 +1,19 @@
+use std::time::Duration;
+
+use smt_log_parser::{LogParser, Z3Parser};
+
+#[test]
+fn parse_all_logs() {
+    std::env::set_var("SLP_TEST_MODE", "true");
+
+    let all_logs = std::fs::read_dir("../logs").unwrap();
+    for log in all_logs {
+        let filename = log.unwrap().path();
+        println!("Parsing {}", filename.display());
+        let (metadata, parser) = Z3Parser::from_file(filename).unwrap();
+        // Gives 10 millis per MB (or 10 secs per GB)
+        let to = Duration::from_millis(500 + (metadata.len() / 100_000));
+        let (timeout, _result) = parser.process_all_timeout(to);
+        assert!(timeout.is_none());
+    }
+}