Test yices2 latest release #36
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| name: Test yices2 latest release | |
| on: | |
| schedule: | |
| - cron: '30 1 * * 0' | |
| workflow_dispatch: | |
| permissions: | |
| contents: write | |
| concurrency: | |
| group: solver-${{ github.workflow }} | |
| cancel-in-progress: false | |
| jobs: | |
| yices2_workflow: | |
| runs-on: ubuntu-latest | |
| env: | |
| NUM_TESTS: 1000 | |
| steps: | |
| - name: Checkout code | |
| uses: actions/checkout@v3 | |
| with: | |
| token: ${{ secrets.GITHUB_TOKEN }} | |
| - name: Set up Python and System Dependencies | |
| run: | | |
| sudo apt update | |
| sudo apt install -y ghc cabal-install sqlite3 | |
| python3 -m venv ./venv | |
| source ./venv/bin/activate | |
| pip install poetry | |
| cabal update | |
| cabal install --lib testing-feat | |
| cabal install --lib size-based | |
| - name: Set up Git user | |
| run: | | |
| git config --local user.name "GitHub Actions" | |
| git config --local user.email "actions@github.com" | |
| - name: Clone ET and Install Python Dependencies | |
| run: | | |
| git clone --branch dev https://github.com/wintered/ET.git | |
| cd ET | |
| source ../venv/bin/activate | |
| poetry install | |
| cd .. | |
| - name: Create solver-specific config | |
| run: | | |
| cp ./solvers.cfg ./solvers-yices2.cfg | |
| - name: Check and update solver version | |
| id: check_version | |
| run: | | |
| source venv/bin/activate | |
| pip install -r requirements.txt | |
| python -m yices2-latest.main | |
| - name: Commit and push version changes | |
| run: | | |
| git pull origin main --rebase || git pull origin main || echo "Pull failed, continuing with local changes" | |
| git add ./versions | |
| git commit -m "Update solver version" --only ./versions | |
| git push | |
| - name: Run experiment for each theory | |
| run: | | |
| chmod +x ./scripts/run_exp.sh | |
| chmod +x ./binaries/cvc5-1.2.0 | |
| chmod +x ./binaries/z3-4.8.11 | |
| chmod +x ./binaries/z3-4.13.3 | |
| for theory in $(cat ./supported_theories/yices2); do | |
| ./scripts/run_exp.sh "$theory" "$NUM_TESTS" "./solvers-yices2.cfg" | |
| done | |
| - name: Store experiment results | |
| run: | | |
| chmod +x ./scripts/create_db.sh | |
| for theory in $(cat ./supported_theories/yices2); do | |
| ./scripts/create_db.sh "$theory" | |
| done | |
| - name: Gather statistics | |
| run: | | |
| chmod +x ./scripts/gather_statistics.sh | |
| ./scripts/gather_statistics.sh ./results ./found_bugs/yices2_bugs | |
| - name: Commit unsoundness bugs | |
| if: env.UNSOUNDNESS_FOUND == 'true' | |
| run: | | |
| git add ./found_bugs/yices2_bugs | |
| git commit -m "Add unsoundness bugs" | |
| git push | |
| - name: Fail the action if unsoundness is found | |
| if: env.UNSOUNDNESS_FOUND == 'true' | |
| run: exit 1 |