test.yml

name: Rust

on:
  push:
  pull_request:

env:
  CARGO_TERM_COLOR: always

jobs:
  tests:
    name: Unit Tests
    runs-on: ubuntu-latest
    strategy:
      matrix:
        toolchain:
          - stable

    steps:
    - name: Update Rust to ${{ matrix.toolchain }}
      run: rustup update ${{ matrix.toolchain }} && rustup default ${{ matrix.toolchain }}
    - uses: actions/checkout@v3
    - name: Build
      run: cargo build --verbose
    - name: Run tests
      run: cargo test --verbose

  examples:
    name: Try Examples
    runs-on: ubuntu-latest
    strategy:
      matrix:
        toolchain:
          - stable

    steps:
      - uses: YosysHQ/setup-oss-cad-suite@v2
        with:
          version: '2023-11-15'
      - name: Update Rust to ${{ matrix.toolchain }}
        run: rustup update ${{ matrix.toolchain }} && rustup default ${{ matrix.toolchain }}
      - uses: actions/checkout@v3
      - name: Build
        run: cargo build --verbose --examples --release
      - name: bmc Quiz1
        run: |
          cargo run --release --example bmc -- inputs/chiseltest/Quiz1.btor > Quiz1.wit
          btorsim inputs/chiseltest/Quiz1.btor Quiz1.wit
      - name: bmc Quiz1 (with additional assumption)
        run: |
          cargo run --release --example bmc -- inputs/chiseltest/Quiz1.unsat.btor
      - name: bmc const array example
        run: |
          cargo run --release --example bmc -- inputs/chiseltest/const_array_example.btor > const_array_example.wit
          btorsim inputs/chiseltest/const_array_example.btor const_array_example.wit
      - name: bmc Quiz2
        run: |
          cargo run --release --example bmc -- inputs/chiseltest/Quiz2.sat.btor > Quiz2.sat.wit
          btorsim inputs/chiseltest/Quiz2.sat.btor Quiz2.sat.wit
      - name: bmc Quiz2 (with counter reset value)
        run: |
          cargo run --release --example bmc -- inputs/chiseltest/Quiz2.unsat.btor
      - name: bmc Quiz4
        run: |
          cargo run --release --example bmc -- inputs/chiseltest/Quiz4.sat.btor > Quiz4.sat.wit
          btorsim inputs/chiseltest/Quiz4.sat.btor Quiz4.sat.wit
      - name: bmc Quiz4 (with counter reset value)
        run: |
          cargo run --release --example bmc -- inputs/chiseltest/Quiz4.unsat.btor

  semver:
    name: Check Semantic Versioning
    runs-on: ubuntu-latest

    steps:
      - uses: actions/checkout@v3
      - uses: obi1kenobi/cargo-semver-checks-action@v2

  format:
    name: Check Formatting
    runs-on: ubuntu-latest

    steps:
      - uses: actions/checkout@v3
      - run: cargo fmt --check