name: Tests

on:
  push:
    branches: [master, refactor]
  pull_request:
    branches: [master]

jobs:
  bdd:
    name: BDD tests
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4

      - name: Install system dependencies
        run: |
          sudo apt-get update
          sudo apt-get install -y g++ make bison flex

      - name: Build CUDD
        working-directory: reactics-bdd
        run: ./build_cudd.sh

      - name: Build ReactICS BDD module
        working-directory: reactics-bdd
        run: make

      - name: Run BDD tests
        run: bash tests/run_tests.sh

  smt:
    name: SMT tests
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4

      - name: Set up Python
        uses: actions/setup-python@v5
        with:
          python-version: "3.12"

      - name: Install Python dependencies
        run: pip install z3-solver pytest

      - name: Run SMT tests
        run: python3 -m pytest tests/test_smt.py -v

  generators:
    name: Generator tests
    runs-on: ubuntu-latest
    needs: bdd
    steps:
      - uses: actions/checkout@v4

      - name: Install system dependencies
        run: |
          sudo apt-get update
          sudo apt-get install -y g++ make bison flex

      - name: Build CUDD
        working-directory: reactics-bdd
        run: ./build_cudd.sh

      - name: Build ReactICS BDD module
        working-directory: reactics-bdd
        run: make

      - name: Set up Python
        uses: actions/setup-python@v5
        with:
          python-version: "3.12"

      - name: Run generator tests
        shell: bash --noprofile --norc {0}
        run: |
          set -uo pipefail
          REACTICS="$PWD/reactics-bdd/reactics"
          GENERATORS="$PWD/examples/bdd/generators"
          passed=0
          failed=0
          check_gen() {
            local name="$1" gen_cmd="$2" property="$3" expected="$4"
            local tmpfile=$(mktemp /tmp/reactics_gen_XXXXXX.drs)
            if ! eval "$gen_cmd" > "$tmpfile" 2>&1; then
              echo "  FAIL: $name (generator crashed)"
              failed=$((failed + 1))
              rm -f "$tmpfile"
              return
            fi
            local result=$("$REACTICS" -c "$property" "$tmpfile" 2>&1 | grep -oE "(holds|does not hold)" || true)
            rm -f "$tmpfile"
            if [ "$result" = "$expected" ]; then
              echo "  PASS: $name"
              passed=$((passed + 1))
            else
              echo "  FAIL: $name (expected '$expected', got '$result')"
              failed=$((failed + 1))
            fi
          }
          check_gen "tgc(3) f1"        "python3 $GENERATORS/gen_tgc.py 3"        f1 "holds"
          check_gen "tgc(3) f3"        "python3 $GENERATORS/gen_tgc.py 3"        f3 "holds"
          check_gen "tgc(4) f2"        "python3 $GENERATORS/gen_tgc.py 4"        f2 "holds"
          check_gen "asm(3) f1"        "python3 $GENERATORS/gen_asm.py 3"        f1 "holds"
          check_gen "asm(3) f2"        "python3 $GENERATORS/gen_asm.py 3"        f2 "holds"
          check_gen "drs(2,2,2,a) f0"  "python3 $GENERATORS/gen_drs.py 2 2 2 a"  f0 "does not hold"
          check_gen "drs(2,2,2,b) f0"  "python3 $GENERATORS/gen_drs.py 2 2 2 b"  f0 "holds"
          echo
          echo "Generator results: $passed passed, $failed failed"
          if [ "$failed" -gt 0 ]; then
            exit 1
          fi