diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 2270c305..72b3ee85 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -24,6 +24,9 @@ jobs: - name: Run checks run: make check + - name: Run tests + run: make tests + tox: runs-on: ubuntu-latest strategy: diff --git a/.gitignore b/.gitignore index e23048c8..63837ac0 100644 --- a/.gitignore +++ b/.gitignore @@ -170,3 +170,4 @@ cython_debug/ schema_doc.css schema_doc.min.js *.feather +tmp/ diff --git a/.pre-commit-config.yaml b/.pre-commit-config.yaml index dfd47d80..00b06a37 100644 --- a/.pre-commit-config.yaml +++ b/.pre-commit-config.yaml @@ -7,9 +7,9 @@ repos: - id: check-toml - id: check-yaml - id: end-of-file-fixer - exclude: web/content/solver_submission/schema.html + exclude: submissions/.*.json - id: trailing-whitespace - exclude: web/content/solver_submission/schema.html + exclude: submissions/.*.json # - repo: https://github.com/astral-sh/ruff-pre-commit # # Ruff version. diff --git a/Makefile b/Makefile index 0dce426f..e5da41ba 100644 --- a/Makefile +++ b/Makefile @@ -17,13 +17,15 @@ check: ## Run code quality tools. @echo "🚀 Checking for obsolete dependencies: Running deptry" @poetry run deptry . --extend-exclude "archive|_site" -.PHONY: test -test: ## Test the code with pytest +.PHONY: test generation +test: generation ## Test the code with pytest @echo "🚀 Generating submissions/Readme.md" @poetry run python3 submissions/template/generate_Readme.py generate @echo "🚀 Testing code: Running pytest" @poetry run pytest +generation: submission-generation #Generation for the website + .PHONY: build build: clean-build ## Build wheel file using poetry @echo "🚀 Creating wheel file" @@ -42,10 +44,12 @@ help: GENERATED_SCHEMA_FILE=web/content/solver_submission/schema.json GENERATED_SCHEMA_HTML=web/content/solver_submission/schema.html -.PHONY: submission-doc -submission-doc: +.PHONY: submission-doc submission-generation +submission-generation: @echo "🚀 Generating schema to $(GENERATED_SCHEMA_FILE)" @poetry run smtcomp dump-json-schema $(GENERATED_SCHEMA_FILE) + +submission-doc: submission-generation @echo "🚀 Generating html doc to $(GENERATED_SCHEMA_HTML)" @echo " Needs 'pip install json-schema-for-humans'" @poetry run generate-schema-doc --expand-buttons --no-link-to-reused-ref $(GENERATED_SCHEMA_FILE) $(GENERATED_SCHEMA_HTML) diff --git a/README.md b/README.md index ae337b0e..5d767c66 100644 --- a/README.md +++ b/README.md @@ -1,4 +1,4 @@ -# smtcomp +# SMT Competition [![Release](https://img.shields.io/github/v/release/smtcomp/smtcomp.github.io)](https://img.shields.io/github/v/release/smtcomp/smtcomp.github.io) [![Build status](https://img.shields.io/github/actions/workflow/status/smtcomp/smtcomp.github.io/main.yml?branch=main)](https://github.com/smtcomp/smtcomp.github.io/actions/workflows/main.yml?query=branch%3Amain) @@ -17,6 +17,19 @@ Tools used for the organization of the SMT competition git clone git@github.com:smtcomp/smtcomp.github.io.git ``` +On Debian/Ubuntu installation a virtual env (here in .venv) is needed: + +``` +python3 -m venv .venv +source .venv/bin/activate +``` + +Poetry is used for handling dependencies: + +``` +pip install poetry +``` + Finally, install the environment with ```bash @@ -25,7 +38,7 @@ make install ## For starting a new SMT-COMP year -Edit the file `smtcomp/defs.py`, in particular `Config.current_year`, `Logic` for adding new logics and `tracks` for new divisions. +Edit the file `smtcomp/defs.py`, in particular `Config.current_year`, `Logic` for adding new logics and `tracks` for new divisions. Reset `Config.NYSE_seed` to `None`, and set the date the New York Stock Exchange Index will be used in `Config.NYSE_date`. Download the new benchmarks from zenodo, unpack them, unpack the .tar.zst, you should get something like: @@ -56,15 +69,14 @@ $DIR/zenodo Then you can run (very io intensive): ``` -smtcomp $DIR/zenodo ./data/ +smtcomp create-benchmarks-list $DIR/zenodo ./data/ ``` -The directory `./data/` is the one present in this repository +The directory `./data/` is the one present in this repository. -## Using the smtcomp tool for selecting the benchmarks +## Using the `smtcomp` tool for selecting the benchmarks -The list of benchmarks and the previous results are in json which are human -readable, but slow to parse (1min). So locally the tool use the feather format. The +The list of benchmarks and the previous results are in `json` which are human-readable, but slow to parse (1min). So locally the tool use the feather format. The feather files are generated with: ``` @@ -74,7 +86,7 @@ smtcomp create-cache ./data/ Working with the feather files with [polars](https://docs.pola.rs/) is very fast, so no more intermediate files are needed. -However statistics can be shown, for example for the selection of single track: +However, statistics can be shown, for example for the selection of single track: ``` smtcomp show-sq-selection-stats ./data/ 0 @@ -97,7 +109,7 @@ Which outputs: ... ``` -## Using the smtcomp tool for generating benchexec +## Using the `smtcomp` tool for generating `benchexec` configuration #### Generate submissions [Optional] @@ -116,37 +128,37 @@ smtcomp show ../tmp/submissions/YicesQS.json The solver downloaded using: ``` -smtcomp download-archive ../tmp/submissions/*.json ../tmp/benchexec/execution +smtcomp download-archive submissions/*.json ../tmp/execution ``` Trivial tests benchmarks generated with: ``` -smtcomp generate-benchmarks ../tmp/benchexec/includes/ +smtcomp generate-trivial-benchmarks ../tmp/execution/benchmarks ``` The benchexec tasks generated using: ``` -smtcomp generate-benchexec ../tmp/submissions/*.json ../tmp/benchexec/includes/all.xml ../tmp/benchexec/execution +smtcomp generate-benchexec submissions/*.json ../tmp/execution ``` The benchexec execution environment generated using: ``` -smtcomp prepare-execution ../tmp/benchexec/execution +smtcomp prepare-execution ../tmp/execution ``` Benchexec started using: ``` -(cd ../tmp/benchexec/execution; benchexec ../includes/all.xml --read-only-dir / --overlay-dir /home --full-access-dir .. --numOfThreads 8 -M 2GB -c 1) +(cd ../tmp/execution; PYTHONPATH=$(pwd) benchexec SOLVERNAME.xml --read-only-dir / --overlay-dir /home --full-access-dir .. --numOfThreads 8 -M 2GB -c 1) ``` Benchexec in verifier cloud started using: ``` -(cd ../tmp/benchexec/execution; PATH_TO_BENCHEXEC/contrib/vcloud-benchmark.py ../includes/all.xml --read-only-dir / --overlay-dir /home --full-access-dir .. --numOfThreads 8 -M 2GB -c 1 --vcloudMaster VCLOUD_MASTER --vcloudClientHeap 500) +(cd ../tmp/execution; PYTHONPATH=$(pwd) PATH_TO_BENCHEXEC/contrib/vcloud-benchmark.py SOLVERNAME.xml --read-only-dir / --overlay-dir /home --full-access-dir .. --numOfThreads 8 -M 2GB -c 1 --vcloudMaster VCLOUD_MASTER --vcloudClientHeap 500) ``` --- diff --git a/poetry.lock b/poetry.lock index 4c0e2dc6..a6edb43e 100644 --- a/poetry.lock +++ b/poetry.lock @@ -1,14 +1,14 @@ -# This file is automatically @generated by Poetry 1.8.2 and should not be changed by hand. +# This file is automatically @generated by Poetry 1.8.3 and should not be changed by hand. [[package]] name = "annotated-types" -version = "0.6.0" +version = "0.7.0" description = "Reusable constraint types to use with typing.Annotated" optional = false python-versions = ">=3.8" files = [ - {file = "annotated_types-0.6.0-py3-none-any.whl", hash = "sha256:0641064de18ba7a25dee8f96403ebc39113d0cb953a01429249d5c7564666a43"}, - {file = "annotated_types-0.6.0.tar.gz", hash = "sha256:563339e807e53ffd9c267e99fc6d9ea23eb8443c08f112651963e24e22f84a5d"}, + {file = "annotated_types-0.7.0-py3-none-any.whl", hash = "sha256:1f02e8b43a8fbbc3f3e0d4f0f4bfc8131bcb4eebe8849b8e5c773f3a1c582a53"}, + {file = "annotated_types-0.7.0.tar.gz", hash = "sha256:aff07c09a53a08bc8cfccb9c85b05f1aa9a2a6f23728d790723543408344ce89"}, ] [[package]] @@ -86,6 +86,70 @@ files = [ {file = "certifi-2024.2.2.tar.gz", hash = "sha256:0569859f95fc761b18b45ef421b1290a0f65f147e92a1e5eb3e635f9a5e4e66f"}, ] +[[package]] +name = "cffi" +version = "1.16.0" +description = "Foreign Function Interface for Python calling C code." +optional = false +python-versions = ">=3.8" +files = [ + {file = "cffi-1.16.0-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:6b3d6606d369fc1da4fd8c357d026317fbb9c9b75d36dc16e90e84c26854b088"}, + {file = "cffi-1.16.0-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:ac0f5edd2360eea2f1daa9e26a41db02dd4b0451b48f7c318e217ee092a213e9"}, + {file = "cffi-1.16.0-cp310-cp310-manylinux_2_12_i686.manylinux2010_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:7e61e3e4fa664a8588aa25c883eab612a188c725755afff6289454d6362b9673"}, + {file = "cffi-1.16.0-cp310-cp310-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:a72e8961a86d19bdb45851d8f1f08b041ea37d2bd8d4fd19903bc3083d80c896"}, + {file = "cffi-1.16.0-cp310-cp310-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:5b50bf3f55561dac5438f8e70bfcdfd74543fd60df5fa5f62d94e5867deca684"}, + {file = "cffi-1.16.0-cp310-cp310-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:7651c50c8c5ef7bdb41108b7b8c5a83013bfaa8a935590c5d74627c047a583c7"}, + {file = "cffi-1.16.0-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:e4108df7fe9b707191e55f33efbcb2d81928e10cea45527879a4749cbe472614"}, + {file = "cffi-1.16.0-cp310-cp310-musllinux_1_1_i686.whl", hash = "sha256:32c68ef735dbe5857c810328cb2481e24722a59a2003018885514d4c09af9743"}, + {file = "cffi-1.16.0-cp310-cp310-musllinux_1_1_x86_64.whl", hash = "sha256:673739cb539f8cdaa07d92d02efa93c9ccf87e345b9a0b556e3ecc666718468d"}, + {file = "cffi-1.16.0-cp310-cp310-win32.whl", hash = "sha256:9f90389693731ff1f659e55c7d1640e2ec43ff725cc61b04b2f9c6d8d017df6a"}, + {file = "cffi-1.16.0-cp310-cp310-win_amd64.whl", hash = "sha256:e6024675e67af929088fda399b2094574609396b1decb609c55fa58b028a32a1"}, + {file = "cffi-1.16.0-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:b84834d0cf97e7d27dd5b7f3aca7b6e9263c56308ab9dc8aae9784abb774d404"}, + {file = "cffi-1.16.0-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:1b8ebc27c014c59692bb2664c7d13ce7a6e9a629be20e54e7271fa696ff2b417"}, + {file = "cffi-1.16.0-cp311-cp311-manylinux_2_12_i686.manylinux2010_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:ee07e47c12890ef248766a6e55bd38ebfb2bb8edd4142d56db91b21ea68b7627"}, + {file = "cffi-1.16.0-cp311-cp311-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:d8a9d3ebe49f084ad71f9269834ceccbf398253c9fac910c4fd7053ff1386936"}, + {file = "cffi-1.16.0-cp311-cp311-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:e70f54f1796669ef691ca07d046cd81a29cb4deb1e5f942003f401c0c4a2695d"}, + {file = "cffi-1.16.0-cp311-cp311-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:5bf44d66cdf9e893637896c7faa22298baebcd18d1ddb6d2626a6e39793a1d56"}, + {file = "cffi-1.16.0-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:7b78010e7b97fef4bee1e896df8a4bbb6712b7f05b7ef630f9d1da00f6444d2e"}, + {file = "cffi-1.16.0-cp311-cp311-musllinux_1_1_i686.whl", hash = "sha256:c6a164aa47843fb1b01e941d385aab7215563bb8816d80ff3a363a9f8448a8dc"}, + {file = "cffi-1.16.0-cp311-cp311-musllinux_1_1_x86_64.whl", hash = "sha256:e09f3ff613345df5e8c3667da1d918f9149bd623cd9070c983c013792a9a62eb"}, + {file = "cffi-1.16.0-cp311-cp311-win32.whl", hash = "sha256:2c56b361916f390cd758a57f2e16233eb4f64bcbeee88a4881ea90fca14dc6ab"}, + {file = "cffi-1.16.0-cp311-cp311-win_amd64.whl", hash = "sha256:db8e577c19c0fda0beb7e0d4e09e0ba74b1e4c092e0e40bfa12fe05b6f6d75ba"}, + {file = "cffi-1.16.0-cp312-cp312-macosx_10_9_x86_64.whl", hash = "sha256:fa3a0128b152627161ce47201262d3140edb5a5c3da88d73a1b790a959126956"}, + {file = "cffi-1.16.0-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:68e7c44931cc171c54ccb702482e9fc723192e88d25a0e133edd7aff8fcd1f6e"}, + {file = "cffi-1.16.0-cp312-cp312-manylinux_2_12_i686.manylinux2010_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:abd808f9c129ba2beda4cfc53bde801e5bcf9d6e0f22f095e45327c038bfe68e"}, + {file = "cffi-1.16.0-cp312-cp312-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:88e2b3c14bdb32e440be531ade29d3c50a1a59cd4e51b1dd8b0865c54ea5d2e2"}, + {file = "cffi-1.16.0-cp312-cp312-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:fcc8eb6d5902bb1cf6dc4f187ee3ea80a1eba0a89aba40a5cb20a5087d961357"}, + {file = "cffi-1.16.0-cp312-cp312-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:b7be2d771cdba2942e13215c4e340bfd76398e9227ad10402a8767ab1865d2e6"}, + {file = "cffi-1.16.0-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:e715596e683d2ce000574bae5d07bd522c781a822866c20495e52520564f0969"}, + {file = "cffi-1.16.0-cp312-cp312-musllinux_1_1_x86_64.whl", hash = "sha256:2d92b25dbf6cae33f65005baf472d2c245c050b1ce709cc4588cdcdd5495b520"}, + {file = "cffi-1.16.0-cp312-cp312-win32.whl", hash = "sha256:b2ca4e77f9f47c55c194982e10f058db063937845bb2b7a86c84a6cfe0aefa8b"}, + {file = "cffi-1.16.0-cp312-cp312-win_amd64.whl", hash = "sha256:68678abf380b42ce21a5f2abde8efee05c114c2fdb2e9eef2efdb0257fba1235"}, + {file = "cffi-1.16.0-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:0c9ef6ff37e974b73c25eecc13952c55bceed9112be2d9d938ded8e856138bcc"}, + {file = "cffi-1.16.0-cp38-cp38-manylinux_2_12_i686.manylinux2010_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:a09582f178759ee8128d9270cd1344154fd473bb77d94ce0aeb2a93ebf0feaf0"}, + {file = "cffi-1.16.0-cp38-cp38-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:e760191dd42581e023a68b758769e2da259b5d52e3103c6060ddc02c9edb8d7b"}, + {file = "cffi-1.16.0-cp38-cp38-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:80876338e19c951fdfed6198e70bc88f1c9758b94578d5a7c4c91a87af3cf31c"}, + {file = "cffi-1.16.0-cp38-cp38-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:a6a14b17d7e17fa0d207ac08642c8820f84f25ce17a442fd15e27ea18d67c59b"}, + {file = "cffi-1.16.0-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:6602bc8dc6f3a9e02b6c22c4fc1e47aa50f8f8e6d3f78a5e16ac33ef5fefa324"}, + {file = "cffi-1.16.0-cp38-cp38-win32.whl", hash = "sha256:131fd094d1065b19540c3d72594260f118b231090295d8c34e19a7bbcf2e860a"}, + {file = "cffi-1.16.0-cp38-cp38-win_amd64.whl", hash = "sha256:31d13b0f99e0836b7ff893d37af07366ebc90b678b6664c955b54561fc36ef36"}, + {file = "cffi-1.16.0-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:582215a0e9adbe0e379761260553ba11c58943e4bbe9c36430c4ca6ac74b15ed"}, + {file = "cffi-1.16.0-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:b29ebffcf550f9da55bec9e02ad430c992a87e5f512cd63388abb76f1036d8d2"}, + {file = "cffi-1.16.0-cp39-cp39-manylinux_2_12_i686.manylinux2010_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:dc9b18bf40cc75f66f40a7379f6a9513244fe33c0e8aa72e2d56b0196a7ef872"}, + {file = "cffi-1.16.0-cp39-cp39-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:9cb4a35b3642fc5c005a6755a5d17c6c8b6bcb6981baf81cea8bfbc8903e8ba8"}, + {file = "cffi-1.16.0-cp39-cp39-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:b86851a328eedc692acf81fb05444bdf1891747c25af7529e39ddafaf68a4f3f"}, + {file = "cffi-1.16.0-cp39-cp39-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:c0f31130ebc2d37cdd8e44605fb5fa7ad59049298b3f745c74fa74c62fbfcfc4"}, + {file = "cffi-1.16.0-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:8f8e709127c6c77446a8c0a8c8bf3c8ee706a06cd44b1e827c3e6a2ee6b8c098"}, + {file = "cffi-1.16.0-cp39-cp39-musllinux_1_1_i686.whl", hash = "sha256:748dcd1e3d3d7cd5443ef03ce8685043294ad6bd7c02a38d1bd367cfd968e000"}, + {file = "cffi-1.16.0-cp39-cp39-musllinux_1_1_x86_64.whl", hash = "sha256:8895613bcc094d4a1b2dbe179d88d7fb4a15cee43c052e8885783fac397d91fe"}, + {file = "cffi-1.16.0-cp39-cp39-win32.whl", hash = "sha256:ed86a35631f7bfbb28e108dd96773b9d5a6ce4811cf6ea468bb6a359b256b1e4"}, + {file = "cffi-1.16.0-cp39-cp39-win_amd64.whl", hash = "sha256:3686dffb02459559c74dd3d81748269ffb0eb027c39a6fc99502de37d501faa8"}, + {file = "cffi-1.16.0.tar.gz", hash = "sha256:bcb3ef43e58665bbda2fb198698fcae6776483e0c4a631aa5647806c25e02cc0"}, +] + +[package.dependencies] +pycparser = "*" + [[package]] name = "cfgv" version = "3.4.0" @@ -234,68 +298,139 @@ files = [ [[package]] name = "coverage" -version = "7.5.1" +version = "7.5.3" description = "Code coverage measurement for Python" optional = false python-versions = ">=3.8" files = [ - {file = "coverage-7.5.1-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:c0884920835a033b78d1c73b6d3bbcda8161a900f38a488829a83982925f6c2e"}, - {file = "coverage-7.5.1-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:39afcd3d4339329c5f58de48a52f6e4e50f6578dd6099961cf22228feb25f38f"}, - {file = "coverage-7.5.1-cp310-cp310-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:4a7b0ceee8147444347da6a66be737c9d78f3353b0681715b668b72e79203e4a"}, - {file = "coverage-7.5.1-cp310-cp310-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:4a9ca3f2fae0088c3c71d743d85404cec8df9be818a005ea065495bedc33da35"}, - {file = "coverage-7.5.1-cp310-cp310-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:5fd215c0c7d7aab005221608a3c2b46f58c0285a819565887ee0b718c052aa4e"}, - {file = "coverage-7.5.1-cp310-cp310-musllinux_1_1_aarch64.whl", hash = "sha256:4bf0655ab60d754491004a5efd7f9cccefcc1081a74c9ef2da4735d6ee4a6223"}, - {file = "coverage-7.5.1-cp310-cp310-musllinux_1_1_i686.whl", hash = "sha256:61c4bf1ba021817de12b813338c9be9f0ad5b1e781b9b340a6d29fc13e7c1b5e"}, - {file = "coverage-7.5.1-cp310-cp310-musllinux_1_1_x86_64.whl", hash = "sha256:db66fc317a046556a96b453a58eced5024af4582a8dbdc0c23ca4dbc0d5b3146"}, - {file = "coverage-7.5.1-cp310-cp310-win32.whl", hash = "sha256:b016ea6b959d3b9556cb401c55a37547135a587db0115635a443b2ce8f1c7228"}, - {file = "coverage-7.5.1-cp310-cp310-win_amd64.whl", hash = "sha256:df4e745a81c110e7446b1cc8131bf986157770fa405fe90e15e850aaf7619bc8"}, - {file = "coverage-7.5.1-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:796a79f63eca8814ca3317a1ea443645c9ff0d18b188de470ed7ccd45ae79428"}, - {file = "coverage-7.5.1-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:4fc84a37bfd98db31beae3c2748811a3fa72bf2007ff7902f68746d9757f3746"}, - {file = "coverage-7.5.1-cp311-cp311-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:6175d1a0559986c6ee3f7fccfc4a90ecd12ba0a383dcc2da30c2b9918d67d8a3"}, - {file = "coverage-7.5.1-cp311-cp311-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:1fc81d5878cd6274ce971e0a3a18a8803c3fe25457165314271cf78e3aae3aa2"}, - {file = "coverage-7.5.1-cp311-cp311-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:556cf1a7cbc8028cb60e1ff0be806be2eded2daf8129b8811c63e2b9a6c43bca"}, - {file = "coverage-7.5.1-cp311-cp311-musllinux_1_1_aarch64.whl", hash = "sha256:9981706d300c18d8b220995ad22627647be11a4276721c10911e0e9fa44c83e8"}, - {file = "coverage-7.5.1-cp311-cp311-musllinux_1_1_i686.whl", hash = "sha256:d7fed867ee50edf1a0b4a11e8e5d0895150e572af1cd6d315d557758bfa9c057"}, - {file = "coverage-7.5.1-cp311-cp311-musllinux_1_1_x86_64.whl", hash = "sha256:ef48e2707fb320c8f139424a596f5b69955a85b178f15af261bab871873bb987"}, - {file = "coverage-7.5.1-cp311-cp311-win32.whl", hash = "sha256:9314d5678dcc665330df5b69c1e726a0e49b27df0461c08ca12674bcc19ef136"}, - {file = "coverage-7.5.1-cp311-cp311-win_amd64.whl", hash = "sha256:5fa567e99765fe98f4e7d7394ce623e794d7cabb170f2ca2ac5a4174437e90dd"}, - {file = "coverage-7.5.1-cp312-cp312-macosx_10_9_x86_64.whl", hash = "sha256:b6cf3764c030e5338e7f61f95bd21147963cf6aa16e09d2f74f1fa52013c1206"}, - {file = "coverage-7.5.1-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:2ec92012fefebee89a6b9c79bc39051a6cb3891d562b9270ab10ecfdadbc0c34"}, - {file = "coverage-7.5.1-cp312-cp312-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:16db7f26000a07efcf6aea00316f6ac57e7d9a96501e990a36f40c965ec7a95d"}, - {file = "coverage-7.5.1-cp312-cp312-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:beccf7b8a10b09c4ae543582c1319c6df47d78fd732f854ac68d518ee1fb97fa"}, - {file = "coverage-7.5.1-cp312-cp312-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:8748731ad392d736cc9ccac03c9845b13bb07d020a33423fa5b3a36521ac6e4e"}, - {file = "coverage-7.5.1-cp312-cp312-musllinux_1_1_aarch64.whl", hash = "sha256:7352b9161b33fd0b643ccd1f21f3a3908daaddf414f1c6cb9d3a2fd618bf2572"}, - {file = "coverage-7.5.1-cp312-cp312-musllinux_1_1_i686.whl", hash = "sha256:7a588d39e0925f6a2bff87154752481273cdb1736270642aeb3635cb9b4cad07"}, - {file = "coverage-7.5.1-cp312-cp312-musllinux_1_1_x86_64.whl", hash = "sha256:68f962d9b72ce69ea8621f57551b2fa9c70509af757ee3b8105d4f51b92b41a7"}, - {file = "coverage-7.5.1-cp312-cp312-win32.whl", hash = "sha256:f152cbf5b88aaeb836127d920dd0f5e7edff5a66f10c079157306c4343d86c19"}, - {file = "coverage-7.5.1-cp312-cp312-win_amd64.whl", hash = "sha256:5a5740d1fb60ddf268a3811bcd353de34eb56dc24e8f52a7f05ee513b2d4f596"}, - {file = "coverage-7.5.1-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:e2213def81a50519d7cc56ed643c9e93e0247f5bbe0d1247d15fa520814a7cd7"}, - {file = "coverage-7.5.1-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:5037f8fcc2a95b1f0e80585bd9d1ec31068a9bcb157d9750a172836e98bc7a90"}, - {file = "coverage-7.5.1-cp38-cp38-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:5c3721c2c9e4c4953a41a26c14f4cef64330392a6d2d675c8b1db3b645e31f0e"}, - {file = "coverage-7.5.1-cp38-cp38-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:ca498687ca46a62ae590253fba634a1fe9836bc56f626852fb2720f334c9e4e5"}, - {file = "coverage-7.5.1-cp38-cp38-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:0cdcbc320b14c3e5877ee79e649677cb7d89ef588852e9583e6b24c2e5072661"}, - {file = "coverage-7.5.1-cp38-cp38-musllinux_1_1_aarch64.whl", hash = "sha256:57e0204b5b745594e5bc14b9b50006da722827f0b8c776949f1135677e88d0b8"}, - {file = "coverage-7.5.1-cp38-cp38-musllinux_1_1_i686.whl", hash = "sha256:8fe7502616b67b234482c3ce276ff26f39ffe88adca2acf0261df4b8454668b4"}, - {file = "coverage-7.5.1-cp38-cp38-musllinux_1_1_x86_64.whl", hash = "sha256:9e78295f4144f9dacfed4f92935fbe1780021247c2fabf73a819b17f0ccfff8d"}, - {file = "coverage-7.5.1-cp38-cp38-win32.whl", hash = "sha256:1434e088b41594baa71188a17533083eabf5609e8e72f16ce8c186001e6b8c41"}, - {file = "coverage-7.5.1-cp38-cp38-win_amd64.whl", hash = "sha256:0646599e9b139988b63704d704af8e8df7fa4cbc4a1f33df69d97f36cb0a38de"}, - {file = "coverage-7.5.1-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:4cc37def103a2725bc672f84bd939a6fe4522310503207aae4d56351644682f1"}, - {file = "coverage-7.5.1-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:fc0b4d8bfeabd25ea75e94632f5b6e047eef8adaed0c2161ada1e922e7f7cece"}, - {file = "coverage-7.5.1-cp39-cp39-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:0d0a0f5e06881ecedfe6f3dd2f56dcb057b6dbeb3327fd32d4b12854df36bf26"}, - {file = "coverage-7.5.1-cp39-cp39-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:9735317685ba6ec7e3754798c8871c2f49aa5e687cc794a0b1d284b2389d1bd5"}, - {file = "coverage-7.5.1-cp39-cp39-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:d21918e9ef11edf36764b93101e2ae8cc82aa5efdc7c5a4e9c6c35a48496d601"}, - {file = "coverage-7.5.1-cp39-cp39-musllinux_1_1_aarch64.whl", hash = "sha256:c3e757949f268364b96ca894b4c342b41dc6f8f8b66c37878aacef5930db61be"}, - {file = "coverage-7.5.1-cp39-cp39-musllinux_1_1_i686.whl", hash = "sha256:79afb6197e2f7f60c4824dd4b2d4c2ec5801ceb6ba9ce5d2c3080e5660d51a4f"}, - {file = "coverage-7.5.1-cp39-cp39-musllinux_1_1_x86_64.whl", hash = "sha256:d1d0d98d95dd18fe29dc66808e1accf59f037d5716f86a501fc0256455219668"}, - {file = "coverage-7.5.1-cp39-cp39-win32.whl", hash = "sha256:1cc0fe9b0b3a8364093c53b0b4c0c2dd4bb23acbec4c9240b5f284095ccf7981"}, - {file = "coverage-7.5.1-cp39-cp39-win_amd64.whl", hash = "sha256:dde0070c40ea8bb3641e811c1cfbf18e265d024deff6de52c5950677a8fb1e0f"}, - {file = "coverage-7.5.1-pp38.pp39.pp310-none-any.whl", hash = "sha256:6537e7c10cc47c595828b8a8be04c72144725c383c4702703ff4e42e44577312"}, - {file = "coverage-7.5.1.tar.gz", hash = "sha256:54de9ef3a9da981f7af93eafde4ede199e0846cd819eb27c88e2b712aae9708c"}, + {file = "coverage-7.5.3-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:a6519d917abb15e12380406d721e37613e2a67d166f9fb7e5a8ce0375744cd45"}, + {file = "coverage-7.5.3-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:aea7da970f1feccf48be7335f8b2ca64baf9b589d79e05b9397a06696ce1a1ec"}, + {file = "coverage-7.5.3-cp310-cp310-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:923b7b1c717bd0f0f92d862d1ff51d9b2b55dbbd133e05680204465f454bb286"}, + {file = "coverage-7.5.3-cp310-cp310-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:62bda40da1e68898186f274f832ef3e759ce929da9a9fd9fcf265956de269dbc"}, + {file = "coverage-7.5.3-cp310-cp310-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:d8b7339180d00de83e930358223c617cc343dd08e1aa5ec7b06c3a121aec4e1d"}, + {file = "coverage-7.5.3-cp310-cp310-musllinux_1_1_aarch64.whl", hash = "sha256:25a5caf742c6195e08002d3b6c2dd6947e50efc5fc2c2205f61ecb47592d2d83"}, + {file = "coverage-7.5.3-cp310-cp310-musllinux_1_1_i686.whl", hash = "sha256:05ac5f60faa0c704c0f7e6a5cbfd6f02101ed05e0aee4d2822637a9e672c998d"}, + {file = "coverage-7.5.3-cp310-cp310-musllinux_1_1_x86_64.whl", hash = "sha256:239a4e75e09c2b12ea478d28815acf83334d32e722e7433471fbf641c606344c"}, + {file = "coverage-7.5.3-cp310-cp310-win32.whl", hash = "sha256:a5812840d1d00eafae6585aba38021f90a705a25b8216ec7f66aebe5b619fb84"}, + {file = "coverage-7.5.3-cp310-cp310-win_amd64.whl", hash = "sha256:33ca90a0eb29225f195e30684ba4a6db05dbef03c2ccd50b9077714c48153cac"}, + {file = "coverage-7.5.3-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:f81bc26d609bf0fbc622c7122ba6307993c83c795d2d6f6f6fd8c000a770d974"}, + {file = "coverage-7.5.3-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:7cec2af81f9e7569280822be68bd57e51b86d42e59ea30d10ebdbb22d2cb7232"}, + {file = "coverage-7.5.3-cp311-cp311-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:55f689f846661e3f26efa535071775d0483388a1ccfab899df72924805e9e7cd"}, + {file = "coverage-7.5.3-cp311-cp311-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:50084d3516aa263791198913a17354bd1dc627d3c1639209640b9cac3fef5807"}, + {file = "coverage-7.5.3-cp311-cp311-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:341dd8f61c26337c37988345ca5c8ccabeff33093a26953a1ac72e7d0103c4fb"}, + {file = "coverage-7.5.3-cp311-cp311-musllinux_1_1_aarch64.whl", hash = "sha256:ab0b028165eea880af12f66086694768f2c3139b2c31ad5e032c8edbafca6ffc"}, + {file = "coverage-7.5.3-cp311-cp311-musllinux_1_1_i686.whl", hash = "sha256:5bc5a8c87714b0c67cfeb4c7caa82b2d71e8864d1a46aa990b5588fa953673b8"}, + {file = "coverage-7.5.3-cp311-cp311-musllinux_1_1_x86_64.whl", hash = "sha256:38a3b98dae8a7c9057bd91fbf3415c05e700a5114c5f1b5b0ea5f8f429ba6614"}, + {file = "coverage-7.5.3-cp311-cp311-win32.whl", hash = "sha256:fcf7d1d6f5da887ca04302db8e0e0cf56ce9a5e05f202720e49b3e8157ddb9a9"}, + {file = "coverage-7.5.3-cp311-cp311-win_amd64.whl", hash = "sha256:8c836309931839cca658a78a888dab9676b5c988d0dd34ca247f5f3e679f4e7a"}, + {file = "coverage-7.5.3-cp312-cp312-macosx_10_9_x86_64.whl", hash = "sha256:296a7d9bbc598e8744c00f7a6cecf1da9b30ae9ad51c566291ff1314e6cbbed8"}, + {file = "coverage-7.5.3-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:34d6d21d8795a97b14d503dcaf74226ae51eb1f2bd41015d3ef332a24d0a17b3"}, + {file = "coverage-7.5.3-cp312-cp312-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:8e317953bb4c074c06c798a11dbdd2cf9979dbcaa8ccc0fa4701d80042d4ebf1"}, + {file = "coverage-7.5.3-cp312-cp312-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:705f3d7c2b098c40f5b81790a5fedb274113373d4d1a69e65f8b68b0cc26f6db"}, + {file = "coverage-7.5.3-cp312-cp312-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:b1196e13c45e327d6cd0b6e471530a1882f1017eb83c6229fc613cd1a11b53cd"}, + {file = "coverage-7.5.3-cp312-cp312-musllinux_1_1_aarch64.whl", hash = "sha256:015eddc5ccd5364dcb902eaecf9515636806fa1e0d5bef5769d06d0f31b54523"}, + {file = "coverage-7.5.3-cp312-cp312-musllinux_1_1_i686.whl", hash = "sha256:fd27d8b49e574e50caa65196d908f80e4dff64d7e592d0c59788b45aad7e8b35"}, + {file = "coverage-7.5.3-cp312-cp312-musllinux_1_1_x86_64.whl", hash = "sha256:33fc65740267222fc02975c061eb7167185fef4cc8f2770267ee8bf7d6a42f84"}, + {file = "coverage-7.5.3-cp312-cp312-win32.whl", hash = "sha256:7b2a19e13dfb5c8e145c7a6ea959485ee8e2204699903c88c7d25283584bfc08"}, + {file = "coverage-7.5.3-cp312-cp312-win_amd64.whl", hash = "sha256:0bbddc54bbacfc09b3edaec644d4ac90c08ee8ed4844b0f86227dcda2d428fcb"}, + {file = "coverage-7.5.3-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:f78300789a708ac1f17e134593f577407d52d0417305435b134805c4fb135adb"}, + {file = "coverage-7.5.3-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:b368e1aee1b9b75757942d44d7598dcd22a9dbb126affcbba82d15917f0cc155"}, + {file = "coverage-7.5.3-cp38-cp38-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:f836c174c3a7f639bded48ec913f348c4761cbf49de4a20a956d3431a7c9cb24"}, + {file = "coverage-7.5.3-cp38-cp38-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:244f509f126dc71369393ce5fea17c0592c40ee44e607b6d855e9c4ac57aac98"}, + {file = "coverage-7.5.3-cp38-cp38-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:c4c2872b3c91f9baa836147ca33650dc5c172e9273c808c3c3199c75490e709d"}, + {file = "coverage-7.5.3-cp38-cp38-musllinux_1_1_aarch64.whl", hash = "sha256:dd4b3355b01273a56b20c219e74e7549e14370b31a4ffe42706a8cda91f19f6d"}, + {file = "coverage-7.5.3-cp38-cp38-musllinux_1_1_i686.whl", hash = "sha256:f542287b1489c7a860d43a7d8883e27ca62ab84ca53c965d11dac1d3a1fab7ce"}, + {file = "coverage-7.5.3-cp38-cp38-musllinux_1_1_x86_64.whl", hash = "sha256:75e3f4e86804023e991096b29e147e635f5e2568f77883a1e6eed74512659ab0"}, + {file = "coverage-7.5.3-cp38-cp38-win32.whl", hash = "sha256:c59d2ad092dc0551d9f79d9d44d005c945ba95832a6798f98f9216ede3d5f485"}, + {file = "coverage-7.5.3-cp38-cp38-win_amd64.whl", hash = "sha256:fa21a04112c59ad54f69d80e376f7f9d0f5f9123ab87ecd18fbb9ec3a2beed56"}, + {file = "coverage-7.5.3-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:f5102a92855d518b0996eb197772f5ac2a527c0ec617124ad5242a3af5e25f85"}, + {file = "coverage-7.5.3-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:d1da0a2e3b37b745a2b2a678a4c796462cf753aebf94edcc87dcc6b8641eae31"}, + {file = "coverage-7.5.3-cp39-cp39-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:8383a6c8cefba1b7cecc0149415046b6fc38836295bc4c84e820872eb5478b3d"}, + {file = "coverage-7.5.3-cp39-cp39-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:9aad68c3f2566dfae84bf46295a79e79d904e1c21ccfc66de88cd446f8686341"}, + {file = "coverage-7.5.3-cp39-cp39-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:2e079c9ec772fedbade9d7ebc36202a1d9ef7291bc9b3a024ca395c4d52853d7"}, + {file = "coverage-7.5.3-cp39-cp39-musllinux_1_1_aarch64.whl", hash = "sha256:bde997cac85fcac227b27d4fb2c7608a2c5f6558469b0eb704c5726ae49e1c52"}, + {file = "coverage-7.5.3-cp39-cp39-musllinux_1_1_i686.whl", hash = "sha256:990fb20b32990b2ce2c5f974c3e738c9358b2735bc05075d50a6f36721b8f303"}, + {file = "coverage-7.5.3-cp39-cp39-musllinux_1_1_x86_64.whl", hash = "sha256:3d5a67f0da401e105753d474369ab034c7bae51a4c31c77d94030d59e41df5bd"}, + {file = "coverage-7.5.3-cp39-cp39-win32.whl", hash = "sha256:e08c470c2eb01977d221fd87495b44867a56d4d594f43739a8028f8646a51e0d"}, + {file = "coverage-7.5.3-cp39-cp39-win_amd64.whl", hash = "sha256:1d2a830ade66d3563bb61d1e3c77c8def97b30ed91e166c67d0632c018f380f0"}, + {file = "coverage-7.5.3-pp38.pp39.pp310-none-any.whl", hash = "sha256:3538d8fb1ee9bdd2e2692b3b18c22bb1c19ffbefd06880f5ac496e42d7bb3884"}, + {file = "coverage-7.5.3.tar.gz", hash = "sha256:04aefca5190d1dc7a53a4c1a5a7f8568811306d7a8ee231c42fb69215571944f"}, ] [package.extras] toml = ["tomli"] +[[package]] +name = "cryptography" +version = "42.0.7" +description = "cryptography is a package which provides cryptographic recipes and primitives to Python developers." +optional = false +python-versions = ">=3.7" +files = [ + {file = "cryptography-42.0.7-cp37-abi3-macosx_10_12_universal2.whl", hash = "sha256:a987f840718078212fdf4504d0fd4c6effe34a7e4740378e59d47696e8dfb477"}, + {file = "cryptography-42.0.7-cp37-abi3-macosx_10_12_x86_64.whl", hash = "sha256:bd13b5e9b543532453de08bcdc3cc7cebec6f9883e886fd20a92f26940fd3e7a"}, + {file = "cryptography-42.0.7-cp37-abi3-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:a79165431551042cc9d1d90e6145d5d0d3ab0f2d66326c201d9b0e7f5bf43604"}, + {file = "cryptography-42.0.7-cp37-abi3-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:a47787a5e3649008a1102d3df55424e86606c9bae6fb77ac59afe06d234605f8"}, + {file = "cryptography-42.0.7-cp37-abi3-manylinux_2_28_aarch64.whl", hash = "sha256:02c0eee2d7133bdbbc5e24441258d5d2244beb31da5ed19fbb80315f4bbbff55"}, + {file = "cryptography-42.0.7-cp37-abi3-manylinux_2_28_x86_64.whl", hash = "sha256:5e44507bf8d14b36b8389b226665d597bc0f18ea035d75b4e53c7b1ea84583cc"}, + {file = "cryptography-42.0.7-cp37-abi3-musllinux_1_1_aarch64.whl", hash = "sha256:7f8b25fa616d8b846aef64b15c606bb0828dbc35faf90566eb139aa9cff67af2"}, + {file = "cryptography-42.0.7-cp37-abi3-musllinux_1_1_x86_64.whl", hash = "sha256:93a3209f6bb2b33e725ed08ee0991b92976dfdcf4e8b38646540674fc7508e13"}, + {file = "cryptography-42.0.7-cp37-abi3-musllinux_1_2_aarch64.whl", hash = "sha256:e6b8f1881dac458c34778d0a424ae5769de30544fc678eac51c1c8bb2183e9da"}, + {file = "cryptography-42.0.7-cp37-abi3-musllinux_1_2_x86_64.whl", hash = "sha256:3de9a45d3b2b7d8088c3fbf1ed4395dfeff79d07842217b38df14ef09ce1d8d7"}, + {file = "cryptography-42.0.7-cp37-abi3-win32.whl", hash = "sha256:789caea816c6704f63f6241a519bfa347f72fbd67ba28d04636b7c6b7da94b0b"}, + {file = "cryptography-42.0.7-cp37-abi3-win_amd64.whl", hash = "sha256:8cb8ce7c3347fcf9446f201dc30e2d5a3c898d009126010cbd1f443f28b52678"}, + {file = "cryptography-42.0.7-cp39-abi3-macosx_10_12_universal2.whl", hash = "sha256:a3a5ac8b56fe37f3125e5b72b61dcde43283e5370827f5233893d461b7360cd4"}, + {file = "cryptography-42.0.7-cp39-abi3-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:779245e13b9a6638df14641d029add5dc17edbef6ec915688f3acb9e720a5858"}, + {file = "cryptography-42.0.7-cp39-abi3-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:0d563795db98b4cd57742a78a288cdbdc9daedac29f2239793071fe114f13785"}, + {file = "cryptography-42.0.7-cp39-abi3-manylinux_2_28_aarch64.whl", hash = "sha256:31adb7d06fe4383226c3e963471f6837742889b3c4caa55aac20ad951bc8ffda"}, + {file = "cryptography-42.0.7-cp39-abi3-manylinux_2_28_x86_64.whl", hash = "sha256:efd0bf5205240182e0f13bcaea41be4fdf5c22c5129fc7ced4a0282ac86998c9"}, + {file = "cryptography-42.0.7-cp39-abi3-musllinux_1_1_aarch64.whl", hash = "sha256:a9bc127cdc4ecf87a5ea22a2556cab6c7eda2923f84e4f3cc588e8470ce4e42e"}, + {file = "cryptography-42.0.7-cp39-abi3-musllinux_1_1_x86_64.whl", hash = "sha256:3577d029bc3f4827dd5bf8bf7710cac13527b470bbf1820a3f394adb38ed7d5f"}, + {file = "cryptography-42.0.7-cp39-abi3-musllinux_1_2_aarch64.whl", hash = "sha256:2e47577f9b18723fa294b0ea9a17d5e53a227867a0a4904a1a076d1646d45ca1"}, + {file = "cryptography-42.0.7-cp39-abi3-musllinux_1_2_x86_64.whl", hash = "sha256:1a58839984d9cb34c855197043eaae2c187d930ca6d644612843b4fe8513c886"}, + {file = "cryptography-42.0.7-cp39-abi3-win32.whl", hash = "sha256:e6b79d0adb01aae87e8a44c2b64bc3f3fe59515280e00fb6d57a7267a2583cda"}, + {file = "cryptography-42.0.7-cp39-abi3-win_amd64.whl", hash = "sha256:16268d46086bb8ad5bf0a2b5544d8a9ed87a0e33f5e77dd3c3301e63d941a83b"}, + {file = "cryptography-42.0.7-pp310-pypy310_pp73-macosx_10_12_x86_64.whl", hash = "sha256:2954fccea107026512b15afb4aa664a5640cd0af630e2ee3962f2602693f0c82"}, + {file = "cryptography-42.0.7-pp310-pypy310_pp73-manylinux_2_28_aarch64.whl", hash = "sha256:362e7197754c231797ec45ee081f3088a27a47c6c01eff2ac83f60f85a50fe60"}, + {file = "cryptography-42.0.7-pp310-pypy310_pp73-manylinux_2_28_x86_64.whl", hash = "sha256:4f698edacf9c9e0371112792558d2f705b5645076cc0aaae02f816a0171770fd"}, + {file = "cryptography-42.0.7-pp310-pypy310_pp73-win_amd64.whl", hash = "sha256:5482e789294854c28237bba77c4c83be698be740e31a3ae5e879ee5444166582"}, + {file = "cryptography-42.0.7-pp39-pypy39_pp73-macosx_10_12_x86_64.whl", hash = "sha256:e9b2a6309f14c0497f348d08a065d52f3020656f675819fc405fb63bbcd26562"}, + {file = "cryptography-42.0.7-pp39-pypy39_pp73-manylinux_2_28_aarch64.whl", hash = "sha256:d8e3098721b84392ee45af2dd554c947c32cc52f862b6a3ae982dbb90f577f14"}, + {file = "cryptography-42.0.7-pp39-pypy39_pp73-manylinux_2_28_x86_64.whl", hash = "sha256:c65f96dad14f8528a447414125e1fc8feb2ad5a272b8f68477abbcc1ea7d94b9"}, + {file = "cryptography-42.0.7-pp39-pypy39_pp73-win_amd64.whl", hash = "sha256:36017400817987670037fbb0324d71489b6ead6231c9604f8fc1f7d008087c68"}, + {file = "cryptography-42.0.7.tar.gz", hash = "sha256:ecbfbc00bf55888edda9868a4cf927205de8499e7fabe6c050322298382953f2"}, +] + +[package.dependencies] +cffi = {version = ">=1.12", markers = "platform_python_implementation != \"PyPy\""} + +[package.extras] +docs = ["sphinx (>=5.3.0)", "sphinx-rtd-theme (>=1.1.1)"] +docstest = ["pyenchant (>=1.6.11)", "readme-renderer", "sphinxcontrib-spelling (>=4.0.1)"] +nox = ["nox"] +pep8test = ["check-sdist", "click", "mypy", "ruff"] +sdist = ["build"] +ssh = ["bcrypt (>=3.1.5)"] +test = ["certifi", "pretend", "pytest (>=6.2.0)", "pytest-benchmark", "pytest-cov", "pytest-xdist"] +test-randomorder = ["pytest-randomly"] + +[[package]] +name = "deprecated" +version = "1.2.14" +description = "Python @deprecated decorator to deprecate old python classes, functions or methods." +optional = false +python-versions = ">=2.7, !=3.0.*, !=3.1.*, !=3.2.*, !=3.3.*" +files = [ + {file = "Deprecated-1.2.14-py2.py3-none-any.whl", hash = "sha256:6fac8b097794a90302bdbb17b9b815e732d3c4720583ff1b198499d78470466c"}, + {file = "Deprecated-1.2.14.tar.gz", hash = "sha256:e5323eb936458dccc2582dc6f9c322c852a775a27065ff2b0c4970b9d53d01b3"}, +] + +[package.dependencies] +wrapt = ">=1.10,<2" + +[package.extras] +dev = ["PyTest", "PyTest-Cov", "bump2version (<1)", "sphinx (<2)", "tox"] + [[package]] name = "deptry" version = "0.12.0" @@ -537,18 +672,15 @@ files = [ [[package]] name = "nodeenv" -version = "1.8.0" +version = "1.9.0" description = "Node.js virtual environment builder" optional = false -python-versions = ">=2.7,!=3.0.*,!=3.1.*,!=3.2.*,!=3.3.*,!=3.4.*,!=3.5.*,!=3.6.*" +python-versions = "!=3.0.*,!=3.1.*,!=3.2.*,!=3.3.*,!=3.4.*,!=3.5.*,!=3.6.*,>=2.7" files = [ - {file = "nodeenv-1.8.0-py2.py3-none-any.whl", hash = "sha256:df865724bb3c3adc86b3876fa209771517b0cfe596beff01a92700e0e8be4cec"}, - {file = "nodeenv-1.8.0.tar.gz", hash = "sha256:d51e0c37e64fbf47d017feac3145cdbb58836d7eee8c6f6d3b6880c5456227d2"}, + {file = "nodeenv-1.9.0-py2.py3-none-any.whl", hash = "sha256:508ecec98f9f3330b636d4448c0f1a56fc68017c68f1e7857ebc52acf0eb879a"}, + {file = "nodeenv-1.9.0.tar.gz", hash = "sha256:07f144e90dae547bf0d4ee8da0ee42664a42a04e02ed68e06324348dafe4bdb1"}, ] -[package.dependencies] -setuptools = "*" - [[package]] name = "option" version = "2.1.0" @@ -584,13 +716,13 @@ files = [ [[package]] name = "platformdirs" -version = "4.2.1" +version = "4.2.2" description = "A small Python package for determining appropriate platform-specific dirs, e.g. a `user data dir`." optional = false python-versions = ">=3.8" files = [ - {file = "platformdirs-4.2.1-py3-none-any.whl", hash = "sha256:17d5a1161b3fd67b390023cb2d3b026bbd40abde6fdb052dfbd3a29c3ba22ee1"}, - {file = "platformdirs-4.2.1.tar.gz", hash = "sha256:031cd18d4ec63ec53e82dceaac0417d218a6863f7745dfcc9efe7793b7039bdf"}, + {file = "platformdirs-4.2.2-py3-none-any.whl", hash = "sha256:2d7a1657e36a80ea911db832a8a6ece5ee53d8de21edd5cc5879af6530b1bfee"}, + {file = "platformdirs-4.2.2.tar.gz", hash = "sha256:38b7b51f512eed9e84a22788b4bce1de17c0adb134d6becb09836e37d8654cd3"}, ] [package.extras] @@ -615,22 +747,22 @@ testing = ["pytest", "pytest-benchmark"] [[package]] name = "polars" -version = "0.20.26" +version = "0.20.30" description = "Blazingly fast DataFrame library" optional = false python-versions = ">=3.8" files = [ - {file = "polars-0.20.26-cp38-abi3-macosx_10_12_x86_64.whl", hash = "sha256:97d0e4b6ab6b47fa07798b447189ee9505d2085ec1a64a6aa8a65fdd429cd49f"}, - {file = "polars-0.20.26-cp38-abi3-macosx_11_0_arm64.whl", hash = "sha256:c270e366b4d8b672b204e7d48e39d255641d3d2b7bdc3a0ccd968cf53934657f"}, - {file = "polars-0.20.26-cp38-abi3-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:db35d6eed508256a797c7f1b8e9dec4aae9c11b891797b2d38fac5627d072d34"}, - {file = "polars-0.20.26-cp38-abi3-manylinux_2_24_aarch64.whl", hash = "sha256:25b00bd5cf44929722aa6389706559c5e8cedd6db2cfc38b27b706ed37e1b2af"}, - {file = "polars-0.20.26-cp38-abi3-win_amd64.whl", hash = "sha256:b22063acc815bc5c6d2e24292ff771ca0df306ecf97e8f6899924a1ec6d3f136"}, - {file = "polars-0.20.26.tar.gz", hash = "sha256:fa83d130562a5180a47f8763a7bb9f408dbbf51eafc1380e8a2951be8ce05a2c"}, + {file = "polars-0.20.30-cp38-abi3-macosx_10_12_x86_64.whl", hash = "sha256:7802cb8a6d3fa0fadf446bf19b61ef8450b81229766f1817980bc6e0b2488c03"}, + {file = "polars-0.20.30-cp38-abi3-macosx_11_0_arm64.whl", hash = "sha256:0d7278f6e12e6623c8ee6e637d866b96b69f960b358125c955ac76abeb942192"}, + {file = "polars-0.20.30-cp38-abi3-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:510f708332a0e0d563a5bac266c11ccd12932606c7331bf28f7173cf669d0c69"}, + {file = "polars-0.20.30-cp38-abi3-manylinux_2_24_aarch64.whl", hash = "sha256:70d58b89cf9902fb5c3506afef76c5c2b247581d0991b082bcdc6d73d983aa2b"}, + {file = "polars-0.20.30-cp38-abi3-win_amd64.whl", hash = "sha256:039c84f7a294aa71438048e14899d59ce005f213872e27fe6bf6ce3ae8730d7d"}, + {file = "polars-0.20.30.tar.gz", hash = "sha256:b9fd2c6b5100caa7c26496ce17ec289cae23c2db6c41713bc52c54c76d4451ae"}, ] [package.extras] adbc = ["adbc-driver-manager", "adbc-driver-sqlite"] -all = ["polars[adbc,async,cloudpickle,connectorx,deltalake,fastexcel,fsspec,gevent,iceberg,numpy,pandas,plot,pyarrow,pydantic,sqlalchemy,timezone,torch,xlsx2csv,xlsxwriter]"] +all = ["polars[adbc,async,cloudpickle,connectorx,deltalake,fastexcel,fsspec,gevent,iceberg,numpy,pandas,plot,pyarrow,pydantic,sqlalchemy,timezone,xlsx2csv,xlsxwriter]"] async = ["nest-asyncio"] cloudpickle = ["cloudpickle"] connectorx = ["connectorx (>=0.3.2)"] @@ -649,7 +781,6 @@ pydantic = ["pydantic"] pyxlsb = ["pyxlsb (>=1.0)"] sqlalchemy = ["pandas", "sqlalchemy"] timezone = ["backports-zoneinfo", "tzdata"] -torch = ["torch"] xlsx2csv = ["xlsx2csv (>=0.8.0)"] xlsxwriter = ["xlsxwriter"] @@ -671,20 +802,31 @@ nodeenv = ">=0.11.1" pyyaml = ">=5.1" virtualenv = ">=20.10.0" +[[package]] +name = "pycparser" +version = "2.22" +description = "C parser in Python" +optional = false +python-versions = ">=3.8" +files = [ + {file = "pycparser-2.22-py3-none-any.whl", hash = "sha256:c3702b6d3dd8c7abc1afa565d7e63d53a1d0bd86cdc24edd75470f4de499cfcc"}, + {file = "pycparser-2.22.tar.gz", hash = "sha256:491c8be9c040f5390f5bf44a5b07752bd07f56edf992381b05c701439eec10f6"}, +] + [[package]] name = "pydantic" -version = "2.7.1" +version = "2.7.2" description = "Data validation using Python type hints" optional = false python-versions = ">=3.8" files = [ - {file = "pydantic-2.7.1-py3-none-any.whl", hash = "sha256:e029badca45266732a9a79898a15ae2e8b14840b1eabbb25844be28f0b33f3d5"}, - {file = "pydantic-2.7.1.tar.gz", hash = "sha256:e9dbb5eada8abe4d9ae5f46b9939aead650cd2b68f249bb3a8139dbe125803cc"}, + {file = "pydantic-2.7.2-py3-none-any.whl", hash = "sha256:834ab954175f94e6e68258537dc49402c4a5e9d0409b9f1b86b7e934a8372de7"}, + {file = "pydantic-2.7.2.tar.gz", hash = "sha256:71b2945998f9c9b7919a45bde9a50397b289937d215ae141c1d0903ba7149fd7"}, ] [package.dependencies] annotated-types = ">=0.4.0" -pydantic-core = "2.18.2" +pydantic-core = "2.18.3" typing-extensions = ">=4.6.1" [package.extras] @@ -692,95 +834,114 @@ email = ["email-validator (>=2.0.0)"] [[package]] name = "pydantic-core" -version = "2.18.2" +version = "2.18.3" description = "Core functionality for Pydantic validation and serialization" optional = false python-versions = ">=3.8" files = [ - {file = "pydantic_core-2.18.2-cp310-cp310-macosx_10_12_x86_64.whl", hash = "sha256:9e08e867b306f525802df7cd16c44ff5ebbe747ff0ca6cf3fde7f36c05a59a81"}, - {file = "pydantic_core-2.18.2-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:f0a21cbaa69900cbe1a2e7cad2aa74ac3cf21b10c3efb0fa0b80305274c0e8a2"}, - {file = "pydantic_core-2.18.2-cp310-cp310-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:0680b1f1f11fda801397de52c36ce38ef1c1dc841a0927a94f226dea29c3ae3d"}, - {file = "pydantic_core-2.18.2-cp310-cp310-manylinux_2_17_armv7l.manylinux2014_armv7l.whl", hash = "sha256:95b9d5e72481d3780ba3442eac863eae92ae43a5f3adb5b4d0a1de89d42bb250"}, - {file = "pydantic_core-2.18.2-cp310-cp310-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:c4fcf5cd9c4b655ad666ca332b9a081112cd7a58a8b5a6ca7a3104bc950f2038"}, - {file = "pydantic_core-2.18.2-cp310-cp310-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:9b5155ff768083cb1d62f3e143b49a8a3432e6789a3abee8acd005c3c7af1c74"}, - {file = "pydantic_core-2.18.2-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:553ef617b6836fc7e4df130bb851e32fe357ce36336d897fd6646d6058d980af"}, - {file = "pydantic_core-2.18.2-cp310-cp310-manylinux_2_5_i686.manylinux1_i686.whl", hash = "sha256:b89ed9eb7d616ef5714e5590e6cf7f23b02d0d539767d33561e3675d6f9e3857"}, - {file = "pydantic_core-2.18.2-cp310-cp310-musllinux_1_1_aarch64.whl", hash = "sha256:75f7e9488238e920ab6204399ded280dc4c307d034f3924cd7f90a38b1829563"}, - {file = "pydantic_core-2.18.2-cp310-cp310-musllinux_1_1_x86_64.whl", hash = "sha256:ef26c9e94a8c04a1b2924149a9cb081836913818e55681722d7f29af88fe7b38"}, - {file = "pydantic_core-2.18.2-cp310-none-win32.whl", hash = "sha256:182245ff6b0039e82b6bb585ed55a64d7c81c560715d1bad0cbad6dfa07b4027"}, - {file = "pydantic_core-2.18.2-cp310-none-win_amd64.whl", hash = "sha256:e23ec367a948b6d812301afc1b13f8094ab7b2c280af66ef450efc357d2ae543"}, - {file = "pydantic_core-2.18.2-cp311-cp311-macosx_10_12_x86_64.whl", hash = "sha256:219da3f096d50a157f33645a1cf31c0ad1fe829a92181dd1311022f986e5fbe3"}, - {file = "pydantic_core-2.18.2-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:cc1cfd88a64e012b74e94cd00bbe0f9c6df57049c97f02bb07d39e9c852e19a4"}, - {file = "pydantic_core-2.18.2-cp311-cp311-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:05b7133a6e6aeb8df37d6f413f7705a37ab4031597f64ab56384c94d98fa0e90"}, - {file = "pydantic_core-2.18.2-cp311-cp311-manylinux_2_17_armv7l.manylinux2014_armv7l.whl", hash = "sha256:224c421235f6102e8737032483f43c1a8cfb1d2f45740c44166219599358c2cd"}, - {file = "pydantic_core-2.18.2-cp311-cp311-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:b14d82cdb934e99dda6d9d60dc84a24379820176cc4a0d123f88df319ae9c150"}, - {file = "pydantic_core-2.18.2-cp311-cp311-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:2728b01246a3bba6de144f9e3115b532ee44bd6cf39795194fb75491824a1413"}, - {file = "pydantic_core-2.18.2-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:470b94480bb5ee929f5acba6995251ada5e059a5ef3e0dfc63cca287283ebfa6"}, - {file = "pydantic_core-2.18.2-cp311-cp311-manylinux_2_5_i686.manylinux1_i686.whl", hash = "sha256:997abc4df705d1295a42f95b4eec4950a37ad8ae46d913caeee117b6b198811c"}, - {file = "pydantic_core-2.18.2-cp311-cp311-musllinux_1_1_aarch64.whl", hash = "sha256:75250dbc5290e3f1a0f4618db35e51a165186f9034eff158f3d490b3fed9f8a0"}, - {file = "pydantic_core-2.18.2-cp311-cp311-musllinux_1_1_x86_64.whl", hash = "sha256:4456f2dca97c425231d7315737d45239b2b51a50dc2b6f0c2bb181fce6207664"}, - {file = "pydantic_core-2.18.2-cp311-none-win32.whl", hash = "sha256:269322dcc3d8bdb69f054681edff86276b2ff972447863cf34c8b860f5188e2e"}, - {file = "pydantic_core-2.18.2-cp311-none-win_amd64.whl", hash = "sha256:800d60565aec896f25bc3cfa56d2277d52d5182af08162f7954f938c06dc4ee3"}, - {file = "pydantic_core-2.18.2-cp311-none-win_arm64.whl", hash = "sha256:1404c69d6a676245199767ba4f633cce5f4ad4181f9d0ccb0577e1f66cf4c46d"}, - {file = "pydantic_core-2.18.2-cp312-cp312-macosx_10_12_x86_64.whl", hash = "sha256:fb2bd7be70c0fe4dfd32c951bc813d9fe6ebcbfdd15a07527796c8204bd36242"}, - {file = "pydantic_core-2.18.2-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:6132dd3bd52838acddca05a72aafb6eab6536aa145e923bb50f45e78b7251043"}, - {file = "pydantic_core-2.18.2-cp312-cp312-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:d7d904828195733c183d20a54230c0df0eb46ec746ea1a666730787353e87182"}, - {file = "pydantic_core-2.18.2-cp312-cp312-manylinux_2_17_armv7l.manylinux2014_armv7l.whl", hash = "sha256:c9bd70772c720142be1020eac55f8143a34ec9f82d75a8e7a07852023e46617f"}, - {file = "pydantic_core-2.18.2-cp312-cp312-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:2b8ed04b3582771764538f7ee7001b02e1170223cf9b75dff0bc698fadb00cf3"}, - {file = "pydantic_core-2.18.2-cp312-cp312-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:e6dac87ddb34aaec85f873d737e9d06a3555a1cc1a8e0c44b7f8d5daeb89d86f"}, - {file = "pydantic_core-2.18.2-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:7ca4ae5a27ad7a4ee5170aebce1574b375de390bc01284f87b18d43a3984df72"}, - {file = "pydantic_core-2.18.2-cp312-cp312-manylinux_2_5_i686.manylinux1_i686.whl", hash = "sha256:886eec03591b7cf058467a70a87733b35f44707bd86cf64a615584fd72488b7c"}, - {file = "pydantic_core-2.18.2-cp312-cp312-musllinux_1_1_aarch64.whl", hash = "sha256:ca7b0c1f1c983e064caa85f3792dd2fe3526b3505378874afa84baf662e12241"}, - {file = "pydantic_core-2.18.2-cp312-cp312-musllinux_1_1_x86_64.whl", hash = "sha256:4b4356d3538c3649337df4074e81b85f0616b79731fe22dd11b99499b2ebbdf3"}, - {file = "pydantic_core-2.18.2-cp312-none-win32.whl", hash = "sha256:8b172601454f2d7701121bbec3425dd71efcb787a027edf49724c9cefc14c038"}, - {file = "pydantic_core-2.18.2-cp312-none-win_amd64.whl", hash = "sha256:b1bd7e47b1558ea872bd16c8502c414f9e90dcf12f1395129d7bb42a09a95438"}, - {file = "pydantic_core-2.18.2-cp312-none-win_arm64.whl", hash = "sha256:98758d627ff397e752bc339272c14c98199c613f922d4a384ddc07526c86a2ec"}, - {file = "pydantic_core-2.18.2-cp38-cp38-macosx_10_12_x86_64.whl", hash = "sha256:9fdad8e35f278b2c3eb77cbdc5c0a49dada440657bf738d6905ce106dc1de439"}, - {file = "pydantic_core-2.18.2-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:1d90c3265ae107f91a4f279f4d6f6f1d4907ac76c6868b27dc7fb33688cfb347"}, - {file = "pydantic_core-2.18.2-cp38-cp38-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:390193c770399861d8df9670fb0d1874f330c79caaca4642332df7c682bf6b91"}, - {file = "pydantic_core-2.18.2-cp38-cp38-manylinux_2_17_armv7l.manylinux2014_armv7l.whl", hash = "sha256:82d5d4d78e4448683cb467897fe24e2b74bb7b973a541ea1dcfec1d3cbce39fb"}, - {file = "pydantic_core-2.18.2-cp38-cp38-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:4774f3184d2ef3e14e8693194f661dea5a4d6ca4e3dc8e39786d33a94865cefd"}, - {file = "pydantic_core-2.18.2-cp38-cp38-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:d4d938ec0adf5167cb335acb25a4ee69a8107e4984f8fbd2e897021d9e4ca21b"}, - {file = "pydantic_core-2.18.2-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:e0e8b1be28239fc64a88a8189d1df7fad8be8c1ae47fcc33e43d4be15f99cc70"}, - {file = "pydantic_core-2.18.2-cp38-cp38-manylinux_2_5_i686.manylinux1_i686.whl", hash = "sha256:868649da93e5a3d5eacc2b5b3b9235c98ccdbfd443832f31e075f54419e1b96b"}, - {file = "pydantic_core-2.18.2-cp38-cp38-musllinux_1_1_aarch64.whl", hash = "sha256:78363590ef93d5d226ba21a90a03ea89a20738ee5b7da83d771d283fd8a56761"}, - {file = "pydantic_core-2.18.2-cp38-cp38-musllinux_1_1_x86_64.whl", hash = "sha256:852e966fbd035a6468fc0a3496589b45e2208ec7ca95c26470a54daed82a0788"}, - {file = "pydantic_core-2.18.2-cp38-none-win32.whl", hash = "sha256:6a46e22a707e7ad4484ac9ee9f290f9d501df45954184e23fc29408dfad61350"}, - {file = "pydantic_core-2.18.2-cp38-none-win_amd64.whl", hash = "sha256:d91cb5ea8b11607cc757675051f61b3d93f15eca3cefb3e6c704a5d6e8440f4e"}, - {file = "pydantic_core-2.18.2-cp39-cp39-macosx_10_12_x86_64.whl", hash = "sha256:ae0a8a797a5e56c053610fa7be147993fe50960fa43609ff2a9552b0e07013e8"}, - {file = "pydantic_core-2.18.2-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:042473b6280246b1dbf530559246f6842b56119c2926d1e52b631bdc46075f2a"}, - {file = "pydantic_core-2.18.2-cp39-cp39-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:1a388a77e629b9ec814c1b1e6b3b595fe521d2cdc625fcca26fbc2d44c816804"}, - {file = "pydantic_core-2.18.2-cp39-cp39-manylinux_2_17_armv7l.manylinux2014_armv7l.whl", hash = "sha256:e25add29b8f3b233ae90ccef2d902d0ae0432eb0d45370fe315d1a5cf231004b"}, - {file = "pydantic_core-2.18.2-cp39-cp39-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:f459a5ce8434614dfd39bbebf1041952ae01da6bed9855008cb33b875cb024c0"}, - {file = "pydantic_core-2.18.2-cp39-cp39-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:eff2de745698eb46eeb51193a9f41d67d834d50e424aef27df2fcdee1b153845"}, - {file = "pydantic_core-2.18.2-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:a8309f67285bdfe65c372ea3722b7a5642680f3dba538566340a9d36e920b5f0"}, - {file = "pydantic_core-2.18.2-cp39-cp39-manylinux_2_5_i686.manylinux1_i686.whl", hash = "sha256:f93a8a2e3938ff656a7c1bc57193b1319960ac015b6e87d76c76bf14fe0244b4"}, - {file = "pydantic_core-2.18.2-cp39-cp39-musllinux_1_1_aarch64.whl", hash = "sha256:22057013c8c1e272eb8d0eebc796701167d8377441ec894a8fed1af64a0bf399"}, - {file = "pydantic_core-2.18.2-cp39-cp39-musllinux_1_1_x86_64.whl", hash = "sha256:cfeecd1ac6cc1fb2692c3d5110781c965aabd4ec5d32799773ca7b1456ac636b"}, - {file = "pydantic_core-2.18.2-cp39-none-win32.whl", hash = "sha256:0d69b4c2f6bb3e130dba60d34c0845ba31b69babdd3f78f7c0c8fae5021a253e"}, - {file = "pydantic_core-2.18.2-cp39-none-win_amd64.whl", hash = "sha256:d9319e499827271b09b4e411905b24a426b8fb69464dfa1696258f53a3334641"}, - {file = "pydantic_core-2.18.2-pp310-pypy310_pp73-macosx_10_12_x86_64.whl", hash = "sha256:a1874c6dd4113308bd0eb568418e6114b252afe44319ead2b4081e9b9521fe75"}, - {file = "pydantic_core-2.18.2-pp310-pypy310_pp73-macosx_11_0_arm64.whl", hash = "sha256:ccdd111c03bfd3666bd2472b674c6899550e09e9f298954cfc896ab92b5b0e6d"}, - {file = "pydantic_core-2.18.2-pp310-pypy310_pp73-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:e18609ceaa6eed63753037fc06ebb16041d17d28199ae5aba0052c51449650a9"}, - {file = "pydantic_core-2.18.2-pp310-pypy310_pp73-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:6e5c584d357c4e2baf0ff7baf44f4994be121e16a2c88918a5817331fc7599d7"}, - {file = "pydantic_core-2.18.2-pp310-pypy310_pp73-manylinux_2_5_i686.manylinux1_i686.whl", hash = "sha256:43f0f463cf89ace478de71a318b1b4f05ebc456a9b9300d027b4b57c1a2064fb"}, - {file = "pydantic_core-2.18.2-pp310-pypy310_pp73-musllinux_1_1_aarch64.whl", hash = "sha256:e1b395e58b10b73b07b7cf740d728dd4ff9365ac46c18751bf8b3d8cca8f625a"}, - {file = "pydantic_core-2.18.2-pp310-pypy310_pp73-musllinux_1_1_x86_64.whl", hash = "sha256:0098300eebb1c837271d3d1a2cd2911e7c11b396eac9661655ee524a7f10587b"}, - {file = "pydantic_core-2.18.2-pp310-pypy310_pp73-win_amd64.whl", hash = "sha256:36789b70d613fbac0a25bb07ab3d9dba4d2e38af609c020cf4d888d165ee0bf3"}, - {file = "pydantic_core-2.18.2-pp39-pypy39_pp73-macosx_10_12_x86_64.whl", hash = "sha256:3f9a801e7c8f1ef8718da265bba008fa121243dfe37c1cea17840b0944dfd72c"}, - {file = "pydantic_core-2.18.2-pp39-pypy39_pp73-macosx_11_0_arm64.whl", hash = "sha256:3a6515ebc6e69d85502b4951d89131ca4e036078ea35533bb76327f8424531ce"}, - {file = "pydantic_core-2.18.2-pp39-pypy39_pp73-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:20aca1e2298c56ececfd8ed159ae4dde2df0781988c97ef77d5c16ff4bd5b400"}, - {file = "pydantic_core-2.18.2-pp39-pypy39_pp73-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:223ee893d77a310a0391dca6df00f70bbc2f36a71a895cecd9a0e762dc37b349"}, - {file = "pydantic_core-2.18.2-pp39-pypy39_pp73-manylinux_2_5_i686.manylinux1_i686.whl", hash = "sha256:2334ce8c673ee93a1d6a65bd90327588387ba073c17e61bf19b4fd97d688d63c"}, - {file = "pydantic_core-2.18.2-pp39-pypy39_pp73-musllinux_1_1_aarch64.whl", hash = "sha256:cbca948f2d14b09d20268cda7b0367723d79063f26c4ffc523af9042cad95592"}, - {file = "pydantic_core-2.18.2-pp39-pypy39_pp73-musllinux_1_1_x86_64.whl", hash = "sha256:b3ef08e20ec49e02d5c6717a91bb5af9b20f1805583cb0adfe9ba2c6b505b5ae"}, - {file = "pydantic_core-2.18.2-pp39-pypy39_pp73-win_amd64.whl", hash = "sha256:c6fdc8627910eed0c01aed6a390a252fe3ea6d472ee70fdde56273f198938374"}, - {file = "pydantic_core-2.18.2.tar.gz", hash = "sha256:2e29d20810dfc3043ee13ac7d9e25105799817683348823f305ab3f349b9386e"}, + {file = "pydantic_core-2.18.3-cp310-cp310-macosx_10_12_x86_64.whl", hash = "sha256:744697428fcdec6be5670460b578161d1ffe34743a5c15656be7ea82b008197c"}, + {file = "pydantic_core-2.18.3-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:37b40c05ced1ba4218b14986fe6f283d22e1ae2ff4c8e28881a70fb81fbfcda7"}, + {file = "pydantic_core-2.18.3-cp310-cp310-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:544a9a75622357076efb6b311983ff190fbfb3c12fc3a853122b34d3d358126c"}, + {file = "pydantic_core-2.18.3-cp310-cp310-manylinux_2_17_armv7l.manylinux2014_armv7l.whl", hash = "sha256:e2e253af04ceaebde8eb201eb3f3e3e7e390f2d275a88300d6a1959d710539e2"}, + {file = "pydantic_core-2.18.3-cp310-cp310-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:855ec66589c68aa367d989da5c4755bb74ee92ccad4fdb6af942c3612c067e34"}, + {file = "pydantic_core-2.18.3-cp310-cp310-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:3d3e42bb54e7e9d72c13ce112e02eb1b3b55681ee948d748842171201a03a98a"}, + {file = "pydantic_core-2.18.3-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:c6ac9ffccc9d2e69d9fba841441d4259cb668ac180e51b30d3632cd7abca2b9b"}, + {file = "pydantic_core-2.18.3-cp310-cp310-manylinux_2_5_i686.manylinux1_i686.whl", hash = "sha256:c56eca1686539fa0c9bda992e7bd6a37583f20083c37590413381acfc5f192d6"}, + {file = "pydantic_core-2.18.3-cp310-cp310-musllinux_1_1_aarch64.whl", hash = "sha256:17954d784bf8abfc0ec2a633108207ebc4fa2df1a0e4c0c3ccbaa9bb01d2c426"}, + {file = "pydantic_core-2.18.3-cp310-cp310-musllinux_1_1_x86_64.whl", hash = "sha256:98ed737567d8f2ecd54f7c8d4f8572ca7c7921ede93a2e52939416170d357812"}, + {file = "pydantic_core-2.18.3-cp310-none-win32.whl", hash = "sha256:9f9e04afebd3ed8c15d67a564ed0a34b54e52136c6d40d14c5547b238390e779"}, + {file = "pydantic_core-2.18.3-cp310-none-win_amd64.whl", hash = "sha256:45e4ffbae34f7ae30d0047697e724e534a7ec0a82ef9994b7913a412c21462a0"}, + {file = "pydantic_core-2.18.3-cp311-cp311-macosx_10_12_x86_64.whl", hash = "sha256:b9ebe8231726c49518b16b237b9fe0d7d361dd221302af511a83d4ada01183ab"}, + {file = "pydantic_core-2.18.3-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:b8e20e15d18bf7dbb453be78a2d858f946f5cdf06c5072453dace00ab652e2b2"}, + {file = "pydantic_core-2.18.3-cp311-cp311-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:c0d9ff283cd3459fa0bf9b0256a2b6f01ac1ff9ffb034e24457b9035f75587cb"}, + {file = "pydantic_core-2.18.3-cp311-cp311-manylinux_2_17_armv7l.manylinux2014_armv7l.whl", hash = "sha256:2f7ef5f0ebb77ba24c9970da18b771711edc5feaf00c10b18461e0f5f5949231"}, + {file = "pydantic_core-2.18.3-cp311-cp311-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:73038d66614d2e5cde30435b5afdced2b473b4c77d4ca3a8624dd3e41a9c19be"}, + {file = "pydantic_core-2.18.3-cp311-cp311-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:6afd5c867a74c4d314c557b5ea9520183fadfbd1df4c2d6e09fd0d990ce412cd"}, + {file = "pydantic_core-2.18.3-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:bd7df92f28d351bb9f12470f4c533cf03d1b52ec5a6e5c58c65b183055a60106"}, + {file = "pydantic_core-2.18.3-cp311-cp311-manylinux_2_5_i686.manylinux1_i686.whl", hash = "sha256:80aea0ffeb1049336043d07799eace1c9602519fb3192916ff525b0287b2b1e4"}, + {file = "pydantic_core-2.18.3-cp311-cp311-musllinux_1_1_aarch64.whl", hash = "sha256:aaee40f25bba38132e655ffa3d1998a6d576ba7cf81deff8bfa189fb43fd2bbe"}, + {file = "pydantic_core-2.18.3-cp311-cp311-musllinux_1_1_x86_64.whl", hash = "sha256:9128089da8f4fe73f7a91973895ebf2502539d627891a14034e45fb9e707e26d"}, + {file = "pydantic_core-2.18.3-cp311-none-win32.whl", hash = "sha256:fec02527e1e03257aa25b1a4dcbe697b40a22f1229f5d026503e8b7ff6d2eda7"}, + {file = "pydantic_core-2.18.3-cp311-none-win_amd64.whl", hash = "sha256:58ff8631dbab6c7c982e6425da8347108449321f61fe427c52ddfadd66642af7"}, + {file = "pydantic_core-2.18.3-cp311-none-win_arm64.whl", hash = "sha256:3fc1c7f67f34c6c2ef9c213e0f2a351797cda98249d9ca56a70ce4ebcaba45f4"}, + {file = "pydantic_core-2.18.3-cp312-cp312-macosx_10_12_x86_64.whl", hash = "sha256:f0928cde2ae416a2d1ebe6dee324709c6f73e93494d8c7aea92df99aab1fc40f"}, + {file = "pydantic_core-2.18.3-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:0bee9bb305a562f8b9271855afb6ce00223f545de3d68560b3c1649c7c5295e9"}, + {file = "pydantic_core-2.18.3-cp312-cp312-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:e862823be114387257dacbfa7d78547165a85d7add33b446ca4f4fae92c7ff5c"}, + {file = "pydantic_core-2.18.3-cp312-cp312-manylinux_2_17_armv7l.manylinux2014_armv7l.whl", hash = "sha256:6a36f78674cbddc165abab0df961b5f96b14461d05feec5e1f78da58808b97e7"}, + {file = "pydantic_core-2.18.3-cp312-cp312-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:ba905d184f62e7ddbb7a5a751d8a5c805463511c7b08d1aca4a3e8c11f2e5048"}, + {file = "pydantic_core-2.18.3-cp312-cp312-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:7fdd362f6a586e681ff86550b2379e532fee63c52def1c666887956748eaa326"}, + {file = "pydantic_core-2.18.3-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:24b214b7ee3bd3b865e963dbed0f8bc5375f49449d70e8d407b567af3222aae4"}, + {file = "pydantic_core-2.18.3-cp312-cp312-manylinux_2_5_i686.manylinux1_i686.whl", hash = "sha256:691018785779766127f531674fa82bb368df5b36b461622b12e176c18e119022"}, + {file = "pydantic_core-2.18.3-cp312-cp312-musllinux_1_1_aarch64.whl", hash = "sha256:60e4c625e6f7155d7d0dcac151edf5858102bc61bf959d04469ca6ee4e8381bd"}, + {file = "pydantic_core-2.18.3-cp312-cp312-musllinux_1_1_x86_64.whl", hash = "sha256:a4e651e47d981c1b701dcc74ab8fec5a60a5b004650416b4abbef13db23bc7be"}, + {file = "pydantic_core-2.18.3-cp312-none-win32.whl", hash = "sha256:ffecbb5edb7f5ffae13599aec33b735e9e4c7676ca1633c60f2c606beb17efc5"}, + {file = "pydantic_core-2.18.3-cp312-none-win_amd64.whl", hash = "sha256:2c8333f6e934733483c7eddffdb094c143b9463d2af7e6bd85ebcb2d4a1b82c6"}, + {file = "pydantic_core-2.18.3-cp312-none-win_arm64.whl", hash = "sha256:7a20dded653e516a4655f4c98e97ccafb13753987434fe7cf044aa25f5b7d417"}, + {file = "pydantic_core-2.18.3-cp38-cp38-macosx_10_12_x86_64.whl", hash = "sha256:eecf63195be644b0396f972c82598cd15693550f0ff236dcf7ab92e2eb6d3522"}, + {file = "pydantic_core-2.18.3-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:2c44efdd3b6125419c28821590d7ec891c9cb0dff33a7a78d9d5c8b6f66b9702"}, + {file = "pydantic_core-2.18.3-cp38-cp38-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:6e59fca51ffbdd1638b3856779342ed69bcecb8484c1d4b8bdb237d0eb5a45e2"}, + {file = "pydantic_core-2.18.3-cp38-cp38-manylinux_2_17_armv7l.manylinux2014_armv7l.whl", hash = "sha256:70cf099197d6b98953468461d753563b28e73cf1eade2ffe069675d2657ed1d5"}, + {file = "pydantic_core-2.18.3-cp38-cp38-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:63081a49dddc6124754b32a3774331467bfc3d2bd5ff8f10df36a95602560361"}, + {file = "pydantic_core-2.18.3-cp38-cp38-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:370059b7883485c9edb9655355ff46d912f4b03b009d929220d9294c7fd9fd60"}, + {file = "pydantic_core-2.18.3-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:5a64faeedfd8254f05f5cf6fc755023a7e1606af3959cfc1a9285744cc711044"}, + {file = "pydantic_core-2.18.3-cp38-cp38-manylinux_2_5_i686.manylinux1_i686.whl", hash = "sha256:19d2e725de0f90d8671f89e420d36c3dd97639b98145e42fcc0e1f6d492a46dc"}, + {file = "pydantic_core-2.18.3-cp38-cp38-musllinux_1_1_aarch64.whl", hash = "sha256:67bc078025d70ec5aefe6200ef094576c9d86bd36982df1301c758a9fff7d7f4"}, + {file = "pydantic_core-2.18.3-cp38-cp38-musllinux_1_1_x86_64.whl", hash = "sha256:adf952c3f4100e203cbaf8e0c907c835d3e28f9041474e52b651761dc248a3c0"}, + {file = "pydantic_core-2.18.3-cp38-none-win32.whl", hash = "sha256:9a46795b1f3beb167eaee91736d5d17ac3a994bf2215a996aed825a45f897558"}, + {file = "pydantic_core-2.18.3-cp38-none-win_amd64.whl", hash = "sha256:200ad4e3133cb99ed82342a101a5abf3d924722e71cd581cc113fe828f727fbc"}, + {file = "pydantic_core-2.18.3-cp39-cp39-macosx_10_12_x86_64.whl", hash = "sha256:304378b7bf92206036c8ddd83a2ba7b7d1a5b425acafff637172a3aa72ad7083"}, + {file = "pydantic_core-2.18.3-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:c826870b277143e701c9ccf34ebc33ddb4d072612683a044e7cce2d52f6c3fef"}, + {file = "pydantic_core-2.18.3-cp39-cp39-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:e201935d282707394f3668380e41ccf25b5794d1b131cdd96b07f615a33ca4b1"}, + {file = "pydantic_core-2.18.3-cp39-cp39-manylinux_2_17_armv7l.manylinux2014_armv7l.whl", hash = "sha256:5560dda746c44b48bf82b3d191d74fe8efc5686a9ef18e69bdabccbbb9ad9442"}, + {file = "pydantic_core-2.18.3-cp39-cp39-manylinux_2_17_ppc64le.manylinux2014_ppc64le.whl", hash = "sha256:6b32c2a1f8032570842257e4c19288eba9a2bba4712af542327de9a1204faff8"}, + {file = "pydantic_core-2.18.3-cp39-cp39-manylinux_2_17_s390x.manylinux2014_s390x.whl", hash = "sha256:929c24e9dea3990bc8bcd27c5f2d3916c0c86f5511d2caa69e0d5290115344a9"}, + {file = "pydantic_core-2.18.3-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:e1a8376fef60790152564b0eab376b3e23dd6e54f29d84aad46f7b264ecca943"}, + {file = "pydantic_core-2.18.3-cp39-cp39-manylinux_2_5_i686.manylinux1_i686.whl", hash = "sha256:dccf3ef1400390ddd1fb55bf0632209d39140552d068ee5ac45553b556780e06"}, + {file = "pydantic_core-2.18.3-cp39-cp39-musllinux_1_1_aarch64.whl", hash = "sha256:41dbdcb0c7252b58fa931fec47937edb422c9cb22528f41cb8963665c372caf6"}, + {file = "pydantic_core-2.18.3-cp39-cp39-musllinux_1_1_x86_64.whl", hash = "sha256:666e45cf071669fde468886654742fa10b0e74cd0fa0430a46ba6056b24fb0af"}, + {file = "pydantic_core-2.18.3-cp39-none-win32.whl", hash = "sha256:f9c08cabff68704a1b4667d33f534d544b8a07b8e5d039c37067fceb18789e78"}, + {file = "pydantic_core-2.18.3-cp39-none-win_amd64.whl", hash = "sha256:4afa5f5973e8572b5c0dcb4e2d4fda7890e7cd63329bd5cc3263a25c92ef0026"}, + {file = "pydantic_core-2.18.3-pp310-pypy310_pp73-macosx_10_12_x86_64.whl", hash = "sha256:77319771a026f7c7d29c6ebc623de889e9563b7087911b46fd06c044a12aa5e9"}, + {file = "pydantic_core-2.18.3-pp310-pypy310_pp73-macosx_11_0_arm64.whl", hash = "sha256:df11fa992e9f576473038510d66dd305bcd51d7dd508c163a8c8fe148454e059"}, + {file = "pydantic_core-2.18.3-pp310-pypy310_pp73-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:d531076bdfb65af593326ffd567e6ab3da145020dafb9187a1d131064a55f97c"}, + {file = "pydantic_core-2.18.3-pp310-pypy310_pp73-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:d33ce258e4e6e6038f2b9e8b8a631d17d017567db43483314993b3ca345dcbbb"}, + {file = "pydantic_core-2.18.3-pp310-pypy310_pp73-manylinux_2_5_i686.manylinux1_i686.whl", hash = "sha256:1f9cd7f5635b719939019be9bda47ecb56e165e51dd26c9a217a433e3d0d59a9"}, + {file = "pydantic_core-2.18.3-pp310-pypy310_pp73-musllinux_1_1_aarch64.whl", hash = "sha256:cd4a032bb65cc132cae1fe3e52877daecc2097965cd3914e44fbd12b00dae7c5"}, + {file = "pydantic_core-2.18.3-pp310-pypy310_pp73-musllinux_1_1_x86_64.whl", hash = "sha256:82f2718430098bcdf60402136c845e4126a189959d103900ebabb6774a5d9fdb"}, + {file = "pydantic_core-2.18.3-pp310-pypy310_pp73-win_amd64.whl", hash = "sha256:c0037a92cf0c580ed14e10953cdd26528e8796307bb8bb312dc65f71547df04d"}, + {file = "pydantic_core-2.18.3-pp39-pypy39_pp73-macosx_10_12_x86_64.whl", hash = "sha256:b95a0972fac2b1ff3c94629fc9081b16371dad870959f1408cc33b2f78ad347a"}, + {file = "pydantic_core-2.18.3-pp39-pypy39_pp73-macosx_11_0_arm64.whl", hash = "sha256:a62e437d687cc148381bdd5f51e3e81f5b20a735c55f690c5be94e05da2b0d5c"}, + {file = "pydantic_core-2.18.3-pp39-pypy39_pp73-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:b367a73a414bbb08507da102dc2cde0fa7afe57d09b3240ce82a16d608a7679c"}, + {file = "pydantic_core-2.18.3-pp39-pypy39_pp73-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:0ecce4b2360aa3f008da3327d652e74a0e743908eac306198b47e1c58b03dd2b"}, + {file = "pydantic_core-2.18.3-pp39-pypy39_pp73-manylinux_2_5_i686.manylinux1_i686.whl", hash = "sha256:bd4435b8d83f0c9561a2a9585b1de78f1abb17cb0cef5f39bf6a4b47d19bafe3"}, + {file = "pydantic_core-2.18.3-pp39-pypy39_pp73-musllinux_1_1_aarch64.whl", hash = "sha256:616221a6d473c5b9aa83fa8982745441f6a4a62a66436be9445c65f241b86c94"}, + {file = "pydantic_core-2.18.3-pp39-pypy39_pp73-musllinux_1_1_x86_64.whl", hash = "sha256:7e6382ce89a92bc1d0c0c5edd51e931432202b9080dc921d8d003e616402efd1"}, + {file = "pydantic_core-2.18.3-pp39-pypy39_pp73-win_amd64.whl", hash = "sha256:ff58f379345603d940e461eae474b6bbb6dab66ed9a851ecd3cb3709bf4dcf6a"}, + {file = "pydantic_core-2.18.3.tar.gz", hash = "sha256:432e999088d85c8f36b9a3f769a8e2b57aabd817bbb729a90d1fe7f18f6f1f39"}, ] [package.dependencies] typing-extensions = ">=4.6.0,<4.7.0 || >4.7.0" +[[package]] +name = "pygithub" +version = "2.3.0" +description = "Use the full Github API v3" +optional = false +python-versions = ">=3.7" +files = [ + {file = "PyGithub-2.3.0-py3-none-any.whl", hash = "sha256:65b499728be3ce7b0cd2cd760da3b32f0f4d7bc55e5e0677617f90f6564e793e"}, + {file = "PyGithub-2.3.0.tar.gz", hash = "sha256:0148d7347a1cdeed99af905077010aef81a4dad988b0ba51d4108bf66b443f7e"}, +] + +[package.dependencies] +Deprecated = "*" +pyjwt = {version = ">=2.4.0", extras = ["crypto"]} +pynacl = ">=1.4.0" +requests = ">=2.14.0" +typing-extensions = ">=4.0.0" +urllib3 = ">=1.26.0" + [[package]] name = "pygments" version = "2.18.0" @@ -795,6 +956,52 @@ files = [ [package.extras] windows-terminal = ["colorama (>=0.4.6)"] +[[package]] +name = "pyjwt" +version = "2.8.0" +description = "JSON Web Token implementation in Python" +optional = false +python-versions = ">=3.7" +files = [ + {file = "PyJWT-2.8.0-py3-none-any.whl", hash = "sha256:59127c392cc44c2da5bb3192169a91f429924e17aff6534d70fdc02ab3e04320"}, + {file = "PyJWT-2.8.0.tar.gz", hash = "sha256:57e28d156e3d5c10088e0c68abb90bfac3df82b40a71bd0daa20c65ccd5c23de"}, +] + +[package.dependencies] +cryptography = {version = ">=3.4.0", optional = true, markers = "extra == \"crypto\""} + +[package.extras] +crypto = ["cryptography (>=3.4.0)"] +dev = ["coverage[toml] (==5.0.4)", "cryptography (>=3.4.0)", "pre-commit", "pytest (>=6.0.0,<7.0.0)", "sphinx (>=4.5.0,<5.0.0)", "sphinx-rtd-theme", "zope.interface"] +docs = ["sphinx (>=4.5.0,<5.0.0)", "sphinx-rtd-theme", "zope.interface"] +tests = ["coverage[toml] (==5.0.4)", "pytest (>=6.0.0,<7.0.0)"] + +[[package]] +name = "pynacl" +version = "1.5.0" +description = "Python binding to the Networking and Cryptography (NaCl) library" +optional = false +python-versions = ">=3.6" +files = [ + {file = "PyNaCl-1.5.0-cp36-abi3-macosx_10_10_universal2.whl", hash = "sha256:401002a4aaa07c9414132aaed7f6836ff98f59277a234704ff66878c2ee4a0d1"}, + {file = "PyNaCl-1.5.0-cp36-abi3-manylinux_2_17_aarch64.manylinux2014_aarch64.manylinux_2_24_aarch64.whl", hash = "sha256:52cb72a79269189d4e0dc537556f4740f7f0a9ec41c1322598799b0bdad4ef92"}, + {file = "PyNaCl-1.5.0-cp36-abi3-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:a36d4a9dda1f19ce6e03c9a784a2921a4b726b02e1c736600ca9c22029474394"}, + {file = "PyNaCl-1.5.0-cp36-abi3-manylinux_2_17_x86_64.manylinux2014_x86_64.manylinux_2_24_x86_64.whl", hash = "sha256:0c84947a22519e013607c9be43706dd42513f9e6ae5d39d3613ca1e142fba44d"}, + {file = "PyNaCl-1.5.0-cp36-abi3-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:06b8f6fa7f5de8d5d2f7573fe8c863c051225a27b61e6860fd047b1775807858"}, + {file = "PyNaCl-1.5.0-cp36-abi3-musllinux_1_1_aarch64.whl", hash = "sha256:a422368fc821589c228f4c49438a368831cb5bbc0eab5ebe1d7fac9dded6567b"}, + {file = "PyNaCl-1.5.0-cp36-abi3-musllinux_1_1_x86_64.whl", hash = "sha256:61f642bf2378713e2c2e1de73444a3778e5f0a38be6fee0fe532fe30060282ff"}, + {file = "PyNaCl-1.5.0-cp36-abi3-win32.whl", hash = "sha256:e46dae94e34b085175f8abb3b0aaa7da40767865ac82c928eeb9e57e1ea8a543"}, + {file = "PyNaCl-1.5.0-cp36-abi3-win_amd64.whl", hash = "sha256:20f42270d27e1b6a29f54032090b972d97f0a1b0948cc52392041ef7831fee93"}, + {file = "PyNaCl-1.5.0.tar.gz", hash = "sha256:8ac7448f09ab85811607bdd21ec2464495ac8b7c66d146bf545b0f08fb9220ba"}, +] + +[package.dependencies] +cffi = ">=1.4.1" + +[package.extras] +docs = ["sphinx (>=1.6.5)", "sphinx-rtd-theme"] +tests = ["hypothesis (>=3.27.0)", "pytest (>=3.2.1,!=3.3.0)"] + [[package]] name = "pyproject-api" version = "1.6.1" @@ -853,18 +1060,18 @@ testing = ["fields", "hunter", "process-tests", "pytest-xdist", "six", "virtuale [[package]] name = "python-gitlab" -version = "4.5.0" +version = "4.6.0" description = "A python wrapper for the GitLab API" optional = false python-versions = ">=3.8.0" files = [ - {file = "python_gitlab-4.5.0-py3-none-any.whl", hash = "sha256:b078b63afab7624ef2084aac64e3a9f4488f55b2234017e05df1b7260169cb52"}, - {file = "python_gitlab-4.5.0.tar.gz", hash = "sha256:0a106174949819912b9abb4232e39059f83f613177fdb1787097eb84481c64b2"}, + {file = "python_gitlab-4.6.0-py3-none-any.whl", hash = "sha256:b22e54344706851815ae5395f5f8f6503f9d3ef180e99ac9fc2ea66f59912a56"}, + {file = "python_gitlab-4.6.0.tar.gz", hash = "sha256:b56ae363890374caede853ef552e92c41551d605800de1c64ba61bcf25f237b0"}, ] [package.dependencies] -requests = ">=2.25.0" -requests-toolbelt = ">=0.10.1" +requests = ">=2.32.0" +requests-toolbelt = ">=1.0.0" [package.extras] autocompletion = ["argcomplete (>=1.10.0,<3)"] @@ -895,7 +1102,6 @@ files = [ {file = "PyYAML-6.0.1-cp311-cp311-win_amd64.whl", hash = "sha256:bf07ee2fef7014951eeb99f56f39c9bb4af143d8aa3c21b1677805985307da34"}, {file = "PyYAML-6.0.1-cp312-cp312-macosx_10_9_x86_64.whl", hash = "sha256:855fb52b0dc35af121542a76b9a84f8d1cd886ea97c84703eaa6d88e37a2ad28"}, {file = "PyYAML-6.0.1-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:40df9b996c2b73138957fe23a16a4f0ba614f4c0efce1e9406a184b6d07fa3a9"}, - {file = "PyYAML-6.0.1-cp312-cp312-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:a08c6f0fe150303c1c6b71ebcd7213c2858041a7e01975da3a99aed1e7a378ef"}, {file = "PyYAML-6.0.1-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:6c22bec3fbe2524cde73d7ada88f6566758a8f7227bfbf93a408a9d86bcc12a0"}, {file = "PyYAML-6.0.1-cp312-cp312-musllinux_1_1_x86_64.whl", hash = "sha256:8d4e9c88387b0f5c7d5f281e55304de64cf7f9c0021a3525bd3b1c542da3b0e4"}, {file = "PyYAML-6.0.1-cp312-cp312-win32.whl", hash = "sha256:d483d2cdf104e7c9fa60c544d92981f12ad66a457afae824d146093b8c294c54"}, @@ -932,13 +1138,13 @@ files = [ [[package]] name = "requests" -version = "2.32.0" +version = "2.32.3" description = "Python HTTP for Humans." optional = false python-versions = ">=3.8" files = [ - {file = "requests-2.32.0-py3-none-any.whl", hash = "sha256:f2c3881dddb70d056c5bd7600a4fae312b2a300e39be6a118d30b90bd27262b5"}, - {file = "requests-2.32.0.tar.gz", hash = "sha256:fa5490319474c82ef1d2c9bc459d3652e3ae4ef4c4ebdd18a21145a47ca4b6b8"}, + {file = "requests-2.32.3-py3-none-any.whl", hash = "sha256:70761cfe03c773ceb22aa2f671b4757976145175cdfca038c02654d061d6dcc6"}, + {file = "requests-2.32.3.tar.gz", hash = "sha256:55365417734eb18255590a9ff9eb97e9e1da868d4ccd6402399eaf68af20a760"}, ] [package.dependencies] @@ -983,22 +1189,6 @@ pygments = ">=2.13.0,<3.0.0" [package.extras] jupyter = ["ipywidgets (>=7.5.1,<9)"] -[[package]] -name = "setuptools" -version = "69.5.1" -description = "Easily download, build, install, upgrade, and uninstall Python packages" -optional = false -python-versions = ">=3.8" -files = [ - {file = "setuptools-69.5.1-py3-none-any.whl", hash = "sha256:c636ac361bc47580504644275c9ad802c50415c7522212252c033bd15f301f32"}, - {file = "setuptools-69.5.1.tar.gz", hash = "sha256:6c1fccdac05a97e598fb0ae3bbed5904ccb317337a51139dcd51453611bbb987"}, -] - -[package.extras] -docs = ["furo", "jaraco.packaging (>=9.3)", "jaraco.tidelift (>=1.4)", "pygments-github-lexers (==0.0.5)", "rst.linker (>=1.9)", "sphinx (>=3.5)", "sphinx-favicon", "sphinx-inline-tabs", "sphinx-lint", "sphinx-notfound-page (>=1,<2)", "sphinx-reredirects", "sphinxcontrib-towncrier"] -testing = ["build[virtualenv]", "filelock (>=3.4.0)", "importlib-metadata", "ini2toml[lite] (>=0.9)", "jaraco.develop (>=7.21)", "jaraco.envs (>=2.2)", "jaraco.path (>=3.2.0)", "mypy (==1.9)", "packaging (>=23.2)", "pip (>=19.1)", "pytest (>=6,!=8.1.1)", "pytest-checkdocs (>=2.4)", "pytest-cov", "pytest-enabler (>=2.2)", "pytest-home (>=0.5)", "pytest-mypy", "pytest-perf", "pytest-ruff (>=0.2.1)", "pytest-timeout", "pytest-xdist (>=3)", "tomli", "tomli-w (>=1.0.0)", "virtualenv (>=13.0.0)", "wheel"] -testing-integration = ["build[virtualenv] (>=1.0.3)", "filelock (>=3.4.0)", "jaraco.envs (>=2.2)", "jaraco.path (>=3.2.0)", "packaging (>=23.2)", "pytest", "pytest-enabler", "pytest-xdist", "tomli", "virtualenv (>=13.0.0)", "wheel"] - [[package]] name = "shellingham" version = "1.5.4" @@ -1084,13 +1274,13 @@ test = ["black (>=22.3.0,<23.0.0)", "coverage (>=6.2,<7.0)", "isort (>=5.0.6,<6. [[package]] name = "types-requests" -version = "2.31.0.20240406" +version = "2.32.0.20240523" description = "Typing stubs for requests" optional = false python-versions = ">=3.8" files = [ - {file = "types-requests-2.31.0.20240406.tar.gz", hash = "sha256:4428df33c5503945c74b3f42e82b181e86ec7b724620419a2966e2de604ce1a1"}, - {file = "types_requests-2.31.0.20240406-py3-none-any.whl", hash = "sha256:6216cdac377c6b9a040ac1c0404f7284bd13199c0e1bb235f4324627e8898cf5"}, + {file = "types-requests-2.32.0.20240523.tar.gz", hash = "sha256:26b8a6de32d9f561192b9942b41c0ab2d8010df5677ca8aa146289d11d505f57"}, + {file = "types_requests-2.32.0.20240523-py3-none-any.whl", hash = "sha256:f19ed0e2daa74302069bbbbf9e82902854ffa780bc790742a810a9aaa52f65ec"}, ] [package.dependencies] @@ -1098,13 +1288,13 @@ urllib3 = ">=2" [[package]] name = "typing-extensions" -version = "4.11.0" +version = "4.12.0" description = "Backported and Experimental Type Hints for Python 3.8+" optional = false python-versions = ">=3.8" files = [ - {file = "typing_extensions-4.11.0-py3-none-any.whl", hash = "sha256:c1f94d72897edaf4ce775bb7558d5b79d8126906a14ea5ed1635921406c0387a"}, - {file = "typing_extensions-4.11.0.tar.gz", hash = "sha256:83f085bd5ca59c80295fc2a82ab5dac679cbe02b9f33f7d83af68e241bea51b0"}, + {file = "typing_extensions-4.12.0-py3-none-any.whl", hash = "sha256:b349c66bea9016ac22978d800cfff206d5f9816951f12a7d0ec5578b0a819594"}, + {file = "typing_extensions-4.12.0.tar.gz", hash = "sha256:8cbcdc8606ebcb0d95453ad7dc5065e6237b6aa230a31e81d0f440c30fed5fd8"}, ] [[package]] @@ -1154,6 +1344,85 @@ files = [ {file = "wget-3.2.zip", hash = "sha256:35e630eca2aa50ce998b9b1a127bb26b30dfee573702782aa982f875e3f16061"}, ] +[[package]] +name = "wrapt" +version = "1.16.0" +description = "Module for decorators, wrappers and monkey patching." +optional = false +python-versions = ">=3.6" +files = [ + {file = "wrapt-1.16.0-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:ffa565331890b90056c01db69c0fe634a776f8019c143a5ae265f9c6bc4bd6d4"}, + {file = "wrapt-1.16.0-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:e4fdb9275308292e880dcbeb12546df7f3e0f96c6b41197e0cf37d2826359020"}, + {file = "wrapt-1.16.0-cp310-cp310-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:bb2dee3874a500de01c93d5c71415fcaef1d858370d405824783e7a8ef5db440"}, + {file = "wrapt-1.16.0-cp310-cp310-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:2a88e6010048489cda82b1326889ec075a8c856c2e6a256072b28eaee3ccf487"}, + {file = "wrapt-1.16.0-cp310-cp310-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:ac83a914ebaf589b69f7d0a1277602ff494e21f4c2f743313414378f8f50a4cf"}, + {file = "wrapt-1.16.0-cp310-cp310-musllinux_1_1_aarch64.whl", hash = "sha256:73aa7d98215d39b8455f103de64391cb79dfcad601701a3aa0dddacf74911d72"}, + {file = "wrapt-1.16.0-cp310-cp310-musllinux_1_1_i686.whl", hash = "sha256:807cc8543a477ab7422f1120a217054f958a66ef7314f76dd9e77d3f02cdccd0"}, + {file = "wrapt-1.16.0-cp310-cp310-musllinux_1_1_x86_64.whl", hash = "sha256:bf5703fdeb350e36885f2875d853ce13172ae281c56e509f4e6eca049bdfb136"}, + {file = "wrapt-1.16.0-cp310-cp310-win32.whl", hash = "sha256:f6b2d0c6703c988d334f297aa5df18c45e97b0af3679bb75059e0e0bd8b1069d"}, + {file = "wrapt-1.16.0-cp310-cp310-win_amd64.whl", hash = "sha256:decbfa2f618fa8ed81c95ee18a387ff973143c656ef800c9f24fb7e9c16054e2"}, + {file = "wrapt-1.16.0-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:1a5db485fe2de4403f13fafdc231b0dbae5eca4359232d2efc79025527375b09"}, + {file = "wrapt-1.16.0-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:75ea7d0ee2a15733684badb16de6794894ed9c55aa5e9903260922f0482e687d"}, + {file = "wrapt-1.16.0-cp311-cp311-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:a452f9ca3e3267cd4d0fcf2edd0d035b1934ac2bd7e0e57ac91ad6b95c0c6389"}, + {file = "wrapt-1.16.0-cp311-cp311-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:43aa59eadec7890d9958748db829df269f0368521ba6dc68cc172d5d03ed8060"}, + {file = "wrapt-1.16.0-cp311-cp311-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:72554a23c78a8e7aa02abbd699d129eead8b147a23c56e08d08dfc29cfdddca1"}, + {file = "wrapt-1.16.0-cp311-cp311-musllinux_1_1_aarch64.whl", hash = "sha256:d2efee35b4b0a347e0d99d28e884dfd82797852d62fcd7ebdeee26f3ceb72cf3"}, + {file = "wrapt-1.16.0-cp311-cp311-musllinux_1_1_i686.whl", hash = "sha256:6dcfcffe73710be01d90cae08c3e548d90932d37b39ef83969ae135d36ef3956"}, + {file = "wrapt-1.16.0-cp311-cp311-musllinux_1_1_x86_64.whl", hash = "sha256:eb6e651000a19c96f452c85132811d25e9264d836951022d6e81df2fff38337d"}, + {file = "wrapt-1.16.0-cp311-cp311-win32.whl", hash = "sha256:66027d667efe95cc4fa945af59f92c5a02c6f5bb6012bff9e60542c74c75c362"}, + {file = "wrapt-1.16.0-cp311-cp311-win_amd64.whl", hash = "sha256:aefbc4cb0a54f91af643660a0a150ce2c090d3652cf4052a5397fb2de549cd89"}, + {file = "wrapt-1.16.0-cp312-cp312-macosx_10_9_x86_64.whl", hash = "sha256:5eb404d89131ec9b4f748fa5cfb5346802e5ee8836f57d516576e61f304f3b7b"}, + {file = "wrapt-1.16.0-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:9090c9e676d5236a6948330e83cb89969f433b1943a558968f659ead07cb3b36"}, + {file = "wrapt-1.16.0-cp312-cp312-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:94265b00870aa407bd0cbcfd536f17ecde43b94fb8d228560a1e9d3041462d73"}, + {file = "wrapt-1.16.0-cp312-cp312-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:f2058f813d4f2b5e3a9eb2eb3faf8f1d99b81c3e51aeda4b168406443e8ba809"}, + {file = "wrapt-1.16.0-cp312-cp312-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:98b5e1f498a8ca1858a1cdbffb023bfd954da4e3fa2c0cb5853d40014557248b"}, + {file = "wrapt-1.16.0-cp312-cp312-musllinux_1_1_aarch64.whl", hash = "sha256:14d7dc606219cdd7405133c713f2c218d4252f2a469003f8c46bb92d5d095d81"}, + {file = "wrapt-1.16.0-cp312-cp312-musllinux_1_1_i686.whl", hash = "sha256:49aac49dc4782cb04f58986e81ea0b4768e4ff197b57324dcbd7699c5dfb40b9"}, + {file = "wrapt-1.16.0-cp312-cp312-musllinux_1_1_x86_64.whl", hash = "sha256:418abb18146475c310d7a6dc71143d6f7adec5b004ac9ce08dc7a34e2babdc5c"}, + {file = "wrapt-1.16.0-cp312-cp312-win32.whl", hash = "sha256:685f568fa5e627e93f3b52fda002c7ed2fa1800b50ce51f6ed1d572d8ab3e7fc"}, + {file = "wrapt-1.16.0-cp312-cp312-win_amd64.whl", hash = "sha256:dcdba5c86e368442528f7060039eda390cc4091bfd1dca41e8046af7c910dda8"}, + {file = "wrapt-1.16.0-cp36-cp36m-macosx_10_9_x86_64.whl", hash = "sha256:d462f28826f4657968ae51d2181a074dfe03c200d6131690b7d65d55b0f360f8"}, + {file = "wrapt-1.16.0-cp36-cp36m-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:a33a747400b94b6d6b8a165e4480264a64a78c8a4c734b62136062e9a248dd39"}, + {file = "wrapt-1.16.0-cp36-cp36m-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:b3646eefa23daeba62643a58aac816945cadc0afaf21800a1421eeba5f6cfb9c"}, + {file = "wrapt-1.16.0-cp36-cp36m-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:3ebf019be5c09d400cf7b024aa52b1f3aeebeff51550d007e92c3c1c4afc2a40"}, + {file = "wrapt-1.16.0-cp36-cp36m-musllinux_1_1_aarch64.whl", hash = "sha256:0d2691979e93d06a95a26257adb7bfd0c93818e89b1406f5a28f36e0d8c1e1fc"}, + {file = "wrapt-1.16.0-cp36-cp36m-musllinux_1_1_i686.whl", hash = "sha256:1acd723ee2a8826f3d53910255643e33673e1d11db84ce5880675954183ec47e"}, + {file = "wrapt-1.16.0-cp36-cp36m-musllinux_1_1_x86_64.whl", hash = "sha256:bc57efac2da352a51cc4658878a68d2b1b67dbe9d33c36cb826ca449d80a8465"}, + {file = "wrapt-1.16.0-cp36-cp36m-win32.whl", hash = "sha256:da4813f751142436b075ed7aa012a8778aa43a99f7b36afe9b742d3ed8bdc95e"}, + {file = "wrapt-1.16.0-cp36-cp36m-win_amd64.whl", hash = "sha256:6f6eac2360f2d543cc875a0e5efd413b6cbd483cb3ad7ebf888884a6e0d2e966"}, + {file = "wrapt-1.16.0-cp37-cp37m-macosx_10_9_x86_64.whl", hash = "sha256:a0ea261ce52b5952bf669684a251a66df239ec6d441ccb59ec7afa882265d593"}, + {file = "wrapt-1.16.0-cp37-cp37m-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:7bd2d7ff69a2cac767fbf7a2b206add2e9a210e57947dd7ce03e25d03d2de292"}, + {file = "wrapt-1.16.0-cp37-cp37m-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:9159485323798c8dc530a224bd3ffcf76659319ccc7bbd52e01e73bd0241a0c5"}, + {file = "wrapt-1.16.0-cp37-cp37m-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:a86373cf37cd7764f2201b76496aba58a52e76dedfaa698ef9e9688bfd9e41cf"}, + {file = "wrapt-1.16.0-cp37-cp37m-musllinux_1_1_aarch64.whl", hash = "sha256:73870c364c11f03ed072dda68ff7aea6d2a3a5c3fe250d917a429c7432e15228"}, + {file = "wrapt-1.16.0-cp37-cp37m-musllinux_1_1_i686.whl", hash = "sha256:b935ae30c6e7400022b50f8d359c03ed233d45b725cfdd299462f41ee5ffba6f"}, + {file = "wrapt-1.16.0-cp37-cp37m-musllinux_1_1_x86_64.whl", hash = "sha256:db98ad84a55eb09b3c32a96c576476777e87c520a34e2519d3e59c44710c002c"}, + {file = "wrapt-1.16.0-cp37-cp37m-win32.whl", hash = "sha256:9153ed35fc5e4fa3b2fe97bddaa7cbec0ed22412b85bcdaf54aeba92ea37428c"}, + {file = "wrapt-1.16.0-cp37-cp37m-win_amd64.whl", hash = "sha256:66dfbaa7cfa3eb707bbfcd46dab2bc6207b005cbc9caa2199bcbc81d95071a00"}, + {file = "wrapt-1.16.0-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:1dd50a2696ff89f57bd8847647a1c363b687d3d796dc30d4dd4a9d1689a706f0"}, + {file = "wrapt-1.16.0-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:44a2754372e32ab315734c6c73b24351d06e77ffff6ae27d2ecf14cf3d229202"}, + {file = "wrapt-1.16.0-cp38-cp38-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:8e9723528b9f787dc59168369e42ae1c3b0d3fadb2f1a71de14531d321ee05b0"}, + {file = "wrapt-1.16.0-cp38-cp38-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:dbed418ba5c3dce92619656802cc5355cb679e58d0d89b50f116e4a9d5a9603e"}, + {file = "wrapt-1.16.0-cp38-cp38-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:941988b89b4fd6b41c3f0bfb20e92bd23746579736b7343283297c4c8cbae68f"}, + {file = "wrapt-1.16.0-cp38-cp38-musllinux_1_1_aarch64.whl", hash = "sha256:6a42cd0cfa8ffc1915aef79cb4284f6383d8a3e9dcca70c445dcfdd639d51267"}, + {file = "wrapt-1.16.0-cp38-cp38-musllinux_1_1_i686.whl", hash = "sha256:1ca9b6085e4f866bd584fb135a041bfc32cab916e69f714a7d1d397f8c4891ca"}, + {file = "wrapt-1.16.0-cp38-cp38-musllinux_1_1_x86_64.whl", hash = "sha256:d5e49454f19ef621089e204f862388d29e6e8d8b162efce05208913dde5b9ad6"}, + {file = "wrapt-1.16.0-cp38-cp38-win32.whl", hash = "sha256:c31f72b1b6624c9d863fc095da460802f43a7c6868c5dda140f51da24fd47d7b"}, + {file = "wrapt-1.16.0-cp38-cp38-win_amd64.whl", hash = "sha256:490b0ee15c1a55be9c1bd8609b8cecd60e325f0575fc98f50058eae366e01f41"}, + {file = "wrapt-1.16.0-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:9b201ae332c3637a42f02d1045e1d0cccfdc41f1f2f801dafbaa7e9b4797bfc2"}, + {file = "wrapt-1.16.0-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:2076fad65c6736184e77d7d4729b63a6d1ae0b70da4868adeec40989858eb3fb"}, + {file = "wrapt-1.16.0-cp39-cp39-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:c5cd603b575ebceca7da5a3a251e69561bec509e0b46e4993e1cac402b7247b8"}, + {file = "wrapt-1.16.0-cp39-cp39-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:b47cfad9e9bbbed2339081f4e346c93ecd7ab504299403320bf85f7f85c7d46c"}, + {file = "wrapt-1.16.0-cp39-cp39-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:f8212564d49c50eb4565e502814f694e240c55551a5f1bc841d4fcaabb0a9b8a"}, + {file = "wrapt-1.16.0-cp39-cp39-musllinux_1_1_aarch64.whl", hash = "sha256:5f15814a33e42b04e3de432e573aa557f9f0f56458745c2074952f564c50e664"}, + {file = "wrapt-1.16.0-cp39-cp39-musllinux_1_1_i686.whl", hash = "sha256:db2e408d983b0e61e238cf579c09ef7020560441906ca990fe8412153e3b291f"}, + {file = "wrapt-1.16.0-cp39-cp39-musllinux_1_1_x86_64.whl", hash = "sha256:edfad1d29c73f9b863ebe7082ae9321374ccb10879eeabc84ba3b69f2579d537"}, + {file = "wrapt-1.16.0-cp39-cp39-win32.whl", hash = "sha256:ed867c42c268f876097248e05b6117a65bcd1e63b779e916fe2e33cd6fd0d3c3"}, + {file = "wrapt-1.16.0-cp39-cp39-win_amd64.whl", hash = "sha256:eb1b046be06b0fce7249f1d025cd359b4b80fc1c3e24ad9eca33e0dcdb2e4a35"}, + {file = "wrapt-1.16.0-py3-none-any.whl", hash = "sha256:6906c4100a8fcbf2fa735f6059214bb13b97f75b1a61777fcf6432121ef12ef1"}, + {file = "wrapt-1.16.0.tar.gz", hash = "sha256:5f370f952971e7d17c7d1ead40e49f32345a7f7a5373571ef44d800d06b1899d"}, +] + [[package]] name = "yattag" version = "1.15.2" @@ -1167,4 +1436,4 @@ files = [ [metadata] lock-version = "2.0" python-versions = ">=3.11,<4.0" -content-hash = "26f0eddec3f9c9b7d95408e902e780c90b93e06986922b6f78660efd1a8f867b" +content-hash = "bc62732e6bc05ab0e74fb70ee002b9b5e2f71c4c8e4ce0b0870aafbb39a1a3ed" diff --git a/pyproject.toml b/pyproject.toml index 63d918fe..b4810eb1 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -28,6 +28,7 @@ requests = "*" bs4 = "*" benchexec = "*" polars = "*" +PyGithub = "*" #pystemd is not set as dependency because it is not in the CI @@ -61,11 +62,19 @@ check_untyped_defs = "True" warn_return_any = "True" warn_unused_ignores = "True" show_error_codes = "True" -ignore_missing_imports = "True" [tool.pytest.ini_options] testpaths = ["tests"] +[[tool.mypy.overrides]] +module = [ + "benchexec","benchexec.util", + "benchexec.result","benchexec.tools.template", + "bs4","wget" +] +ignore_missing_imports = true + + [tool.ruff] target-version = "py37" line-length = 120 diff --git a/smtcomp/archive.py b/smtcomp/archive.py index d0d75f2c..426c34b9 100644 --- a/smtcomp/archive.py +++ b/smtcomp/archive.py @@ -38,6 +38,10 @@ def is_unpack_present(archive: defs.Archive, dst: Path) -> bool: return any(True for _ in d.iterdir()) +def command_path(command: defs.Command, archive: defs.Archive, dst: Path) -> Path: + return archive_unpack_dir(archive, dst).joinpath(command.binary) + + def find_command(command: defs.Command, archive: defs.Archive, dst: Path) -> Path: d = archive_unpack_dir(archive, dst) if not (d.exists()): @@ -101,3 +105,17 @@ def unpack(archive: defs.Archive, dst: Path) -> None: if not (is_unpack_present(archive, dst)): print("[red]Empty archive", archive_file) exit(1) + + +def download_unpack(s: defs.Submission, dst: Path) -> None: + """ + Download and unpack + """ + dst.mkdir(parents=True, exist_ok=True) + if s.archive: + download(s.archive, dst) + unpack(s.archive, dst) + for p in s.participations.root: + if p.archive: + download(p.archive, dst) + unpack(p.archive, dst) diff --git a/smtcomp/benchexec.py b/smtcomp/benchexec.py index 0c94f230..30a333ef 100644 --- a/smtcomp/benchexec.py +++ b/smtcomp/benchexec.py @@ -1,14 +1,40 @@ from pathlib import Path +import rich from os.path import relpath from typing import List, cast, Dict, Optional from yattag import Doc, indent from smtcomp import defs -from smtcomp.archive import find_command +from smtcomp.archive import find_command, archive_unpack_dir, command_path from pydantic import BaseModel import shlex +from re import sub + + +def get_suffix(track: defs.Track) -> str: + match track: + case defs.Track.Incremental: + return "_inc" + case defs.Track.ModelValidation: + return "_model" + case defs.Track.UnsatCore: + return "_unsatcore" + case defs.Track.SingleQuery: + return "" + case _: + raise ValueError("No Cloud or Parallel") + + +def get_xml_name(s: defs.Submission, track: defs.Track) -> str: + suffix = get_suffix(track) + return sub(r"\W+", "", s.name.lower()) + suffix + ".xml" + + +def tool_module_name(s: defs.Submission, incremental: bool) -> str: + suffix = "_inc" if incremental else "" + return sub(r"\W+", "", s.name.lower()) + suffix class CmdTask(BaseModel): @@ -17,7 +43,66 @@ class CmdTask(BaseModel): includesfiles: List[str] -def generate_xml(timelimit_s: int, memlimit_M: int, cpuCores: int, cmdtasks: List[CmdTask], file: Path) -> None: +def generate_benchmark_yml(benchmark: Path, expected_result: Optional[bool], orig_file: Optional[Path]) -> None: + ymlfile = benchmark.with_suffix(".yml") + with ymlfile.open("w") as f: + f.write("format_version: '2.0'\n\n") + + f.write(f"input_files: '{str(benchmark.name)}'\n\n") + + if orig_file is not None: + f.write(f"# original_files: '{str(orig_file)}'\n\n") + + expected_str = "true" if expected_result else "false" + f.write("properties:\n") + f.write(f" - property_file: '../../properties/SMT.prp'\n") + if expected_result is not None: + f.write(f" expected_verdict: {expected_str}\n") + + +def generate_tool_module(s: defs.Submission, cachedir: Path, incremental: bool) -> None: + name = tool_module_name(s, incremental) + file = cachedir / "tools" / f"{name}.py" + + with file.open("w") as f: + if incremental: + base_module = "incremental_tool" + base_class = "IncrementalSMTCompTool" + else: + base_module = "tool" + base_class = "SMTCompTool" + f.write(f"from tools.{base_module} import {base_class}\n\n") + f.write(f"class Tool({base_class}): # type: ignore\n") + + f.write(f" NAME = '{s.name}'\n") + if s.command is not None: + assert s.archive is not None + if s.command.compa_starexec: + executable_path = find_command(s.command, s.archive, cachedir) + executable = str(relpath(executable_path, start=str(cachedir))) + else: + executable = str(command_path(s.command, s.archive, Path())) + f.write(f" EXECUTABLE = '{executable}'\n") + + required_paths = [] + + if s.archive is not None: + archive_path = relpath(archive_unpack_dir(s.archive, cachedir), start=str(cachedir)) + required_paths.append(str(archive_path)) + for p in s.participations.root: + if p.archive is not None: + archive_path = relpath(archive_unpack_dir(p.archive, cachedir), start=str(cachedir)) + required_paths.append(str(archive_path)) + if required_paths: + f.write(f" REQUIRED_PATHS = {required_paths}\n") + + +def generate_tool_modules(s: defs.Submission, cachedir: Path) -> None: + generate_tool_module(s, cachedir, True) + generate_tool_module(s, cachedir, False) + + +def generate_xml(config: defs.Config, cmdtasks: List[CmdTask], file: Path, tool_module_name: str) -> None: doc, tag, text = Doc().tagtext() doc.asis('') @@ -27,13 +112,18 @@ def generate_xml(timelimit_s: int, memlimit_M: int, cpuCores: int, cmdtasks: Lis ) with tag( "benchmark", - tool=f"smtcomp.tool", - timelimit=f"{timelimit_s}s", - hardlimit=f"{timelimit_s+30}s", - memlimit=f"{memlimit_M} MB", - cpuCores=f"{cpuCores}", - displayname="SC", + tool=f"tools.{tool_module_name}", + timelimit=f"{config.timelimit_s}s", + hardlimit=f"{config.timelimit_s+30}s", + memlimit=f"{config.memlimit_M} MB", + cpuCores=f"{config.cpuCores}", ): + with tag("require", cpuModel="Intel Xeon E3-1230 v5 @ 3.40 GHz"): + text() + + with tag("resultfiles"): + text("**/error.log") + for cmdtask in cmdtasks: for includesfile in cmdtask.includesfiles: with tag("rundefinition", name=f"{cmdtask.name},{includesfile}"): @@ -42,67 +132,45 @@ def generate_xml(timelimit_s: int, memlimit_M: int, cpuCores: int, cmdtasks: Lis text(option) with tag("tasks", name="task"): with tag("includesfile"): - text(includesfile) + text(f"benchmarks/{includesfile}") + + with tag("propertyfile"): + text("benchmarks/properties/SMT.prp") file.write_text(indent(doc.getvalue())) -def cmdtask_for_submission(s: defs.Submission, cachedir: Path) -> List[CmdTask]: +def cmdtask_for_submission(s: defs.Submission, cachedir: Path, target_track: defs.Track) -> List[CmdTask]: res: List[CmdTask] = [] i = -1 for p in s.participations.root: command = cast(defs.Command, p.command if p.command else s.command) archive = cast(defs.Archive, p.archive if p.archive else s.archive) for track, divisions in p.get().items(): + if track != target_track: + continue + i = i + 1 - match track: - case defs.Track.Incremental: - suffix = "_inc" - mode = "trace" - case defs.Track.ModelValidation: - suffix = "_model" - mode = "direct" - case defs.Track.UnsatCore: - suffix = "" - mode = "direct" - case defs.Track.ProofExhibition: - suffix = "" - mode = "direct" - case defs.Track.SingleQuery: - suffix = "" - mode = "direct" - case defs.Track.Cloud | defs.Track.Parallel: - continue + suffix = get_suffix(track) tasks: list[str] = [] for _, logics in divisions.items(): tasks.extend([str(logic) + suffix for logic in logics]) if tasks: - executable_path = find_command(command, archive, cachedir) - executable = str(relpath(executable_path, start=str(cachedir))) if command.compa_starexec: assert command.arguments == [] + executable_path = find_command(command, archive, cachedir) + executable = str(relpath(executable_path, start=str(cachedir))) dirname = str(relpath(executable_path.parent, start=str(cachedir))) - if mode == "direct": - options = [ - "bash", - "-c", - f'FILE=$(realpath $1); (cd {shlex.quote(dirname)}; exec ./{shlex.quote(executable_path.name)} "$FILE")', - "compa_starexec", - ] - else: - assert mode == "trace" - options = [ - "bash", - "-c", - f'ROOT=$(pwd); FILE=$(realpath $1); (cd {shlex.quote(dirname)}; exec $ROOT/smtlib2_trace_executor ./{shlex.quote(executable_path.name)} "$FILE")', - "compa_starexec", - ] + options = [ + "bash", + "-c", + f'FILE=$(realpath $1); (cd {shlex.quote(dirname)}; exec ./{shlex.quote(executable_path.name)} "$FILE")', + "compa_starexec", + ] else: - if mode == "direct": - options = [executable] + command.arguments - else: - options = ["./smtlib2_trace_executor", executable] + command.arguments + executable = str(command_path(command, archive, Path())) + options = [executable] + command.arguments cmdtask = CmdTask( name=f"{s.name},{i},{track}", options=options, @@ -110,3 +178,24 @@ def cmdtask_for_submission(s: defs.Submission, cachedir: Path) -> List[CmdTask]: ) res.append(cmdtask) return res + + +def generate(s: defs.Submission, cachedir: Path, config: defs.Config) -> None: + generate_tool_modules(s, cachedir) + + for target_track in [ + defs.Track.SingleQuery, + defs.Track.Incremental, + defs.Track.ModelValidation, + defs.Track.UnsatCore, + ]: + res = cmdtask_for_submission(s, cachedir, target_track) + if res: + basename = get_xml_name(s, target_track) + file = cachedir / basename + generate_xml( + config=config, + cmdtasks=res, + file=file, + tool_module_name=tool_module_name(s, target_track == defs.Track.Incremental), + ) diff --git a/smtcomp/defs.py b/smtcomp/defs.py index 80abf247..75e2da42 100644 --- a/smtcomp/defs.py +++ b/smtcomp/defs.py @@ -5,50 +5,14 @@ import re from enum import Enum from pathlib import Path, PurePath -from typing import Any, Dict, cast, Optional +from typing import Any, Dict, cast, Optional, Iterable, TypeVar from pydantic import BaseModel, Field, RootModel, model_validator, ConfigDict from pydantic.networks import HttpUrl, validate_email +from datetime import date +from rich import print - -## Parameters that can change each year -class Config: - current_year = 2024 - oldest_previous_results = 2018 - timelimit_s = 60 - memlimit_M = 1024 * 20 - cpuCores = 4 - min_used_benchmarks = 300 - ratio_of_used_benchmarks = 0.5 - old_criteria = False - """"Do we try to emulate <= 2023 criteria that does not really follow the rules""" - invert_triviality = False - """Prioritize triviality as much as possible for testing purpose. - Look for simple problems instead of hard one""" - - def __init__(self: Config, seed: int | None) -> None: - self.__seed = seed - - def seed(self) -> int: - if self.__seed is None: - raise ValueError("The seed as not been set") - s = self.__seed - self.__seed = +1 - return s - - -class DataFiles: - def __init__(self, data: Path) -> None: - self.previous_results = [ - (year, data.joinpath(f"results-sq-{year}.json.gz")) - for year in range(Config.oldest_previous_results, Config.current_year) - ] - self.benchmarks = data.joinpath(f"benchmarks-{Config.current_year}.json.gz") - self.cached_non_incremental_benchmarks = data.joinpath( - f"benchmarks-non-incremental-{Config.current_year}.feather" - ) - self.cached_incremental_benchmarks = data.joinpath(f"benchmarks-incremental-{Config.current_year}.feather") - self.cached_previous_results = data.joinpath(f"previous-sq-results-{Config.current_year}.feather") +U = TypeVar("U") class EnumAutoInt(Enum): @@ -167,12 +131,14 @@ class SolverType(EnumAutoInt): wrapped = "wrapped" derived = "derived" standalone = "Standalone" + portfolio = "Portfolio" class Status(EnumAutoInt): Unsat = "unsat" Sat = "sat" Unknown = "unknown" + Incremental = "incremental" class Track(EnumAutoInt): @@ -1174,7 +1140,7 @@ class Participation(BaseModel, extra="forbid"): divisions: add all the logics of those divisions in each track logics: add all the specified logics in each selected track it exists - aws_dockerfile should be used only in conjunction with Cloud and Parallel track + aws_repository should be used only in conjunction with Cloud and Parallel track archive and command should not be used with Cloud and Parallel track. They superseed the one given at the root. """ @@ -1184,14 +1150,16 @@ class Participation(BaseModel, extra="forbid"): divisions: list[Division] = [] archive: Archive | None = None command: Command | None = None - aws_dockerfile: str | None = None + aws_repository: str | None = None experimental: bool = False @model_validator(mode="after") def check_archive(self) -> Participation: aws_track = {Track.Cloud, Track.Parallel} - if self.aws_dockerfile is not None and not set(self.tracks).issubset(aws_track): - raise ValueError("aws_dockerfile can be used only with Cloud and Parallel track") + if self.aws_repository is None and not set(self.tracks).isdisjoint(aws_track): + raise ValueError("aws_repository is required by Cloud and Parallel track") + if self.aws_repository is not None and not set(self.tracks).issubset(aws_track): + raise ValueError("aws_repository can be used only with Cloud and Parallel track") if (self.archive is not None or self.command is not None) and not set(self.tracks).isdisjoint(aws_track): raise ValueError("archive and command field can't be used with Cloud and Parallel track") return self @@ -1214,6 +1182,8 @@ def get(self, d: None | dict[Track, dict[Division, set[Logic]]] = None) -> dict[ def complete(self, archive: Archive | None, command: Command | None) -> ParticipationCompleted: archive = cast(Archive, archive if self.archive is None else self.archive) command = cast(Command, command if self.command is None else self.command) + if (self.aws_repository is not None) or set(self.tracks).issubset({Track.Cloud, Track.Parallel}): + raise ValueError("can't complete Cloud and Parallel track participations") return ParticipationCompleted( tracks=self.get(), archive=archive, command=command, experimental=self.experimental ) @@ -1222,20 +1192,27 @@ def complete(self, archive: Archive | None, command: Command | None) -> Particip import itertools +def union(s: Iterable[set[U]]) -> set[U]: + return functools.reduce(lambda x, y: x | y, s, set()) + + class Participations(RootModel): root: list[Participation] def get_divisions(self, l: list[Track] = list(Track)) -> set[Division]: """ " Return the divisions in which the solver participates""" tracks = self.get() - divs = [set(tracks[track].keys()) for track in l] - return functools.reduce(lambda x, y: x | y, divs) + return union(set(tracks[track].keys()) for track in l if track in tracks) def get_logics(self, l: list[Track] = list(Track)) -> set[Logic]: """ " Return the logics in which the solver participates""" tracks = self.get() - logics = itertools.chain.from_iterable([iter(tracks[track].values()) for track in l]) - return functools.reduce(lambda x, y: x | y, logics) + return union(itertools.chain.from_iterable([tracks[track].values() for track in l if track in tracks])) + + def get_logics_by_track(self) -> dict[Track, set[Logic]]: + """Return the logics in which the solver participates""" + tracks = self.get() + return dict((track, union(tracks[track].values())) for track in tracks) def get(self, d: None | dict[Track, dict[Division, set[Logic]]] = None) -> dict[Track, dict[Division, set[Logic]]]: if d is None: @@ -1258,13 +1235,18 @@ class Submission(BaseModel, extra="forbid"): solver_type: SolverType participations: Participations seed: int | None = None + competitive: bool = True @model_validator(mode="after") def check_archive(self) -> Submission: - if self.archive is None and not all(p.archive for p in self.participations.root): - raise ValueError("Field archive is needed in all participations if not present at the root") - if self.command is None and not all(p.command for p in self.participations.root): - raise ValueError("Field command is needed in all participations if not present at the root") + if self.archive is None and not all(p.archive or p.aws_repository for p in self.participations.root): + raise ValueError( + "Field archive (or aws_repository) is needed in all participations if not present at the root" + ) + if self.command is None and not all(p.command or p.aws_repository for p in self.participations.root): + raise ValueError( + "Field command (or aws_repository) is needed in all participations if not present at the root" + ) return self def uniq_id(self) -> str: @@ -1272,7 +1254,7 @@ def uniq_id(self) -> str: def complete_participations(self) -> list[ParticipationCompleted]: """Push defaults from the submission into participations""" - return [p.complete(self.archive, self.command) for p in self.participations.root] + return [p.complete(self.archive, self.command) for p in self.participations.root if p.aws_repository is None] class Smt2File(BaseModel): @@ -1360,3 +1342,94 @@ class Result(BaseModel): class Results(BaseModel): results: list[Result] + + +## Parameters that can change each year +class Config: + current_year = 2024 + oldest_previous_results = 2018 + timelimit_s = 60 + memlimit_M = 1024 * 20 + cpuCores = 4 + min_used_benchmarks = 300 + ratio_of_used_benchmarks = 0.5 + use_previous_results_for_status = True + """ + Complete the status given in the benchmarks using previous results + """ + old_criteria = False + """"Do we try to emulate <= 2023 criteria that does not really follow the rules""" + invert_triviality = False + """Prioritize triviality as much as possible for testing purpose. + Look for simple problems instead of hard one""" + + nyse_seed = None + """The integer part of one hundred times the opening value of the New York Stock Exchange Composite Index on the first day the exchange is open on or after the date specified in nyse_date""" + nyse_date = date(year=2024, month=6, day=10) + + aws_timelimit_hard = 600 + """ + Time in seconds upon which benchmarks are considered hards + """ + aws_num_selected = 400 + """ + Number of selected benchmarks + """ + + def __init__(self, data: Path | None) -> None: + if data is not None and data.name != "data": + raise ValueError("Consistency check, data directory must be named 'data'") + self._data = data + + @functools.cached_property + def data(self) -> Path: + if self._data is None: + raise ValueError("Configuration without data") + return self._data + + @functools.cached_property + def previous_results(self) -> list[tuple[int, Path]]: + return [ + (year, self.data.joinpath(f"results-sq-{year}.json.gz")) + for year in range(Config.oldest_previous_results, Config.current_year) + ] + + @functools.cached_property + def benchmarks(self) -> Path: + return self.data.joinpath(f"benchmarks-{Config.current_year}.json.gz") + + @functools.cached_property + def cached_non_incremental_benchmarks(self) -> Path: + return self.data.joinpath(f"benchmarks-non-incremental-{Config.current_year}.feather") + + @functools.cached_property + def cached_incremental_benchmarks(self) -> Path: + return self.data.joinpath(f"benchmarks-incremental-{Config.current_year}.feather") + + @functools.cached_property + def cached_previous_results(self) -> Path: + return self.data.joinpath(f"previous-sq-results-{Config.current_year}.feather") + + @functools.cached_property + def submissions(self) -> list[Submission]: + return [ + Submission.model_validate_json(Path(file).read_text()) for file in self.data.glob("../submissions/*.json") + ] + + @functools.cached_property + def seed(self) -> int: + unknown_seed = 0 + seed = 0 + for s in self.submissions: + if s.seed is None: + unknown_seed += 1 + else: + seed += s.seed + seed = seed % (2**30) + if self.nyse_seed is None: + print(f"[red]Warning[/red] NYSE seed not set, and {unknown_seed} submissions are missing a seed") + else: + if unknown_seed > 0: + raise ValueError(f"{unknown_seed} submissions are missing a seed") + seed += self.nyse_seed + return seed diff --git a/smtcomp/execution.py b/smtcomp/execution.py index 0f37cbb6..de31cefa 100644 --- a/smtcomp/execution.py +++ b/smtcomp/execution.py @@ -6,13 +6,11 @@ def trace_executor_url() -> str: - return ( - "https://github.com/SMT-COMP/trace-executor/releases/download/smtcomp2022/SMT-COMP-2022-trace-executor.tar.gz" - ) + return "https://github.com/SMT-COMP/trace-executor/releases/download/smtcomp2024-rc1/SMT-COMP-2024-trace-executor.tar.gz" def trace_executor_filename() -> str: - return "SMT-COMP-2022-trace-executor.tar.gz" + return "SMT-COMP-2024-trace-executor.tar.gz" def download_trace_executor(dst: Path) -> None: @@ -33,4 +31,8 @@ def unpack_trace_executor(dst: Path) -> None: def copy_tool_module(dst: Path) -> None: script_path = Path(__file__).parent - subprocess.run(["cp", script_path / "tool.py", dst]) + tools = dst / "tools" + tools.mkdir(parents=True, exist_ok=True) + subprocess.run(["cp", script_path / "tool.py", tools]) + subprocess.run(["cp", script_path / "incremental_tool.py", tools]) + subprocess.run(["touch", "__init__.py"]) diff --git a/smtcomp/generate_benchmarks.py b/smtcomp/generate_benchmarks.py index af819401..68d6eb83 100644 --- a/smtcomp/generate_benchmarks.py +++ b/smtcomp/generate_benchmarks.py @@ -1,50 +1,107 @@ from typing import Set, Dict from pathlib import Path from smtcomp import defs +from smtcomp.benchexec import generate_benchmark_yml, get_suffix def path_trivial_benchmark(dst: Path, track: defs.Track, logic: defs.Logic, status: defs.Status) -> Path: + """ + dst is the root of the generated benchmarks directory + """ match track: case defs.Track.Incremental: - suffix = "_inc" + assert status == defs.Status.Incremental + suffix = get_suffix(track) case defs.Track.ModelValidation: - suffix = "_model" + assert status != defs.Status.Incremental + suffix = get_suffix(track) case defs.Track.SingleQuery: - suffix = "" + assert status != defs.Status.Incremental + suffix = get_suffix(track) case defs.Track.UnsatCore | defs.Track.ProofExhibition | defs.Track.Cloud | defs.Track.Parallel: raise (ValueError("No trivial benchmarks yet for f{track}")) + logic_dir = dst.joinpath(f"files{suffix}", str(logic)) match status: case defs.Status.Sat: - return dst.joinpath("files", str(logic) + suffix + ".sat.smt2") + return logic_dir.joinpath(str(logic) + suffix + ".sat.smt2") case defs.Status.Unsat: - return dst.joinpath("files", str(logic) + suffix + ".unsat.smt2") + return logic_dir.joinpath(str(logic) + suffix + ".unsat.smt2") + case defs.Status.Incremental: + return logic_dir.joinpath(str(logic) + suffix + ".incremental.smt2") case defs.Status.Unknown: raise (ValueError("No trivial benchmarks yet for unknown")) def generate_trivial_benchmarks(dst: Path) -> None: + prop_dir = dst.joinpath("properties") + prop_dir.mkdir(parents=True, exist_ok=True) + (prop_dir / "SingleQuery.prp").touch() + dst.joinpath("files").mkdir(parents=True, exist_ok=True) + dst.joinpath("files_inc").mkdir(parents=True, exist_ok=True) for track, divisions in defs.tracks.items(): match track: - case defs.Track.Incremental: - suffix = "_inc" - case defs.Track.ModelValidation: - suffix = "_model" - case defs.Track.SingleQuery: - suffix = "" + case defs.Track.Incremental | defs.Track.ModelValidation | defs.Track.SingleQuery: + suffix = get_suffix(track) case defs.Track.UnsatCore | defs.Track.ProofExhibition | defs.Track.Cloud | defs.Track.Parallel: continue - for _, theories in divisions.items(): - for theory in theories: - file = dst.joinpath(str(theory) + suffix) - file_sat = path_trivial_benchmark(dst, track, theory, defs.Status.Sat) - file_unsat = path_trivial_benchmark(dst, track, theory, defs.Status.Unsat) + for _, logics in divisions.items(): + for logic in logics: + logic_name = str(logic) + logic_dir = dst.joinpath(f"files{suffix}", logic_name) + logic_dir.mkdir(parents=True, exist_ok=True) + file = dst.joinpath(logic_name + suffix) + + if track == defs.Track.Incremental: + file_incremental = path_trivial_benchmark(dst, track, logic, defs.Status.Incremental) + + file.write_text(f"files{suffix}/{logic_name}/*.smt2\n") + + benchmark = "\n".join([ + "sat", + "sat", + "unsat", + "--- BENCHMARK BEGINS HERE ---", + f"(set-logic {logic.value})", + "(assert true)", + "(check-sat)", + "(assert true)", + "(check-sat)", + "(assert false)", + "(check-sat)\n", + ]) + file_incremental.write_text(benchmark) + else: + file_sat = path_trivial_benchmark(dst, track, logic, defs.Status.Sat) + file_unsat = path_trivial_benchmark(dst, track, logic, defs.Status.Unsat) + file.write_text(f"files{suffix}/{logic_name}/*.yml\n") + + file_sat.write_text(f"(set-logic {logic.value})(check-sat)") + file_unsat.write_text(f"(set-logic {logic.value})(assert false)(check-sat)") - file.write_text("\n".join([str(file_sat.relative_to(dst)), str(file_unsat.relative_to(dst))])) + generate_benchmark_yml(file_sat, True, None) + generate_benchmark_yml(file_unsat, False, None) - file_sat.write_text(f"(set-logic {theory.value})(check-sat)") - file_unsat.write_text(f"(set-logic {theory.value})(assert false)(check-sat)") +def generate_benchmarks(cachedir: Path) -> None: + """ + Generate files included by benchexec + """ + dst = cachedir / "benchmarks" + prop_dir = dst.joinpath("properties") + prop_dir.mkdir(parents=True, exist_ok=True) + (prop_dir / "SMT.prp").touch() -def generate_benchmarks(dst: Path, seed: int) -> None: - return + dst.joinpath("files").mkdir(parents=True, exist_ok=True) + dst.joinpath("files_inc").mkdir(parents=True, exist_ok=True) + for track, divisions in defs.tracks.items(): + match track: + case defs.Track.Incremental | defs.Track.ModelValidation | defs.Track.SingleQuery: + suffix = get_suffix(track) + case defs.Track.UnsatCore | defs.Track.ProofExhibition | defs.Track.Cloud | defs.Track.Parallel: + continue + for _, theories in divisions.items(): + for theory in theories: + theory_name = str(theory) + file = dst.joinpath(theory_name + suffix) + file.write_text(f"files{suffix}/{theory_name}/*.yml\n") diff --git a/smtcomp/incremental_tool.py b/smtcomp/incremental_tool.py new file mode 100644 index 00000000..40de13a5 --- /dev/null +++ b/smtcomp/incremental_tool.py @@ -0,0 +1,86 @@ +from typing import List, Optional, Any +import benchexec.util as util +import benchexec.result as result +from benchexec.tools.template import BaseTool2 +import sys, re +import os + +TRACE_EXECUTOR = "./smtlib2_trace_executor" + + +class IncrementalSMTCompTool(BaseTool2): # type: ignore + """ + Generic incremental tool for smtcomp execution + """ + + REQUIRED_PATHS = ["."] + EXECUTABLE = "./false" + NAME = "SMT-COMP generic incremental tool" + + def determine_result(self, run: BaseTool2.Run) -> Any: # type: ignore + returncode: int = run.exit_code.value + returnsignal: int = run.exit_code.signal + output: List[str] = run.output + isTimeout: bool = run.was_timeout + + correct = 0 + status = None + + for line in output: + line = line.strip() + if line in ("sat", "unsat"): + correct += 1 + if line.startswith("WRONG"): + return "WRONG" + + if returnsignal is None: + status = "DONE" + elif ((returnsignal == 9) or (returnsignal == 15)) and isTimeout: + status = "TIMEOUT" + elif returnsignal == 9: + status = "KILLED BY SIGNAL 9" + elif returnsignal == 6: + status = "ABORTED" + elif returnsignal == 15: + status = "KILLED" + else: + status = "ERROR" + + return f"{status} ({correct} correct)" + + def executable(self, _: Any) -> str | Any | None: + return util.find_executable(self.EXECUTABLE, exitOnError=True) + + def version(self, executable: str) -> str: + return "" + + def name(self) -> str: + return self.NAME + + def cmdline( # type: ignore + self, + executable: str, + options: List[str], + task: BaseTool2.Task, + rlimits: BaseTool2.ResourceLimits, + ) -> Any: + tasks = task.input_files + options = options + ([] if task.options is None else task.options) + assert len(tasks) <= 1, "only one inputfile supported" + if options: + # executable and options were overridden by the task definition + return [TRACE_EXECUTOR, *options, *tasks] + else: + # using default executable + return [TRACE_EXECUTOR, executable, *tasks] + + def program_files(self, executable: str) -> Any: + files = [TRACE_EXECUTOR, executable] + self._program_files_from_executable(executable, self.REQUIRED_PATHS) + return files + + @staticmethod + def _program_files_from_executable(executable: str, required_paths: list[str]) -> Any: + scriptdir = os.path.dirname(os.path.abspath(__file__)) + basedir = os.path.join(scriptdir, os.path.pardir) + + return util.flatten(util.expand_filename_pattern(path, basedir) for path in required_paths) diff --git a/smtcomp/main.py b/smtcomp/main.py index b834c788..8e38b0a5 100644 --- a/smtcomp/main.py +++ b/smtcomp/main.py @@ -3,7 +3,7 @@ from pathlib import Path from typing import List, Optional, cast, Dict, Any, Annotated, TextIO import rich -from rich.progress import track +from rich.progress import track, Progress import rich.style from rich.tree import Tree from rich.table import Table @@ -11,14 +11,18 @@ import typer from pydantic import ValidationError from collections import defaultdict +import json import polars as pl import smtcomp.archive as archive import smtcomp.benchexec as benchexec +import smtcomp.benchexec import smtcomp.defs as defs import smtcomp.submission as submission import smtcomp.execution as execution +import smtcomp.model_validation as model_validation +import smtcomp.results as results from smtcomp.benchmarks import clone_group import smtcomp.convert_csv import smtcomp.generate_benchmarks @@ -28,6 +32,7 @@ import smtcomp.scramble_benchmarks from rich.console import Console import smtcomp.test_solver as test_solver +from concurrent.futures import ThreadPoolExecutor app = typer.Typer() @@ -54,32 +59,56 @@ def show( if prefix is not None: files = list(map(prefix.joinpath, files)) - def read_submission(file: Path) -> defs.Submission: - try: - return submission.read(str(file)) - except Exception as e: - rich.print(f"[red]Error during file parsing of {file}[/red]") - print(e) - exit(1) - - l = list(map(read_submission, files)) + l = list(map(submission.read_submission_or_exit, files)) - console = Console(record=into_comment_file is not None) - if into_comment_file is not None: - console.print("
Summary of modified submissions") + console = Console() for s in l: - if into_comment_file is not None: - console.print("") - console.print("```") - t = submission.tree_summary(s) + t = submission.rich_tree_summary(s) console.print(t) - if into_comment_file is not None: - console.print("```") - if into_comment_file is not None: - console.print("
") if into_comment_file is not None: - into_comment_file.write_text(console.export_text()) + with into_comment_file.open("w") as md: + md.write("
Summary of modified submissions\n\n") + for s in l: + submission.markdown_tree_summary(s, md) + md.write("
\n") + + +@app.command(rich_help_panel=submissions_panel) +def show_json(files: list[Path] = typer.Argument(None), prefix: Optional[Path] = None) -> None: + """ + Show information about solver submissions in JSON format + """ + + if prefix is not None: + files = list(map(prefix.joinpath, files)) + + l = list(map(submission.read_submission_or_exit, files)) + + data = [submission.raw_summary(s) for s in l] + print(json.dumps(data, indent=4)) + + +@app.command(rich_help_panel=submissions_panel) +def get_contacts(files: list[Path] = typer.Argument(None)) -> None: + """ + Find contact from submissions given as arguments + """ + l = list(map(submission.read_submission_or_exit, files)) + contacts = list(str(c) for c in itertools.chain.from_iterable([s.contacts for s in l])) + contacts.sort() + print("\n".join(contacts)) + + +@app.command(rich_help_panel=submissions_panel) +def get_seed(data: Path) -> None: + conf = defs.Config(data) + print(conf.seed) + + +@app.command(rich_help_panel=submissions_panel) +def merge_pull_requests_locally(C: str = ".") -> None: + submission.merge_all_submissions(C) @app.command(rich_help_panel=submissions_panel) @@ -125,7 +154,6 @@ def prepare_execution(dst: Path) -> None: @app.command(rich_help_panel=benchexec_panel) def generate_benchexec( files: List[Path], - dst: Path, cachedir: Path, timelimit_s: int = defs.Config.timelimit_s, memlimit_M: int = defs.Config.memlimit_M, @@ -133,30 +161,18 @@ def generate_benchexec( ) -> None: """ Generate the benchexec file for the given submissions + + (The cachedir directory need to contain unpacked archive only with compa_starexec command) """ - cmdtasks: List[benchexec.CmdTask] = [] + config = defs.Config(data=None) + config.timelimit_s = timelimit_s + config.memlimit_M = memlimit_M + config.cpuCores = cpuCores + + (cachedir / "tools").mkdir(parents=True, exist_ok=True) for file in track(files): s = submission.read(str(file)) - res = benchexec.cmdtask_for_submission(s, cachedir) - cmdtasks.extend(res) - benchexec.generate_xml( - timelimit_s=timelimit_s, memlimit_M=memlimit_M, cpuCores=cpuCores, cmdtasks=cmdtasks, file=dst - ) - - -# Should be moved somewhere else -def download_archive_aux(s: defs.Submission, dst: Path) -> None: - """ - Download and unpack - """ - dst.mkdir(parents=True, exist_ok=True) - if s.archive: - archive.download(s.archive, dst) - archive.unpack(s.archive, dst) - for p in s.participations.root: - if p.archive: - archive.download(p.archive, dst) - archive.unpack(p.archive, dst) + smtcomp.benchexec.generate(s, cachedir, config) @app.command(rich_help_panel=benchexec_panel) @@ -166,7 +182,7 @@ def download_archive(files: List[Path], dst: Path) -> None: """ for file in track(files): s = submission.read(str(file)) - download_archive_aux(s, dst) + archive.download_unpack(s, dst) @app.command() @@ -178,11 +194,11 @@ def generate_trivial_benchmarks(dst: Path) -> None: @app.command() -def generate_benchmarks(dst: Path, seed: int = 0) -> None: +def generate_benchmarks(cachedir: Path) -> None: """ Generate benchmarks for smtcomp """ - smtcomp.generate_benchmarks.generate_benchmarks(dst, seed) + smtcomp.generate_benchmarks.generate_benchmarks(cachedir) @app.command(rich_help_panel=benchmarks_panel) @@ -221,9 +237,9 @@ def create_benchmarks_list(src: Path, data: Path, scrambler: Optional[Path] = No incremental=cast(List[defs.InfoIncremental], files_incremental), non_incremental=cast(List[defs.InfoNonIncremental], files_non_incremental), ) - datafiles = defs.DataFiles(data) + config = defs.Config(data) print("Writing benchmarks file") - write_cin(datafiles.benchmarks, benchmarks.model_dump_json(indent=1)) + write_cin(config.benchmarks, benchmarks.model_dump_json(indent=1)) @app.command(rich_help_panel=benchmarks_panel) @@ -279,67 +295,14 @@ def merge_benchmarks(files: list[Path], dst: Path) -> None: OLD_CRITERIA = Annotated[bool, typer.Option(help="Simulate previous year criteria (needs only to be trivial one year)")] -@app.command(rich_help_panel=selection_panel) -def show_benchmarks_trivial_stats(data: Path, old_criteria: OLD_CRITERIA = False) -> None: - """ - Show statistics on the trivial benchmarks - - Never compet.: old benchmarks never run competitively (more than one prover) - """ - config = defs.Config(seed=None) - config.old_criteria = old_criteria - datafiles = defs.DataFiles(data) - benchmarks = pl.read_ipc(datafiles.cached_non_incremental_benchmarks) - results = pl.read_ipc(datafiles.cached_previous_results) - benchmarks_with_trivial_info = smtcomp.selection.add_trivial_run_info(benchmarks.lazy(), results.lazy(), config) - b3 = ( - benchmarks_with_trivial_info.group_by(["logic"]) - .agg( - trivial=pl.col("file").filter(trivial=True).len(), - not_trivial=pl.col("file").filter(trivial=False, run=True).len(), - old_never_ran=pl.col("file").filter(run=False, new=False).len(), - new=pl.col("file").filter(new=True).len(), - ) - .sort(by="logic") - .collect() - ) - table = Table(title="Statistics on the benchmark pruning") - - table.add_column("Logic", justify="left", style="cyan", no_wrap=True) - table.add_column("trivial", justify="right", style="green") - table.add_column("not trivial", justify="right", style="orange_red1") - table.add_column("never compet.", justify="right", style="magenta") - table.add_column("new", justify="right", style="magenta1") - - for d in b3.to_dicts(): - table.add_row( - str(defs.Logic.of_int(d["logic"])), - str(d["trivial"]), - str(d["not_trivial"]), - str(d["old_never_ran"]), - str(d["new"]), - ) - - table.add_section() - table.add_row( - "Total", - str(b3["trivial"].sum()), - str(b3["not_trivial"].sum()), - str(b3["old_never_ran"].sum()), - str(b3["new"].sum()), - ) - - print(table) - - @app.command(rich_help_panel=selection_panel) def show_sq_selection_stats( data: Path, - seed: int, old_criteria: OLD_CRITERIA = False, min_use_benchmarks: int = defs.Config.min_used_benchmarks, ratio_of_used_benchmarks: float = defs.Config.ratio_of_used_benchmarks, invert_triviality: bool = False, + use_previous_results_for_status: bool = defs.Config.use_previous_results_for_status, ) -> None: """ Show statistics on the benchmarks selected for single query track @@ -348,12 +311,13 @@ def show_sq_selection_stats( Never compet.: old benchmarks never run competitively (more than one prover) """ - config = defs.Config(seed=seed) + config = defs.Config(data) config.min_used_benchmarks = min_use_benchmarks config.ratio_of_used_benchmarks = ratio_of_used_benchmarks config.invert_triviality = invert_triviality config.old_criteria = old_criteria - benchmarks_with_info = smtcomp.selection.helper_compute_sq(data, config) + config.use_previous_results_for_status = use_previous_results_for_status + benchmarks_with_info = smtcomp.selection.helper_compute_sq(config) b3 = ( benchmarks_with_info.group_by(["logic"]) .agg( @@ -362,6 +326,8 @@ def show_sq_selection_stats( old_never_ran=pl.col("file").filter(run=False, new=False).len(), new=pl.col("new").sum(), selected=pl.col("file").filter(selected=True).len(), + selected_sat=pl.col("file").filter(selected=True, status=int(defs.Status.Sat)).len(), + selected_unsat=pl.col("file").filter(selected=True, status=int(defs.Status.Unsat)).len(), selected_already_run=pl.col("file").filter(selected=True, run=True).len(), ) .sort(by="logic") @@ -375,6 +341,8 @@ def show_sq_selection_stats( table.add_column("never compet.", justify="right", style="magenta") table.add_column("new", justify="right", style="magenta1") table.add_column("selected", justify="right", style="green3") + table.add_column("selected sat", justify="right", style="green4") + table.add_column("selected unsat", justify="right", style="green4") table.add_column("selected already run", justify="right", style="green4") used_logics = defs.logic_used_for_track(defs.Track.SingleQuery) @@ -392,6 +360,8 @@ def show_sq_selection_stats( str(d["old_never_ran"]), str(d["new"]), str(d["selected"]), + str(d["selected_sat"]), + str(d["selected_unsat"]), str(d["selected_already_run"]), ) @@ -403,6 +373,8 @@ def show_sq_selection_stats( str(b3["old_never_ran"].sum()), str(b3["new"].sum()), str(b3["selected"].sum()), + str(b3["selected_sat"].sum()), + str(b3["selected_unsat"].sum()), str(b3["selected_already_run"].sum()), ) @@ -420,9 +392,9 @@ def print_iterable(i: int, tree: Tree, a: Any) -> None: @app.command(rich_help_panel=data_panel) def create_cache(data: Path) -> None: - datafiles = defs.DataFiles(data) + config = defs.Config(data) print("Loading benchmarks") - bench = defs.Benchmarks.model_validate_json(read_cin(datafiles.benchmarks)) + bench = defs.Benchmarks.model_validate_json(read_cin(config.benchmarks)) bd: Dict[defs.Smt2File, int] = {} for i, smtfile in enumerate( itertools.chain(map(lambda x: x.file, bench.non_incremental), map(lambda x: x.file, bench.incremental)) @@ -445,7 +417,7 @@ def create_cache(data: Path) -> None: df = pl.DataFrame(bench_simplified) # df["family"] = df["family"].astype("string") # df["name"] = df["name"].astype("string") - df.write_ipc(datafiles.cached_non_incremental_benchmarks) + df.write_ipc(config.cached_non_incremental_benchmarks) print("Creating incremental benchmarks cache as feather file") bench_simplified = map( @@ -461,7 +433,7 @@ def create_cache(data: Path) -> None: df = pl.DataFrame(bench_simplified) # df["family"] = df["family"].astype("string") # df["name"] = df["name"].astype("string") - df.write_ipc(datafiles.cached_incremental_benchmarks) + df.write_ipc(config.cached_incremental_benchmarks) def convert(x: defs.Result, year: int) -> dict[str, int | str | float] | None: if x.file not in bd: @@ -478,39 +450,42 @@ def convert(x: defs.Result, year: int) -> dict[str, int | str | float] | None: } results_filtered: list[Any] = [] - for year, file in track(datafiles.previous_results, description="Loading json results"): + for year, file in track(config.previous_results, description="Loading json results"): results = defs.Results.model_validate_json(read_cin(file)) results_filtered.extend(filter(lambda x: x is not None, map(lambda r: convert(r, year), results.results))) print("Creating old results cache as feather file") df = pl.DataFrame(results_filtered) # df["solver"] = df["solver"].astype("string") - df.write_ipc(datafiles.cached_previous_results) - - -# def conv(x:defs.Smt2FileOld) -> defs.Info: -# return defs.Info( file = defs.Smt2File(logic=x.logic,family=x.family,name=x.name), status= x.status, asserts = x.asserts, check_sats = x.check_sats) - -# @app.command() -# def convert(src:Path,dst:Path) -> None: -# benchmarks = defs.BenchmarksOld.model_validate_json(read_cin(src)) -# benchmarks2 = defs.Benchmarks(files=list(map(conv,benchmarks.files))) -# write_cin(dst,benchmarks2.model_dump_json(indent=1)) + df.write_ipc(config.cached_previous_results) @app.command(rich_help_panel=benchexec_panel) -def scramble_benchmarks( - competition_track: str, src: Path, dstdir: Path, scrambler: Path, seed: int, max_workers: int = 8 +def select_and_scramble( + competition_track: defs.Track, + data: Path, + srcdir: Path, + cachedir: Path, + scrambler: Path, + max_workers: int = 8, + test: bool = False, ) -> None: """ - Use the scrambler to scramble the listed benchmarks and - write them to the destination directory. - Acceptable competition track names are single-query, - incremental, unsat-core, and model-validation. - The src file must contain one benchmark path per line. + Selects and scrambles the benchmarks and + writes them to the destination directory. + The srcdir must contain all benchmarks as + outlined in the data. """ - smtcomp.scramble_benchmarks.scramble(competition_track, src, dstdir, scrambler, seed, max_workers) + config = defs.Config(data) + + if test: + config.min_used_benchmarks = 20 + config.ratio_of_used_benchmarks = 0.0 + config.invert_triviality = True + config.seed = 1 + + smtcomp.scramble_benchmarks.select_and_scramble(competition_track, config, srcdir, cachedir, scrambler, max_workers) @app.command() @@ -538,17 +513,21 @@ def read_submission(file: Path) -> defs.Submission: out.write("""print("Testing provers")\n""") for sub in l: out.write(f"print({sub.name!r})\n") - download_archive_aux(sub, outdir) + archive.download_unpack(sub, outdir) for part in sub.complete_participations(): for track, divisions in part.tracks.items(): match track: - case defs.Track.Incremental: - statuses = [defs.Status.Sat, defs.Status.Unsat] case defs.Track.ModelValidation: statuses = [defs.Status.Sat] case defs.Track.SingleQuery: statuses = [defs.Status.Sat, defs.Status.Unsat] - case defs.Track.UnsatCore | defs.Track.ProofExhibition | defs.Track.Cloud | defs.Track.Parallel: + case ( + defs.Track.Incremental + | defs.Track.UnsatCore + | defs.Track.ProofExhibition + | defs.Track.Cloud + | defs.Track.Parallel + ): continue for _, logics in divisions.items(): for logic in logics: @@ -569,3 +548,16 @@ def read_submission(file: Path) -> defs.Submission: f"test({str(cmd)!r},{part.command.arguments!r},{str(file_sat)!r},{expected!r})\n" ) out.write("end()\n") + + +@app.command() +def check_model_locally(cachedir: Path, resultdirs: list[Path], max_workers: int = 8) -> None: + l: list[tuple[results.RunId, results.Run, model_validation.ValidationResult]] = [] + with Progress() as progress: + with ThreadPoolExecutor(max_workers) as executor: + for resultdir in resultdirs: + l2 = model_validation.check_results_locally(cachedir, resultdir, executor, progress) + for rid, r, result in l2: + if result.status != defs.Status.Sat: + l.append((rid, r, result)) + print(l) diff --git a/smtcomp/model_validation.py b/smtcomp/model_validation.py new file mode 100644 index 00000000..f553a51a --- /dev/null +++ b/smtcomp/model_validation.py @@ -0,0 +1,92 @@ +from dataclasses import dataclass +from pathlib import Path +import smtcomp.defs as defs +import subprocess +import smtcomp.results as results +from smtcomp.benchexec import get_suffix +from smtcomp.scramble_benchmarks import benchmark_files_dir +from concurrent.futures import ThreadPoolExecutor +from rich.progress import Progress + + +# ./dolmen --time=1h --size=40G --strict=false --check-model=true --report-style=minimal "$2" < "$1" &> error.txt +# EXITSTATUS=$? + +# if [ "$EXITSTATUS" = "0" ]; then +# echo "starexec-result=sat" +# echo "model_validator_status=VALID" +# elif [ "$EXITSTATUS" = "2" ]; then +# echo "starexec-result=unknown" +# echo "model_validator_status=LIMITREACHED" +# elif [ "$EXITSTATUS" = "5" ]; then +# echo "starexec-result=unsat" +# echo "model_validator_status=INVALID" +# else +# echo "starexec-result=unknown" +# echo "model_validator_status=UNKNOWN" +# fi +# echo "dolmenexit=$EXITSTATUS" +# if grep -q '^[EF]:' error.txt; then +# echo "model_validator_error="$(grep '^[EF]:' error.txt | head -1) +# fi +# exit 0 + + +@dataclass +class ValidationResult: + status: defs.Status + stderr: str + + +def check_locally(smt2_file: Path, model: str) -> ValidationResult: + r = subprocess.run( + [ + "dolmen", + "--time=1h", + "--size=40G", + "--strict=false", + "--check-model=true", + "--report-style=minimal", + smt2_file, + ], + input=model.encode(), + capture_output=True, + ) + match r.returncode: + case 0: + status = defs.Status.Sat + case 5: + status = defs.Status.Unsat + case 2: + # LimitReached + status = defs.Status.Unknown + case _: + status = defs.Status.Unknown + return ValidationResult(status, r.stderr.decode()) + + +def check_result_locally( + cachedir: Path, logfiles: results.LogFile, rid: results.RunId, r: results.Run +) -> ValidationResult: + if r.status == "true": + filedir = benchmark_files_dir(cachedir, rid.track) + logic = rid.includefile.removesuffix(get_suffix(rid.track)) + smt2_file = filedir / logic / (r.basename.removesuffix(".yml") + ".smt2") + model = logfiles.get_output(rid, r.basename) + return check_locally(smt2_file, model) + else: + return ValidationResult(defs.Status.Unknown, "") + + +def check_results_locally( + cachedir: Path, resultdir: Path, executor: ThreadPoolExecutor, progress: Progress +) -> list[tuple[results.RunId, results.Run, ValidationResult]]: + with results.LogFile(resultdir) as logfiles: + l = [(r.runid, b) for r in results.parse_results(resultdir) for b in r.runs if b.status == "true"] + return list( + progress.track( + executor.map((lambda v: (v[0], v[1], check_result_locally(cachedir, logfiles, v[0], v[1]))), l), + total=len(l), + description="checking models", + ) + ) diff --git a/smtcomp/results.py b/smtcomp/results.py new file mode 100644 index 00000000..975cb666 --- /dev/null +++ b/smtcomp/results.py @@ -0,0 +1,197 @@ +from typing import Optional, Iterator, Any +import functools +import smtcomp.defs as defs +import polars as pl +import xml.etree.ElementTree as ET +from pathlib import Path +from smtcomp.unpack import read_cin +from pydantic import BaseModel +from datetime import timedelta +from zipfile import ZipFile + + +class RunId(BaseModel): + solver: str + participation: int + track: defs.Track + includefile: str + + @classmethod + def unmangle(cls, s: str) -> "RunId": + name_l = s.split(",") + return RunId( + solver=name_l[0], + participation=int(name_l[1]), + track=defs.Track(name_l[2]), + # The name "task" is currently added at the end, name of the task + includefile=name_l[3].split(".")[0], + ) + + def mangle(self) -> str: + return ",".join([self.solver, str(self.participation), str(self.track), self.includefile]) + + +class Run(BaseModel): + basename: str + cputime_s: float + """ example: 0.211880968s""" + memory_B: int + """ example: 21127168B""" + status: str + """ example: true""" + walltime_s: float + """ example: 0.21279739192686975s""" + + # host: str + # """ example: pontos07""" + # blkio-read: str + # """ example: 0B """ + # blkio-write: str + # """ example: 0B """ + # category: str + # """ example: missing """ + # cpuCores: str + # """ example: 0 """ + # cputime-cpu0: str + # """ example: 0.211880968s """ + # memoryNodes: str + # """ example: 0 """ + # returnvalue: str + # """ example: 1 """ + # starttime: str + # """ example: 2024-06-07T19:57:32.499898+02:00""" + # vcloud-additionalEnvironment: str + # """ example: """ + # vcloud-cpuCoresDetails: str + # """ example: [Processor{0, core=0, socket=0} """ + # vcloud-debug: str + # """ example: false """ + # vcloud-generatedFilesCount: str + # """ example: 1 """ + # vcloud-matchedResultFilesCount: str + # """ example: 1 """ + # vcloud-maxLogFileSize: str + # """ example: 20 MB """ + # vcloud-memoryNodesAllocation: str + # """ example: {0=2.0 GB} """ + # vcloud-newEnvironment: str + # """ example: """ + # vcloud-outerwalltime: str + # """ example: 0.554s """ + # vcloud-runId: str + # """ example: 6a08ebbd-2af2-4c18-af44-429a0439fab """ + + +class Results(BaseModel): + runid: RunId + options: str + runs: list[Run] + + +def parse_time(s: str) -> float: + assert s[-1] == "s" + return float(s[:-1]) + + +def parse_size(s: str) -> int: + assert s[-1] == "B" + return int(s[:-1]) + + +def convert_run(r: ET.Element) -> Run: + basename = Path(r.attrib["name"]).name + cputime_s: Optional[float] = None + memory_B: Optional[int] = None + status: Optional[str] = None + walltime_s: Optional[float] = None + + for col in r.iterfind("column"): + value = col.attrib["value"] + match col.attrib["title"]: + case "cputime": + cputime_s = parse_time(value) + case "memory": + memory_B = parse_size(value) + case "status": + status = value + case "walltime": + walltime_s = parse_time(value) + + if cputime_s is None or memory_B is None or status is None or walltime_s is None: + raise ValueError("xml of results doesn't contains some expected column") + + return Run(basename=basename, cputime_s=cputime_s, memory_B=memory_B, status=status, walltime_s=walltime_s) + + +def parse_xml(file: Path) -> Results: + result = ET.fromstring(read_cin(file)) + runs = list(map(convert_run, result.iterfind("run"))) + return Results(runid=RunId.unmangle(result.attrib["name"]), options=result.attrib["options"], runs=runs) + + +def parse_results(resultdir: Path) -> Iterator[Results]: + return map(parse_xml, (resultdir.glob("*.xml.bz2"))) + + +def to_pl(r: Results) -> pl.LazyFrame: + lf = pl.LazyFrame(r.runs) + return lf.with_columns(solver=pl.lit(r.runid.solver), participation=r.runid.participation, track=int(r.runid.track)) + + +def parse_dir(dir: Path) -> pl.LazyFrame: + return pl.concat(map(lambda file: to_pl(parse_xml(file)), dir.glob("*.xml.bz2"))) + + +def log_filename(dir: Path) -> Path: + l = list(dir.glob("*.logfiles.zip")) + if len(l) != 1: + raise (ValueError(f"Directory {dir!r} doesn't contains *.logfiles.zip archive")) + return l[0] + + +### Benchexec add this header +# output_file.write( +# " ".join(map(util.escape_string_shell, args)) +# + "\n\n\n" +# + "-" * 80 +# + "\n\n\n" +# ) + + +@functools.cache +def benchexec_log_separator() -> str: + return "\n\n\n" + "-" * 80 + "\n\n\n" + + +class LogFile: + def __init__(self: "LogFile", dir: Path) -> None: + filename = log_filename(dir) + self.logfiles = ZipFile(filename) + self.name = Path(filename.name.removesuffix(".zip")) + + def __enter__(self: "LogFile") -> "LogFile": + return self + + def __exit__(self: "LogFile", exc_type: Any, exc_value: Any, traceback: Any) -> None: + self.close() + + def close(self) -> None: + self.logfiles.close() + + def get_log(self: "LogFile", r: RunId, basename: str) -> str: + """ + Return the output of the prover and the header with the commandline used + """ + p = str(self.name.joinpath(".".join([r.mangle(), basename, "log"]))) + return self.logfiles.read(p).decode() + + def get_output(self: "LogFile", r: RunId, basename: str) -> str: + """ + Return the output of the prover + """ + s = self.get_log(r, basename) + index = s.find(benchexec_log_separator()) + if index == -1: + raise ValueError(f"Log Header not found {r!r} {basename!r}") + index += len(benchexec_log_separator()) + return s[index:] diff --git a/smtcomp/scramble_benchmarks.py b/smtcomp/scramble_benchmarks.py index 1cf660c2..959f78b0 100644 --- a/smtcomp/scramble_benchmarks.py +++ b/smtcomp/scramble_benchmarks.py @@ -3,38 +3,138 @@ from rich.progress import track import subprocess import concurrent.futures +import smtcomp.defs as defs +from smtcomp.benchexec import generate_benchmark_yml, get_suffix +import polars as pl +import smtcomp.selection +from typing import Optional +import re -def scramble_file(files: list, line: int, dstdir: Path, args: list) -> None: - dst = Path.joinpath(dstdir, "scrambled" + str(line) + ".smt2") - subprocess.run(args, stdin=Path(str(files[line]).strip()).open("r"), stdout=dst.open("w")) +def benchmark_files_dir(cachedir: Path, track: defs.Track) -> Path: + suffix = get_suffix(track) + return cachedir / "benchmarks" / f"files{suffix}" -def scramble( - competition_track: str, benchmark_list: Path, dstdir: Path, scrambler: Path, seed: int, max_workers: int +status_pattern = re.compile(r"(set-info :status (sat|unsat|unknown))") + + +def get_expected_result(benchmark: Path) -> Optional[bool]: + for line in open(benchmark).readlines(): + m = status_pattern.search(line) + if m and m.group(2) != "unknown": + return m.group(2) == "sat" + + return None + + +def scramble_file(fdict: dict, incremental: bool, srcdir: Path, dstdir: Path, args: list) -> None: + if incremental: + i = "incremental" + else: + i = "non-incremental" + fsrc = ( + srcdir.joinpath(i) + .joinpath(str(defs.Logic.of_int(fdict["logic"]))) + .joinpath(Path(fdict["family"])) + .joinpath(fdict["name"]) + ) + dstdir = dstdir.joinpath(str(defs.Logic.of_int(fdict["logic"]))) + fdst = dstdir.joinpath("scrambled" + str(fdict["scramble_id"]) + ".smt2") + dstdir.mkdir(parents=True, exist_ok=True) + + if incremental: + subprocess.run( + ["grep", "-o", "(set-info :status \\(sat\\|unsat\\|unknown\\))"], + stdin=fsrc.open("r"), + stdout=fdst.open("w"), + ) + subprocess.run(["sed", "-i", "s/(set-info :status \\(.*\\))/\\1/", str(fdst)]) + with fdst.open("a") as dstfile: + dstfile.write("--- BENCHMARK BEGINS HERE ---\n") + subprocess.run(args, stdin=fsrc.open("r"), stdout=fdst.open("a")) + else: + subprocess.run(args, stdin=fsrc.open("r"), stdout=fdst.open("w")) + + expected = get_expected_result(fsrc) if not incremental else None + generate_benchmark_yml(fdst, expected, fsrc.relative_to(srcdir)) + + +def create_scramble_id(benchmarks: pl.LazyFrame, config: defs.Config) -> pl.LazyFrame: + files = benchmarks.sort("file").select(pl.col("file").shuffle(seed=config.seed)) + files = files.with_row_index(name="scramble_id") + return benchmarks.join(files, on="file") + + +def scramble_lazyframe( + benchmarks: pl.LazyFrame, + competition_track: defs.Track, + config: defs.Config, + srcdir: Path, + dstdir: Path, + scrambler: Path, + max_workers: int, ) -> None: args = [] - if competition_track == "single-query": - args = [scrambler, "-term_annot", "pattern", "-seed", str(seed)] - elif competition_track == "incremental": - args = [scrambler, "-term_annot", "pattern", "-incremental", "true", "-seed", str(seed)] - elif competition_track == "model-validation": - args = [scrambler, "-term_annot", "pattern", "-gen-model-val", "true", "-seed", str(seed)] - elif competition_track == "unsat-core": - args = [scrambler, "-term_annot", "pattern", "-gen-unsat-core", "true", "-seed", str(seed)] - else: - rich.print(f"[red]Not a known track name: {track}[/red]") - exit(1) + df = benchmarks.select("scramble_id", "logic", "family", "name", "file").collect() + df.select("scramble_id", "file").write_csv(dstdir / "original_id.csv") + files = df.to_dicts() + incremental = False + seed = config.seed - line = int(0) - files = benchmark_list.open().readlines() - dstdir.mkdir(parents=True, exist_ok=True) - executor = concurrent.futures.ThreadPoolExecutor(max_workers=max_workers) - results = list( - track( - executor.map(lambda line: scramble_file(files, line, dstdir, args), range(len(files))), - total=len(files), - description="Scrambling selected benchmarks...", + match competition_track: + case defs.Track.SingleQuery: + args = [scrambler, "-term_annot", "pattern", "-seed", str(seed)] + case defs.Track.Incremental: + args = [scrambler, "-term_annot", "pattern", "-incremental", "true", "-seed", str(seed)] + incremental = True + case defs.Track.ModelValidation: + args = [scrambler, "-term_annot", "pattern", "-gen-model-val", "true", "-seed", str(seed)] + case defs.Track.UnsatCore: + args = [scrambler, "-term_annot", "pattern", "-gen-unsat-core", "true", "-seed", str(seed)] + case defs.Track.ProofExhibition | defs.Track.Cloud | defs.Track.Parallel: + rich.print( + f"[red]The scramble_benchmarks command does not yet work for the competition track: {competition_track}[/red]" + ) + exit(1) + + with concurrent.futures.ThreadPoolExecutor(max_workers=max_workers) as executor: + results = list( + track( + executor.map(lambda fdict: scramble_file(fdict, incremental, srcdir, dstdir, args), files), + total=len(files), + description="Scrambling selected benchmarks...", + ) ) - ) - executor.shutdown() + + +def select_and_scramble( + competition_track: defs.Track, + config: defs.Config, + srcdir: Path, + cachedir: Path, + scrambler: Path, + max_workers: int, +) -> None: + dstdir = benchmark_files_dir(cachedir, competition_track) + dstdir.mkdir(parents=True, exist_ok=True) + match competition_track: + case defs.Track.SingleQuery: + selected = smtcomp.selection.helper_compute_sq(config) + case defs.Track.Incremental: + selected = smtcomp.selection.helper_compute_incremental(config) + case defs.Track.ModelValidation: + selected = smtcomp.selection.helper_compute_sq(config) + selected = selected.filter(status=int(defs.Status.Sat)) + case defs.Track.UnsatCore: + selected = smtcomp.selection.helper_compute_sq(config) + selected = selected.filter(status=int(defs.Status.Unsat)) + case defs.Track.ProofExhibition | defs.Track.Cloud | defs.Track.Parallel: + selected = smtcomp.selection.helper_compute_sq(config) + rich.print( + f"[red]The scramble_benchmarks command does not yet work for the competition track: {competition_track}[/red]" + ) + exit(1) + + selected = create_scramble_id(selected, config).filter(selected=True) + scramble_lazyframe(selected, competition_track, config, srcdir, dstdir, scrambler, max_workers) diff --git a/smtcomp/selection.py b/smtcomp/selection.py index 3dd1cc7e..ad8409f7 100644 --- a/smtcomp/selection.py +++ b/smtcomp/selection.py @@ -1,6 +1,6 @@ # mypy: allow-any-unimported -import functools +import functools, itertools from typing import Set, Dict, Optional, cast, List, DefaultDict from pathlib import Path, PurePath from smtcomp import defs @@ -38,29 +38,49 @@ def find_trivial(results: pl.LazyFrame, config: defs.Config) -> pl.LazyFrame: .agg( trivial= # All the results are sat or unsat and the time is below 1s - ((c_result != int(defs.Status.Unknown)) & (c_cpu_time <= 1.0)).all() + ((c_result != int(defs.Status.Unknown)) & (c_cpu_time <= 1.0)).all(), + # Compute the full result by year + result=pl.when((c_result == int(defs.Status.Sat)).sum() >= 2) + .then(int(defs.Status.Sat)) + .when((c_result == int(defs.Status.Unsat)).sum() >= 2) + .then(int(defs.Status.Unsat)) + .otherwise(int(defs.Status.Unknown)), ) .group_by("file") .agg( trivial=c_trivial.any() if config.old_criteria else c_trivial.all(), run=True, + result=pl.when((c_result == int(defs.Status.Sat)).any()) + .then(int(defs.Status.Sat)) + .when((c_result == int(defs.Status.Unsat)).any()) + .then(int(defs.Status.Unsat)) + .otherwise(int(defs.Status.Unknown)), ) ) return tally +def join_default_with_False(original: pl.LazyFrame, new: pl.LazyFrame, on: str) -> pl.LazyFrame: + return original.join(new, on="file", how="left", coalesce=True).fill_null(False) + + def add_trivial_run_info(benchmarks: pl.LazyFrame, previous_results: pl.LazyFrame, config: defs.Config) -> pl.LazyFrame: is_trivial = find_trivial(previous_results, config) - return ( - benchmarks.join(is_trivial, on="file", how="outer_coalesce") - .fill_null(False) - .with_columns(new=pl.col("family").str.starts_with(str(config.current_year))) + with_info = join_default_with_False(benchmarks, is_trivial, on="file").with_columns( + new=pl.col("family").str.starts_with(str(config.current_year)) ) + if config.use_previous_results_for_status: + with_info = with_info.with_columns( + status=pl.when(pl.col("status") != int(defs.Status.Unknown)).then(pl.col("status")).otherwise(c_result) + ) + + return with_info + -def sq_selection(benchmarks_with_info: pl.LazyFrame, config: defs.Config) -> pl.LazyFrame: - used_logics = defs.logic_used_for_track(defs.Track.SingleQuery) +def track_selection(benchmarks_with_info: pl.LazyFrame, config: defs.Config, target_track: defs.Track) -> pl.LazyFrame: + used_logics = defs.logic_used_for_track(target_track) # Keep only logics used by single query b = benchmarks_with_info.filter(c_logic.is_in(set(map(int, used_logics)))) @@ -93,14 +113,14 @@ def sq_selection(benchmarks_with_info: pl.LazyFrame, config: defs.Config) -> pl. new_benchmarks_sampled = ( pl.col("new_benchmarks") .filter(new_sample_size > 0) - .list.sample(n=new_sample_size.filter(new_sample_size > 0), seed=config.seed()) + .list.sample(n=new_sample_size.filter(new_sample_size > 0), seed=config.seed) .list.explode() .drop_nulls() ) old_benchmarks_sampled = ( pl.col("old_benchmarks") .filter(old_sample_size > 0) - .list.sample(n=old_sample_size.filter(old_sample_size > 0), seed=config.seed()) + .list.sample(n=old_sample_size.filter(old_sample_size > 0), seed=config.seed) .list.explode() .drop_nulls() ) @@ -115,16 +135,99 @@ def sq_selection(benchmarks_with_info: pl.LazyFrame, config: defs.Config) -> pl. ) -def helper_compute_sq(data: Path, config: defs.Config) -> pl.LazyFrame: +def helper_compute_sq(config: defs.Config) -> pl.LazyFrame: """ Returned columns: file (uniq id), logic, family,name, status, asserts nunmber, trivial, run (in previous year), new (benchmarks), selected """ - datafiles = defs.DataFiles(data) - benchmarks = pl.read_ipc(datafiles.cached_non_incremental_benchmarks) - results = pl.read_ipc(datafiles.cached_previous_results) + benchmarks = pl.read_ipc(config.cached_non_incremental_benchmarks) + results = pl.read_ipc(config.cached_previous_results) benchmarks_with_info = add_trivial_run_info(benchmarks.lazy(), results.lazy(), config) if config.invert_triviality: trivial_in_logic = pl.col("trivial").any().over(["logic"]) inverted_or_not_trivial = pl.when(trivial_in_logic).then(pl.col("trivial").not_()).otherwise(pl.col("trivial")) benchmarks_with_info = benchmarks_with_info.with_columns(trivial=inverted_or_not_trivial) - return sq_selection(benchmarks_with_info, config) + return track_selection(benchmarks_with_info, config, defs.Track.SingleQuery) + + +def helper_compute_incremental(config: defs.Config) -> pl.LazyFrame: + """ + Returned columns: file (uniq id), logic, family,name, status, asserts nunmber, trivial, run (in previous year), new (benchmarks), selected + """ + benchmarks = pl.read_ipc(config.cached_incremental_benchmarks) + results = pl.read_ipc(config.cached_previous_results) + benchmarks_with_info = add_trivial_run_info(benchmarks.lazy(), results.lazy(), config) + if config.invert_triviality: + trivial_in_logic = pl.col("trivial").any().over(["logic"]) + inverted_or_not_trivial = pl.when(trivial_in_logic).then(pl.col("trivial").not_()).otherwise(pl.col("trivial")) + benchmarks_with_info = benchmarks_with_info.with_columns(trivial=inverted_or_not_trivial) + return track_selection(benchmarks_with_info, config, defs.Track.Incremental) + + +def competitive_logics(config: defs.Config) -> pl.LazyFrame: + """ + returned columns track, logic, competitive:bool + """ + l = (s.participations.get_logics_by_track() for s in config.submissions) + dd = list(itertools.chain.from_iterable(map((lambda x: ((int(k), list(map(int, s))) for k, s in x.items())), l))) + return ( + pl.DataFrame(dd, schema=["track", "logic"]) + .lazy() + .explode("logic") + .group_by("track", "logic") + .agg(competitive=(pl.col("logic").len() > 1)) + ) + + +@functools.cache +def tracks() -> pl.LazyFrame: + """ + returned columns track, division, logic + """ + l = ( + (int(track), int(division), int(logic)) + for track, divisions in defs.tracks.items() + for division, logics in divisions.items() + for logic in logics + ) + return pl.DataFrame(l, schema=["track", "division", "logic"]).lazy() + + +def aws_selection(benchmarks: pl.LazyFrame, previous_results: pl.LazyFrame, config: defs.Config) -> pl.LazyFrame: + aws_track = [defs.Track.Cloud, defs.Track.Parallel] + + # Add division information to competitive logic + logics = competitive_logics(config).filter(pl.col("track").is_in(list(map(int, aws_track))), competitive=True) + logics = logics.join(tracks(), on=["track", "logic"], how="inner") + + # Keep only competitive logic from this track + b = benchmarks.join(logics, on="logic", how="inner") + previous_results = previous_results.join(b, on="file", how="semi") + + # Keep only hard and unsolved benchmarks + solved = c_result.is_in({int(defs.Status.Sat), int(defs.Status.Unsat)}) + solved_within_timelimit = solved & (c_cpu_time <= config.aws_timelimit_hard) + + hard_unsolved = ( + previous_results + # Remove bench solved within the timelimit by any solver + .filter(solved_within_timelimit.not_().all().over("file")) + .group_by("file") + .agg(hard=solved.any(), unsolved=solved.not_().all()) + ) + + b = b.join(hard_unsolved, how="inner", on="file") + + def sample(lf: pl.LazyFrame) -> pl.LazyFrame: + n = pl.min_horizontal(pl.col("file").list.len(), config.aws_num_selected) + return lf.with_columns(file=pl.col("file").list.sample(n=n, seed=config.seed)) + + # Sample at the logic level + b = sample(b.group_by("track", "division", "logic").agg(file=c_file)) + + # Sample at the division level + b = sample(b.group_by("track", "division").agg(file=c_file.flatten())) + + # Sample at the track level + b = sample(b.group_by("track").agg(file=c_file.flatten())) + + return b.explode("file").join(benchmarks, on="file", how="inner") diff --git a/smtcomp/submission.py b/smtcomp/submission.py index 01a1dbb5..35393559 100644 --- a/smtcomp/submission.py +++ b/smtcomp/submission.py @@ -1,17 +1,32 @@ from pathlib import Path - import rich from rich.tree import Tree - +from rich.progress import track +from typing import Any, TextIO from smtcomp.defs import Submission import smtcomp.defs as defs +from github import Github +from github.Repository import Repository +from github.ContentFile import ContentFile +import itertools +import subprocess +import git def read(file: str) -> Submission: return Submission.model_validate_json(Path(file).read_text()) -def tree_summary(s: Submission) -> Tree: +def read_submission_or_exit(file: Path) -> defs.Submission: + try: + return read(str(file)) + except Exception as e: + rich.print(f"[red]Error during file parsing of {file}[/red]") + print(e) + exit(1) + + +def rich_tree_summary(s: Submission) -> Tree: tree = Tree(f"[bold]{s.name}[/bold]") tree.add(f"{len(s.contributors)} authors") tree.add(f"website: {s.website}") @@ -35,5 +50,84 @@ def tree_summary(s: Submission) -> Tree: return tree +def raw_summary(s: Submission) -> dict[str, Any]: + data = dict[str, Any]() + data["name"] = s.name + data["authors"] = [c.name for c in s.contributors] + data["website"] = str(s.website) + data["archive_url"] = str(s.archive.url if s.archive is not None else "") + data["system_description"] = str(s.system_description) + data["tracks"] = dict[str, dict[str, list[str]]]() + + tracks = s.participations.get() + for track, divs in sorted(tracks.items()): + divisions = {} + for div, logics in sorted(divs.items()): + divisions[str(div)] = [str(l) for l in logics] + data["tracks"][str(track)] = divisions + + return data + + +def md_item(md: TextIO, s: str, level: int) -> None: + md.write(" " * level) + md.write("* ") + md.write(s) + md.write("\n") + + +def markdown_tree_summary(s: Submission, md: TextIO) -> None: + md.write(f"#### {s.name}\n\n") + md_item(md, f"{len(s.contributors)} authors", level=1) + md_item(md, f"website: {s.website}", level=1) + tracks = s.participations.get() + md_item(md, "Participations", level=1) + for track, divs in sorted(tracks.items()): + md_item(md, str(track), level=2) + for div, logics in sorted(divs.items()): + md_item(md, str(div), level=3) + not_logics = defs.tracks[track][div].difference(logics) + if len(not_logics) == 0: + md_item(md, "_all_", level=4) + elif len(not_logics) <= 3 and len(not_logics) < len(logics): + slogics = map(str, not_logics) + for logic in sorted(slogics): + md_item(md, f"~~{logic}~~", level=4) + else: + slogics = map(str, logics) + for logic in sorted(slogics): + md_item(md, logic, level=4) + + def show(s: Submission) -> None: - rich.print(tree_summary(s)) + rich.print(rich_tree_summary(s)) + + +def smtcomp_repo(g: Github) -> Repository: + return g.get_repo("SMT-COMP/smt-comp.github.io") + + +def commit_exists(repo: git.Repo, sha: str) -> git.Commit | None: + try: + return repo.commit(sha) + except Exception as e: + return None + + +def merge_all_submissions(local_repo_path: str) -> None: + with Github() as g: + with git.Repo(local_repo_path) as local_repo: + repo = smtcomp_repo(g) + pulls = repo.get_pulls(state="open") + fpulls = [p for p in pulls if "submission" in map(lambda l: l.name, p.labels)] + for p in track(fpulls, description="Fetch branch", total=pulls.totalCount): + if commit_exists(local_repo, p.head.sha) is None: + print(p.head.repo.ssh_url) + subprocess.run( + ["git", "-C", local_repo_path, "fetch", "--no-auto-gc", p.head.repo.ssh_url, p.head.ref] + ) + print("merge") + shas = [p.head.sha for p in fpulls] + message = "merge submissions\n\n" + "\n".join(f"#{p.number}: {p.title}" for p in fpulls) + print(shas) + subprocess.run(["git", "-C", local_repo_path, "merge", "-m", message] + shas) diff --git a/smtcomp/test_solver.py b/smtcomp/test_solver.py index f5225133..bdf4a94a 100644 --- a/smtcomp/test_solver.py +++ b/smtcomp/test_solver.py @@ -17,7 +17,7 @@ def parse_result(returnsignal: int | None, returncode: int, output: list[str]) - for line in output: line = line.strip() # ignore - if re.compile("^\s*(success|;.*)?\s*$").match(line): + if re.compile(r"^\s*(success|;.*)?\s*$").match(line): continue if line == "unsat": return "unsat" diff --git a/smtcomp/tool.py b/smtcomp/tool.py index d8030907..6a7144a5 100644 --- a/smtcomp/tool.py +++ b/smtcomp/tool.py @@ -3,16 +3,17 @@ import benchexec.result as result from benchexec.tools.template import BaseTool2 import sys, re +import os -fallback_name = "./false" - -class Tool(BaseTool2): # type: ignore +class SMTCompTool(BaseTool2): # type: ignore """ Generic tool for smtcomp execution """ - REQUIRED_PATHS = ["unpack"] + REQUIRED_PATHS = ["."] + EXECUTABLE = "./false" + NAME = "SMT-COMP generic tool" def determine_result(self, run: BaseTool2.Run) -> Any: # type: ignore """Adaptation of Jochen Hoenicke process script @@ -37,7 +38,7 @@ def determine_result(self, run: BaseTool2.Run) -> Any: # type: ignore for line in output: line = line.strip() # ignore - if re.compile("^\s*(success|;.*)?\s*$").match(line): + if re.compile(r"^\s*(success|;.*)?\s*$").match(line): continue if line == "unsat": return result.RESULT_FALSE_PROP @@ -62,13 +63,13 @@ def determine_result(self, run: BaseTool2.Run) -> Any: # type: ignore return status def executable(self, _: Any) -> str | Any | None: - return util.find_executable("smtlib2_trace_executor", fallback=fallback_name, exitOnError=False) + return util.find_executable(self.EXECUTABLE, exitOnError=True) def version(self, executable: str) -> str: return "" def name(self) -> str: - return "SC" + return self.NAME def cmdline( # type: ignore self, @@ -80,6 +81,21 @@ def cmdline( # type: ignore tasks = task.input_files options = options + ([] if task.options is None else task.options) assert len(tasks) <= 1, "only one inputfile supported" - assert len(options) >= 1, "options give the command to run" - return [executable, *options, *tasks] + if options: + # executable and options were overridden by the task definition + return [*options, *tasks] + else: + # using default executable + return [executable, *tasks] + + def program_files(self, executable: str) -> Any: + files = [executable] + self._program_files_from_executable(executable, self.REQUIRED_PATHS) + return files + + @staticmethod + def _program_files_from_executable(executable: str, required_paths: list[str]) -> Any: + scriptdir = os.path.dirname(os.path.abspath(__file__)) + basedir = os.path.join(scriptdir, os.path.pardir) + + return util.flatten(util.expand_filename_pattern(path, basedir) for path in required_paths) diff --git a/smtcomp/unpack.py b/smtcomp/unpack.py index cf6fc1ad..a06285c6 100644 --- a/smtcomp/unpack.py +++ b/smtcomp/unpack.py @@ -5,17 +5,31 @@ from zipfile import ZipFile import tarfile from stat import S_IXUSR -import gzip +import gzip, bz2 import io from typing import AnyStr, cast, IO +from subprocess import check_output, STDOUT +import os ZIP_UNIX_SYSTEM = 3 +def is_zip(file: Path) -> bool: + try: + with ZipFile(file, "r") as zf: + return zf.testzip() is None + except Exception as ex: + return False + + def zip_extract_all_with_executable_permission(file: Path, target_dir: Path) -> None: + # extract by calling `unzip`, because ZipFile does not handle symlinks + # https://stackoverflow.com/questions/19737570/how-do-i-preserve-symlinks-when-unzipping-an-archive-using-python + check_output(["unzip", "-q", str(file), "-d", str(target_dir)], stderr=STDOUT) + with ZipFile(file, "r") as zf: for info in zf.infolist(): - extracted_path = Path(zf.extract(info, target_dir)) + extracted_path = target_dir / Path(info.filename) if info.create_system == ZIP_UNIX_SYSTEM and extracted_path.is_file(): unix_attributes = info.external_attr >> 16 @@ -29,7 +43,7 @@ def tar_extract_all_with_executable_permission(file: Path, target_dir: Path) -> def extract_all_with_executable_permission(file: Path, target_dir: Path) -> None: - if str(file).endswith(".zip"): + if is_zip(file): zip_extract_all_with_executable_permission(file, target_dir) else: tar_extract_all_with_executable_permission(file, target_dir) @@ -48,5 +62,8 @@ def read_cin(file: Path) -> str: if file.name.endswith(".gz"): with gzip.open(file, "rt") as f: return f.read() + elif file.name.endswith(".bz2"): + with bz2.open(file, "rt") as f: + return f.read() else: return file.read_text() diff --git a/submissions/Amaya.json b/submissions/Amaya.json new file mode 100644 index 00000000..b112b506 --- /dev/null +++ b/submissions/Amaya.json @@ -0,0 +1,22 @@ +{ + "name": "Amaya", + "contributors": [ + "Vojtěch Havlena", "Michal Hečko", "Lukáš Holík", "Ondřej Lengál" + ], + "contacts": ["Michal Hečko ", "Ondřej Lengál "], + "archive": { + "url": "https://zenodo.org/records/11625128/files/amaya-smt-comp-2024-v6.tar.gz", + "h": { "sha256": "5a2e5051741fa5ab1110bb5829304301f222e3aa23e2124fb8ad4e07041bc630" } + }, + "website": "https://github.com/MichalHe/amaya", + "system_description": "https://github.com/VeriFIT/amaya-smt-comp/blob/master/system-description-2024/main.pdf", + "command": ["amaya/run.sh"], + "solver_type": "Standalone", + "participations": [ + { + "tracks": ["SingleQuery"], + "logics": ["LIA", "NIA"] + } + ], + "seed": "1337001337" +} diff --git a/submissions/COLIBRI.json b/submissions/COLIBRI.json new file mode 100644 index 00000000..4daeb6a7 --- /dev/null +++ b/submissions/COLIBRI.json @@ -0,0 +1,21 @@ +{ + "name": "COLIBRI", + "contributors": [ + "Bruno Marre", "François Bobot", "Christophe Junke" + ], + "contacts": ["Christophe Junke "], + "archive": { + "url": "https://drive.google.com/uc?export=download&id=1lJjQNgHRF14sGEW84eJ6tBsZ0-DBPMW2", + "h": { "sha256": "829fb89fc4a61dbc3180f400d75a283e967fef9c910ce4404a824608fb0b1c58" } + }, + "website": "http://colibri.frama-c.com/", + "system_description": "https://drive.google.com/file/d/13c5E0iNMvpTRjmhWKb286V25Dw4f6JOF/view?usp=sharing", + "command": ["smtcomp_2024/bin/starexec_run_default"], + "solver_type": "Standalone", + "participations": [ + { + "tracks": ["SingleQuery"], + "logics": "QF_.*FP.*" + } + ] +} diff --git a/submissions/STP.json b/submissions/STP.json new file mode 100644 index 00000000..8274f04f --- /dev/null +++ b/submissions/STP.json @@ -0,0 +1,40 @@ +{ + "name": "STP", + "contributors": [ + "Vijay Ganesh", + "Trevor Hansen", + "Mate Soos", + "Dan Liew", + "Ryan Govostes", + "Andrew V. Jones" + ], + "contacts": [ + "Trevor Hansen " + ], + "archive": { + "url": "https://github.com/stp/stp/releases/download/2.3.4_cadical/stp.tar", + "h": { "sha256": "33fa567fcc2467107dc147bace4324fe751ca9d65752264d624b7b4c1b52b432" } + }, + "website": "https://stp.github.io/", + "system_description": "https://github.com/stp/docs/tree/master/smt2024-descr/descr.pdf", + "solver_type": "Standalone", + "seed": "1343", + "participations": [ + { + "tracks": ["SingleQuery"], + "logics": ["QF_BV"], + "command": ["./stp"] + }, + { + "tracks": ["Incremental"], + "logics": ["QF_BV"], + "command": ["./stp"] + }, + { + "tracks": ["ModelValidation"], + "logics": ["QF_BV"], + "command": ["./stp"] + } + ] +} + diff --git a/submissions/Z3-alpha.json b/submissions/Z3-alpha.json new file mode 100644 index 00000000..85e6c680 --- /dev/null +++ b/submissions/Z3-alpha.json @@ -0,0 +1,35 @@ +{ + "name": "Z3-alpha", + "contributors": [ + "Zhengyang John Lu", "Paul Sarnighausen-Cahn", "Stefan Siemer", "Florin Manea", "Vijay Ganesh" + ], + "contacts": ["John Lu "], + "archive": { + "url": "https://zenodo.org/records/11643334/files/z3alpha.tar.gz?download=1" + }, + "website": "https://github.com/JohnLyu2/z3alpha", + "system_description": "https://drive.google.com/uc?export=download&id=17IULX6QpcqKJ51BzeT6XttAtyRwJIFyY", + "solver_type": "derived", + "command": ["z3alpha_submission/z3alpha.py"], + "seed": "1231", + "participations": [ + { + "tracks": ["SingleQuery"], + "divisions": [ + "Bitvec", + "QF_Bitvec", + "QF_Datatypes", + "QF_Equality", + "QF_LinearIntArith", + "QF_LinearRealArith", + "QF_NonLinearIntArith", + "QF_NonLinearRealArith", + "QF_Strings" + ] + }, + { + "tracks": ["SingleQuery"], + "logics": ["QF_AUFBV", "QF_UFBV"] + } + ] +} diff --git a/submissions/algaroba.json b/submissions/algaroba.json new file mode 100644 index 00000000..3c330242 --- /dev/null +++ b/submissions/algaroba.json @@ -0,0 +1,19 @@ +{ + "name": "Algaroba", + "contributors": [ + { "name": "Amar Shah", "website": "https://amarshah1.github.io/" }, + { "name": "Federico Mora", "website": "https://federico.morarocha.ca/" }, + { "name": "Sanjit Seshia", "website": "https://people.eecs.berkeley.edu/~sseshia/" } + ], + "contacts": ["Amar Shah "], + "archive": { + "url": "https://github.com/user-attachments/files/15844330/algaroba.tar.gz" + }, + "website": "https://github.com/uclid-org/algaroba", + "system_description": "https://github.com/uclid-org/algaroba/files/15255360/Algaroba_at_the_2024_SMTCOMP.pdf", + "command": ["algaroba/algaroba.exe"], + "solver_type": "wrapped", + "participations": [ + { "tracks": ["SingleQuery"], "logics": ["QF_DT", "QF_UFDT"], "divisions": ["QF_Datatypes"] } + ] +} diff --git a/submissions/bitwuzla.json b/submissions/bitwuzla.json new file mode 100644 index 00000000..594f4f43 --- /dev/null +++ b/submissions/bitwuzla.json @@ -0,0 +1,39 @@ +{ + "name": "Bitwuzla", + "contributors": ["Aina Niemetz", "Mathias Preiner"], + "contacts": ["Mathias Preiner "], + + "archive": { + "url": "https://zenodo.org/records/11754739/files/bitwuzla-submission-smtcomp-2024.zip?download=1", + "h": {"sha256": "f5bbe44bc12465ed2e1be9512d8b9a9f2bb9f8f16d1bd2bbef0f348e659a6e4d"} + }, + + "command": ["bin/bitwuzla"], + + "website": "https://bitwuzla.github.io", + "system_description": "https://bitwuzla.github.io/data/smtcomp2024/paper.pdf", + "solver_type": "Standalone", + "seed": "42", + "participations": [ + { + "tracks": ["SingleQuery"], + "logics": "^((QF_)?(A)?(UF)?(BV|FP|FPLRA)+)$", + "command": ["bin/bitwuzla", "--abstraction", "--abstraction-bv-size=33"] + }, + { + "tracks": ["Incremental"], + "logics": "^((QF_)?(A)?(UF)?(BV|FP|FPLRA)+)$", + "command": ["bin/bitwuzla", "--no-pp-normalize"] + }, + { + "tracks": ["UnsatCore"], + "logics": "^((QF_)?(A)?(UF)?(BV|FP|FPLRA)+)$", + "command": ["bin/bitwuzla", "--abstraction", "--abstraction-bv-size=33"] + }, + { + "tracks": ["ModelValidation"], + "logics": "^((QF_)?(A)?(UF)?(BV|FP|FPLRA)+)$", + "command": ["bin/bitwuzla", "--abstraction", "--abstraction-bv-size=33"] + } + ] +} diff --git a/submissions/cvc5.json b/submissions/cvc5.json new file mode 100644 index 00000000..576dfad3 --- /dev/null +++ b/submissions/cvc5.json @@ -0,0 +1,62 @@ +{ + "name": "cvc5", + "contributors": [ + "Leni Aniva", + "Haniel Barbosa", + "Clark Barrett", + "Hanna Lachnitt", + "Daniel Larraz", + "Abdalrhman Mohamed", + "Mudathir Mohamed", + "Aina Niemetz", + "Alex Ozdemir", + "Mathias Preiner", + "Andrew Reynolds", + "Hans-Jörg Schurr", + "Cesare Tinelli", + "Amalee Wilson", + "Yoni Zohar" + ], + "contacts": [ + "Hans-Jörg Schurr ", + "Amalee Wilson ", + "Clark Barrett " + ], + "archive": { + "url": "https://zenodo.org/records/11581520/files/cvc5-default.zip", + "h": { + "sha256": "4e8b6f6aaa8a22afec427633e66d1880f9f106efca4aa35d143cd97f90f2b3bb" + } + }, + "website": "https://cvc5.github.io/", + "system_description": "https://zenodo.org/records/11581520/files/cvc5.pdf", + "command": [ "bin/starexec_run_sq" ], + "solver_type": "Standalone", + "participations": [ + { + "tracks": [ "SingleQuery" ], + "logics": ".*" + }, + { + "tracks": [ "UnsatCore" ], + "logics": ".*", + "command": [ "bin/starexec_run_uc" ] + }, + { + "tracks": [ "ModelValidation" ], + "logics": ".*", + "command": [ "bin/starexec_run_mv" ] + }, + { + "tracks": [ "Incremental" ], + "logics": ".*", + "archive": { + "url": "https://zenodo.org/records/11581520/files/cvc5-inc.zip", + "h": { + "sha256": "25d7fb5461a5b4b96e75145d95700085db81f3b0f6c7af556b47a2aaf1fbcd96" + } + }, + "command": [ "bin/smtcomp_run_incremental" ] + } + ] +} diff --git a/submissions/iprover_smtcomp.json b/submissions/iprover_smtcomp.json new file mode 100644 index 00000000..d7c630c1 --- /dev/null +++ b/submissions/iprover_smtcomp.json @@ -0,0 +1,37 @@ +{ + "archive" : { + "h" : { + "sha256" : "8f7f4bad13e87d6aaa1bb8ca78b102edaa5495caf65d5fe39c3c16d6f70003d6" + }, + "url" : "https://zenodo.org/records/11671867/files/iprover_v3.9_smt_comp_2024.zip" + }, + "command" : [ + "bin/iprover_smtcomp.sh" + ], + "contacts" : [ + "Konstantin Korovin " + ], + "contributors" : [ + { + "name" : "Konstantin Korovin", + "website" : "http://www.cs.man.ac.uk/~korovink/" + } + ], + "name" : "iProver v3.9", + "participations" : [ + { + "divisions" : [ + "Arith", + "Equality", + "Equality+LinearArith", + "Equality+NonLinearArith" + ], + "tracks" : [ + "SingleQuery" + ] + } + ], + "solver_type" : "wrapped", + "system_description" : "http://www.cs.man.ac.uk/~korovink/iprover-smt-comp-2024.pdf", + "website" : "https://gitlab.com/korovin/iprover" +} diff --git a/submissions/opensmt.json b/submissions/opensmt.json new file mode 100644 index 00000000..837e587d --- /dev/null +++ b/submissions/opensmt.json @@ -0,0 +1,44 @@ +{ + "name": "OpenSMT", + "contributors": [ + { "name": "Tomáš Kolárik", "website": "https://github.com/Tomaqa" } + , + { "name": "Martin Blicha", "website": "https://github.com/blishko" } + ], + "contacts": [ + "Tomáš Kolárik " + , + "Martin Blicha " + ], + "archive": { + "url": "https://zenodo.org/records/11371847/files/opensmt.tgz" + , + "h": { "sha256": "f42b6f25012344f76886305d3177eda610999508224135445bb119582d12b30c" } + }, + "command": ["./opensmt"], + "website": "https://github.com/usi-verification-and-security/opensmt", + "system_description": "https://github.com/usi-verification-and-security/opensmt-doc/blob/master/smt-comp/abstract-2024.pdf", + "solver_type": "Standalone", + "participations": [ + { + "tracks": ["SingleQuery", "Incremental", "UnsatCore"], + "logics": [ + "QF_UF", "QF_AX", + "QF_IDL", "QF_RDL", "QF_LIA", "QF_LRA", + "QF_UFIDL", "QF_UFLIA", "QF_UFLRA", + "QF_ALIA", + "QF_AUFLIA" + ] + } + , + { + "tracks": ["ModelValidation"], + "logics": [ + "QF_UF", + "QF_IDL", "QF_RDL", "QF_LIA", "QF_LRA", + "QF_UFIDL", "QF_UFLIA", "QF_UFLRA" + ] + } + ], + "seed": 13 +} diff --git a/submissions/ostrich.json b/submissions/ostrich.json new file mode 100644 index 00000000..b51457ae --- /dev/null +++ b/submissions/ostrich.json @@ -0,0 +1,27 @@ +{ + "name": "OSTRICH", + "contributors": [ + "Matthew Hague", + "Denghang Hu", + "Anthony W. Lin", + "Oliver Markgraf", + "Philipp Rümmer", + "Zhilin Wu" + ], + "contacts": [ + "Oliver Markgraf ", + "Philipp Rümmer " + ], + "archive": { + "url": "https://philipp.ruemmer.org/ostrich-2024.tar.gz", + "h": { "sha256": "bd9abdeb26c1b4541fee5ad61ef190c6055ef00b306d62739ad5704cb6e0ca4c" } + }, + "website": "https://github.com/uuverifiers/ostrich", + "system_description": "https://philipp.ruemmer.org/ostrich-2024.pdf", + "command": ["./ostrich", "-portfolio=strings", "+quiet"], + "solver_type": "Standalone", + "seed": "753", + "participations": [ + { "tracks": ["SingleQuery"], "divisions": ["QF_Strings"] } + ] +} diff --git a/submissions/plat-smt.json b/submissions/plat-smt.json new file mode 100644 index 00000000..79b01aa8 --- /dev/null +++ b/submissions/plat-smt.json @@ -0,0 +1,35 @@ +{ + "name": "plat-smt", + "contributors": [ + "David Ewert" + ], + "contacts": ["David Ewert "], + "archive": { + "url": "https://github.com/dewert99/plat-smt/releases/download/SMT-COMP2024-v2/plat-smt.zip", + "h": { "sha256": "6f209d0fe11e3aca548a769d39cf5bb8294fda64e3a3667514246ec2b3d95966" } + }, + "website": "https://github.com/dewert99/plat-smt", + "system_description": "https://github.com/user-attachments/files/15831637/PlatSMT_2024_System_Description.pdf", + "command": ["./plat-smt"], + "solver_type": "wrapped", + "seed": 6536, + "participations": [ + { + "tracks": ["SingleQuery"], + "logics": ["QF_UF"] + }, + { + "tracks": ["Incremental"], + "logics": ["QF_UF"], + "command": ["./plat-smt", "-i"] + }, + { + "tracks": ["UnsatCore"], + "logics": ["QF_UF"] + }, + { + "tracks": ["ModelValidation"], + "logics": ["QF_UF"] + } + ] +} diff --git a/submissions/smtinterpol.json b/submissions/smtinterpol.json new file mode 100644 index 00000000..6ee63061 --- /dev/null +++ b/submissions/smtinterpol.json @@ -0,0 +1,55 @@ +{ + "name": "SMTInterpol", + "contributors": [ + "Max Barth", "Leon Cacace", + "Jürgen Christ", "Daniel Dietsch", "Leonard Fichtner", + "Joanna Greulich", "Elisabeth Henkel", "Matthias Heizmann", + "Jochen Hoenicke", "Moritz Mohr", "Alexander Nutz", + "Markus Pomrehn", "Pascal Raiola", "Tanja Schindler" + ], + "contacts": [ + "Max Barth ", + "Jochen Hoenicke " + ], + "archive": { + "url": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/smtinterpol-2.5-1381-g0e9bd0bf.tar.gz", + "h": { "sha256": "3616fff7345b8ef9b12e488d4757bffb487fef3cd118737ede67f22382877c2e" } + }, + "website": "https://ultimate.informatik.uni-freiburg.de/smtinterpol", + "system_description": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/sysdesc2024.pdf", + "command": ["smtinterpol"], + "solver_type": "Standalone", + "seed": "4223469823", + "participations": [ + { + "tracks": ["SingleQuery"], + "logics": "(QF_)?(AX?)?(UF)?(DT)?([IR]DL|[NL][IR]*A)?", + "command": ["smtinterpol"] + }, + { + "tracks": ["SingleQuery"], + "logics": "(QF_)?(AX?)?(UF)?BV(DT)?([IR]DL|[NL][IR]*A)?", + "command": ["smtinterpol-bv"] + }, + { + "tracks": ["Incremental"], + "logics": "(QF_)?(AX?)?(UF)?(DT)?([IR]DL|[NL][IR]*A)?", + "command": ["smtinterpol"] + }, + { + "tracks": ["Incremental"], + "logics": "(QF_)?(AX?)?(UF)?BV(DT)?([IR]DL|[NL][IR]*A)?", + "command": ["smtinterpol-bv"] + }, + { + "tracks": ["ModelValidation"], + "logics": "(QF_)(AX?)?(UF)?(BV)?(DT)?([IR]DL|[NL][IR]*A)?", + "command": ["smtinterpol"] + }, + { + "tracks": ["UnsatCore"], + "logics": "(QF_)?(AX?)?(UF)?(DT)?([IR]DL|[NL][IR]*A)?", + "command": ["smtinterpol"] + } + ] +} diff --git a/submissions/smtrat.json b/submissions/smtrat.json new file mode 100644 index 00000000..f5a82b9d --- /dev/null +++ b/submissions/smtrat.json @@ -0,0 +1,21 @@ +{ + "name": "SMT-RAT", + "contributors": [ + "Jasper Nalbach", + "Valentin Promies", + "Erika Ábrahám" + ], + "contacts": ["Jasper Nalbach ", "Valentin Promies "], + "archive": { + "url": "https://github.com/ths-rwth/smtrat/releases/download/24.06/smtrat.tgz" + }, + "website": "https://github.com/ths-rwth/smtrat", + "system_description": "https://github.com/ths-rwth/smtrat/blob/master/doc/smtcomp-description/smtcomp-2024.pdf", + "command": [ "./smtrat" ], + "solver_type": "Standalone", + "seed": 174228, + "participations": [ + { "tracks": ["SingleQuery"], "logics": "(QF_)?NRA" }, + { "tracks": ["ModelValidation"], "logics": "QF_NRA" } + ] +} diff --git a/submissions/template/template_aws_tracks.json b/submissions/template/template_aws_tracks.json new file mode 100644 index 00000000..5fe802d1 --- /dev/null +++ b/submissions/template/template_aws_tracks.json @@ -0,0 +1,29 @@ +{ + "name": "", + "contributors": [ + "First Smith", + { "name": "Second Baker", "website": "http://baker.com/" } + ], + "contacts": ["contact name "], + "website": "http://example.com/", + "system_description": "http://example.com/system.pdf", + "solver_type": "Standalone", + "seed": "42", + "participations": [ + { + "tracks": ["Cloud"], + "divisions": ["Equality"], + "aws_repository": "https://github.com/project/repository" + }, + { + "tracks": ["Parallel"], + "logics": "QF_.*LRA.*", + "aws_repository": "https://github.com/project/repository" + }, + { + "tracks": ["Cloud"], + "logics": ["LIA"], + "aws_repository": "https://github.com/project/repository" + } + ] +} diff --git a/submissions/yices2.json b/submissions/yices2.json new file mode 100644 index 00000000..7c65cc0f --- /dev/null +++ b/submissions/yices2.json @@ -0,0 +1,138 @@ +{ + "name": "Yices2", + "contributors": [ + "Bruno Dutertre", + "Aman Goel", + "Stéphane Graham-Lengrand", + "Thomas Hader", + "Ahmed Irfan", + "Dejan Jovanovic", + "Ian A Mason" + ], + "contacts": [ + "Ahmed Irfan ", + "Stéphane Graham-Lengrand " + ], + "archive": { + "url": "https://ahmed-irfan.github.io/smtcomp2024/yices2-smtcomp-2024.zip" + }, + "website": "https://yices.csl.sri.com", + "system_description": "https://ahmed-irfan.github.io/smtcomp2024/yices2-smtcomp-2024.pdf", + "solver_type": "Standalone", + "participations": [ + { + "tracks": ["SingleQuery"], + "logics": ["QF_ABV", + "QF_ALIA", + "QF_ANIA", + "QF_AUFBV", + "QF_AUFBVLIA", + "QF_AUFBVNIA", + "QF_AUFLIA", + "QF_AUFNIA", + "QF_AX", + "QF_BVLRA", + "QF_IDL", + "QF_LIA", + "QF_LIRA", + "QF_LRA", + "QF_NIA", + "QF_NIRA", + "QF_NRA", + "QF_RDL", + "QF_UF", + "QF_UFBV", + "QF_UFBVLIA", + "QF_UFIDL", + "QF_UFLIA", + "QF_UFLRA", + "QF_UFNIA", + "QF_UFNRA", + "UF"], + "command": ["./yices_smt2"] + }, + { + "tracks": ["SingleQuery"], + "logics": ["QF_BV"], + "command": ["./yices_smt2", "--delegate=kissat"] + }, + { + "tracks": ["Incremental"], + "logics": ["QF_ABV", + "QF_ALIA", + "QF_ANIA", + "QF_AUFBV", + "QF_AUFBVLIA", + "QF_AUFBVNIA", + "QF_AUFLIA", + "QF_AUFNIA", + "QF_AX", + "QF_BV", + "QF_BVLRA", + "QF_IDL", + "QF_LIA", + "QF_LIRA", + "QF_LRA", + "QF_NIA", + "QF_NIRA", + "QF_NRA", + "QF_RDL", + "QF_UF", + "QF_UFBV", + "QF_UFBVLIA", + "QF_UFIDL", + "QF_UFLIA", + "QF_UFLRA", + "QF_UFNIA", + "QF_UFNRA"], + "command": ["./yices_smt2", "--incremental"] + }, + { + "tracks": ["UnsatCore"], + "logics": ["QF_ABV", + "QF_ALIA", + "QF_AUFBV", + "QF_AUFBVLIA", + "QF_AUFLIA", + "QF_AX", + "QF_BV", + "QF_BVLRA", + "QF_IDL", + "QF_LIA", + "QF_LIRA", + "QF_LRA", + "QF_RDL", + "QF_UF", + "QF_UFBV", + "QF_UFBVLIA", + "QF_UFIDL", + "QF_UFLIA", + "QF_UFLRA", + "UF"], + "command": ["./yices_smt2"] + }, + { + "tracks": ["ModelValidation"], + "logics": ["QF_BV", + "QF_BVLRA", + "QF_IDL", + "QF_LIA", + "QF_LIRA", + "QF_LRA", + "QF_NIA", + "QF_NIRA", + "QF_NRA", + "QF_RDL", + "QF_UF", + "QF_UFBV", + "QF_UFBVLIA", + "QF_UFIDL", + "QF_UFLIA", + "QF_UFLRA", + "QF_UFNIA", + "QF_UFNRA"], + "command": ["./yices_smt2"] + } + ], + "seed": 0 +} diff --git a/submissions/yicesQS.json b/submissions/yicesQS.json new file mode 100644 index 00000000..09f1eb61 --- /dev/null +++ b/submissions/yicesQS.json @@ -0,0 +1,27 @@ +{ + "name": "YicesQS", + "contributors": [ + "Stéphane Graham-Lengrand" + ], + "contacts": [ + "Stéphane Graham-Lengrand " + ], + "archive": { + "url": "https://zenodo.org/records/11607999/files/yicesQS.zip?download=1" + }, + "website": "https://github.com/disteph/yicesQS", + "system_description": "https://www.csl.sri.com/users/sgl/Work/Reports/2024-yicesQS.pdf", + "solver_type": "derived", + "participations": [ + { + "tracks": ["SingleQuery"], + "logics": ["BV", + "LIA", + "LRA", + "NIA", + "NRA" + ], + "command": ["./starexec_run_default"] + } + ] +} diff --git a/submissions/z3-noodler.json b/submissions/z3-noodler.json new file mode 100644 index 00000000..b7c93bb2 --- /dev/null +++ b/submissions/z3-noodler.json @@ -0,0 +1,22 @@ +{ + "name": "Z3-Noodler", + "contributors": [ + "Vojtěch Havlena", + "Juraj Síč", + "David Chocholatý", + "Lukáš Holík", + "Ondřej Lengál" + ], + "contacts": ["Lukáš Holík "], + "archive": { + "url": "https://drive.google.com/uc?export=download&id=1XSj2PiVJLDx-JQyJRt76OEloC0dWFJqH" + }, + "website": "https://github.com/VeriFIT/z3-noodler", + "system_description": "https://github.com/VeriFIT/z3-noodler/blob/devel/doc/noodler/z3-noodler-system-description-2024.pdf", + "command": ["z3-noodler_linux", "smt.string_solver=noodler"], + "solver_type": "derived", + "participations": [ + { "tracks": ["SingleQuery"], "divisions": ["QF_Strings"] } + ], + "seed": 1465867 +} diff --git a/tests/test_validate.py b/tests/test_validate.py index c4d56b2c..5fca6113 100644 --- a/tests/test_validate.py +++ b/tests/test_validate.py @@ -6,10 +6,12 @@ from smtcomp.convert_csv import convert_csv from smtcomp.main import app +import smtcomp.defs as defs from smtcomp.submission import read +from smtcomp.generate_benchmarks import generate_trivial_benchmarks, path_trivial_benchmark runner = CliRunner() -good_cases = ["tests/test1.json", "submissions/template/template.json"] +good_cases = ["tests/test1.json", "submissions/template/template.json", "submissions/template/template_aws_tracks.json"] bad_cases = ["test_bad.json"] @@ -38,3 +40,19 @@ def test_show_json(name: str) -> None: @pytest.mark.parametrize("submission", submissions) def test_submission(submission: str) -> None: read(submission) + + +def test_generate_trivial(tmp_path: Path) -> None: + generate_trivial_benchmarks(tmp_path) + for track, divisions in defs.tracks.items(): + match track: + case defs.Track.Incremental: + statuses = [defs.Status.Incremental] + case defs.Track.ModelValidation | defs.Track.SingleQuery: + statuses = [defs.Status.Unsat, defs.Status.Sat] + case defs.Track.UnsatCore | defs.Track.ProofExhibition | defs.Track.Cloud | defs.Track.Parallel: + continue + for _, logics in divisions.items(): + for logic in logics: + for status in statuses: + assert path_trivial_benchmark(tmp_path, track, logic, status).exists() diff --git a/web/content/model/index.md b/web/content/model/index.md index 2b502f28..f2ed2775 100644 --- a/web/content/model/index.md +++ b/web/content/model/index.md @@ -2,6 +2,7 @@ title = 'Model Validation Track' date = 2023-12-11T21:09:02+01:00 draft = false +aliases = ['/model.html'] +++ ## Experimental model validation track diff --git a/web/content/parallel_cloud/index.md b/web/content/parallel_cloud/index.md index 8c4e6dba..c36d83b1 100644 --- a/web/content/parallel_cloud/index.md +++ b/web/content/parallel_cloud/index.md @@ -2,6 +2,7 @@ title = 'Parallel and Cloud Tracks' date = 2024-05-07T10:09:02+01:00 draft = false +aliases = ['/parallel-and-cloud-tracks.html'] +++ ## Parallel and Cloud Tracks diff --git a/web/content/participants/_index.md b/web/content/participants/_index.md new file mode 100644 index 00000000..a6bc5348 --- /dev/null +++ b/web/content/participants/_index.md @@ -0,0 +1,8 @@ ++++ +layout = 'single' +title = 'Participants' ++++ + +The following solvers have been submitted to SMT-COMP 2024 or were entered as non-competing solvers by the organizers for comparison. + +{{< participants >}} diff --git a/web/data/participants.json b/web/data/participants.json new file mode 100644 index 00000000..e4c9c24c --- /dev/null +++ b/web/data/participants.json @@ -0,0 +1,1032 @@ +[ + { + "name": "Algaroba", + "authors": ["Amar Shah", "Federico Mora", "Sanjit Seshia"], + "website": "https://github.com/uclid-org/algaroba", + "archive_url": "https://github.com/uclid-org/algaroba/archive/refs/tags/v1.0.0.tar.gz", + "system_description": "https://github.com/uclid-org/algaroba/files/15255360/Algaroba_at_the_2024_SMTCOMP.pdf", + "tracks": { + "SingleQuery": { + "QF_Datatypes": ["QF_DT", "QF_UFDT"] + } + } + }, + { + "name": "Amaya", + "authors": [ + "Vojt\u011bch Havlena", + "Michal He\u010dko", + "Luk\u00e1\u0161 Hol\u00edk", + "Ond\u0159ej Leng\u00e1l" + ], + "website": "https://github.com/MichalHe/amaya", + "archive_url": "https://github.com/VeriFIT/amaya-smt-comp/raw/master/archives/amaya-smt-comp-2024-v5.tar.gz", + "system_description": "https://github.com/VeriFIT/amaya-smt-comp/blob/master/system-description-2024/main.pdf", + "tracks": { + "SingleQuery": { + "Arith": ["LRA", "NIA", "NRA", "LIA"] + } + } + }, + { + "name": "Bitwuzla", + "authors": ["Aina Niemetz", "Mathias Preiner"], + "website": "https://bitwuzla.github.io/", + "archive_url": "https://zenodo.org/records/11288326/files/bitwuzla-submission-smtcomp-2024.zip?download=1", + "system_description": "https://bitwuzla.github.io/data/smtcomp2024/paper.pdf", + "tracks": { + "UnsatCore": { + "Bitvec": ["BV"], + "Equality+MachineArith": [ + "ABV", + "ABVFP", + "ABVFPLRA", + "AUFBV", + "AUFBVFP", + "UFBV", + "UFBVFP" + ], + "FPArith": ["BVFP", "BVFPLRA", "FP", "FPLRA"], + "QF_Bitvec": ["QF_BV"], + "QF_Equality+Bitvec": ["QF_AUFBV", "QF_UFBV", "QF_ABV"], + "QF_FPArith": [ + "QF_AUFBVFP", + "QF_UFFP", + "QF_BVFP", + "QF_BVFPLRA", + "QF_FP", + "QF_FPLRA", + "QF_ABVFP", + "QF_ABVFPLRA" + ] + }, + "SingleQuery": { + "Bitvec": ["BV"], + "Equality+MachineArith": [ + "ABV", + "ABVFP", + "ABVFPLRA", + "AUFBV", + "AUFBVFP", + "UFBV", + "UFBVFP" + ], + "FPArith": ["BVFP", "BVFPLRA", "FP", "FPLRA"], + "QF_Bitvec": ["QF_BV"], + "QF_Equality+Bitvec": ["QF_AUFBV", "QF_UFBV", "QF_ABV"], + "QF_FPArith": [ + "QF_AUFBVFP", + "QF_UFFP", + "QF_BVFP", + "QF_BVFPLRA", + "QF_FP", + "QF_FPLRA", + "QF_ABVFP", + "QF_ABVFPLRA" + ] + }, + "ModelValidation": { + "QF_ADT+BitVec": ["QF_AUFBV", "QF_ABV"], + "QF_Bitvec": ["QF_BV"], + "QF_Equality+Bitvec": ["QF_UFBV"], + "QF_FPArith": [ + "QF_AUFBVFP", + "QF_UFFP", + "QF_BVFP", + "QF_BVFPLRA", + "QF_FP", + "QF_FPLRA", + "QF_ABVFP", + "QF_ABVFPLRA" + ] + }, + "Incremental": { + "Bitvec": ["BV"], + "Equality+MachineArith": ["ABVFPLRA"], + "FPArith": ["BVFP", "BVFPLRA"], + "QF_Bitvec": ["QF_BV"], + "QF_Equality+Bitvec": ["QF_AUFBV", "QF_UFBV", "QF_ABV"], + "QF_FPArith": [ + "QF_UFFP", + "QF_BVFP", + "QF_BVFPLRA", + "QF_FP", + "QF_ABVFP", + "QF_ABVFPLRA" + ] + } + } + }, + { + "name": "COLIBRI", + "authors": ["Bruno Marre", "Fran\u00e7ois Bobot", "Christophe Junke"], + "website": "http://colibri.frama-c.com/", + "archive_url": "https://drive.google.com/uc?export=download&id=1lJjQNgHRF14sGEW84eJ6tBsZ0-DBPMW2", + "system_description": "https://drive.google.com/file/d/13c5E0iNMvpTRjmhWKb286V25Dw4f6JOF/view?usp=sharing", + "tracks": { + "SingleQuery": { + "QF_FPArith": [ + "QF_AUFBVFP", + "QF_UFFP", + "QF_UFFPDTNIRA", + "QF_BVFP", + "QF_BVFPLRA", + "QF_FP", + "QF_FPLRA", + "QF_ABVFP", + "QF_ABVFPLRA" + ] + } + } + }, + { + "name": "cvc5", + "authors": [ + "Leni Aniva", + "Haniel Barbosa", + "Clark Barrett", + "Hanna Lachnitt", + "Daniel Larraz", + "Abdalrhman Mohamed", + "Mudathir Mohamed", + "Aina Niemetz", + "Alex Ozdemir", + "Mathias Preiner", + "Andrew Reynolds", + "Hans-J\u00f6rg Schurr", + "Cesare Tinelli", + "Amalee Wilson", + "Yoni Zohar" + ], + "website": "https://cvc5.github.io/", + "archive_url": "https://homepage.divms.uiowa.edu/~hschrr/smtcomp2024/cvc5-default.zip", + "system_description": "https://homepage.divms.uiowa.edu/~hschrr/smtcomp2024/cvc5.pdf", + "tracks": { + "UnsatCore": { + "Arith": ["LRA", "NIA", "NRA", "LIA"], + "Bitvec": ["BV"], + "Equality": ["UF", "UFDT"], + "Equality+LinearArith": [ + "ALIA", + "AUFDTLIA", + "AUFDTLIRA", + "AUFLIA", + "AUFLIRA", + "UFDTLIA", + "UFDTLIRA", + "UFIDL", + "UFLIA", + "UFLRA" + ], + "Equality+MachineArith": [ + "ABV", + "ABVFP", + "ABVFPLRA", + "AUFBV", + "AUFBVDTLIA", + "AUFBVDTNIA", + "AUFBVDTNIRA", + "AUFBVFP", + "UFBV", + "UFBVDT", + "UFBVFP", + "AUFFPDTNIRA", + "UFBVLIA", + "UFFPDTNIRA" + ], + "Equality+NonLinearArith": [ + "ANIA", + "AUFDTNIRA", + "AUFNIA", + "AUFNIRA", + "UFDTNIA", + "UFDTNIRA", + "UFNIA", + "UFNIRA" + ], + "FPArith": ["BVFP", "BVFPLRA", "FP", "FPLRA"], + "QF_Bitvec": ["QF_BV"], + "QF_Datatypes": ["QF_DT", "QF_UFDT"], + "QF_Equality": ["QF_UF", "QF_AX"], + "QF_Equality+Bitvec": [ + "QF_AUFBV", + "QF_UFBVDT", + "QF_UFBV", + "QF_ABV" + ], + "QF_Equality+LinearArith": [ + "QF_UFIDL", + "QF_AUFLIA", + "QF_UFLIA", + "QF_UFLRA", + "QF_ALIA", + "QF_UFDTLIA", + "QF_UFDTLIRA" + ], + "QF_Equality+NonLinearArith": [ + "QF_UFDTNIA", + "QF_AUFNIA", + "QF_UFNIA", + "QF_UFNRA", + "QF_ANIA" + ], + "QF_FPArith": [ + "QF_AUFBVFP", + "QF_UFFP", + "QF_UFFPDTNIRA", + "QF_BVFP", + "QF_BVFPLRA", + "QF_FP", + "QF_FPLRA", + "QF_ABVFP", + "QF_ABVFPLRA" + ], + "QF_LinearIntArith": ["QF_LIRA", "QF_IDL", "QF_LIA"], + "QF_LinearRealArith": ["QF_LRA", "QF_RDL"], + "QF_NonLinearIntArith": ["QF_NIA", "QF_NIRA"], + "QF_NonLinearRealArith": ["QF_NRA"], + "QF_Strings": ["QF_SNIA", "QF_S", "QF_SLIA"] + }, + "SingleQuery": { + "Arith": ["LRA", "NIA", "NRA", "LIA"], + "Bitvec": ["BV"], + "Equality": ["UF", "UFDT"], + "Equality+LinearArith": [ + "ALIA", + "AUFDTLIA", + "AUFDTLIRA", + "AUFLIA", + "AUFLIRA", + "UFDTLIA", + "UFDTLIRA", + "UFIDL", + "UFLIA", + "UFLRA" + ], + "Equality+MachineArith": [ + "ABV", + "ABVFP", + "ABVFPLRA", + "AUFBV", + "AUFBVDTLIA", + "AUFBVDTNIA", + "AUFBVDTNIRA", + "AUFBVFP", + "UFBV", + "UFBVDT", + "UFBVFP", + "AUFFPDTNIRA", + "UFBVLIA", + "UFFPDTNIRA" + ], + "Equality+NonLinearArith": [ + "ANIA", + "AUFDTNIRA", + "AUFNIA", + "AUFNIRA", + "UFDTNIA", + "UFDTNIRA", + "UFNIA", + "UFNIRA" + ], + "FPArith": ["BVFP", "BVFPLRA", "FP", "FPLRA"], + "QF_Bitvec": ["QF_BV"], + "QF_Datatypes": ["QF_DT", "QF_UFDT"], + "QF_Equality": ["QF_UF", "QF_AX"], + "QF_Equality+Bitvec": [ + "QF_AUFBV", + "QF_UFBVDT", + "QF_UFBV", + "QF_ABV" + ], + "QF_Equality+LinearArith": [ + "QF_UFIDL", + "QF_AUFLIA", + "QF_UFLIA", + "QF_UFLRA", + "QF_ALIA", + "QF_UFDTLIA", + "QF_UFDTLIRA" + ], + "QF_Equality+NonLinearArith": [ + "QF_UFDTNIA", + "QF_AUFNIA", + "QF_UFNIA", + "QF_UFNRA", + "QF_ANIA" + ], + "QF_FPArith": [ + "QF_AUFBVFP", + "QF_UFFP", + "QF_UFFPDTNIRA", + "QF_BVFP", + "QF_BVFPLRA", + "QF_FP", + "QF_FPLRA", + "QF_ABVFP", + "QF_ABVFPLRA" + ], + "QF_LinearIntArith": ["QF_LIRA", "QF_IDL", "QF_LIA"], + "QF_LinearRealArith": ["QF_LRA", "QF_RDL"], + "QF_NonLinearIntArith": ["QF_NIA", "QF_NIRA"], + "QF_NonLinearRealArith": ["QF_NRA"], + "QF_Strings": ["QF_SNIA", "QF_S", "QF_SLIA"] + }, + "ModelValidation": { + "QF_ADT+BitVec": ["QF_AUFBV", "QF_UFBVDT", "QF_ABV"], + "QF_ADT+LinArith": [ + "QF_AUFLIA", + "QF_AX", + "QF_ALIA", + "QF_UFDTLIA", + "QF_UFDTLIRA" + ], + "QF_Bitvec": ["QF_BV"], + "QF_Datatypes": ["QF_DT", "QF_UFDT"], + "QF_Equality": ["QF_UF"], + "QF_Equality+Bitvec": ["QF_UFBV"], + "QF_Equality+LinearArith": ["QF_UFIDL", "QF_UFLIA", "QF_UFLRA"], + "QF_Equality+NonLinearArith": [ + "QF_UFDTNIA", + "QF_AUFNIA", + "QF_UFNIA", + "QF_UFNRA", + "QF_ANIA" + ], + "QF_FPArith": [ + "QF_AUFBVFP", + "QF_UFFP", + "QF_UFFPDTNIRA", + "QF_BVFP", + "QF_BVFPLRA", + "QF_FP", + "QF_FPLRA", + "QF_ABVFP", + "QF_ABVFPLRA" + ], + "QF_LinearIntArith": ["QF_LIRA", "QF_IDL", "QF_LIA"], + "QF_LinearRealArith": ["QF_LRA", "QF_RDL"], + "QF_NonLinearIntArith": ["QF_NIA", "QF_NIRA"], + "QF_NonLinearRealArith": ["QF_NRA"] + }, + "Incremental": { + "Arith": ["LRA", "LIA"], + "Bitvec": ["BV"], + "Equality": ["UF"], + "Equality+LinearArith": ["ALIA", "UFLRA"], + "Equality+MachineArith": ["ABVFPLRA"], + "Equality+NonLinearArith": [ + "ANIA", + "UFDTNIA", + "AUFNIRA", + "UFNIA", + "UFNRA" + ], + "FPArith": ["BVFP", "BVFPLRA"], + "QF_Bitvec": ["QF_BV"], + "QF_Equality": ["QF_UF"], + "QF_Equality+Bitvec": ["QF_AUFBV", "QF_UFBV", "QF_ABV"], + "QF_Equality+Bitvec+Arith": [ + "QF_AUFBVLIA", + "QF_AUFBVNIA", + "QF_UFBVLIA" + ], + "QF_Equality+LinearArith": [ + "QF_AUFLIA", + "QF_UFLRA", + "QF_ALIA", + "QF_UFLIA" + ], + "QF_Equality+NonLinearArith": [ + "QF_UFNRA", + "QF_UFNIA", + "QF_ANIA" + ], + "QF_FPArith": [ + "QF_UFFP", + "QF_BVFP", + "QF_BVFPLRA", + "QF_FP", + "QF_ABVFP", + "QF_ABVFPLRA" + ], + "QF_LinearIntArith": ["QF_LIA"], + "QF_LinearRealArith": ["QF_LRA"], + "QF_NonLinearIntArith": ["QF_NIA"] + }, + "Cloud": { + "Arith": ["LRA", "NIA", "NRA", "LIA"], + "Bitvec": ["BV"], + "Equality": ["UF", "UFDT"], + "Equality+LinearArith": [ + "ALIA", + "AUFDTLIA", + "AUFDTLIRA", + "AUFLIA", + "AUFLIRA", + "UFDTLIA", + "UFDTLIRA", + "UFIDL", + "UFLIA", + "UFLRA" + ], + "Equality+MachineArith": [ + "ABV", + "ABVFP", + "ABVFPLRA", + "AUFBV", + "AUFBVDTLIA", + "AUFBVDTNIA", + "AUFBVDTNIRA", + "AUFBVFP", + "UFBV", + "UFBVDT", + "UFBVFP", + "AUFFPDTNIRA", + "UFBVLIA", + "UFFPDTNIRA" + ], + "Equality+NonLinearArith": [ + "ANIA", + "AUFDTNIRA", + "AUFNIA", + "AUFNIRA", + "UFDTNIA", + "UFDTNIRA", + "UFNIA", + "UFNIRA" + ], + "FPArith": ["BVFP", "BVFPLRA", "FP", "FPLRA"], + "QF_Bitvec": ["QF_BV"], + "QF_Datatypes": ["QF_DT", "QF_UFDT"], + "QF_Equality": ["QF_UF", "QF_AX"], + "QF_Equality+Bitvec": [ + "QF_AUFBV", + "QF_UFBVDT", + "QF_UFBV", + "QF_ABV" + ], + "QF_Equality+LinearArith": [ + "QF_UFIDL", + "QF_AUFLIA", + "QF_UFLIA", + "QF_UFLRA", + "QF_ALIA", + "QF_UFDTLIA", + "QF_UFDTLIRA" + ], + "QF_Equality+NonLinearArith": [ + "QF_UFDTNIA", + "QF_AUFNIA", + "QF_UFNIA", + "QF_UFNRA", + "QF_ANIA" + ], + "QF_FPArith": [ + "QF_AUFBVFP", + "QF_UFFP", + "QF_UFFPDTNIRA", + "QF_BVFP", + "QF_BVFPLRA", + "QF_FP", + "QF_FPLRA", + "QF_ABVFP", + "QF_ABVFPLRA" + ], + "QF_LinearIntArith": ["QF_LIRA", "QF_IDL", "QF_LIA"], + "QF_LinearRealArith": ["QF_LRA", "QF_RDL"], + "QF_NonLinearIntArith": ["QF_NIA", "QF_NIRA"], + "QF_NonLinearRealArith": ["QF_NRA"], + "QF_Strings": ["QF_SNIA", "QF_S", "QF_SLIA"] + } + } + }, + { + "name": "iProver v3.9", + "authors": ["Konstantin Korovin"], + "website": "https://gitlab.com/korovin/iprover", + "archive_url": "http://tba/", + "system_description": "http://www.cs.man.ac.uk/~korovink/iprover-smt-comp-2024.pdf", + "tracks": { + "SingleQuery": { + "Arith": ["LRA", "NIA", "NRA", "LIA"], + "Equality": ["UF", "UFDT"], + "Equality+LinearArith": [ + "ALIA", + "AUFDTLIA", + "AUFDTLIRA", + "AUFLIA", + "AUFLIRA", + "UFDTLIA", + "UFDTLIRA", + "UFIDL", + "UFLIA", + "UFLRA" + ], + "Equality+NonLinearArith": [ + "ANIA", + "AUFDTNIRA", + "AUFNIA", + "AUFNIRA", + "UFDTNIA", + "UFDTNIRA", + "UFNIA", + "UFNIRA" + ] + }, + "Parallel": { + "Arith": ["LRA", "NIA", "NRA", "LIA"], + "Equality": ["UF", "UFDT"], + "Equality+LinearArith": [ + "ALIA", + "AUFDTLIA", + "AUFDTLIRA", + "AUFLIA", + "AUFLIRA", + "UFDTLIA", + "UFDTLIRA", + "UFIDL", + "UFLIA", + "UFLRA" + ], + "Equality+NonLinearArith": [ + "ANIA", + "AUFDTNIRA", + "AUFNIA", + "AUFNIRA", + "UFDTNIA", + "UFDTNIRA", + "UFNIA", + "UFNIRA" + ] + } + } + }, + { + "name": "OpenSMT", + "authors": ["Tom\u00e1\u0161 Kol\u00e1rik", "Martin Blicha"], + "website": "https://github.com/usi-verification-and-security/opensmt", + "archive_url": "https://zenodo.org/records/11371847/files/opensmt.tgz", + "system_description": "https://github.com/usi-verification-and-security/opensmt-doc/blob/master/smt-comp/abstract-2024.pdf", + "tracks": { + "UnsatCore": { + "QF_Equality": ["QF_UF", "QF_AX"], + "QF_Equality+LinearArith": [ + "QF_UFIDL", + "QF_UFLIA", + "QF_UFLRA", + "QF_AUFLIA", + "QF_ALIA" + ], + "QF_LinearIntArith": ["QF_IDL", "QF_LIA"], + "QF_LinearRealArith": ["QF_LRA", "QF_RDL"] + }, + "SingleQuery": { + "QF_Equality": ["QF_UF", "QF_AX"], + "QF_Equality+LinearArith": [ + "QF_UFIDL", + "QF_UFLIA", + "QF_UFLRA", + "QF_AUFLIA", + "QF_ALIA" + ], + "QF_LinearIntArith": ["QF_IDL", "QF_LIA"], + "QF_LinearRealArith": ["QF_LRA", "QF_RDL"] + }, + "ModelValidation": { + "QF_Equality": ["QF_UF"], + "QF_Equality+LinearArith": ["QF_UFIDL", "QF_UFLIA", "QF_UFLRA"], + "QF_LinearIntArith": ["QF_IDL", "QF_LIA"], + "QF_LinearRealArith": ["QF_LRA", "QF_RDL"] + }, + "Incremental": { + "QF_Equality": ["QF_UF"], + "QF_Equality+LinearArith": [ + "QF_UFLIA", + "QF_UFLRA", + "QF_ALIA", + "QF_AUFLIA" + ], + "QF_LinearIntArith": ["QF_LIA"], + "QF_LinearRealArith": ["QF_LRA"] + } + } + }, + { + "name": "OSTRICH", + "authors": [ + "Matthew Hague", + "Denghang Hu", + "Anthony W. Lin", + "Oliver Markgraf", + "Philipp R\u00fcmmer", + "Zhilin Wu" + ], + "website": "https://github.com/uuverifiers/ostrich", + "archive_url": "https://philipp.ruemmer.org/ostrich-2024.tar.gz", + "system_description": "https://philipp.ruemmer.org/ostrich-2024.pdf", + "tracks": { + "SingleQuery": { + "QF_Strings": ["QF_SNIA", "QF_S", "QF_SLIA"] + } + } + }, + { + "name": "plat-smt", + "authors": ["David Ewert"], + "website": "https://github.com/dewert99/plat-smt", + "archive_url": "https://github.com/dewert99/plat-smt/releases/download/SMT-COMP2024/plat-smt.zip", + "system_description": "https://github.com/dewert99/plat-smt/files/15505357/PlatSMT_2024_System_Description.pdf", + "tracks": { + "UnsatCore": {}, + "SingleQuery": {}, + "ModelValidation": {}, + "Incremental": {} + } + }, + { + "name": "SMTInterpol", + "authors": [ + "Max Barth", + "Leon Cacace", + "J\u00fcrgen Christ", + "Daniel Dietsch", + "Leonard Fichtner", + "Joanna Greulich", + "Elisabeth Henkel", + "Matthias Heizmann", + "Jochen Hoenicke", + "Moritz Mohr", + "Alexander Nutz", + "Markus Pomrehn", + "Pascal Raiola", + "Tanja Schindler" + ], + "website": "https://ultimate.informatik.uni-freiburg.de/smtinterpol", + "archive_url": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/smtinterpol-2.5-1338-g35b19d44.tar.gz", + "system_description": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/sysdesc2024.pdf", + "tracks": { + "UnsatCore": { + "Arith": ["LRA", "NIA", "NRA", "LIA"], + "Equality": ["UF", "UFDT"], + "Equality+LinearArith": [ + "ALIA", + "AUFDTLIA", + "AUFDTLIRA", + "AUFLIA", + "AUFLIRA", + "UFDTLIA", + "UFDTLIRA", + "UFIDL", + "UFLIA", + "UFLRA" + ], + "Equality+NonLinearArith": [ + "ANIA", + "AUFDTNIRA", + "AUFNIA", + "AUFNIRA", + "UFDTNIA", + "UFDTNIRA", + "UFNIA", + "UFNIRA" + ], + "QF_Datatypes": ["QF_DT", "QF_UFDT"], + "QF_Equality": ["QF_UF", "QF_AX"], + "QF_Equality+LinearArith": [ + "QF_UFIDL", + "QF_AUFLIA", + "QF_UFLIA", + "QF_UFLRA", + "QF_ALIA", + "QF_UFDTLIA", + "QF_UFDTLIRA" + ], + "QF_Equality+NonLinearArith": [ + "QF_UFDTNIA", + "QF_AUFNIA", + "QF_UFNIA", + "QF_UFNRA", + "QF_ANIA" + ], + "QF_LinearIntArith": ["QF_LIRA", "QF_IDL", "QF_LIA"], + "QF_LinearRealArith": ["QF_LRA", "QF_RDL"], + "QF_NonLinearIntArith": ["QF_NIA", "QF_NIRA"], + "QF_NonLinearRealArith": ["QF_NRA"] + }, + "SingleQuery": { + "Arith": ["LRA", "NIA", "NRA", "LIA"], + "Bitvec": ["BV"], + "Equality": ["UF", "UFDT"], + "Equality+LinearArith": [ + "ALIA", + "AUFDTLIA", + "AUFDTLIRA", + "AUFLIA", + "AUFLIRA", + "UFDTLIA", + "UFDTLIRA", + "UFIDL", + "UFLIA", + "UFLRA" + ], + "Equality+MachineArith": [ + "ABV", + "AUFBV", + "AUFBVDTLIA", + "AUFBVDTNIA", + "AUFBVDTNIRA", + "UFBV", + "UFBVDT", + "UFBVLIA" + ], + "Equality+NonLinearArith": [ + "ANIA", + "AUFDTNIRA", + "AUFNIA", + "AUFNIRA", + "UFDTNIA", + "UFDTNIRA", + "UFNIA", + "UFNIRA" + ], + "QF_Bitvec": ["QF_BV"], + "QF_Datatypes": ["QF_DT", "QF_UFDT"], + "QF_Equality": ["QF_UF", "QF_AX"], + "QF_Equality+Bitvec": [ + "QF_AUFBV", + "QF_UFBVDT", + "QF_UFBV", + "QF_ABV" + ], + "QF_Equality+LinearArith": [ + "QF_UFIDL", + "QF_AUFLIA", + "QF_UFLIA", + "QF_UFLRA", + "QF_ALIA", + "QF_UFDTLIA", + "QF_UFDTLIRA" + ], + "QF_Equality+NonLinearArith": [ + "QF_UFDTNIA", + "QF_AUFNIA", + "QF_UFNIA", + "QF_UFNRA", + "QF_ANIA" + ], + "QF_LinearIntArith": ["QF_LIRA", "QF_IDL", "QF_LIA"], + "QF_LinearRealArith": ["QF_LRA", "QF_RDL"], + "QF_NonLinearIntArith": ["QF_NIA", "QF_NIRA"], + "QF_NonLinearRealArith": ["QF_NRA"] + }, + "ModelValidation": { + "QF_ADT+LinArith": [ + "QF_AUFLIA", + "QF_AX", + "QF_ALIA", + "QF_UFDTLIA", + "QF_UFDTLIRA" + ], + "QF_Datatypes": ["QF_DT", "QF_UFDT"], + "QF_Equality": ["QF_UF"], + "QF_Equality+LinearArith": ["QF_UFIDL", "QF_UFLIA", "QF_UFLRA"], + "QF_Equality+NonLinearArith": [ + "QF_UFDTNIA", + "QF_AUFNIA", + "QF_UFNIA", + "QF_UFNRA", + "QF_ANIA" + ], + "QF_LinearIntArith": ["QF_LIRA", "QF_IDL", "QF_LIA"], + "QF_LinearRealArith": ["QF_LRA", "QF_RDL"], + "QF_NonLinearIntArith": ["QF_NIA", "QF_NIRA"], + "QF_NonLinearRealArith": ["QF_NRA"] + }, + "Incremental": { + "Arith": ["LRA", "LIA"], + "Bitvec": ["BV"], + "Equality": ["UF"], + "Equality+LinearArith": ["ALIA", "UFLRA"], + "Equality+NonLinearArith": [ + "ANIA", + "UFDTNIA", + "AUFNIRA", + "UFNIA", + "UFNRA" + ], + "QF_Bitvec": ["QF_BV"], + "QF_Equality": ["QF_UF"], + "QF_Equality+Bitvec": ["QF_AUFBV", "QF_UFBV", "QF_ABV"], + "QF_Equality+Bitvec+Arith": [ + "QF_AUFBVLIA", + "QF_AUFBVNIA", + "QF_UFBVLIA" + ], + "QF_Equality+LinearArith": [ + "QF_AUFLIA", + "QF_UFLRA", + "QF_ALIA", + "QF_UFLIA" + ], + "QF_Equality+NonLinearArith": [ + "QF_UFNRA", + "QF_UFNIA", + "QF_ANIA" + ], + "QF_LinearIntArith": ["QF_LIA"], + "QF_LinearRealArith": ["QF_LRA"], + "QF_NonLinearIntArith": ["QF_NIA"] + } + } + }, + { + "name": "SMT-RAT", + "authors": [ + "Jasper Nalbach", + "Valentin Promies", + "Erika \u00c1brah\u00e1m" + ], + "website": "https://github.com/ths-rwth/smtrat", + "archive_url": "https://github.com/ths-rwth/smtrat/releases/download/24.05/smtrat.tgz", + "system_description": "https://github.com/ths-rwth/smtrat/blob/master/doc/smtcomp-description/smtcomp-2024.pdf", + "tracks": { + "SingleQuery": { + "Arith": ["NRA"], + "QF_NonLinearRealArith": ["QF_NRA"] + }, + "ModelValidation": { + "QF_NonLinearRealArith": ["QF_NRA"] + } + } + }, + { + "name": "STP", + "authors": [ + "Vijay Ganesh", + "Trevor Hansen", + "Mate Soos", + "Dan Liew", + "Ryan Govostes", + "Andrew V. Jones" + ], + "website": "https://stp.github.io/", + "archive_url": "https://github.com/stp/stp/releases/download/smtcomp2024/smtcomp-2024.zip", + "system_description": "https://github.com/stp/docs/tree/master/smt2024-descr/descr.pdf", + "tracks": { + "SingleQuery": { + "QF_Bitvec": ["QF_BV"] + }, + "ModelValidation": { + "QF_Bitvec": ["QF_BV"] + }, + "Incremental": { + "QF_Bitvec": ["QF_BV"] + } + } + }, + { + "name": "Yices2", + "authors": [ + "Bruno Dutertre", + "Aman Goel", + "St\u00e9phane Graham-Lengrand", + "Thomas Hader", + "Ahmed Irfan", + "Dejan Jovanovic", + "Ian A Mason" + ], + "website": "https://yices.csl.sri.com/", + "archive_url": "https://ahmed-irfan.github.io/smtcomp2024/yices2-smtcomp-2024.zip", + "system_description": "https://ahmed-irfan.github.io/smtcomp2024/yices2-smtcomp-2024.pdf", + "tracks": { + "UnsatCore": { + "Equality": ["UF"], + "QF_Bitvec": ["QF_BV"], + "QF_Equality": ["QF_UF", "QF_AX"], + "QF_Equality+Bitvec": ["QF_AUFBV", "QF_UFBV", "QF_ABV"], + "QF_Equality+LinearArith": [ + "QF_UFIDL", + "QF_AUFLIA", + "QF_UFLRA", + "QF_UFLIA", + "QF_ALIA" + ], + "QF_LinearIntArith": ["QF_LIRA", "QF_IDL", "QF_LIA"], + "QF_LinearRealArith": ["QF_LRA", "QF_RDL"] + }, + "SingleQuery": { + "Equality": ["UF"], + "QF_Bitvec": ["QF_BV"], + "QF_Equality": ["QF_UF", "QF_AX"], + "QF_Equality+Bitvec": ["QF_AUFBV", "QF_UFBV", "QF_ABV"], + "QF_Equality+LinearArith": [ + "QF_UFIDL", + "QF_AUFLIA", + "QF_UFLRA", + "QF_UFLIA", + "QF_ALIA" + ], + "QF_Equality+NonLinearArith": [ + "QF_UFNRA", + "QF_AUFNIA", + "QF_UFNIA", + "QF_ANIA" + ], + "QF_LinearIntArith": ["QF_LIRA", "QF_IDL", "QF_LIA"], + "QF_LinearRealArith": ["QF_LRA", "QF_RDL"], + "QF_NonLinearIntArith": ["QF_NIA", "QF_NIRA"], + "QF_NonLinearRealArith": ["QF_NRA"] + }, + "ModelValidation": { + "QF_Bitvec": ["QF_BV"], + "QF_Equality": ["QF_UF"], + "QF_Equality+Bitvec": ["QF_UFBV"], + "QF_Equality+LinearArith": ["QF_UFIDL", "QF_UFLIA", "QF_UFLRA"], + "QF_Equality+NonLinearArith": ["QF_UFNIA", "QF_UFNRA"], + "QF_LinearIntArith": ["QF_LIRA", "QF_IDL", "QF_LIA"], + "QF_LinearRealArith": ["QF_LRA", "QF_RDL"], + "QF_NonLinearIntArith": ["QF_NIA", "QF_NIRA"], + "QF_NonLinearRealArith": ["QF_NRA"] + }, + "Incremental": { + "QF_Bitvec": ["QF_BV"], + "QF_Equality": ["QF_UF"], + "QF_Equality+Bitvec": ["QF_AUFBV", "QF_UFBV", "QF_ABV"], + "QF_Equality+Bitvec+Arith": [ + "QF_AUFBVLIA", + "QF_AUFBVNIA", + "QF_UFBVLIA" + ], + "QF_Equality+LinearArith": [ + "QF_AUFLIA", + "QF_UFLRA", + "QF_ALIA", + "QF_UFLIA" + ], + "QF_Equality+NonLinearArith": [ + "QF_UFNRA", + "QF_UFNIA", + "QF_ANIA" + ], + "QF_LinearIntArith": ["QF_LIA"], + "QF_LinearRealArith": ["QF_LRA"], + "QF_NonLinearIntArith": ["QF_NIA"] + } + } + }, + { + "name": "YicesQS", + "authors": ["St\u00e9phane Graham-Lengrand"], + "website": "https://github.com/disteph/yicesQS", + "archive_url": "https://www.csl.sri.com/users/sgl/yicesQS.zip", + "system_description": "https://www.csl.sri.com/users/sgl/Work/Reports/2024-yicesQS.pdf", + "tracks": { + "SingleQuery": { + "Arith": ["LRA", "NIA", "NRA", "LIA"], + "Bitvec": ["BV"] + } + } + }, + { + "name": "Z3-alpha", + "authors": [ + "Zhengyang John Lu", + "Stefan Siemer", + "Paul Sarnighausen-Cahn", + "Florin Manea", + "Vijay Ganesh" + ], + "website": "https://github.com/JohnLyu2/z3alpha", + "archive_url": "https://drive.google.com/file/d/1uQqVQw_DvG7McBxqE_BzjMtrviY1L_bl/view?usp=sharing", + "system_description": "https://drive.google.com/file/d/1aJOiNzKac_kwhZm8DoT-EFCa_2RHwVwj/view?usp=drive_link", + "tracks": { + "SingleQuery": { + "QF_Bitvec": ["QF_BV"], + "QF_LinearIntArith": ["QF_LIRA", "QF_IDL", "QF_LIA"], + "QF_LinearRealArith": ["QF_LRA", "QF_RDL"], + "QF_NonLinearIntArith": ["QF_NIA", "QF_NIRA"], + "QF_NonLinearRealArith": ["QF_NRA"], + "QF_Strings": ["QF_S", "QF_SLIA"] + } + } + }, + { + "name": "Z3-Noodler", + "authors": [ + "Vojt\u011bch Havlena", + "Juraj S\u00ed\u010d", + "David Chocholat\u00fd", + "Luk\u00e1\u0161 Hol\u00edk", + "Ond\u0159ej Leng\u00e1l" + ], + "website": "https://github.com/VeriFIT/z3-noodler", + "archive_url": "https://drive.google.com/uc?export=download&id=1XSj2PiVJLDx-JQyJRt76OEloC0dWFJqH", + "system_description": "https://github.com/VeriFIT/z3-noodler/blob/devel/doc/noodler/z3-noodler-system-description-2024.pdf", + "tracks": { + "SingleQuery": { + "QF_Strings": ["QF_SNIA", "QF_S", "QF_SLIA"] + } + } + } +] diff --git a/web/hugo.toml b/web/hugo.toml index 34e81bd1..501a689d 100644 --- a/web/hugo.toml +++ b/web/hugo.toml @@ -64,3 +64,8 @@ theme = 'smtcomp' name = 'Parallel & Cloud Tracks' pageRef = 'parallel_cloud' weight = 30 + +[[menu.year]] + name = 'Participants' + pageRef = 'participants' + weight = 50 diff --git a/web/themes/smtcomp/assets/css/main.css b/web/themes/smtcomp/assets/css/main.css index d77cdc62..40c5a6a0 100644 --- a/web/themes/smtcomp/assets/css/main.css +++ b/web/themes/smtcomp/assets/css/main.css @@ -687,3 +687,20 @@ ul li ul { ul li p { margin: 0; } + +table.participants { + table-layout: fixed; + width: 200%; +} + +col.authors, +td.authors { + width: 35%; + white-space: normal; +} + +col.track, +td.track { + width: 6em; + white-space: normal; +} diff --git a/web/themes/smtcomp/layouts/partials/participant.html b/web/themes/smtcomp/layouts/partials/participant.html new file mode 100644 index 00000000..f7cefe5f --- /dev/null +++ b/web/themes/smtcomp/layouts/partials/participant.html @@ -0,0 +1,13 @@ + + {{ .name }} + + {{ if (gt (len .tracks.SingleQuery) 0) }}X{{ end }} + {{ with .tracks.Incremental }}X{{ end }} + {{ with .tracks.UnsatCore }}X{{ end }} + {{ with .tracks.ModelValidation }}X{{ end }} + {{ with .tracks.Cloud }}X{{ end }} + + {{ delimit .authors ",\n" }} + Archive + System description + diff --git a/web/themes/smtcomp/layouts/shortcodes/participants.html b/web/themes/smtcomp/layouts/shortcodes/participants.html new file mode 100644 index 00000000..48881610 --- /dev/null +++ b/web/themes/smtcomp/layouts/shortcodes/participants.html @@ -0,0 +1,35 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + {{ range $.Site.Data.participants }} + {{ partial "participant.html" . }} + {{ end }} + + +
SolverSingle Query TrackIncremental TrackUnsat Core TrackModel Validation TrackCloud TrackContributorsArchiveSystem description