diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index a0a7cc2..97766db 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -84,7 +84,11 @@ jobs: echo "::warning::GUROBI_LICENSE is not a working full Gurobi license here: the tests use the size-limited license shipped with gurobipy" fi - # yices2 and cvc5 are used from solvers/ + # The tests use the SMT solvers that configure-solvers finds: z3 from z3-solver, and the yices2, cvc5 and + # OpenSMT release binaries it downloads into solvers/ (checking their sha256). This prints what they find. + - name: Download SMT solvers + run: ./configure-solvers --download -o - + - name: Run tests with coverage run: pytest -v -rxs --cov --cov-report=xml --cov-report=term diff --git a/.gitignore b/.gitignore index dcf86c6..470989e 100644 --- a/.gitignore +++ b/.gitignore @@ -11,3 +11,7 @@ excel/ coverage.xml .coverage + +# written by ./configure-solvers +/solvers.toml +/solvers/ diff --git a/README.md b/README.md index ffd1781..7d6907f 100644 --- a/README.md +++ b/README.md @@ -12,22 +12,21 @@ Supported solvers: dReal, z3, cvc5, opensmt, yices2, smtinterpol, Gurobi +MILQ does not ship the SMT solvers. Run `./configure-solvers --download` to download yices2, cvc5 and OpenSMT, or install the ones you want and run `./configure-solvers`, which writes their paths and command-line arguments to `solvers.toml`; see the [solver configuration](https://quantum.fit.vut.cz/milq/installation#solver-configuration) docs. + ## Installation Guide **Dependencies:** -- dReal solver 4.21.06.2 -- Refer to the [Installation Guide](https://github.com/dreal/dreal4) +- SMT solvers of your choice (yices2, cvc5, OpenSMT, SMTInterpol, dReal); see the [installation docs](https://quantum.fit.vut.cz/milq/installation#solvers) - z3 solver -- comes with `z3-solver` from `requirements.txt` (on `PATH` while the virtual environment is active), or `sudo apt install z3` -- to use `smtinterpol`, Java 21.0.10 is required (`sudo apt install openjdk-21-jdk`) - Python 3.11 or newer, with the dependencies in `requirements.txt` ``` pip install -r requirements.txt ``` - Gurobi License for 13.0.1 version (Get free academic license on [Gurobi site](https://www.gurobi.com/)), refer to their installation manuals and create `gurobi.lic` file. (The license is not re-distributable without explicit agreement with Gurobi) +Then download yices2, cvc5 and OpenSMT and write the solver configuration for them and the SMT solvers on your `PATH` (with the virtual environment active): ``` -chmod +x solvers/smtinterpol/smtinterpol -chmod +x solvers/cvc5/cvc5 -chmod +x solvers/opensmt/opensmt -chmod +x solvers/yices2/yices_smt2 +./configure-solvers --download ``` ## Usage @@ -70,7 +69,7 @@ Examples, run from the repository root: pip install pytest pytest ``` -The tests use the bundled yices2/cvc5 binaries and the size-limited license shipped with `gurobipy`. They run in CI on every push and pull request; CI uses the full Gurobi license from the organization secret `GUROBI_LICENSE` when it works there, and the size-limited one otherwise. Known bugs are marked `xfail` with their issue number. Strict mode is on, so a fix must remove its marker from `KNOWN_BUGS` in `tests/test_simulator.py`. +The tests use the SMT solvers that `configure-solvers` finds on `PATH` (most need yices2; your `solvers.toml` is not used) and the size-limited license shipped with `gurobipy`. They run in CI on every push and pull request; CI downloads yices2, cvc5 and OpenSMT with `configure-solvers --download` and uses the full Gurobi license from the organization secret `GUROBI_LICENSE` when it works there, and the size-limited one otherwise. Known bugs are marked `xfail` with their issue number. Strict mode is on, so a fix must remove its marker from `KNOWN_BUGS` in `tests/test_simulator.py`. ## Project Structure @@ -78,14 +77,15 @@ The tests use the bundled yices2/cvc5 binaries and the size-limited license ship - README.md - milq (CLI for synthesis) - requirements.txt +- configure-solvers (writes solvers.toml for the installed SMT solvers, --download downloads some) +- solvers.toml (paths and arguments of the SMT solvers, not tracked) +- solvers/ (solvers downloaded by configure-solvers --download, not tracked) - benchmarks/ | - ghz (GHZ circuits) | - bernstein-vazirani (BV circuits) | - qsharp (benchmarks for comparison with Quokka#) | - mqt-bench (MQT benchmark library Clifford+T circuits) | - rus (repeat-until-success circuits) -- solvers/ -| ... (solver binaries from SMT-comp -- cvc5, opensmt, yices2...) - cli/ | - simulator.py (CLI interface for our small simulator module) - src/ @@ -99,6 +99,9 @@ The tests use the bundled yices2/cvc5 binaries and the size-limited license ship | - pareto.py (pareto front) | - parser.py (parsing of solver outputs) | - sim.py (simulator module) +| - solver_config.py (loading of solvers.toml) +| - solver_detection.py (the known SMT solvers with their release downloads, finding the installed ones) +| - solver_download.py (downloading the releases, for configure-solvers --download) | - solvers.py (abstraction over SMT solvers and Portfolio solver) | - synth.py (main synthesis module) | - timing.py (phase timings) diff --git a/codecov.yml b/codecov.yml index 8744709..9c85fc5 100644 --- a/codecov.yml +++ b/codecov.yml @@ -27,7 +27,6 @@ coverage: ignore: - "tests/**" - "benchmarks/**" - - "solvers/**" comment: layout: "condensed_header, diff, files" diff --git a/configure-solvers b/configure-solvers new file mode 100755 index 0000000..1ca30bf --- /dev/null +++ b/configure-solvers @@ -0,0 +1,72 @@ +#!/usr/bin/env python3 +""" +@file: configure-solvers +@brief: writes the SMT solver configuration (solvers.toml) for the solvers installed on this computer, + optionally after downloading some of them +""" + +import argparse +import os +import sys + +sys.path.insert(0, os.path.join(os.path.dirname(os.path.realpath(__file__)), 'src')) +from solver_config import DEFAULT_PATH +from solver_detection import KNOWN_SOLVERS, detect, render +from solver_download import DEFAULT_DIR as DOWNLOAD_DIR, DownloadError, bin_dir, download, downloadable + +parser = argparse.ArgumentParser( + description='Find the SMT solvers installed on this computer and write the solver configuration for them. ' + f'Looks for {", ".join(s.name for s in KNOWN_SOLVERS)} in the --search directories, the ' + 'downloaded solvers and on PATH (and dReal also in /opt/dreal), and keeps those that answer a ' + 'trivial formula.') +parser.add_argument('-o', '--output', help=f'file to write, - for standard output (default: {DEFAULT_PATH})', + default=DEFAULT_PATH) +parser.add_argument('-f', '--force', action='store_true', help='overwrite the output file if it exists') +parser.add_argument('-s', '--search', action='append', default=[], metavar='DIR', + help='also look in DIR and DIR/bin, before PATH (can be repeated)') +parser.add_argument('-d', '--download', nargs='?', const='all', metavar='SOLVERS', + help='first download release binaries of these solvers (comma-separated; default: all of ' + f'{", ".join(downloadable()) or "none on this platform"})') +parser.add_argument('--download-dir', default=DOWNLOAD_DIR, metavar='DIR', + help=f'where downloaded solvers are kept (default: {DOWNLOAD_DIR})') +parser.add_argument('-t', '--timeout', type=float, default=30, help='seconds a solver has to answer (default: 30)') +args = parser.parse_args() + +if args.output != '-' and os.path.exists(args.output) and not args.force: + print(f"configure-solvers: error: {args.output} exists, use --force to overwrite it", file=sys.stderr) + sys.exit(2) + +if args.download: + available = downloadable() + wanted = list(available) if args.download == 'all' else args.download.split(',') + unknown = [name for name in wanted if name not in available] + if unknown: + print(f"configure-solvers: error: no download of {', '.join(unknown)} for this platform " + f"(available: {', '.join(available) or 'none'})", file=sys.stderr) + sys.exit(2) + for name in wanted: + solver, release = available[name] + print(f"downloading {name} {release.version} from {release.url}", file=sys.stderr) + try: + download(solver, release, args.download_dir) + except DownloadError as e: + print(f"configure-solvers: error: {e}", file=sys.stderr) + sys.exit(1) + +detections = detect([*args.search, bin_dir(args.download_dir)], timeout=args.timeout) +for detection in detections: + for executable, problem in detection.rejected: + print(f"{detection.solver.name}: {executable} does not work ({problem})", file=sys.stderr) + print(f"{detection.solver.name}: {detection.path or 'not found'}", file=sys.stderr) + +if not any(detection.path for detection in detections): + print("configure-solvers: error: no SMT solver found (-s gurobi and -s milp need none)", file=sys.stderr) + sys.exit(1) + +config = render(detections) +if args.output == '-': + sys.stdout.write(config) +else: + with open(args.output, 'w') as f: + f.write(config) + print(f"wrote {args.output}", file=sys.stderr) diff --git a/docs/index.md b/docs/index.md index de0c26e..edf2b1f 100644 --- a/docs/index.md +++ b/docs/index.md @@ -15,7 +15,7 @@ MILQ simulates the input circuit on a set of input states and asks a solver for ## Quick example -The GHZ state preparation circuit in `benchmarks/ghz/3.qasm` is synthesized with yices2 (bundled with MILQ) in about a second: +The GHZ state preparation circuit in `benchmarks/ghz/3.qasm` is synthesized with yices2 in about a second: ```console $ ./milq -s smt -a yices2 benchmarks/ghz/3.qasm diff --git a/docs/installation.md b/docs/installation.md index 4ccdc0b..19edc8b 100644 --- a/docs/installation.md +++ b/docs/installation.md @@ -8,7 +8,7 @@ title: Installation ## Requirements -- **Linux on x86-64.** The bundled solver binaries are Linux x86-64 executables. +- **Linux.** MILQ is developed and tested on Linux (CI runs Ubuntu on x86-64). - **Python 3.11 or newer.** CI tests Python 3.11 with the lowest versions of the dependencies that `requirements.txt` allows, and Python 3.12 and 3.14 with the newest. ## Get MILQ and its Python dependencies @@ -24,24 +24,67 @@ MILQ is not packaged; it runs from the repository (see [Usage](usage)). ## Solvers -You need at least one solver. **yices2 and cvc5 work out of the box** and are enough to get started. +You need at least one solver. MILQ does not ship SMT solvers: `./configure-solvers --download` downloads yices2, cvc5 and OpenSMT, or install the ones you want yourself and let `./configure-solvers` find them (see [below](#solver-configuration)). z3 comes with the Python dependencies; **yices2** is the solver the examples and tests use, and a good one to add. | Solver | How to get it | Notes | |---|---|---| -| yices2, cvc5, OpenSMT | bundled in `solvers/` | Ready to use | -| SMTInterpol | bundled in `solvers/` | Needs Java 21 (`sudo apt install openjdk-21-jdk`) | -| z3 | `z3-solver` (installed by `requirements.txt`), or `sudo apt install z3` | Must be on `PATH` as `z3`; `z3-solver` puts it into the virtual environment's `bin`, which is on `PATH` while the environment is active | -| dReal | [dReal 4.21.06.2](https://github.com/dreal/dreal4) | Expected at `/opt/dreal/4.21.06.2/bin/dreal` | -| Gurobi | `gurobipy` (installed by `requirements.txt`) | See below | +| yices2 | [release binaries](https://github.com/SRI-CSL/yices2/releases) (`bin/yices-smt2` in e.g. `yices-2.6.5-x86_64-pc-linux-gnu-static-gmp.tar.gz`) | | +| cvc5 | [release binaries](https://github.com/cvc5/cvc5/releases) (e.g. `cvc5-Linux-x86_64-static.zip`) | | +| OpenSMT | [OpenSMT](https://github.com/usi-verification-and-security/opensmt) | FiveTuple only | +| SMTInterpol | [smtinterpol.jar](https://ultimate.informatik.uni-freiburg.de/smtinterpol/) | Needs Java 21 (`sudo apt install openjdk-21-jdk`) and an executable `smtinterpol` wrapper, e.g. `java -jar /path/to/smtinterpol.jar "$@"`. FiveTuple only | +| z3 | `z3-solver` (installed by `requirements.txt`), or `sudo apt install z3` | `z3-solver` puts `z3` into the virtual environment's `bin` | +| dReal | [dReal 4](https://github.com/dreal/dreal4) | Classic only; also found in `/opt/dreal/*/bin` | +| Gurobi | `gurobipy` (installed by `requirements.txt`) | See [below](#gurobi-license); needs no configuration | -The `portfolio` option runs every compatible SMT solver. Solvers that are not installed or that fail (e.g. SMTInterpol without Java) are skipped, so it works with just the bundled ones. +The `portfolio` option runs every configured SMT solver that supports the formula's logic. Solvers that fail are skipped. -If the bundled binaries lost their executable bit (e.g. after copying the repository), restore it: +### Solver configuration + +Where the SMT solvers are and how they are called is set in `solvers.toml` in the repository root. `./configure-solvers` writes it for the solvers it finds on your `PATH` (with the virtual environment active, so that it finds `z3`): ```console -$ chmod +x solvers/cvc5/cvc5 solvers/opensmt/opensmt solvers/yices2/yices_smt2 solvers/smtinterpol/smtinterpol +$ ./configure-solvers +yices2: /usr/local/bin/yices-smt2 +cvc5: /home/me/cvc5/bin/cvc5 +opensmt: not found +smtinterpol: not found +z3: /home/me/milq/.venv/bin/z3 +dreal: not found +wrote /home/me/milq/solvers.toml +``` + +It looks for `yices-smt2` (or `yices_smt2`), `cvc5`, `opensmt`, `smtinterpol`, `z3` and `dreal` on `PATH` and among the downloaded solvers, and keeps each one only if it answers a trivial formula, so e.g. SMTInterpol without Java is left out. `-s DIR` also looks in `DIR` and `DIR/bin`, `-o FILE` writes another file (`-` for standard output), and `--force` overwrites an existing one. Run it again after installing a solver. + +`--download` first downloads the release binaries of yices2 2.7.0, cvc5 1.3.1 and OpenSMT 2.9.2 from GitHub into `solvers/` in the repository root (not tracked by git), checks their SHA-256 and links the executables into `solvers/bin`. `--download yices2,cvc5` downloads only those. Releases are available for Linux x86-64 and macOS (Linux arm64: cvc5 only); solvers that are already downloaded are kept. `--download-dir DIR` keeps them elsewhere. + +```console +$ ./configure-solvers --download +``` + +Each `[solvers.NAME]` table of the file defines one solver, and `-a NAME` selects it: + +### Solver configuration + +The SMT solvers are defined in `solvers.toml` in the repository root. Each `[solvers.NAME]` table defines one solver, and `-a NAME` selects it: + +```toml +[solvers.cvc5] +path = "/home/me/cvc5/bin/cvc5" # a relative path is relative to solvers.toml, a bare name is looked up on PATH +args = ["--produce-models"] # always passed +incremental_args = ["--incremental"] # added in the incremental modes, which send the formula through stdin +logics = ["QF_LIA", "QF_NIA", "QF_NRA"] ``` +| Key | Required | Meaning | +|---|---|---| +| `path` | yes | The executable. A relative path is relative to the configuration file, a bare name (e.g. `"z3"`) is looked up on `PATH`, and `~` and `$VARIABLES` are expanded. | +| `logics` | yes | SMT-LIB logics the solver supports, from `QF_LIA`, `QF_LRA`, `QF_NIA`, `QF_NRA`. FiveTuple formulas are `QF_LIA`, Classic ones `QF_NRA`. | +| `args` | no | Arguments always passed to the solver. | +| `incremental_args` | no | Extra arguments for the incremental modes. | +| `portfolio` | no | `false` keeps `-a portfolio` from running the solver (default `true`). | + +You can edit the file: to add a solver that `configure-solvers` does not know, add a table; the names `portfolio`, `gurobi` and `cbc` are reserved. `solvers.toml` is not tracked by git. To use another file, pass it with `--solver-config FILE`, or set the `MILQ_SOLVER_CONFIG` environment variable (`--solver-config` takes precedence). + ### Gurobi license `pip install gurobipy` comes with a **size-limited license**: models with at most 2000 variables and constraints. That is enough for very small instances, e.g. a 2-qubit circuit with `-v zero -c Classic`. Larger instances fail with *"Model too large for size-limited license"*. The license also expires about two years after the major release of gurobipy (13.x on 2027-11-29); after that, every Gurobi run fails with *"License expired"*, and `pip install -U gurobipy` brings a newer one. Gurobi offers [free academic licenses](https://www.gurobi.com/academia/academic-program-and-licenses/). Follow Gurobi's instructions to install the `gurobi.lic` file. diff --git a/docs/reference.md b/docs/reference.md index 2d94a87..ee3f620 100644 --- a/docs/reference.md +++ b/docs/reference.md @@ -17,7 +17,8 @@ $ ./milq [options] | `qasm_file` | path | *(required)* | Input circuit ([format](usage#input-circuits)). | | `-v`, `--vectors` | `all`, `zero`, `jamiolkowski`, `rus` | `all` | Input states the circuits must agree on ([details](usage#1-pick-what-must-be-preserved--v)). | | `-s`, `--solving` | `smt`, `gurobi`, `milp` | `gurobi` | Solving method ([details](usage#2-pick-a-backend--s--a--c)). | -| `-a`, `--solver` | `yices2`, `cvc5`, `opensmt`, `smtinterpol`, `z3`, `dreal`, `portfolio`, `gurobi`, `cbc` | `gurobi` | Solver; SMT solvers require `-s smt`, and `cbc` requires `-s milp`. | +| `-a`, `--solver` | a solver from the [solver configuration](installation#solver-configuration) (as written by `configure-solvers`: `yices2`, `cvc5`, `opensmt`, `smtinterpol`, `z3`, `dreal`, those installed), `portfolio`, `gurobi`, `cbc` | `gurobi` | Solver; SMT solvers and `portfolio` require `-s smt`, and `cbc` requires `-s milp`. | +| `--solver-config` | path | `$MILQ_SOLVER_CONFIG`, else `solvers.toml` in the repository root | [Solver configuration](installation#solver-configuration) file. | | `-c`, `--complex_representation` | `FiveTuple`, `Classic` | `FiveTuple` | Representation of amplitudes. | | `-m`, `--mode` | `incremental`, `basic`, `bottomup`, `topdown`, `binary`, `pareto-incremental` | `incremental` | Search mode ([details](usage#3-pick-a-search-mode--m)). | | `-d`, `--depth` | integer | input gate count | Number of layers for the fixed-depth modes. | @@ -81,7 +82,7 @@ Without `output_qasm`, no files are written: the circuit and the last formula go The synthesizer logs through the standard `logging` module (loggers `synth`, `generator`, `parser`) and writes no log file of its own. To see its progress, configure logging, e.g. `logging.basicConfig(level=logging.INFO)`. -The keyword arguments mirror the command-line options (`vectors` ↔ `-v`, `solving` ↔ `-s`, `solver` ↔ `-a`, `mode` ↔ `-m`, `complex_representation` ↔ `-c`, `d` ↔ `-d`, `up_to_global_phase` ↔ `-u`, `approx` ↔ `-ap`, `fidelity_threshold` ↔ `-f`, `targets` ↔ `-T`, `ancillas` ↔ `-A`, `no_measurement` ↔ `-nm`, `max_depth` ↔ `--max-depth`, `pareto_timeout` ↔ `-pt`). Three more are available only from Python: +The keyword arguments mirror the command-line options (`vectors` ↔ `-v`, `solving` ↔ `-s`, `solver` ↔ `-a`, `mode` ↔ `-m`, `complex_representation` ↔ `-c`, `d` ↔ `-d`, `up_to_global_phase` ↔ `-u`, `approx` ↔ `-ap`, `fidelity_threshold` ↔ `-f`, `targets` ↔ `-T`, `ancillas` ↔ `-A`, `no_measurement` ↔ `-nm`, `max_depth` ↔ `--max-depth`, `pareto_timeout` ↔ `-pt`, `solver_config` ↔ `--solver-config`). Three more are available only from Python: - `gate_set=GateSet([...])` (from `gates`), or just a list of gate names, restricts the gates the synthesized circuit may use. It is used as it is, also with `vectors="rus"`: only without a `gate_set` does RUS mode add Clifford+T and weight by T-count (call `set_t_optimal()` on your gate set for that). The caller's object is not changed. - `vectors="custom"` with `input_vectors` and a `qasm_file` (or `matrix`, which requires `complex_representation="Classic"`) synthesizes a circuit that agrees with the input circuit only on the given input states. With a `matrix`, the fixed-depth modes need `d`, since a matrix has no gate count. The expected outputs are simulated from the circuit, and `q`, `d`, the gate set and the measured qubits are taken from it unless passed explicitly. Each input state is a `Vector` (from `complex.vector`) with 2q amplitudes in the chosen representation: diff --git a/milq b/milq index ed4dd4d..3a8a309 100755 --- a/milq +++ b/milq @@ -16,16 +16,18 @@ import time sys.path.insert(0, os.path.join(os.path.dirname(os.path.realpath(__file__)), 'src')) from synth import Synthesizer from solvers import SolverError +from solver_config import SolverConfigError parser = argparse.ArgumentParser(description='CLI for the synthesis tool') parser.add_argument('qasm_file', type=str, help='qasm file to synthesize') parser.add_argument('-v', '--vectors', type=str, help='vectors mode to use for the synthesis', choices=["zero", "all", "rus", "jamiolkowski"], default="all") parser.add_argument('-s', '--solving', type=str, help='solving method to use', choices=["smt", "milp", "gurobi"], default="gurobi") parser.add_argument('-m', '--mode', type=str, help='solving mode to use', choices=["basic", "incremental", "binary", "topdown", "bottomup", "pareto-incremental"], default="incremental") -parser.add_argument('-a', '--solver', type=str, help='solver to use', required=False, choices=["z3", "cvc5", "yices2", "opensmt", "smtinterpol", "dreal", "gurobi", "cbc", "portfolio"], default="gurobi") +parser.add_argument('-a', '--solver', type=str, help='solver to use: with -s smt a solver from the solver configuration or portfolio, with -s milp gurobi or cbc', required=False, default="gurobi") +parser.add_argument('--solver-config', type=str, help='SMT solver configuration file (default: $MILQ_SOLVER_CONFIG, else solvers.toml next to this script)', required=False, default=None) parser.add_argument('-o', '--output_qasm', type=str, help='also write the synthesized circuit to this qasm file', required=False, default=None) parser.add_argument('-c', '--complex_representation', type=str, help='complex representation to use', required=False, choices=["FiveTuple", "Classic"], default="FiveTuple") -parser.add_argument('-f', '--fidelity_threshold', type=float, help='fidelity threshold (use with dreal solver)', required=False, default=1.0) +parser.add_argument('-f', '--fidelity_threshold', type=float, help='minimum average fidelity for approximate synthesis (-ap)', required=False, default=1.0) parser.add_argument('-ap', '--approx', action='store_true', help='approximate equivalence', default=False) parser.add_argument('-T', '--targets', type=int, help='number of target qubits', required=False, default=1) parser.add_argument('-A', '--ancillas', type=int, help='number of ancilla qubits', required=False, default=1) @@ -74,7 +76,11 @@ try: approx=args.approx, no_measurement=args.no_measurement, max_depth=args.max_depth, - pareto_timeout=args.pareto_timeout) + pareto_timeout=args.pareto_timeout, + solver_config=args.solver_config) +except SolverConfigError as e: + print(f"milq: error: {e}", file=sys.stderr) + sys.exit(2) except SolverError as e: print(f"synthesis failed: {e}", file=sys.stderr) sys.exit(1) diff --git a/solvers/cvc5/cvc5 b/solvers/cvc5/cvc5 deleted file mode 100755 index 7b0f50d..0000000 Binary files a/solvers/cvc5/cvc5 and /dev/null differ diff --git a/solvers/cvc5/cvc5.json b/solvers/cvc5/cvc5.json deleted file mode 100644 index b781a6f..0000000 --- a/solvers/cvc5/cvc5.json +++ /dev/null @@ -1,64 +0,0 @@ -{ - "name": "cvc5", - "contributors": [ - "Haniel Barbosa", - "Clark Barrett", - "Hanna Lachnitt", - "Daniel Larraz", - "Abdalrhman Mohamed", - "Mudathir Mohamed", - "José Neto", - "Aina Niemetz", - "Alex Ozdemir", - "Mathias Preiner", - "Andrew Reynolds", - "Hans-Jörg Schurr", - "Cesare Tinelli", - "Amalee Wilson", - "Yoni Zohar" - ], - "contacts": [ - "Hans-Jörg Schurr ", - "Daniel Larraz ", - "Clark Barrett " - ], - "archive": { - "url": "https://zenodo.org/records/15760304/files/cvc5-default.zip", - "h": { - "sha256": "627082d4c9b70d74787fbb8f78214fd4bc20924de1be294f658df4ea2e20c63f" - } - }, - "website": "https://cvc5.github.io/", - "system_description": "https://zenodo.org/records/15760304/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/15760304/files/cvc5-inc.zip", - "h": { - "sha256": "e5c29e6ae5a6193e06812f62c7eeb574f64939dd3ff61f08ae2ac87e6296fc48" - } - }, - "command": [ "bin/smtcomp_run_incremental" ] - } - ], - "seed": 8465677983, - "final" : true -} \ No newline at end of file diff --git a/solvers/cvc5/starexec_run_mv b/solvers/cvc5/starexec_run_mv deleted file mode 100755 index 3867f7f..0000000 --- a/solvers/cvc5/starexec_run_mv +++ /dev/null @@ -1,22 +0,0 @@ -#!/bin/bash - -cvc5=$(dirname "$(readlink -f "$0")")/cvc5 -bench="$1" - -# Output other than "sat"/"unsat" is either written to stderr or to "err.log" -# in the directory specified by $2 if it has been set (e.g. when running on -# StarExec). -out_file=/dev/stderr - -if [ -n "$STAREXEC_WALLCLOCK_LIMIT" ]; then - # If we are running on StarExec, don't print to `/dev/stderr/` even when $2 - # is not provided. - out_file="/dev/null" -fi - -if [ -n "$2" ]; then - out_file="$2/err.log" -fi - -$cvc5 -L smt2.6 --no-incremental --no-type-checking --no-interactive --fp-exp --use-portfolio $bench - diff --git a/solvers/cvc5/starexec_run_sq b/solvers/cvc5/starexec_run_sq deleted file mode 100755 index 8638610..0000000 --- a/solvers/cvc5/starexec_run_sq +++ /dev/null @@ -1,22 +0,0 @@ -#!/bin/bash - -cvc5=$(dirname "$(readlink -f "$0")")/cvc5 -bench="$1" - -# Output other than "sat"/"unsat" is either written to stderr or to "err.log" -# in the directory specified by $2 if it has been set (e.g. when running on -# StarExec). -out_file=/dev/stderr - -if [ -n "$STAREXEC_WALLCLOCK_LIMIT" ]; then - # If we are running on StarExec, don't print to `/dev/stderr/` even when $2 - # is not provided. - out_file="/dev/null" -fi - -if [ -n "$2" ]; then - out_file="$2/err.log" -fi - -result="$({ $cvc5 -L smt2.6 --no-incremental --produce-models --no-type-checking --no-interactive --fp-exp --use-portfolio $bench; } 2>&1)" -echo "$result" diff --git a/solvers/cvc5/starexec_run_uc b/solvers/cvc5/starexec_run_uc deleted file mode 100755 index 3867f7f..0000000 --- a/solvers/cvc5/starexec_run_uc +++ /dev/null @@ -1,22 +0,0 @@ -#!/bin/bash - -cvc5=$(dirname "$(readlink -f "$0")")/cvc5 -bench="$1" - -# Output other than "sat"/"unsat" is either written to stderr or to "err.log" -# in the directory specified by $2 if it has been set (e.g. when running on -# StarExec). -out_file=/dev/stderr - -if [ -n "$STAREXEC_WALLCLOCK_LIMIT" ]; then - # If we are running on StarExec, don't print to `/dev/stderr/` even when $2 - # is not provided. - out_file="/dev/null" -fi - -if [ -n "$2" ]; then - out_file="$2/err.log" -fi - -$cvc5 -L smt2.6 --no-incremental --no-type-checking --no-interactive --fp-exp --use-portfolio $bench - diff --git a/solvers/opensmt/opensmt b/solvers/opensmt/opensmt deleted file mode 100755 index a2790ad..0000000 Binary files a/solvers/opensmt/opensmt and /dev/null differ diff --git a/solvers/opensmt/opensmt.json b/solvers/opensmt/opensmt.json deleted file mode 100644 index b920f50..0000000 --- a/solvers/opensmt/opensmt.json +++ /dev/null @@ -1,45 +0,0 @@ -{ - "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/15720348/files/opensmt-x64-linux-static.tar.bz2" - , - "h": { "sha256": "be4767bf5d6c08bc7f4f49ae1480f2ae2ac8f38a277d0ec39d56badd974b84bd" } - }, - "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-2025.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": 87, - "final": true -} \ No newline at end of file diff --git a/solvers/smtinterpol/smtinterpol b/solvers/smtinterpol/smtinterpol deleted file mode 100755 index 11b0265..0000000 --- a/solvers/smtinterpol/smtinterpol +++ /dev/null @@ -1,4 +0,0 @@ -#!/bin/bash -# Run script for SMTInterpol for SMT-COMP 2024+ -SCRIPTDIR=`dirname $0` -java -da -dsa -jar $SCRIPTDIR/smtinterpol.jar -w -o continue-on-error=false -o proof-check-mode -o model-check-mode "$@" 2>error.log diff --git a/solvers/smtinterpol/smtinterpol-bv b/solvers/smtinterpol/smtinterpol-bv deleted file mode 100755 index 21348d5..0000000 --- a/solvers/smtinterpol/smtinterpol-bv +++ /dev/null @@ -1,4 +0,0 @@ -#!/bin/bash -# Run script for SMTInterpol for SMT-COMP 2024+ for bitvector theories -SCRIPTDIR=`dirname $0` -java -da -dsa -jar $SCRIPTDIR/smtinterpol.jar -w -o continue-on-error=false -o proof-check-mode -o model-check-mode "$@" 2>error.log diff --git a/solvers/smtinterpol/smtinterpol.jar b/solvers/smtinterpol/smtinterpol.jar deleted file mode 100644 index 94804e1..0000000 Binary files a/solvers/smtinterpol/smtinterpol.jar and /dev/null differ diff --git a/solvers/smtinterpol/smtinterpol.json b/solvers/smtinterpol/smtinterpol.json deleted file mode 100644 index b3aaaeb..0000000 --- a/solvers/smtinterpol/smtinterpol.json +++ /dev/null @@ -1,45 +0,0 @@ -{ - "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": [ - "Jochen Hoenicke " - ], - "archive": { - "url": "https://zenodo.org/records/15756957/files/smtinterpol-2.5-1405-gae7e68ef.tar.gz?download=1", - "h": { "sha256": "41a3ce3d38417a807865a389df3b8466492d584070c21888ac2732d8470d601c" } - }, - "website": "https://ultimate.informatik.uni-freiburg.de/smtinterpol", - "system_description": "https://ultimate.informatik.uni-freiburg.de/smtinterpol/sysdesc2025.pdf", - "command": ["smtinterpol"], - "solver_type": "Standalone", - "seed": "2030142482", - "participations": [ - { - "tracks": ["SingleQuery"], - "logics": "(QF_)?(AX?)?(UF)?(BV)?(DT)?([IR]DL|[NL][IR]*A)?", - "command": ["smtinterpol"] - }, - { - "tracks": ["Incremental"], - "logics": "(QF_)?(AX?)?(UF)?(BV)?(DT)?([IR]DL|[NL][IR]*A)?", - "command": ["smtinterpol"] - }, - { - "tracks": ["ModelValidation"], - "logics": "(QF_)(AX?)?(UF)?(BV)?(DT)?([IR]DL|[NL][IR]*A)?", - "command": ["smtinterpol"] - }, - { - "tracks": ["UnsatCore"], - "logics": "(QF_)?(AX?)?(UF)?(BV)?(DT)?([IR]DL|[NL][IR]*A)?", - "command": ["smtinterpol"] - } - ], - "final" : true -} \ No newline at end of file diff --git a/solvers/yices2/LICENSE.txt b/solvers/yices2/LICENSE.txt deleted file mode 100644 index 94a9ed0..0000000 --- a/solvers/yices2/LICENSE.txt +++ /dev/null @@ -1,674 +0,0 @@ - GNU GENERAL PUBLIC LICENSE - Version 3, 29 June 2007 - - Copyright (C) 2007 Free Software Foundation, Inc. - Everyone is permitted to copy and distribute verbatim copies - of this license document, but changing it is not allowed. - - Preamble - - The GNU General Public License is a free, copyleft license for -software and other kinds of works. - - The licenses for most software and other practical works are designed -to take away your freedom to share and change the works. By contrast, -the GNU General Public License is intended to guarantee your freedom to -share and change all versions of a program--to make sure it remains free -software for all its users. We, the Free Software Foundation, use the -GNU General Public License for most of our software; it applies also to -any other work released this way by its authors. You can apply it to -your programs, too. - - When we speak of free software, we are referring to freedom, not -price. Our General Public Licenses are designed to make sure that you -have the freedom to distribute copies of free software (and charge for -them if you wish), that you receive source code or can get it if you -want it, that you can change the software or use pieces of it in new -free programs, and that you know you can do these things. - - To protect your rights, we need to prevent others from denying you -these rights or asking you to surrender the rights. Therefore, you have -certain responsibilities if you distribute copies of the software, or if -you modify it: responsibilities to respect the freedom of others. - - For example, if you distribute copies of such a program, whether -gratis or for a fee, you must pass on to the recipients the same -freedoms that you received. You must make sure that they, too, receive -or can get the source code. And you must show them these terms so they -know their rights. - - Developers that use the GNU GPL protect your rights with two steps: -(1) assert copyright on the software, and (2) offer you this License -giving you legal permission to copy, distribute and/or modify it. - - For the developers' and authors' protection, the GPL clearly explains -that there is no warranty for this free software. For both users' and -authors' sake, the GPL requires that modified versions be marked as -changed, so that their problems will not be attributed erroneously to -authors of previous versions. - - Some devices are designed to deny users access to install or run -modified versions of the software inside them, although the manufacturer -can do so. This is fundamentally incompatible with the aim of -protecting users' freedom to change the software. The systematic -pattern of such abuse occurs in the area of products for individuals to -use, which is precisely where it is most unacceptable. Therefore, we -have designed this version of the GPL to prohibit the practice for those -products. If such problems arise substantially in other domains, we -stand ready to extend this provision to those domains in future versions -of the GPL, as needed to protect the freedom of users. - - Finally, every program is threatened constantly by software patents. -States should not allow patents to restrict development and use of -software on general-purpose computers, but in those that do, we wish to -avoid the special danger that patents applied to a free program could -make it effectively proprietary. To prevent this, the GPL assures that -patents cannot be used to render the program non-free. - - The precise terms and conditions for copying, distribution and -modification follow. - - TERMS AND CONDITIONS - - 0. Definitions. - - "This License" refers to version 3 of the GNU General Public License. - - "Copyright" also means copyright-like laws that apply to other kinds of -works, such as semiconductor masks. - - "The Program" refers to any copyrightable work licensed under this -License. Each licensee is addressed as "you". "Licensees" and -"recipients" may be individuals or organizations. - - To "modify" a work means to copy from or adapt all or part of the work -in a fashion requiring copyright permission, other than the making of an -exact copy. The resulting work is called a "modified version" of the -earlier work or a work "based on" the earlier work. - - A "covered work" means either the unmodified Program or a work based -on the Program. - - To "propagate" a work means to do anything with it that, without -permission, would make you directly or secondarily liable for -infringement under applicable copyright law, except executing it on a -computer or modifying a private copy. Propagation includes copying, -distribution (with or without modification), making available to the -public, and in some countries other activities as well. - - To "convey" a work means any kind of propagation that enables other -parties to make or receive copies. Mere interaction with a user through -a computer network, with no transfer of a copy, is not conveying. - - An interactive user interface displays "Appropriate Legal Notices" -to the extent that it includes a convenient and prominently visible -feature that (1) displays an appropriate copyright notice, and (2) -tells the user that there is no warranty for the work (except to the -extent that warranties are provided), that licensees may convey the -work under this License, and how to view a copy of this License. If -the interface presents a list of user commands or options, such as a -menu, a prominent item in the list meets this criterion. - - 1. Source Code. - - The "source code" for a work means the preferred form of the work -for making modifications to it. "Object code" means any non-source -form of a work. - - A "Standard Interface" means an interface that either is an official -standard defined by a recognized standards body, or, in the case of -interfaces specified for a particular programming language, one that -is widely used among developers working in that language. - - The "System Libraries" of an executable work include anything, other -than the work as a whole, that (a) is included in the normal form of -packaging a Major Component, but which is not part of that Major -Component, and (b) serves only to enable use of the work with that -Major Component, or to implement a Standard Interface for which an -implementation is available to the public in source code form. A -"Major Component", in this context, means a major essential component -(kernel, window system, and so on) of the specific operating system -(if any) on which the executable work runs, or a compiler used to -produce the work, or an object code interpreter used to run it. - - The "Corresponding Source" for a work in object code form means all -the source code needed to generate, install, and (for an executable -work) run the object code and to modify the work, including scripts to -control those activities. However, it does not include the work's -System Libraries, or general-purpose tools or generally available free -programs which are used unmodified in performing those activities but -which are not part of the work. For example, Corresponding Source -includes interface definition files associated with source files for -the work, and the source code for shared libraries and dynamically -linked subprograms that the work is specifically designed to require, -such as by intimate data communication or control flow between those -subprograms and other parts of the work. - - The Corresponding Source need not include anything that users -can regenerate automatically from other parts of the Corresponding -Source. - - The Corresponding Source for a work in source code form is that -same work. - - 2. Basic Permissions. - - All rights granted under this License are granted for the term of -copyright on the Program, and are irrevocable provided the stated -conditions are met. This License explicitly affirms your unlimited -permission to run the unmodified Program. The output from running a -covered work is covered by this License only if the output, given its -content, constitutes a covered work. This License acknowledges your -rights of fair use or other equivalent, as provided by copyright law. - - You may make, run and propagate covered works that you do not -convey, without conditions so long as your license otherwise remains -in force. You may convey covered works to others for the sole purpose -of having them make modifications exclusively for you, or provide you -with facilities for running those works, provided that you comply with -the terms of this License in conveying all material for which you do -not control copyright. Those thus making or running the covered works -for you must do so exclusively on your behalf, under your direction -and control, on terms that prohibit them from making any copies of -your copyrighted material outside their relationship with you. - - Conveying under any other circumstances is permitted solely under -the conditions stated below. Sublicensing is not allowed; section 10 -makes it unnecessary. - - 3. Protecting Users' Legal Rights From Anti-Circumvention Law. - - No covered work shall be deemed part of an effective technological -measure under any applicable law fulfilling obligations under article -11 of the WIPO copyright treaty adopted on 20 December 1996, or -similar laws prohibiting or restricting circumvention of such -measures. - - When you convey a covered work, you waive any legal power to forbid -circumvention of technological measures to the extent such circumvention -is effected by exercising rights under this License with respect to -the covered work, and you disclaim any intention to limit operation or -modification of the work as a means of enforcing, against the work's -users, your or third parties' legal rights to forbid circumvention of -technological measures. - - 4. Conveying Verbatim Copies. - - You may convey verbatim copies of the Program's source code as you -receive it, in any medium, provided that you conspicuously and -appropriately publish on each copy an appropriate copyright notice; -keep intact all notices stating that this License and any -non-permissive terms added in accord with section 7 apply to the code; -keep intact all notices of the absence of any warranty; and give all -recipients a copy of this License along with the Program. - - You may charge any price or no price for each copy that you convey, -and you may offer support or warranty protection for a fee. - - 5. Conveying Modified Source Versions. - - You may convey a work based on the Program, or the modifications to -produce it from the Program, in the form of source code under the -terms of section 4, provided that you also meet all of these conditions: - - a) The work must carry prominent notices stating that you modified - it, and giving a relevant date. - - b) The work must carry prominent notices stating that it is - released under this License and any conditions added under section - 7. This requirement modifies the requirement in section 4 to - "keep intact all notices". - - c) You must license the entire work, as a whole, under this - License to anyone who comes into possession of a copy. This - License will therefore apply, along with any applicable section 7 - additional terms, to the whole of the work, and all its parts, - regardless of how they are packaged. This License gives no - permission to license the work in any other way, but it does not - invalidate such permission if you have separately received it. - - d) If the work has interactive user interfaces, each must display - Appropriate Legal Notices; however, if the Program has interactive - interfaces that do not display Appropriate Legal Notices, your - work need not make them do so. - - A compilation of a covered work with other separate and independent -works, which are not by their nature extensions of the covered work, -and which are not combined with it such as to form a larger program, -in or on a volume of a storage or distribution medium, is called an -"aggregate" if the compilation and its resulting copyright are not -used to limit the access or legal rights of the compilation's users -beyond what the individual works permit. Inclusion of a covered work -in an aggregate does not cause this License to apply to the other -parts of the aggregate. - - 6. Conveying Non-Source Forms. - - You may convey a covered work in object code form under the terms -of sections 4 and 5, provided that you also convey the -machine-readable Corresponding Source under the terms of this License, -in one of these ways: - - a) Convey the object code in, or embodied in, a physical product - (including a physical distribution medium), accompanied by the - Corresponding Source fixed on a durable physical medium - customarily used for software interchange. - - b) Convey the object code in, or embodied in, a physical product - (including a physical distribution medium), accompanied by a - written offer, valid for at least three years and valid for as - long as you offer spare parts or customer support for that product - model, to give anyone who possesses the object code either (1) a - copy of the Corresponding Source for all the software in the - product that is covered by this License, on a durable physical - medium customarily used for software interchange, for a price no - more than your reasonable cost of physically performing this - conveying of source, or (2) access to copy the - Corresponding Source from a network server at no charge. - - c) Convey individual copies of the object code with a copy of the - written offer to provide the Corresponding Source. This - alternative is allowed only occasionally and noncommercially, and - only if you received the object code with such an offer, in accord - with subsection 6b. - - d) Convey the object code by offering access from a designated - place (gratis or for a charge), and offer equivalent access to the - Corresponding Source in the same way through the same place at no - further charge. You need not require recipients to copy the - Corresponding Source along with the object code. If the place to - copy the object code is a network server, the Corresponding Source - may be on a different server (operated by you or a third party) - that supports equivalent copying facilities, provided you maintain - clear directions next to the object code saying where to find the - Corresponding Source. Regardless of what server hosts the - Corresponding Source, you remain obligated to ensure that it is - available for as long as needed to satisfy these requirements. - - e) Convey the object code using peer-to-peer transmission, provided - you inform other peers where the object code and Corresponding - Source of the work are being offered to the general public at no - charge under subsection 6d. - - A separable portion of the object code, whose source code is excluded -from the Corresponding Source as a System Library, need not be -included in conveying the object code work. - - A "User Product" is either (1) a "consumer product", which means any -tangible personal property which is normally used for personal, family, -or household purposes, or (2) anything designed or sold for incorporation -into a dwelling. In determining whether a product is a consumer product, -doubtful cases shall be resolved in favor of coverage. For a particular -product received by a particular user, "normally used" refers to a -typical or common use of that class of product, regardless of the status -of the particular user or of the way in which the particular user -actually uses, or expects or is expected to use, the product. A product -is a consumer product regardless of whether the product has substantial -commercial, industrial or non-consumer uses, unless such uses represent -the only significant mode of use of the product. - - "Installation Information" for a User Product means any methods, -procedures, authorization keys, or other information required to install -and execute modified versions of a covered work in that User Product from -a modified version of its Corresponding Source. The information must -suffice to ensure that the continued functioning of the modified object -code is in no case prevented or interfered with solely because -modification has been made. - - If you convey an object code work under this section in, or with, or -specifically for use in, a User Product, and the conveying occurs as -part of a transaction in which the right of possession and use of the -User Product is transferred to the recipient in perpetuity or for a -fixed term (regardless of how the transaction is characterized), the -Corresponding Source conveyed under this section must be accompanied -by the Installation Information. But this requirement does not apply -if neither you nor any third party retains the ability to install -modified object code on the User Product (for example, the work has -been installed in ROM). - - The requirement to provide Installation Information does not include a -requirement to continue to provide support service, warranty, or updates -for a work that has been modified or installed by the recipient, or for -the User Product in which it has been modified or installed. Access to a -network may be denied when the modification itself materially and -adversely affects the operation of the network or violates the rules and -protocols for communication across the network. - - Corresponding Source conveyed, and Installation Information provided, -in accord with this section must be in a format that is publicly -documented (and with an implementation available to the public in -source code form), and must require no special password or key for -unpacking, reading or copying. - - 7. Additional Terms. - - "Additional permissions" are terms that supplement the terms of this -License by making exceptions from one or more of its conditions. -Additional permissions that are applicable to the entire Program shall -be treated as though they were included in this License, to the extent -that they are valid under applicable law. If additional permissions -apply only to part of the Program, that part may be used separately -under those permissions, but the entire Program remains governed by -this License without regard to the additional permissions. - - When you convey a copy of a covered work, you may at your option -remove any additional permissions from that copy, or from any part of -it. (Additional permissions may be written to require their own -removal in certain cases when you modify the work.) You may place -additional permissions on material, added by you to a covered work, -for which you have or can give appropriate copyright permission. - - Notwithstanding any other provision of this License, for material you -add to a covered work, you may (if authorized by the copyright holders of -that material) supplement the terms of this License with terms: - - a) Disclaiming warranty or limiting liability differently from the - terms of sections 15 and 16 of this License; or - - b) Requiring preservation of specified reasonable legal notices or - author attributions in that material or in the Appropriate Legal - Notices displayed by works containing it; or - - c) Prohibiting misrepresentation of the origin of that material, or - requiring that modified versions of such material be marked in - reasonable ways as different from the original version; or - - d) Limiting the use for publicity purposes of names of licensors or - authors of the material; or - - e) Declining to grant rights under trademark law for use of some - trade names, trademarks, or service marks; or - - f) Requiring indemnification of licensors and authors of that - material by anyone who conveys the material (or modified versions of - it) with contractual assumptions of liability to the recipient, for - any liability that these contractual assumptions directly impose on - those licensors and authors. - - All other non-permissive additional terms are considered "further -restrictions" within the meaning of section 10. If the Program as you -received it, or any part of it, contains a notice stating that it is -governed by this License along with a term that is a further -restriction, you may remove that term. If a license document contains -a further restriction but permits relicensing or conveying under this -License, you may add to a covered work material governed by the terms -of that license document, provided that the further restriction does -not survive such relicensing or conveying. - - If you add terms to a covered work in accord with this section, you -must place, in the relevant source files, a statement of the -additional terms that apply to those files, or a notice indicating -where to find the applicable terms. - - Additional terms, permissive or non-permissive, may be stated in the -form of a separately written license, or stated as exceptions; -the above requirements apply either way. - - 8. Termination. - - You may not propagate or modify a covered work except as expressly -provided under this License. Any attempt otherwise to propagate or -modify it is void, and will automatically terminate your rights under -this License (including any patent licenses granted under the third -paragraph of section 11). - - However, if you cease all violation of this License, then your -license from a particular copyright holder is reinstated (a) -provisionally, unless and until the copyright holder explicitly and -finally terminates your license, and (b) permanently, if the copyright -holder fails to notify you of the violation by some reasonable means -prior to 60 days after the cessation. - - Moreover, your license from a particular copyright holder is -reinstated permanently if the copyright holder notifies you of the -violation by some reasonable means, this is the first time you have -received notice of violation of this License (for any work) from that -copyright holder, and you cure the violation prior to 30 days after -your receipt of the notice. - - Termination of your rights under this section does not terminate the -licenses of parties who have received copies or rights from you under -this License. If your rights have been terminated and not permanently -reinstated, you do not qualify to receive new licenses for the same -material under section 10. - - 9. Acceptance Not Required for Having Copies. - - You are not required to accept this License in order to receive or -run a copy of the Program. Ancillary propagation of a covered work -occurring solely as a consequence of using peer-to-peer transmission -to receive a copy likewise does not require acceptance. However, -nothing other than this License grants you permission to propagate or -modify any covered work. These actions infringe copyright if you do -not accept this License. Therefore, by modifying or propagating a -covered work, you indicate your acceptance of this License to do so. - - 10. Automatic Licensing of Downstream Recipients. - - Each time you convey a covered work, the recipient automatically -receives a license from the original licensors, to run, modify and -propagate that work, subject to this License. You are not responsible -for enforcing compliance by third parties with this License. - - An "entity transaction" is a transaction transferring control of an -organization, or substantially all assets of one, or subdividing an -organization, or merging organizations. If propagation of a covered -work results from an entity transaction, each party to that -transaction who receives a copy of the work also receives whatever -licenses to the work the party's predecessor in interest had or could -give under the previous paragraph, plus a right to possession of the -Corresponding Source of the work from the predecessor in interest, if -the predecessor has it or can get it with reasonable efforts. - - You may not impose any further restrictions on the exercise of the -rights granted or affirmed under this License. For example, you may -not impose a license fee, royalty, or other charge for exercise of -rights granted under this License, and you may not initiate litigation -(including a cross-claim or counterclaim in a lawsuit) alleging that -any patent claim is infringed by making, using, selling, offering for -sale, or importing the Program or any portion of it. - - 11. Patents. - - A "contributor" is a copyright holder who authorizes use under this -License of the Program or a work on which the Program is based. The -work thus licensed is called the contributor's "contributor version". - - A contributor's "essential patent claims" are all patent claims -owned or controlled by the contributor, whether already acquired or -hereafter acquired, that would be infringed by some manner, permitted -by this License, of making, using, or selling its contributor version, -but do not include claims that would be infringed only as a -consequence of further modification of the contributor version. For -purposes of this definition, "control" includes the right to grant -patent sublicenses in a manner consistent with the requirements of -this License. - - Each contributor grants you a non-exclusive, worldwide, royalty-free -patent license under the contributor's essential patent claims, to -make, use, sell, offer for sale, import and otherwise run, modify and -propagate the contents of its contributor version. - - In the following three paragraphs, a "patent license" is any express -agreement or commitment, however denominated, not to enforce a patent -(such as an express permission to practice a patent or covenant not to -sue for patent infringement). To "grant" such a patent license to a -party means to make such an agreement or commitment not to enforce a -patent against the party. - - If you convey a covered work, knowingly relying on a patent license, -and the Corresponding Source of the work is not available for anyone -to copy, free of charge and under the terms of this License, through a -publicly available network server or other readily accessible means, -then you must either (1) cause the Corresponding Source to be so -available, or (2) arrange to deprive yourself of the benefit of the -patent license for this particular work, or (3) arrange, in a manner -consistent with the requirements of this License, to extend the patent -license to downstream recipients. "Knowingly relying" means you have -actual knowledge that, but for the patent license, your conveying the -covered work in a country, or your recipient's use of the covered work -in a country, would infringe one or more identifiable patents in that -country that you have reason to believe are valid. - - If, pursuant to or in connection with a single transaction or -arrangement, you convey, or propagate by procuring conveyance of, a -covered work, and grant a patent license to some of the parties -receiving the covered work authorizing them to use, propagate, modify -or convey a specific copy of the covered work, then the patent license -you grant is automatically extended to all recipients of the covered -work and works based on it. - - A patent license is "discriminatory" if it does not include within -the scope of its coverage, prohibits the exercise of, or is -conditioned on the non-exercise of one or more of the rights that are -specifically granted under this License. You may not convey a covered -work if you are a party to an arrangement with a third party that is -in the business of distributing software, under which you make payment -to the third party based on the extent of your activity of conveying -the work, and under which the third party grants, to any of the -parties who would receive the covered work from you, a discriminatory -patent license (a) in connection with copies of the covered work -conveyed by you (or copies made from those copies), or (b) primarily -for and in connection with specific products or compilations that -contain the covered work, unless you entered into that arrangement, -or that patent license was granted, prior to 28 March 2007. - - Nothing in this License shall be construed as excluding or limiting -any implied license or other defenses to infringement that may -otherwise be available to you under applicable patent law. - - 12. No Surrender of Others' Freedom. - - If conditions are imposed on you (whether by court order, agreement or -otherwise) that contradict the conditions of this License, they do not -excuse you from the conditions of this License. If you cannot convey a -covered work so as to satisfy simultaneously your obligations under this -License and any other pertinent obligations, then as a consequence you may -not convey it at all. For example, if you agree to terms that obligate you -to collect a royalty for further conveying from those to whom you convey -the Program, the only way you could satisfy both those terms and this -License would be to refrain entirely from conveying the Program. - - 13. Use with the GNU Affero General Public License. - - Notwithstanding any other provision of this License, you have -permission to link or combine any covered work with a work licensed -under version 3 of the GNU Affero General Public License into a single -combined work, and to convey the resulting work. The terms of this -License will continue to apply to the part which is the covered work, -but the special requirements of the GNU Affero General Public License, -section 13, concerning interaction through a network will apply to the -combination as such. - - 14. Revised Versions of this License. - - The Free Software Foundation may publish revised and/or new versions of -the GNU General Public License from time to time. Such new versions will -be similar in spirit to the present version, but may differ in detail to -address new problems or concerns. - - Each version is given a distinguishing version number. If the -Program specifies that a certain numbered version of the GNU General -Public License "or any later version" applies to it, you have the -option of following the terms and conditions either of that numbered -version or of any later version published by the Free Software -Foundation. If the Program does not specify a version number of the -GNU General Public License, you may choose any version ever published -by the Free Software Foundation. - - If the Program specifies that a proxy can decide which future -versions of the GNU General Public License can be used, that proxy's -public statement of acceptance of a version permanently authorizes you -to choose that version for the Program. - - Later license versions may give you additional or different -permissions. However, no additional obligations are imposed on any -author or copyright holder as a result of your choosing to follow a -later version. - - 15. Disclaimer of Warranty. - - THERE IS NO WARRANTY FOR THE PROGRAM, TO THE EXTENT PERMITTED BY -APPLICABLE LAW. EXCEPT WHEN OTHERWISE STATED IN WRITING THE COPYRIGHT -HOLDERS AND/OR OTHER PARTIES PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY -OF ANY KIND, EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, -THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR -PURPOSE. THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE PROGRAM -IS WITH YOU. SHOULD THE PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF -ALL NECESSARY SERVICING, REPAIR OR CORRECTION. - - 16. Limitation of Liability. - - IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING -WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MODIFIES AND/OR CONVEYS -THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, INCLUDING ANY -GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE -USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED TO LOSS OF -DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY YOU OR THIRD -PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER PROGRAMS), -EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE POSSIBILITY OF -SUCH DAMAGES. - - 17. Interpretation of Sections 15 and 16. - - If the disclaimer of warranty and limitation of liability provided -above cannot be given local legal effect according to their terms, -reviewing courts shall apply local law that most closely approximates -an absolute waiver of all civil liability in connection with the -Program, unless a warranty or assumption of liability accompanies a -copy of the Program in return for a fee. - - END OF TERMS AND CONDITIONS - - How to Apply These Terms to Your New Programs - - If you develop a new program, and you want it to be of the greatest -possible use to the public, the best way to achieve this is to make it -free software which everyone can redistribute and change under these terms. - - To do so, attach the following notices to the program. It is safest -to attach them to the start of each source file to most effectively -state the exclusion of warranty; and each file should have at least -the "copyright" line and a pointer to where the full notice is found. - - - Copyright (C) - - This program is free software: you can redistribute it and/or modify - it under the terms of the GNU General Public License as published by - the Free Software Foundation, either version 3 of the License, or - (at your option) any later version. - - This program is distributed in the hope that it will be useful, - but WITHOUT ANY WARRANTY; without even the implied warranty of - MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - GNU General Public License for more details. - - You should have received a copy of the GNU General Public License - along with this program. If not, see . - -Also add information on how to contact you by electronic and paper mail. - - If the program does terminal interaction, make it output a short -notice like this when it starts in an interactive mode: - - Copyright (C) - This program comes with ABSOLUTELY NO WARRANTY; for details type `show w'. - This is free software, and you are welcome to redistribute it - under certain conditions; type `show c' for details. - -The hypothetical commands `show w' and `show c' should show the appropriate -parts of the General Public License. Of course, your program's commands -might be different; for a GUI interface, you would use an "about box". - - You should also get your employer (if you work as a programmer) or school, -if any, to sign a "copyright disclaimer" for the program, if necessary. -For more information on this, and how to apply and follow the GNU GPL, see -. - - The GNU General Public License does not permit incorporating your program -into proprietary programs. If your program is a subroutine library, you -may consider it more useful to permit linking proprietary applications with -the library. If this is what you want to do, use the GNU Lesser General -Public License instead of this License. But first, please read -. diff --git a/solvers/yices2/yices2.json b/solvers/yices2/yices2.json deleted file mode 100644 index 3bb4468..0000000 --- a/solvers/yices2/yices2.json +++ /dev/null @@ -1,191 +0,0 @@ -{ - "name": "Yices2", - "contributors": [ - "Bruno Dutertre", - "Aman Goel", - "Stéphane Graham-Lengrand", - "Thomas Hader", - "Ahmed Irfan", - "Dejan Jovanovic", - "Enrico Lipparini", - "Ian A Mason", - "Karthik Nukala", - "Harald Ruess" - ], - "contacts": [ - "Ahmed Irfan ", - "Stéphane Graham-Lengrand " - ], - "final" : true, - "archive": { - "url": "https://zenodo.org/records/15766479/files/yices2-smtcomp-2025.zip?download=1" - }, - "website": "https://yices.csl.sri.com", - "system_description": "https://ahmed-irfan.github.io/smtcomp/yices2-smtcomp-2025.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_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": ["SingleQuery"], - "logics": ["QF_NIA"], - "command": ["./yices_smt2", "--mcsat-l2o"] - }, - { - "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_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"] - }, - { - "tracks": ["ModelValidation"], - "logics": ["QF_BV", - "QF_BVLRA", - "QF_IDL", - "QF_LIA", - "QF_LIRA", - "QF_LRA", - "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"] - }, - { - "tracks": ["ModelValidation"], - "logics": ["QF_NIA"], - "command": ["./yices_smt2", "--mcsat-l2o"] - }, - { - "tracks": ["Parallel"], - "logics": ["QF_NIA"], - "command": ["./yices2_parallel.py", "--yices", "./yices_smt2", "-n", "128", "--mcsat-l2o"] - }, - { - "tracks": ["Parallel"], - "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_NIRA", - "QF_NRA", - "QF_RDL", - "QF_UF", - "QF_UFBV", - "QF_UFBVLIA", - "QF_UFIDL", - "QF_UFLIA", - "QF_UFLRA", - "QF_UFNIA", - "QF_UFNRA"], - "command": ["./yices2_parallel.py", "--yices", "./yices_smt2", "-n", "128"] - } - ], - "seed": 0 -} \ No newline at end of file diff --git a/solvers/yices2/yices2_parallel.py b/solvers/yices2/yices2_parallel.py deleted file mode 100755 index 5d25727..0000000 --- a/solvers/yices2/yices2_parallel.py +++ /dev/null @@ -1,218 +0,0 @@ -#!/usr/bin/env python3 - -import subprocess -import threading -import sys -import os -import signal -import time -import argparse -import random -from typing import List - -def _global_signal_handler(signum, frame): - """Global signal handler for the main process""" - if signum == signal.SIGINT: - print("\nReceived Ctrl+C, shutting down gracefully...", file=sys.stderr) - else: - print(f"\nReceived signal {signum}, shutting down gracefully...", file=sys.stderr) - - # Clean up any running threads - if hasattr(_global_signal_handler, 'solver'): - _global_signal_handler.solver.cleanup_threads() - - sys.exit(0) - -class ConfigGenerator: - def __init__(self, num_configs: int, seed: int = None, use_l2o: bool = False): - self.num_configs = num_configs - self.use_l2o = use_l2o - if seed is not None: - random.seed(seed) - - def generate_configs(self) -> List[List[str]]: - configs = [[], ["--mcsat", "--mcsat-nra-bound"]] # Always include empty config and nra bound - if self.use_l2o: - configs.append(["--mcsat", "--mcsat-l2o"]) - - for _ in range(self.num_configs - 2): - options = ["--mcsat"] # Start with base mcsat option - if random.random() < 0.9: - options.append(f"--mcsat-rand-dec-seed={random.randint(1, 1000000)}") - if random.random() < 0.9: - options.append(f"--mcsat-rand-dec-freq={random.uniform(0, 1):.2f}") - if random.random() < 0.5: - options.append("--mcsat-nra-nlsat") - if random.random() < 0.5: - options.append("--mcsat-nra-mgcd") - if random.random() < 0.5: - options.append("--mcsat-nra-bound") - if random.random() < 0.5: - options.append("--mcsat-partial-restart") - if self.use_l2o and random.random() < 0.5: - options.append("--mcsat-l2o") - - if len(options) == 1: # If only base option, add a random one - options.append(random.choice([ - f"--mcsat-rand-dec-freq={random.uniform(0, 1):.2f}", - f"--mcsat-rand-dec-seed={random.randint(1, 1000000)}" - ])) - - configs.append(options) - - return configs - -class PortfolioSolver: - def __init__(self, yices_path, smt2_file, num_threads, verbose=False, seed=None, use_l2o=False): - self.yices_path = yices_path - self.smt2_file = smt2_file - self.num_threads = num_threads - self.verbose = verbose - self.seed = seed - self.use_l2o = use_l2o - self.threads = [] - self.stop_event = threading.Event() - self.start_time = None - self.processes = [] - self._solution = None - _global_signal_handler.solver = self - - @property - def solution(self): - return self._solution - - @solution.setter - def solution(self, value): - if not self.stop_event.is_set(): - self._solution = value - self.stop_event.set() - self.cleanup_threads() - - def log(self, message): - if self.verbose: - print(f"[{time.time() - self.start_time:.2f}s] {message}", file=sys.stderr) - - def cleanup_threads(self): - self.stop_event.set() - for process in self.processes: - try: - if process and process.poll() is None: - process.kill() - except (ProcessLookupError, OSError): - pass - self.threads.clear() - self.processes.clear() - - def run_yices(self, thread_id, params): - process = None - try: - cmd = [self.yices_path] + params + [self.smt2_file] - self.log(f"Thread {thread_id} starting with params: {' '.join(params)}") - - process = subprocess.Popen( - cmd, - stdout=subprocess.PIPE, - stderr=subprocess.PIPE, - text=True - ) - self.processes.append(process) - - stdout, stderr = process.communicate() - - if not self.stop_event.is_set(): - if "unsat" in stdout.lower(): - self.log(f"Thread {thread_id} found UNSAT solution") - self.solution = ("unsat", stdout, thread_id, params) - elif "sat" in stdout.lower(): - self.log(f"Thread {thread_id} found SAT solution") - self.solution = ("sat", stdout, thread_id, params) - else: - self.log(f"Thread {thread_id} finished without finding solution") - - except Exception as e: - if not self.stop_event.is_set(): - self.log(f"Error in thread {thread_id}: {e}") - finally: - if process and process.poll() is None: - try: - process.kill() - except (ProcessLookupError, OSError): - pass - - def solve(self): - try: - config_generator = ConfigGenerator(self.num_threads, self.seed, self.use_l2o) - param_sets = config_generator.generate_configs() - - self.start_time = time.time() - self.log(f"Starting portfolio solver with {self.num_threads} threads") - self.log(f"Using yices_smt2 from: {self.yices_path}") - self.log(f"Solving file: {self.smt2_file}") - if self.seed is not None: - self.log(f"Using random seed: {self.seed}") - self.log("Generated configurations:") - for i, params in enumerate(param_sets): - self.log(f" Config {i}: {' '.join(params) if params else '(default)'}") - - for i in range(min(self.num_threads, len(param_sets))): - thread = threading.Thread(target=self.run_yices, args=(i, param_sets[i])) - thread.daemon = True - self.threads.append(thread) - thread.start() - self.log(f"Started thread {i}") - - for thread in self.threads: - thread.join() - - if self.solution is not None: - result, output, thread_id, params = self.solution - self.log(f"Solution found by thread {thread_id} with params: {' '.join(params) if params else '(default)'}") - return result, output - return "unknown", "No solution found" - - finally: - self.cleanup_threads() - -def main(): - signal.signal(signal.SIGINT, _global_signal_handler) - signal.signal(signal.SIGTERM, _global_signal_handler) - signal.signal(signal.SIGQUIT, _global_signal_handler) - - parser = argparse.ArgumentParser(description='Portfolio solver using yices_smt2') - parser.add_argument('--yices', default='yices_smt2', help='Path to yices_smt2 executable (default: yices_smt2)') - parser.add_argument('-n', '--num-threads', type=int, default=4, help='Number of threads to use (default: 4)') - parser.add_argument('-v', '--verbose', action='store_true', help='Enable verbose output') - parser.add_argument('--seed', type=int, help='Random seed for configuration generation') - parser.add_argument('--mcsat-l2o', action='store_true', help='Use MCSAT L2O option as one of the configuration') - parser.add_argument('smt2_file', help='Path to SMT2 benchmark file') - - args = parser.parse_args() - - # Get the directory of this script - script_dir = os.path.dirname(os.path.abspath(__file__)) - - # If yices path is not absolute, make it relative to script directory - if not os.path.isabs(args.yices): - args.yices = os.path.join(script_dir, args.yices) - - if not os.path.exists(args.yices): - print(f"Error: yices_smt2 executable not found at {args.yices}", file=sys.stderr) - sys.exit(1) - - if not os.path.exists(args.smt2_file): - print(f"Error: SMT2 file not found at {args.smt2_file}", file=sys.stderr) - sys.exit(1) - - try: - solver = PortfolioSolver(args.yices, args.smt2_file, args.num_threads, args.verbose, args.seed, args.mcsat_l2o) - result, output = solver.solve() - print(result) - except KeyboardInterrupt: - print("\nInterrupted by user", file=sys.stderr) - sys.exit(1) - except Exception as e: - print(f"Error: {e}", file=sys.stderr) - sys.exit(1) - -if __name__ == "__main__": - main() diff --git a/solvers/yices2/yices_smt2 b/solvers/yices2/yices_smt2 deleted file mode 100755 index 7f04b78..0000000 Binary files a/solvers/yices2/yices_smt2 and /dev/null differ diff --git a/solvers/z3alpha/strats/lia.txt b/solvers/z3alpha/strats/lia.txt deleted file mode 100644 index aae1bf0..0000000 --- a/solvers/z3alpha/strats/lia.txt +++ /dev/null @@ -1 +0,0 @@ -(par-or (then (then propagate-ineqs ctx-simplify lia) fail-if-undecided) (then (then solve-eqs normalize-bounds lia) fail-if-undecided) (then (then degree-shift (using-params simplify :elim_and true :blast_distinct true :local_ctx true :pull_cheap_ite true :som true :flat true :push_ite_arith true :hoist_ite true :arith_lhs true) elim-uncnstr solve-eqs elim-uncnstr lia) fail-if-undecided) (then (then cofactor-term-ite solve-eqs propagate-ineqs lia) fail-if-undecided)) \ No newline at end of file diff --git a/solvers/z3alpha/strats/logic_strategies.json b/solvers/z3alpha/strats/logic_strategies.json deleted file mode 100644 index cee3f8e..0000000 --- a/solvers/z3alpha/strats/logic_strategies.json +++ /dev/null @@ -1,15 +0,0 @@ -{ - "LIA": "lia.txt", - "LRA": "lra.txt", - "NIA": "nia.txt", - "NRA": "nra.txt", - "QF_BV": "qfbv.txt", - "QF_IDL": "qfidl.txt", - "QF_LIA": "qflia.txt", - "QF_LRA": "qflra.txt", - "QF_RDL": "qfrdl.txt", - "QF_NIA": "qfnia.txt", - "QF_NRA": "qfnra.txt", - "QF_S": "qfs.txt", - "QF_SLIA": "qfslia.txt" -} \ No newline at end of file diff --git a/solvers/z3alpha/strats/lra.txt b/solvers/z3alpha/strats/lra.txt deleted file mode 100644 index e81dd8b..0000000 --- a/solvers/z3alpha/strats/lra.txt +++ /dev/null @@ -1 +0,0 @@ -(par-or (then (then ctx-simplify cofactor-term-ite degree-shift propagate-values fm propagate-values lra) fail-if-undecided) (then (then purify-arith (using-params simplify :elim_and true :blast_distinct true :local_ctx true :pull_cheap_ite true :som true :flat true :push_ite_arith true :hoist_ite true :arith_lhs true) propagate-values lra) fail-if-undecided) (then (then fm ctx-simplify lia2card lra) fail-if-undecided) (then (then (using-params simplify :elim_and false :blast_distinct false :local_ctx false :pull_cheap_ite false :som false :flat false :push_ite_arith false :hoist_ite false :arith_lhs false) lra) fail-if-undecided)) \ No newline at end of file diff --git a/solvers/z3alpha/strats/nia.txt b/solvers/z3alpha/strats/nia.txt deleted file mode 100644 index ff2eff0..0000000 --- a/solvers/z3alpha/strats/nia.txt +++ /dev/null @@ -1 +0,0 @@ -(par-or (then (then degree-shift (using-params smt :random_seed 500)) fail-if-undecided) (then (then cofactor-term-ite lia) fail-if-undecided) (then (then purify-arith (using-params simplify :elim_and true :blast_distinct true :local_ctx true :pull_cheap_ite true :som true :flat true :push_ite_arith true :hoist_ite true :arith_lhs true) lia2pb lia) fail-if-undecided) (then (then recover-01 elim-uncnstr solve-eqs purify-arith smt) fail-if-undecided)) \ No newline at end of file diff --git a/solvers/z3alpha/strats/nra.txt b/solvers/z3alpha/strats/nra.txt deleted file mode 100644 index dc7aa9f..0000000 --- a/solvers/z3alpha/strats/nra.txt +++ /dev/null @@ -1,4 +0,0 @@ -(par-or (then (then (using-params lia2pb :lia2pb_max_bits 16) factor elim-uncnstr fix-dl-var elim-uncnstr fix-dl-var nra) fail-if-undecided) -(then (then fix-dl-var (using-params smt :random_seed 400)) fail-if-undecided) -(then (then elim-uncnstr (using-params smt :random_seed 200)) fail-if-undecided) -(then (then purify-arith elim-uncnstr eq2bv smt) fail-if-undecided)) \ No newline at end of file diff --git a/solvers/z3alpha/strats/qfbv.txt b/solvers/z3alpha/strats/qfbv.txt deleted file mode 100644 index 0678544..0000000 --- a/solvers/z3alpha/strats/qfbv.txt +++ /dev/null @@ -1,6 +0,0 @@ -(par-or -(then (then (using-params simplify :elim_and false :blast_distinct false :local_ctx false :pull_cheap_ite false :som false :flat false :push_ite_bv false :hoist_mul false) qfbv) fail-if-undecided) -(then (then aig purify-arith simplify purify-arith smt) fail-if-undecided) -(then (then max-bv-sharing solve-eqs ctx-simplify ackermannize_bv simplify bit-blast smt) fail-if-undecided) -(then (then max-bv-sharing simplify bit-blast elim-uncnstr sat) fail-if-undecided) -) \ No newline at end of file diff --git a/solvers/z3alpha/strats/qfidl.txt b/solvers/z3alpha/strats/qfidl.txt deleted file mode 100644 index 737572d..0000000 --- a/solvers/z3alpha/strats/qfidl.txt +++ /dev/null @@ -1,2 +0,0 @@ -(par-or (then -(then (using-params simplify :elim_and true :blast_distinct true :local_ctx true :pull_cheap_ite true :som true :flat true :push_ite_arith true :hoist_ite true :arith_lhs true) (using-params simplify :elim_and false :blast_distinct false :local_ctx false :pull_cheap_ite false :som false :flat false :push_ite_arith false :hoist_ite false :arith_lhs false) (using-params simplify :elim_and true :blast_distinct true :local_ctx true :pull_cheap_ite true :som true :flat true :push_ite_arith true :hoist_ite true :arith_lhs true) solve-eqs elim-uncnstr solve-eqs qfidl) fail-if-undecided) (then (then solve-eqs (using-params smt :random_seed 400)) fail-if-undecided) (then (then ctx-simplify (using-params smt :random_seed 300)) fail-if-undecided) (then (then elim-uncnstr solve-eqs propagate-values solve-eqs solve-eqs smt) fail-if-undecided)) \ No newline at end of file diff --git a/solvers/z3alpha/strats/qflia.txt b/solvers/z3alpha/strats/qflia.txt deleted file mode 100644 index a0935f8..0000000 --- a/solvers/z3alpha/strats/qflia.txt +++ /dev/null @@ -1,5 +0,0 @@ -(par-or -(then (then (using-params simplify :elim_and false :blast_distinct false :local_ctx false :pull_cheap_ite false :som false :flat false :push_ite_arith false :hoist_ite false :arith_lhs false) propagate-values smt) fail-if-undecided) -(then (then elim-uncnstr propagate-ineqs qflia) fail-if-undecided) -(then (then propagate-ineqs (using-params simplify :elim_and false :blast_distinct false :local_ctx false :pull_cheap_ite false :som false :flat false :push_ite_arith false :hoist_ite false :arith_lhs false) smt) fail-if-undecided) -(then (then (using-params simplify :elim_and false :blast_distinct false :local_ctx false :pull_cheap_ite false :som false :flat false :push_ite_arith false :hoist_ite false :arith_lhs false) (using-params smt :random_seed 500)) fail-if-undecided)) \ No newline at end of file diff --git a/solvers/z3alpha/strats/qflra.txt b/solvers/z3alpha/strats/qflra.txt deleted file mode 100644 index 00d64d1..0000000 --- a/solvers/z3alpha/strats/qflra.txt +++ /dev/null @@ -1 +0,0 @@ -(par-or (then (then propagate-values propagate-values (using-params simplify :elim_and true :blast_distinct true :local_ctx true :pull_cheap_ite true :som true :flat true) ctx-simplify qflra) fail-if-undecided) (then (then ctx-simplify (using-params smt :random_seed 400)) fail-if-undecided) (then (then (using-params simplify :elim_and true :blast_distinct true :local_ctx true :pull_cheap_ite true :som true :flat true) (using-params smt :random_seed 500)) fail-if-undecided) (then (then (using-params simplify :elim_and false :blast_distinct false :local_ctx false :pull_cheap_ite false :som false :flat false) (using-params simplify :elim_and true :blast_distinct true :local_ctx true :pull_cheap_ite true :som true :flat true) qflra) fail-if-undecided)) \ No newline at end of file diff --git a/solvers/z3alpha/strats/qfnia.txt b/solvers/z3alpha/strats/qfnia.txt deleted file mode 100644 index 68a53a1..0000000 --- a/solvers/z3alpha/strats/qfnia.txt +++ /dev/null @@ -1,5 +0,0 @@ -(par-or -(then (then solve-eqs (using-params simplify :elim_and false :blast_distinct false :local_ctx false :pull_cheap_ite false :som false :flat false :hi_div0 false :hoist_mul false :push_ite_bv false) qfnia) fail-if-undecided) -(then (then (using-params nla2bv :nla2bv_max_bv_size 64) qfbv) fail-if-undecided) -(then (then (using-params propagate-values :push_ite_bv true) (using-params smt :random_seed 100)) fail-if-undecided) -(then (then lia2card (using-params simplify :elim_and false :blast_distinct false :local_ctx false :pull_cheap_ite false :som false :flat false :hi_div0 false :hoist_mul false :push_ite_bv false) card2bv solve-eqs lia2card smt) fail-if-undecided)) \ No newline at end of file diff --git a/solvers/z3alpha/strats/qfnra.txt b/solvers/z3alpha/strats/qfnra.txt deleted file mode 100644 index 99e9868..0000000 --- a/solvers/z3alpha/strats/qfnra.txt +++ /dev/null @@ -1,6 +0,0 @@ -(par-or -(then (then solve-eqs solve-eqs elim-uncnstr propagate-values smt) fail-if-undecided) -(then (then (using-params propagate-values :push_ite_bv true) (using-params simplify :elim_and true :blast_distinct true :local_ctx true :pull_cheap_ite true :som true :flat true :hi_div0 true :hoist_mul true :push_ite_bv true) (using-params simplify :elim_and true :blast_distinct true :local_ctx true :pull_cheap_ite true :som true :flat true :hi_div0 true :hoist_mul true :push_ite_bv true) solve-eqs simplify propagate-values ctx-simplify qfnra) fail-if-undecided) -(then (then elim-uncnstr (using-params smt :random_seed 500)) fail-if-undecided) -(then (using-params qfnra-nlsat :inline_vars true :factor true :seed 100) fail-if-undecided) -) \ No newline at end of file diff --git a/solvers/z3alpha/strats/qfrdl.txt b/solvers/z3alpha/strats/qfrdl.txt deleted file mode 100644 index f89deeb..0000000 --- a/solvers/z3alpha/strats/qfrdl.txt +++ /dev/null @@ -1 +0,0 @@ -(par-or (then (then degree-shift (using-params smt :random_seed 300)) fail-if-undecided) (then (then degree-shift elim-uncnstr smt) fail-if-undecided) (then (then propagate-values (using-params smt :random_seed 200)) fail-if-undecided) (then (then card2bv (using-params smt :random_seed 100)) fail-if-undecided)) \ No newline at end of file diff --git a/solvers/z3alpha/strats/qfs.txt b/solvers/z3alpha/strats/qfs.txt deleted file mode 100644 index 127286c..0000000 --- a/solvers/z3alpha/strats/qfs.txt +++ /dev/null @@ -1,5 +0,0 @@ -(par-or -(then (then solve-eqs (using-params simplify :elim_and false :blast_distinct false :local_ctx false :pull_cheap_ite false) (using-params smt :smt.string_solver z3str3) fail-if-undecided)) -(then (then solve-eqs (using-params smt :random_seed 400) fail-if-undecided)) -(then (then (using-params simplify :elim_and true :blast_distinct true :local_ctx true :pull_cheap_ite true) (using-params smt :random_seed 200) fail-if-undecided)) -(then (then (using-params simplify :elim_and false :blast_distinct false :local_ctx false :pull_cheap_ite false) propagate-values (using-params simplify :elim_and true :blast_distinct true :local_ctx true :pull_cheap_ite true) simplify (using-params smt :smt.string_solver z3str3) fail-if-undecided))) \ No newline at end of file diff --git a/solvers/z3alpha/strats/qfslia.txt b/solvers/z3alpha/strats/qfslia.txt deleted file mode 100644 index 7baad8a..0000000 --- a/solvers/z3alpha/strats/qfslia.txt +++ /dev/null @@ -1 +0,0 @@ -(par-or (then (then cofactor-term-ite (using-params smt :random_seed 100)) fail-if-undecided) (then (then propagate-values solve-eqs factor elim-uncnstr (using-params smt :smt.string_solver z3str3)) fail-if-undecided) (then (then fm (using-params smt :random_seed 100)) fail-if-undecided) (then (using-params smt :random_seed 300) fail-if-undecided)) \ No newline at end of file diff --git a/solvers/z3alpha/z3alpha.json b/solvers/z3alpha/z3alpha.json deleted file mode 100644 index d31dc19..0000000 --- a/solvers/z3alpha/z3alpha.json +++ /dev/null @@ -1,34 +0,0 @@ -{ - "name": "Z3-alpha", - "contributors": [ - "John Lu", - "Paul Sarnighausen-Cahn", - "Jiahao Chen", - "Florin Manea", - "Vijay Ganesh" - ], - "contacts": ["John Lu "], - "archive": { - "url": "https://zenodo.org/records/15765918/files/submission25.zip?download=1" - }, - "website": "https://github.com/JohnLyu2/z3alpha", - "system_description": "https://drive.google.com/uc?export=download&id=17n4WbrukfKz7CxdVBXtSQjU_EYmwo1ZR", - "solver_type": "derived", - "command": ["./z3alpha.py"], - "seed": "33", - "participations": [ - { - "tracks": ["SingleQuery"], - "divisions": [ - "Arith", - "QF_Bitvec", - "QF_LinearIntArith", - "QF_LinearRealArith", - "QF_NonLinearIntArith", - "QF_NonLinearRealArith", - "QF_Strings" - ] - } - ], - "final" : true -} \ No newline at end of file diff --git a/solvers/z3alpha/z3alpha.py b/solvers/z3alpha/z3alpha.py deleted file mode 100755 index 0e73cd0..0000000 --- a/solvers/z3alpha/z3alpha.py +++ /dev/null @@ -1,113 +0,0 @@ -#!/usr/bin/env python3 - -import sys -from pathlib import Path -import subprocess -import json -import time -import os -import argparse - -def load_logic_strategies(): - script_path = Path(__file__).resolve() - z3alpha_dir = script_path.parent - strategies_path = z3alpha_dir / "strats" / "logic_strategies.json" - with open(strategies_path, 'r') as f: - return json.load(f) - -def read_smtlib_logic(smt2_str): - for line in smt2_str.split('\n'): - if line.startswith('(set-logic'): - return line.split()[1][:-1] - return None - -def rewrite_smt2_with_strat(smt2_str, strat): - new_smt2_str = "" - for line in smt2_str.split('\n'): - if "check-sat" in line: - new_smt2_str += f"(check-sat-using {strat})\n" - else: - new_smt2_str += line + "\n" - return new_smt2_str - -def debug_print(msg, debug=False): - if debug: - print(f"[DEBUG] {msg}", file=sys.stderr) - -def main(): - parser = argparse.ArgumentParser(description='Run Z3 with appropriate strategy based on SMT-LIB logic.') - parser.add_argument('smt2_path', help='Path to the SMT2 file') - parser.add_argument('--debug', action='store_true', help='Enable debug output') - args = parser.parse_args() - - script_path = Path(__file__).resolve() - z3alpha_dir = script_path.parent - - smt2_path = Path(args.smt2_path) - debug_print(f"Processing SMT2 file: {smt2_path}", args.debug) - - with open(smt2_path, 'r') as f: - smt2_str = f.read() - - solver_path = z3alpha_dir / "z3bin" / "z3" - debug_print(f"Using solver: {solver_path}", args.debug) - - logic = read_smtlib_logic(smt2_str) - debug_print(f"Detected logic: {logic}", args.debug) - - if logic: - logic_strategies = load_logic_strategies() - if logic in logic_strategies: - strat_filename = logic_strategies[logic] - strat_path = z3alpha_dir / "strats" / strat_filename - debug_print(f"Found strategy file: {strat_path}", args.debug) - - # check whether strat_path exists - if strat_path.exists(): - with open(strat_path, 'r') as f: - strat = f.read() - debug_print(f"Using strategy: {strat.strip()}", args.debug) - smt2_str = rewrite_smt2_with_strat(smt2_str, strat) - else: - debug_print(f"Strategy file not found: {strat_path}", args.debug) - else: - debug_print(f"No strategy found for logic: {logic}", args.debug) - - # write into a new smt2 file in tmp with unique name - timestamp = int(time.time() * 1000) # milliseconds - pid = os.getpid() - rw_smt2_path = Path(f"/tmp/{pid}_{timestamp}.smt2") - debug_print(f"Writing temporary file: {rw_smt2_path}", args.debug) - - with open(rw_smt2_path, 'w') as f: - f.write(smt2_str) - - try: - debug_print(f"Running Z3 with command: {solver_path} {rw_smt2_path}", args.debug) - result = subprocess.run( - [str(solver_path), str(rw_smt2_path)], - capture_output=True, - text=True, - check=True - ) - # Print stdout to stdout and stderr to stderr - if result.stdout: - sys.stdout.write(result.stdout) - if result.stderr: - sys.stderr.write(result.stderr) - except subprocess.CalledProcessError as e: - sys.stderr.write("error\n") - sys.exit(1) - except Exception as e: - sys.stderr.write("error\n") - sys.exit(1) - finally: - # Clean up the temporary file - try: - rw_smt2_path.unlink() - debug_print(f"Cleaned up temporary file: {rw_smt2_path}", args.debug) - except Exception: - pass # Ignore cleanup errors - -if __name__ == "__main__": - main() \ No newline at end of file diff --git a/solvers/z3alpha/z3bin/z3 b/solvers/z3alpha/z3bin/z3 deleted file mode 100755 index e6805b5..0000000 Binary files a/solvers/z3alpha/z3bin/z3 and /dev/null differ diff --git a/src/generator.py b/src/generator.py index 4a51f99..332f155 100644 --- a/src/generator.py +++ b/src/generator.py @@ -84,8 +84,6 @@ def __init__(self, mode : str = "pysmt", solver : str = "opensmt", logic : str = self.d = 0 self.num_of_vectors = 0 self.model = None - if self.solver == "dreal": - self.logic = "QF_NRA" def _new_gurobi_model(self): self.lp_problem = gp.Model("Circuit_Synthesis", env=quiet_gurobi_env()) diff --git a/src/solver_config.py b/src/solver_config.py new file mode 100644 index 0000000..8ce8372 --- /dev/null +++ b/src/solver_config.py @@ -0,0 +1,99 @@ +""" +@file: solver_config.py +@brief: loading of the SMT solver configuration (solvers.toml in the repository root, written by ./configure-solvers) +""" + +import os +import tomllib +from dataclasses import dataclass + +DEFAULT_PATH = os.path.normpath(os.path.join(os.path.dirname(__file__), "..", "solvers.toml")) +ENV_VARIABLE = "MILQ_SOLVER_CONFIG" +LOGICS = ("QF_LIA", "QF_LRA", "QF_NIA", "QF_NRA") +# values of -a that do not name an SMT solver +RESERVED_NAMES = ("portfolio", "gurobi", "cbc") +_KEYS = {"path", "args", "incremental_args", "logics", "portfolio"} + + +class SolverConfigError(ValueError): + """the solver configuration is missing or invalid, or names no usable solver""" + + +@dataclass(frozen=True) +class SolverConfig: + name: str + path: str + logics: tuple[str, ...] + args: tuple[str, ...] = () + incremental_args: tuple[str, ...] = () + portfolio: bool = True + + def command(self, incremental: bool = False) -> list[str]: + return [self.path, *self.args, *(self.incremental_args if incremental else ())] + + +def config_path(path: str | None = None) -> str: + # an explicit path wins over the environment variable, which wins over the file in the repository root + return path or os.environ.get(ENV_VARIABLE) or DEFAULT_PATH + + +def _resolve(executable: str, base_dir: str) -> str: + executable = os.path.expandvars(os.path.expanduser(executable)) + if os.sep not in executable: + return executable # a bare name is looked up on PATH when the solver starts + return os.path.normpath(os.path.join(base_dir, executable)) + + +def _string_list(where: str, key: str, value) -> tuple[str, ...]: + if not isinstance(value, list) or not all(isinstance(item, str) for item in value): + raise SolverConfigError(f"{where}: '{key}' must be a list of strings") + return tuple(value) + + +def load_solver_config(path: str | None = None) -> dict[str, SolverConfig]: + path = config_path(path) + try: + with open(path, "rb") as f: + data = tomllib.load(f) + except FileNotFoundError: + hint = f"; run {os.path.join(os.path.dirname(DEFAULT_PATH), 'configure-solvers')} to write it" if path == DEFAULT_PATH else "" + raise SolverConfigError(f"{path}: solver configuration not found{hint}") from None + except tomllib.TOMLDecodeError as e: + raise SolverConfigError(f"{path}: {e}") from None + + unknown = set(data) - {"solvers"} + if unknown: + raise SolverConfigError(f"{path}: unknown top-level key(s) {sorted(unknown)}, expected [solvers.NAME] tables") + tables = data.get("solvers", {}) + if not isinstance(tables, dict): + raise SolverConfigError(f"{path}: 'solvers' must contain [solvers.NAME] tables") + + base_dir = os.path.dirname(os.path.abspath(path)) + solvers = {} + for name, table in tables.items(): + where = f"{path}: [solvers.{name}]" + if name in RESERVED_NAMES: + raise SolverConfigError(f"{where}: '{name}' is reserved for -a {name}") + if not isinstance(table, dict): + raise SolverConfigError(f"{where}: must be a table") + unknown = set(table) - _KEYS + if unknown: + raise SolverConfigError(f"{where}: unknown key(s) {sorted(unknown)}, expected {sorted(_KEYS)}") + executable = table.get("path") + if not isinstance(executable, str) or not executable: + raise SolverConfigError(f"{where}: 'path' must be a non-empty string") + logics = _string_list(where, "logics", table.get("logics")) + if not logics or not set(logics) <= set(LOGICS): + raise SolverConfigError(f"{where}: 'logics' must be a non-empty list from {list(LOGICS)}") + portfolio = table.get("portfolio", True) + if not isinstance(portfolio, bool): + raise SolverConfigError(f"{where}: 'portfolio' must be true or false") + solvers[name] = SolverConfig(name=name, + path=_resolve(executable, base_dir), + logics=logics, + args=_string_list(where, "args", table.get("args", [])), + incremental_args=_string_list(where, "incremental_args", table.get("incremental_args", [])), + portfolio=portfolio) + if not solvers: + raise SolverConfigError(f"{path}: no solvers configured") + return solvers diff --git a/src/solver_detection.py b/src/solver_detection.py new file mode 100644 index 0000000..463050a --- /dev/null +++ b/src/solver_detection.py @@ -0,0 +1,204 @@ +""" +@file: solver_detection.py +@brief: the SMT solvers MILQ knows (how to find, call and download them), and generation of the solver + configuration (solvers.toml) from the solvers installed on the computer +""" + +import glob +import json +import os +import shutil +import subprocess +import tempfile +from dataclasses import dataclass, field + +from solver_config import SolverConfig + + +@dataclass(frozen=True) +class Release: + version: str + url: str + sha256: str # as GitHub reports it for the release asset + + +@dataclass(frozen=True) +class KnownSolver: + name: str + executables: tuple[str, ...] # names to look for, in order of preference; a download links the first + logics: tuple[str, ...] + args: tuple[str, ...] = () + incremental_args: tuple[str, ...] = () + globs: tuple[str, ...] = () # where else the solver is usually installed + comment: str = "" + releases: dict[str, Release] = field(default_factory=dict) # by platform, for configure-solvers --download + + +_YICES = "https://github.com/SRI-CSL/yices2/releases/download/yices-2.7.0/yices-2.7.0-" +_CVC5 = "https://github.com/cvc5/cvc5/releases/download/cvc5-1.3.1/cvc5-" +_OPENSMT = "https://github.com/usi-verification-and-security/opensmt/releases/download/v2.9.2/opensmt-" + +# the solvers MILQ knows how to call, in the order the portfolio lists them +KNOWN_SOLVERS = ( + # yices_smt2 is the name in the SMT-COMP builds + KnownSolver("yices2", ("yices-smt2", "yices_smt2"), ("QF_LIA", "QF_LRA", "QF_NIA", "QF_NRA"), + incremental_args=("--incremental",), + releases={ + "linux-x86_64": Release("2.7.0", _YICES + "x86_64-pc-linux-gnu-static-gmp.tar.gz", + "49566b6f817692820538df78fe406878400d79810631c9372b2495bc81d3e00a"), + "darwin-arm64": Release("2.7.0", _YICES + "arm-apple-darwin24.5.0-static-gmp.tar.gz", + "5682fedf13add7818e8d05796b9133e67844fce2bb72fd1ecc75dcb73167c7ac"), + "darwin-x86_64": Release("2.7.0", _YICES + "x86_64-apple-darwin21.6.0-static-gmp.tar.gz", + "dff40838ae5674abed2c08c383d702c1358ad64627c15799d2a15e67d1b4495a"), + }), + KnownSolver("cvc5", ("cvc5",), ("QF_LIA", "QF_NIA", "QF_NRA"), + args=("--produce-models",), incremental_args=("--incremental",), + releases={ + "linux-x86_64": Release("1.3.1", _CVC5 + "Linux-x86_64-static.zip", + "1a1cda20d2df4938fa4944a69f33ddc9172e319ece0eed0aa09c4d7abede3ed1"), + "linux-arm64": Release("1.3.1", _CVC5 + "Linux-arm64-static.zip", + "fe2b661834a82fd8830f7a757c340f0e20041fa41e19b038fa02ace0eaf1c6f2"), + "darwin-arm64": Release("1.3.1", _CVC5 + "macOS-arm64-static.zip", + "a0e7f5b03b1bc4284fbfff7cdfb08c704801701cf7ece83a13f8a505e7581215"), + "darwin-x86_64": Release("1.3.1", _CVC5 + "macOS-x86_64-static.zip", + "e7fe4af9491bd7c0db7591c0a483775735bd1a98b23933fd337a73ae39c10ff9"), + }), + KnownSolver("opensmt", ("opensmt",), ("QF_LIA", "QF_LRA"), + releases={ + "linux-x86_64": Release("2.9.2", _OPENSMT + "x64-linux-static.tar.bz2", + "be4767bf5d6c08bc7f4f49ae1480f2ae2ac8f38a277d0ec39d56badd974b84bd"), + "darwin-arm64": Release("2.9.2", _OPENSMT + "arm-osx.tar.bz2", + "6c8605db38e0f62ea040cffc670e65bd5f47e4fb65ecd65c6aaf4170cd19c51c"), + "darwin-x86_64": Release("2.9.2", _OPENSMT + "x64-osx.tar.bz2", + "b376e0339793f1ed5c546155f865de10fb39d1346d1788b57c80dfb538375ada"), + }), + KnownSolver("smtinterpol", ("smtinterpol",), ("QF_LIA", "QF_NIA"), + comment="no QF_NRA: SMTInterpol answers unknown to any nonlinear real term"), + KnownSolver("z3", ("z3",), ("QF_LIA", "QF_NIA", "QF_NRA"), incremental_args=("-in",)), + KnownSolver("dreal", ("dreal",), ("QF_NRA",), + args=("--precision", "1e-9", "--produce-models"), incremental_args=("--in",), + globs=("/opt/dreal/*/bin/dreal",), + comment="--precision is dReal's delta: it answers delta-sat when the formula holds up to that precision"), +) + +# a satisfiable formula for each logic, to check that a solver runs +_CHECKS = { + "QF_LIA": "(set-logic QF_LIA)\n(declare-fun x () Int)\n(assert (> x 1))\n(check-sat)\n(exit)\n", + "QF_LRA": "(set-logic QF_LRA)\n(declare-fun x () Real)\n(assert (> x 1.0))\n(check-sat)\n(exit)\n", + "QF_NIA": "(set-logic QF_NIA)\n(declare-fun x () Int)\n(assert (> (* x x) 1))\n(check-sat)\n(exit)\n", + "QF_NRA": "(set-logic QF_NRA)\n(declare-fun x () Real)\n(assert (> (* x x) 1.0))\n(check-sat)\n(exit)\n", +} + +HEADER = """\ +# SMT solvers available to `milq -s smt`, generated by ./configure-solvers from the solvers installed on this +# computer. Run it again after installing a solver, or edit this file. Each [solvers.NAME] table defines one +# solver; NAME is what `-a NAME` selects. The names `portfolio`, `gurobi` and `cbc` are reserved. +# +# path the executable. A relative path is relative to this file, a bare name (e.g. "z3") +# is looked up on PATH, and ~ and $VARIABLES are expanded. +# args arguments always passed to the solver (default: none) +# incremental_args extra arguments for the incremental modes, where MILQ sends the formula through +# stdin instead of a file (default: none) +# logics SMT-LIB logics the solver supports, from QF_LIA, QF_LRA, QF_NIA, QF_NRA. +# FiveTuple formulas are QF_LIA, Classic ones QF_NRA. +# portfolio whether `-a portfolio` runs this solver (default: true). The portfolio runs every +# such solver whose logics include the formula's logic. +# +# To use another file, pass `--solver-config FILE` or set the MILQ_SOLVER_CONFIG environment variable. +""" + + +def candidates(solver: KnownSolver, search_dirs: list[str] = (), path: str | None = None) -> list[str]: + # executables that may be the solver: from search_dirs (and their bin/), then PATH, then the usual places + found = [] + for directory in search_dirs: + for subdir in (directory, os.path.join(directory, "bin")): + for executable in solver.executables: + candidate = os.path.join(subdir, executable) + if os.path.isfile(candidate) and os.access(candidate, os.X_OK): + found.append(candidate) + for executable in solver.executables: + candidate = shutil.which(executable, path=path) + if candidate: + found.append(candidate) + for pattern in solver.globs: + # the newest version first + found.extend(sorted((p for p in glob.glob(pattern) if os.access(p, os.X_OK)), reverse=True)) + unique = [] + for candidate in map(os.path.abspath, found): + if candidate not in unique: + unique.append(candidate) + return unique + + +def check(solver: KnownSolver, executable: str, timeout: float = 30) -> str | None: + # None if the solver answers sat to a trivial formula, else why it doesn't work + with tempfile.TemporaryDirectory() as tmp: + formula = os.path.join(tmp, "check.smt2") + with open(formula, "w") as f: + f.write(_CHECKS[solver.logics[0]]) + try: + # in tmp: some solvers write files into the working directory + result = subprocess.run([executable, *solver.args, formula], cwd=tmp, capture_output=True, text=True, + timeout=timeout) + except OSError as e: + return str(e) + except subprocess.TimeoutExpired: + return f"no answer within {timeout:g} s" + # SMTInterpol may answer "success" to every command + words = [word for word in result.stdout.split() if word != "success"] + if words and words[0] in ("sat", "delta-sat"): + return None + output = (result.stdout + result.stderr).strip().splitlines() + return f"exit code {result.returncode}" + (f": {output[0]}" if output else ", no output") + + +@dataclass(frozen=True) +class Detection: + solver: KnownSolver + path: str | None # the working executable, None if there is none + rejected: tuple[tuple[str, str], ...] = () # (executable, why it doesn't work) + + def config(self) -> SolverConfig: + return SolverConfig(name=self.solver.name, path=self.path, logics=self.solver.logics, args=self.solver.args, + incremental_args=self.solver.incremental_args) + + +def detect(search_dirs: list[str] = (), path: str | None = None, timeout: float = 30) -> list[Detection]: + detections = [] + for solver in KNOWN_SOLVERS: + rejected = [] + working = None + for executable in candidates(solver, search_dirs, path): + problem = check(solver, executable, timeout) + if problem is None: + working = executable + break + rejected.append((executable, problem)) + detections.append(Detection(solver, working, tuple(rejected))) + return detections + + +def _toml_list(items) -> str: + # JSON strings are valid TOML basic strings + return "[" + ", ".join(json.dumps(item) for item in items) + "]" + + +def render(detections: list[Detection]) -> str: + tables = [] + for detection in detections: + solver = detection.solver + if detection.path is None: + continue + lines = [f"# {solver.comment}"] if solver.comment else [] + lines.append(f"[solvers.{solver.name}]") + lines.append(f"path = {json.dumps(detection.path)}") + if solver.args: + lines.append(f"args = {_toml_list(solver.args)}") + if solver.incremental_args: + lines.append(f"incremental_args = {_toml_list(solver.incremental_args)}") + lines.append(f"logics = {_toml_list(solver.logics)}") + tables.append("\n".join(lines) + "\n") + missing = [d.solver.name for d in detections if d.path is None] + footer = [f"# not found: {', '.join(missing)}\n"] if missing else [] + return "\n".join([HEADER, *tables, *footer]) diff --git a/src/solver_download.py b/src/solver_download.py new file mode 100644 index 0000000..128dc3c --- /dev/null +++ b/src/solver_download.py @@ -0,0 +1,100 @@ +""" +@file: solver_download.py +@brief: download of SMT solver release binaries (configure-solvers --download); the releases are listed + with the known solvers in solver_detection.py +""" + +import hashlib +import os +import platform +import shutil +import sys +import tarfile +import tempfile +import urllib.request +import zipfile + +import solver_detection +from solver_detection import KnownSolver, Release + +DEFAULT_DIR = os.path.normpath(os.path.join(os.path.dirname(__file__), "..", "solvers")) + + +class DownloadError(Exception): + """a solver could not be downloaded or unpacked""" + + +def platform_name() -> str: + # the keys of KnownSolver.releases, e.g. linux-x86_64 or darwin-arm64 + machine = platform.machine().lower() + machine = {"amd64": "x86_64", "aarch64": "arm64"}.get(machine, machine) + return f"{sys.platform}-{machine}" + + +def downloadable(platform_key: str | None = None) -> dict[str, tuple[KnownSolver, Release]]: + # the known solvers that have a release for the platform (default: this one), by name + platform_key = platform_key or platform_name() + return {solver.name: (solver, solver.releases[platform_key]) + for solver in solver_detection.KNOWN_SOLVERS if platform_key in solver.releases} + + +def bin_dir(directory: str = DEFAULT_DIR) -> str: + # where the downloaded executables are linked; configure-solvers looks there + return os.path.join(directory, "bin") + + +def _unpack(archive: str, destination: str) -> None: + if zipfile.is_zipfile(archive): + with zipfile.ZipFile(archive) as z: + z.extractall(destination) + else: + with tarfile.open(archive) as t: + if hasattr(tarfile, "data_filter"): # Python 3.11.4+ + t.extractall(destination, filter="data") + else: + t.extractall(destination) + + +def _find(directory: str, name: str) -> str | None: + for root, _, files in sorted(os.walk(directory)): + if name in files: + return os.path.join(root, name) + return None + + +def download(solver: KnownSolver, release: Release, directory: str = DEFAULT_DIR, force: bool = False) -> str: + # downloads and unpacks the release into directory/NAME-VERSION, links its executable into directory/bin, + # and returns the link; a release that is already there is kept unless force + executable_name = solver.executables[0] + target = os.path.join(directory, f"{solver.name}-{release.version}") + link = os.path.join(bin_dir(directory), executable_name) + if os.path.isdir(target) and not force and os.path.realpath(link).startswith(os.path.realpath(target) + os.sep): + return link + os.makedirs(directory, exist_ok=True) + with tempfile.TemporaryDirectory(dir=directory) as tmp: + archive = os.path.join(tmp, os.path.basename(release.url)) + try: + with urllib.request.urlopen(release.url, timeout=60) as response, open(archive, "wb") as f: + shutil.copyfileobj(response, f) + except OSError as e: + raise DownloadError(f"{release.url}: {e}") from None + with open(archive, "rb") as f: + digest = hashlib.file_digest(f, "sha256").hexdigest() + if digest != release.sha256: + raise DownloadError(f"{release.url}: sha256 {digest}, expected {release.sha256}") + unpacked = os.path.join(tmp, "unpacked") + try: + _unpack(archive, unpacked) + except (tarfile.TarError, zipfile.BadZipFile, OSError) as e: + raise DownloadError(f"{release.url}: cannot unpack: {e}") from None + if _find(unpacked, executable_name) is None: + raise DownloadError(f"{release.url}: no {executable_name} in the archive") + shutil.rmtree(target, ignore_errors=True) + os.replace(unpacked, target) + executable = _find(target, executable_name) + os.chmod(executable, os.stat(executable).st_mode | 0o111) # zip files keep no permissions + os.makedirs(bin_dir(directory), exist_ok=True) + if os.path.lexists(link): + os.remove(link) + os.symlink(os.path.relpath(executable, bin_dir(directory)), link) + return link diff --git a/src/synth.py b/src/synth.py index 9b9d9e4..52614b0 100644 --- a/src/synth.py +++ b/src/synth.py @@ -24,6 +24,7 @@ from pulp import * from gurobipy import GRB from solvers import PortfolioSMTSolver, SMTSolver, SolverError +from solver_config import LOGICS, SolverConfigError, config_path, load_solver_config import time import logging from timing import run, timed, times @@ -76,6 +77,7 @@ def __init__(self) -> None: self.ancillas = 0 self.vector_mode = None self.solvers = {} + self.solver_config = {} self.qubits_to_measure = None self.post_measurement = False # written to the synthesized circuit: (qubit, classical bit) and the classical declarations of the input @@ -102,44 +104,36 @@ def close(self) -> None: elif self.gen.mode == "pysmt" and hasattr(solver, "exit"): # pySMT's Solver or Portfolio solver.exit() + def _load_solver_config(self, solver: str, path: str | None) -> None: + self.solver_config = load_solver_config(path) + if solver not in [*self.solver_config, "portfolio"]: + raise SolverConfigError(f"Invalid solver: {solver}; {config_path(path)} configures " + f"{', '.join(self.solver_config)} (or use portfolio)") + def add_solvers(self, incremental_mode : bool = False) -> None: - # register custom solvers for pySMT portfolio solving - repo_root = os.path.normpath(os.path.join(os.path.dirname(__file__), "..")) - qf_lia = QF_LIA if self.gen.mode == "pysmt" else "QF_LIA" - qf_nra = QF_NRA if self.gen.mode == "pysmt" else "QF_NRA" - qf_nia = QF_NIA if self.gen.mode == "pysmt" else "QF_NIA" - qf_lra = QF_LRA if self.gen.mode == "pysmt" else "QF_LRA" - path = [os.path.join(repo_root, "solvers", "opensmt", "opensmt")] - self.add_one_solver(name="opensmt", args=path, logics=[qf_lia, qf_lra], incremental_mode=incremental_mode) - - path = ["z3"] - smtlib_flags = ["-in"] if incremental_mode else None - self.add_one_solver(name="z3", args=path, logics=[qf_lia, qf_nra, qf_nia], smtlib_flags=smtlib_flags, incremental_mode=incremental_mode) - - smtlib_flags = ["--incremental"] if incremental_mode else None - path = [os.path.join(repo_root, "solvers", "yices2", "yices_smt2")] - self.add_one_solver(name="yices2", args=path, logics=[qf_lia, qf_nra, qf_nia, qf_lra],smtlib_flags=smtlib_flags, incremental_mode=incremental_mode) - - # no QF_NRA: SMTInterpol answers unknown to any nonlinear term (even x*y = 1 with x = 2) - path = [os.path.join(repo_root, "solvers", "smtinterpol", "smtinterpol")] - self.add_one_solver(name="smtinterpol", args=path, logics=[qf_lia, qf_nia], incremental_mode=incremental_mode) - - smtlib_flags = ["--produce-models"] - smtlib_flags.append("--incremental") if incremental_mode else None - path = [os.path.join(repo_root, "solvers", "cvc5", "cvc5")] - self.add_one_solver(name="cvc5", args=path, logics=[qf_lia, qf_nra, qf_nia], smtlib_flags=smtlib_flags, incremental_mode=incremental_mode) - - smtlib_flags = ["--precision", "1e-9", "--produce-models"] - smtlib_flags.append("--in") if incremental_mode else None - path = ['/opt/dreal/4.21.06.2/bin/dreal'] - self.add_one_solver(name="dreal", args=path, logics=[qf_nra], smtlib_flags=smtlib_flags, incremental_mode=incremental_mode) + # register the solvers from the solver configuration (solvers.toml) + if self.gen.mode == "pysmt": + logics = {"QF_LIA": QF_LIA, "QF_LRA": QF_LRA, "QF_NIA": QF_NIA, "QF_NRA": QF_NRA} + else: + logics = {logic: logic for logic in LOGICS} + for name, config in self.solver_config.items(): + # pySMT drives its generic solvers through stdin by itself + args = config.command(incremental_mode and self.gen.mode != "pysmt") + self.add_one_solver(name=name, args=args, logics=[logics[logic] for logic in config.logics], + incremental_mode=incremental_mode) def add_one_solver(self, name: str, args: list[str], logics: list[str], smtlib_flags: list[str] = [], incremental_mode: bool = False) -> None: if name == "z3" and self.gen.mode == "pysmt": return if self.gen.mode == "pysmt": - env = get_env() - env.factory.add_generic_solver(name=name, args=args, logics=logics) + factory = get_env().factory + # pySMT keeps solvers registered for the whole process, e.g. by an earlier synthesis + if factory.is_generic_solver(name): + if factory.get_generic_solver_info(name) != (args, logics): + raise SolverConfigError(f"pySMT already has a solver {name} with another command or logics; " + "use one solver configuration per process") + return + factory.add_generic_solver(name=name, args=args, logics=logics) else: self.solvers[name] = SMTSolver(name, args, logics, smtlib_flags, incremental_mode) @@ -768,7 +762,7 @@ def set_initial_values(self): def synthesis(self, qasm_file=None, matrix=None, vectors=None, vector_pairs=None, solving="gurobi", solver=None, mode="incremental", output_qasm=None, complex_representation="FiveTuple", gate_set=None, q=None, d=None, fidelity_threshold=1.0, targets=1, ancillas=1, up_to_global_phase=False, basis="cb", approx=False, no_measurement=False, max_depth=None, pareto_timeout=10*60*60, - input_vectors=None) -> tuple[bool, Circuit, list[Vector]]: + input_vectors=None, solver_config=None) -> tuple[bool, Circuit, list[Vector]]: """ qasm_file -> file to synthesize vectors -> specify what set of input vectors to use (zero -> only |0>^n state, all -> all cbs, rus -> |0>, |1>, |+> on target, |0> on ancillas, @@ -777,6 +771,7 @@ def synthesis(self, qasm_file=None, matrix=None, vectors=None, vector_pairs=None input_vectors -> with vectors=custom and a qasm_file or matrix: the input states; the expected outputs are simulated from the circuit solving -> smt, pysmt, milp (these need a solver) or gurobi solver -> specify specific solver or portfolio of solvers + solver_config -> SMT solver configuration file (default: $MILQ_SOLVER_CONFIG, else solvers.toml in the repository root) mode -> specify solving method (basic -> create whole formula and get the best model, incremental -> incrementally generate the formula, binary, topdown, bottomup -> searches to optimize cost function) output_qasm -> file to write the output circuit to (and the last formula, with .smt2 or .lp); None writes no files complex_representation -> specify the complex representation ["FiveTuple", "Classic"] @@ -940,28 +935,27 @@ def synthesis(self, qasm_file=None, matrix=None, vectors=None, vector_pairs=None incremental_mode = False # set generator mode and solver if solving == "smt": - if solver not in ["z3", "cvc5", "yices2", "opensmt", "smtinterpol", "dreal", "portfolio"]: - raise ValueError(f"Invalid solver: {solver}") + self._load_solver_config(solver, solver_config) self.gen.mode = "smtlib" incremental_mode = True if (mode == "incremental" or mode == "pareto-incremental") and solver != "portfolio" else False self.add_solvers(incremental_mode=incremental_mode) - if solver == "dreal": - self.gen.logic = "QF_NRA" - + new_dict = {} for name, s in self.solvers.items(): - if self.gen.logic in s.logics: + if self.gen.logic in s.logics and self.solver_config[name].portfolio: new_dict[name] = s if solver == "portfolio": + if not new_dict: + raise SolverConfigError(f"{config_path(solver_config)}: no portfolio solver supports {self.gen.logic}") self.gen.solver = PortfolioSMTSolver(new_dict, logic=self.gen.logic) else: - if solver not in new_dict: - raise ValueError(f"{solver} does not support {self.gen.logic}") - self.gen.solver = new_dict[solver] + if self.gen.logic not in self.solvers[solver].logics: + raise SolverConfigError(f"{solver} does not support {self.gen.logic} (logics in {config_path(solver_config)}: " + f"{', '.join(self.solvers[solver].logics)})") + self.gen.solver = self.solvers[solver] elif solving == "pysmt": - if solver not in ["z3", "cvc5", "yices2", "opensmt", "smtinterpol", "dreal", "portfolio"]: - raise ValueError(f"Invalid solver: {solver}") + self._load_solver_config(solver, solver_config) self.gen.mode = "pysmt" incremental_mode = True if mode == "incremental" or mode == "pareto-incremental" else False self.add_solvers(incremental_mode=incremental_mode) @@ -971,6 +965,9 @@ def synthesis(self, qasm_file=None, matrix=None, vectors=None, vector_pairs=None else: log.warning("pySMT parser does not support some outputs from solvers that support NRA even though LIA works just fine.") solvers = ["z3", "cvc5", "yices2"] + # z3 is pySMT's own (z3-solver), the others have to be configured + solvers = [name for name in solvers if name == "z3" or (name in self.solver_config and self.solver_config[name].portfolio + and self.gen.logic in self.solver_config[name].logics)] self.gen.solver = Portfolio(solvers, logic=self.gen.logic, incremental=incremental_mode, generate_models=True) else: self.gen.solver = Solver(name=solver, logic=self.gen.logic, incremental=incremental_mode, generate_models=True) @@ -1406,7 +1403,6 @@ def solve_and_extract_circuit(self, formula_file="formula.smt2", output_qasm="ci """ formula_file: Path to the formula file output_qasm: Output filename for QASM circuit - solver: z3, z3alpha, cvc5, opensmt, smtinterpol, yices2, dreal (experimental) """ log.info("Solving formula") with timed("solving"): diff --git a/tests/conftest.py b/tests/conftest.py index b5922b3..2a24d92 100644 --- a/tests/conftest.py +++ b/tests/conftest.py @@ -1,5 +1,7 @@ import os +import shutil import sys +import tempfile import time import numpy as np @@ -12,9 +14,34 @@ from complex.classic import Complex from complex.fivetuple import FiveTuple from sim import Simulator +from solver_config import ENV_VARIABLE, load_solver_config +from solver_detection import detect, render +from solver_download import bin_dir OMEGA = np.exp(1j * np.pi / 4) +# the tests use the SMT solvers installed on this computer, through the configuration ./configure-solvers would +# write for them; the user's solvers.toml is neither read nor changed +_solver_config_dir = tempfile.mkdtemp(prefix="milq-solvers-") +SOLVER_CONFIG = os.path.join(_solver_config_dir, "solvers.toml") +_detections = detect([bin_dir()]) +with open(SOLVER_CONFIG, "w") as f: + f.write(render(_detections)) +SOLVERS = load_solver_config(SOLVER_CONFIG) if any(d.path for d in _detections) else {} + + +def pytest_configure(config): + # in os.environ, so that the milq processes started by the tests see it too + os.environ[ENV_VARIABLE] = SOLVER_CONFIG + + +def pytest_unconfigure(config): + shutil.rmtree(_solver_config_dir, ignore_errors=True) + + +def pytest_report_header(config): + return "SMT solvers: " + ", ".join(f"{name} ({solver.path})" for name, solver in SOLVERS.items()) + def to_complex(element, k, representation): # numeric value of a simulated amplitude diff --git a/tests/test_modes.py b/tests/test_modes.py index 955a704..ded9ed9 100644 --- a/tests/test_modes.py +++ b/tests/test_modes.py @@ -27,7 +27,9 @@ def test_fixed_depth_modes(workdir, mode, solving, solver, representation): np.testing.assert_allclose(unitary("out.qasm")[:, 0], unitary(GHZ2)[:, 0], atol=1e-9) -@pytest.mark.parametrize("solving, solver", [("smt", "yices2"), ("gurobi", "gurobi")]) +# z3: yices2 2.7.0 does not answer the depth-1 query of the incremental search within minutes (2.6.5 does in +# about a second, but not without the depth-0 query before it), while z3 and cvc5 take well under a second +@pytest.mark.parametrize("solving, solver", [("smt", "z3"), ("gurobi", "gurobi")]) def test_approximate_synthesis(workdir, solving, solver): res, circuit, _ = Synthesizer().synthesis(qasm_file=GHZ2, vectors="zero", solving=solving, solver=solver, mode="incremental", complex_representation="Classic", approx=True, diff --git a/tests/test_solver_config.py b/tests/test_solver_config.py new file mode 100644 index 0000000..548f791 --- /dev/null +++ b/tests/test_solver_config.py @@ -0,0 +1,214 @@ +"""The SMT solver configuration (solvers.toml) and how synthesis uses it.""" + +import multiprocessing +import os +import subprocess +import sys + +import pytest + +import solver_config +from conftest import BENCHMARKS, REPO_ROOT, SOLVER_CONFIG, SOLVERS +from solver_config import ENV_VARIABLE, SolverConfigError, load_solver_config +from synth import Synthesizer + +FAKE = os.path.join(os.path.dirname(__file__), "fake_solver.py") +YICES = SOLVERS["yices2"].path if "yices2" in SOLVERS else "yices-smt2" +GHZ2 = os.path.join(BENCHMARKS, "ghz/2.qasm") + + +def write_config(path, text): + path.write_text(text) + return str(path) + + +@pytest.fixture(autouse=True) +def default_config(monkeypatch): + # without --solver-config and the environment variable, the configuration of the tests (see conftest.py) + # stands in for solvers.toml in the repository root + monkeypatch.delenv(ENV_VARIABLE, raising=False) + monkeypatch.setattr(solver_config, "DEFAULT_PATH", SOLVER_CONFIG) + + +def test_default_config(): + config = load_solver_config() + assert config == SOLVERS + assert config["yices2"].command() == [YICES] + assert config["yices2"].command(incremental=True) == [YICES, "--incremental"] + assert all(solver.portfolio for solver in config.values()) + + +def test_paths(tmp_path, monkeypatch): + monkeypatch.setenv("HOME", "/home/someone") + monkeypatch.setenv("SOLVERS", "/opt/solvers") + path = write_config(tmp_path / "s.toml", """ +[solvers.relative] +path = "bin/solver" +logics = ["QF_LIA"] +[solvers.home] +path = "~/solver" +logics = ["QF_LIA"] +[solvers.variable] +path = "$SOLVERS/solver" +logics = ["QF_LIA"] +[solvers.bare] +path = "solver" +logics = ["QF_LIA"] +""") + config = load_solver_config(path) + assert config["relative"].path == str(tmp_path / "bin" / "solver") # relative to the configuration file + assert config["home"].path == "/home/someone/solver" + assert config["variable"].path == "/opt/solvers/solver" + assert config["bare"].path == "solver" + + +def test_file_selection(tmp_path, monkeypatch): + from_env = write_config(tmp_path / "env.toml", '[solvers.env]\npath = "a"\nlogics = ["QF_LIA"]\n') + explicit = write_config(tmp_path / "explicit.toml", '[solvers.explicit]\npath = "a"\nlogics = ["QF_LIA"]\n') + assert "yices2" in load_solver_config() + monkeypatch.setenv(ENV_VARIABLE, from_env) + assert list(load_solver_config()) == ["env"] + assert list(load_solver_config(explicit)) == ["explicit"] + + +@pytest.mark.parametrize("text, message", [ + ('[solvers.a]\nlogics = ["QF_LIA"]\n', "'path' must be a non-empty string"), + ('[solvers.a]\npath = "a"\n', "'logics' must be a list of strings"), + ('[solvers.a]\npath = "a"\nlogics = ["QF_BV"]\n', "'logics' must be a non-empty list"), + ('[solvers.a]\npath = "a"\nlogics = []\n', "'logics' must be a non-empty list"), + ('[solvers.a]\npath = "a"\nlogics = ["QF_LIA"]\nargs = "-v"\n', "'args' must be a list of strings"), + ('[solvers.a]\npath = "a"\nlogics = ["QF_LIA"]\nportfolio = "no"\n', "'portfolio' must be true or false"), + ('[solvers.a]\npath = "a"\nlogics = ["QF_LIA"]\nflags = []\n', "unknown key(s) ['flags']"), + ('[solvers.portfolio]\npath = "a"\nlogics = ["QF_LIA"]\n', "'portfolio' is reserved"), + ('[solver.a]\npath = "a"\n', "unknown top-level key(s) ['solver']"), + ('solvers = 1\n', "'solvers' must contain [solvers.NAME] tables"), + ('[solvers]\na = 1\n', "[solvers.a]: must be a table"), + ('', "no solvers configured"), + ('[solvers.a\n', "s.toml: "), # invalid TOML +]) +def test_invalid_config(tmp_path, text, message): + with pytest.raises(SolverConfigError) as error: + load_solver_config(write_config(tmp_path / "s.toml", text)) + assert message in str(error.value) + + +def test_missing_config(tmp_path): + with pytest.raises(SolverConfigError, match="solver configuration not found$"): + load_solver_config(str(tmp_path / "missing.toml")) + + +def test_missing_default_config_names_configure_solvers(tmp_path, monkeypatch): + monkeypatch.setattr(solver_config, "DEFAULT_PATH", str(tmp_path / "solvers.toml")) + with pytest.raises(SolverConfigError, match=f"not found; run {tmp_path}/configure-solvers to write it"): + load_solver_config() + + +def synthesize(solver, config=None, mode="incremental", representation="FiveTuple"): + return Synthesizer().synthesis(qasm_file=GHZ2, vectors="zero", solving="smt", solver=solver, mode=mode, + complex_representation=representation, output_qasm="out.qasm", solver_config=config) + + +@pytest.mark.parametrize("mode", ["incremental", "basic"]) +def test_synthesis_with_a_configured_solver(workdir, mode): + config = write_config(workdir / "s.toml", f""" +[solvers.my-yices] +path = "{YICES}" +incremental_args = ["--incremental"] +logics = ["QF_LIA"] +""") + res, circuit, _ = synthesize("my-yices", config, mode=mode) + assert res + assert circuit.gate_count() == 2 + + +def test_portfolio_skips_excluded_solvers(workdir): + config = write_config(workdir / "s.toml", f""" +[solvers.yices2] +path = "{YICES}" +logics = ["QF_LIA"] + +[solvers.excluded] +path = "{sys.executable}" +args = ["{FAKE}", "unsat", "0"] +logics = ["QF_LIA"] +portfolio = false + +[solvers.nra-only] +path = "{sys.executable}" +args = ["{FAKE}", "unsat", "0"] +logics = ["QF_NRA"] +""") + synthesizer = Synthesizer() + res, circuit, _ = synthesizer.synthesis(qasm_file=GHZ2, vectors="zero", solving="smt", solver="portfolio", mode="basic", + output_qasm="out.qasm", solver_config=config) + assert list(synthesizer.gen.solver.solvers) == ["yices2"] + assert res + assert circuit.gate_count() == 2 + + +def test_environment_variable_selects_config(workdir, monkeypatch): + monkeypatch.setenv(ENV_VARIABLE, write_config(workdir / "s.toml", f'[solvers.only]\npath = "{YICES}"\nlogics = ["QF_LIA"]\n')) + with pytest.raises(SolverConfigError, match="Invalid solver: yices2; .* configures only"): + synthesize("yices2") + assert synthesize("only", mode="basic")[0] + + +def test_solver_without_the_logic(workdir): + config = write_config(workdir / "s.toml", '[solvers.opensmt]\npath = "opensmt"\nlogics = ["QF_LIA", "QF_LRA"]\n') + with pytest.raises(SolverConfigError, match="opensmt does not support QF_NRA"): + synthesize("opensmt", config, representation="Classic") + + +def test_dreal_needs_classic(workdir): + # dReal supports only QF_NRA; forcing QF_NRA on a FiveTuple formula failed in the encoding + config = write_config(workdir / "s.toml", '[solvers.dreal]\npath = "dreal"\nlogics = ["QF_NRA"]\n') + with pytest.raises(SolverConfigError, match="dreal does not support QF_LIA"): + synthesize("dreal", config) + + +def test_portfolio_without_a_solver_for_the_logic(workdir): + config = write_config(workdir / "s.toml", f'[solvers.yices2]\npath = "{YICES}"\nlogics = ["QF_LIA"]\n') + with pytest.raises(SolverConfigError, match="no portfolio solver supports QF_NRA"): + synthesize("portfolio", config, representation="Classic") + + +# pySMT's portfolio creates its solvers in child processes, which see the generic solvers only when forked (#93) +PORTFOLIO_NOT_FORKED = pytest.mark.xfail(multiprocessing.get_start_method() != "fork", strict=True, + reason="#93: the configured solvers are missing in pySMT's portfolio processes") + + +@pytest.mark.parametrize("solver", ["yices2", pytest.param("portfolio", marks=PORTFOLIO_NOT_FORKED)]) +def test_pysmt_solving(workdir, solver): + # the pySMT backend registers the configured solvers as pySMT generic solvers + res, circuit, _ = Synthesizer().synthesis(qasm_file=GHZ2, vectors="zero", solving="pysmt", solver=solver, mode="basic", + output_qasm="out.qasm") + assert res + assert circuit.gate_count() == 2 + + +def test_pysmt_solving_rejects_a_changed_solver(workdir): + Synthesizer().synthesis(qasm_file=GHZ2, vectors="zero", solving="pysmt", solver="yices2", mode="basic") + config = write_config(workdir / "s.toml", f'[solvers.yices2]\npath = "{YICES}"\nargs = ["-v", "0"]\nlogics = ["QF_LIA"]\n') + with pytest.raises(SolverConfigError, match="pySMT already has a solver yices2"): + Synthesizer().synthesis(qasm_file=GHZ2, vectors="zero", solving="pysmt", solver="yices2", mode="basic", + solver_config=config) + + +def test_pysmt_solving_rejects_unknown_solver(workdir): + with pytest.raises(SolverConfigError, match="Invalid solver: yices"): + Synthesizer().synthesis(qasm_file=GHZ2, vectors="zero", solving="pysmt", solver="yices", mode="basic") + + +def test_cli_reports_config_errors(workdir): + result = subprocess.run([sys.executable, os.path.join(REPO_ROOT, "milq"), "-s", "smt", "-a", "yices", GHZ2], + capture_output=True, text=True, env={**os.environ, ENV_VARIABLE: SOLVER_CONFIG}) + assert result.returncode == 2 + assert f"milq: error: Invalid solver: yices; {SOLVER_CONFIG} configures" in result.stderr + + +def test_cli_solver_config_option(workdir): + config = write_config(workdir / "s.toml", f'[solvers.my-yices]\npath = "{YICES}"\nlogics = ["QF_LIA"]\n') + result = subprocess.run([sys.executable, os.path.join(REPO_ROOT, "milq"), "-v", "zero", "-s", "smt", "-m", "basic", + "-a", "my-yices", "--solver-config", config, GHZ2], capture_output=True, text=True) + assert result.returncode == 0, result.stderr + assert "synthesis successful" in result.stdout diff --git a/tests/test_solver_detection.py b/tests/test_solver_detection.py new file mode 100644 index 0000000..0902239 --- /dev/null +++ b/tests/test_solver_detection.py @@ -0,0 +1,164 @@ +"""Generation of the solver configuration from the installed solvers (configure-solvers).""" + +import hashlib +import io +import os +import subprocess +import sys +import tarfile + +import pytest + +from conftest import REPO_ROOT +from solver_config import load_solver_config +from solver_detection import KNOWN_SOLVERS, check, detect, render + +SOLVER = {solver.name: solver for solver in KNOWN_SOLVERS} +CONFIGURE = os.path.join(REPO_ROOT, "configure-solvers") + + +def fake_solver(directory, name, script="echo sat"): + # an executable that stands in for a solver + directory.mkdir(parents=True, exist_ok=True) + path = directory / name + path.write_text(f"#!/bin/sh\n{script}\n") + path.chmod(0o755) + return str(path) + + +def detected(detections): + return {d.solver.name: d for d in detections} + + +def test_detect_looks_in_search_dirs_then_path(tmp_path): + yices = fake_solver(tmp_path / "yices" / "bin", "yices-smt2") + cvc5 = fake_solver(tmp_path / "path", "cvc5") + found = detected(detect([str(tmp_path / "yices")], path=str(tmp_path / "path"))) + assert found["yices2"].path == yices # DIR/bin + assert found["cvc5"].path == cvc5 + assert found["opensmt"].path is None + assert found["z3"].path is None + + +def test_detect_skips_solvers_that_do_not_work(tmp_path): + broken = fake_solver(tmp_path / "search", "yices-smt2", "echo 'java: not found' >&2; exit 127") + working = fake_solver(tmp_path / "path", "yices_smt2") # the name in the SMT-COMP builds + found = detected(detect([str(tmp_path / "search")], path=str(tmp_path / "path"))) + assert found["yices2"].path == working + assert found["yices2"].rejected == ((broken, "exit code 127: java: not found"),) + + +def test_detect_finds_nothing(tmp_path): + found = detected(detect(path=str(tmp_path))) + assert all(found[name].path is None for name in ("yices2", "cvc5", "opensmt", "smtinterpol", "z3")) + + +@pytest.mark.parametrize("script, problem", [ + ("echo unsat", "exit code 0: unsat"), + ("exit 3", "exit code 3, no output"), + ("sleep 5", "no answer within 0.5 s"), +]) +def test_check_reports_why_a_solver_does_not_work(tmp_path, script, problem): + assert check(SOLVER["z3"], fake_solver(tmp_path, "z3", script), timeout=0.5) == problem + + +@pytest.mark.parametrize("script", ["echo sat", "echo success; echo success; echo sat", "echo 'delta-sat with delta = 0.001'"]) +def test_check_accepts_sat(tmp_path, script): + assert check(SOLVER["dreal"], fake_solver(tmp_path, "dreal", script)) is None + + +def test_check_passes_the_arguments_and_a_formula_of_the_first_logic(tmp_path): + arguments = tmp_path / "arguments" + solver = fake_solver(tmp_path, "dreal", f'echo "$@" > {arguments}; cat "$4" >> {arguments}; echo sat') + assert check(SOLVER["dreal"], solver) is None + text = arguments.read_text() + assert text.startswith("--precision 1e-9 --produce-models ") + assert "(set-logic QF_NRA)" in text + + +def test_render_round_trip(tmp_path): + fake_solver(tmp_path / "path", "cvc5") + fake_solver(tmp_path / "path", "smtinterpol") + detections = detect(path=str(tmp_path / "path")) + text = render(detections) + (tmp_path / "solvers.toml").write_text(text) + config = load_solver_config(str(tmp_path / "solvers.toml")) + assert config == {d.solver.name: d.config() for d in detections if d.path} + assert list(config) == ["cvc5", "smtinterpol"] + assert config["cvc5"].command(incremental=True) == [str(tmp_path / "path" / "cvc5"), "--produce-models", "--incremental"] + assert "# no QF_NRA: SMTInterpol" in text + assert "# not found: yices2, opensmt, z3" in text + + +def configure(*args, path): + # --download-dir: not the solvers the user downloaded + return subprocess.run([sys.executable, CONFIGURE, "--download-dir", str(path / "downloads"), *args], + capture_output=True, text=True, env={**os.environ, "PATH": str(path)}) + + +def test_configure_solvers_writes_the_config(tmp_path): + cvc5 = fake_solver(tmp_path / "path", "cvc5") + output = tmp_path / "solvers.toml" + result = configure("-o", str(output), path=tmp_path / "path") + assert result.returncode == 0, result.stderr + assert f"cvc5: {cvc5}\n" in result.stderr + assert "yices2: not found\n" in result.stderr + assert list(load_solver_config(str(output))) == ["cvc5"] + + # an existing file is kept without --force + result = configure("-o", str(output), path=tmp_path) + assert result.returncode == 2 + assert "exists, use --force" in result.stderr + assert list(load_solver_config(str(output))) == ["cvc5"] + + +def test_configure_solvers_to_stdout(tmp_path): + fake_solver(tmp_path / "path", "z3") + result = configure("-o", "-", "-s", str(tmp_path / "extra"), path=tmp_path / "path") + assert result.returncode == 0, result.stderr + assert "[solvers.z3]" in result.stdout + + +def test_configure_solvers_reports_broken_solvers(tmp_path): + broken = fake_solver(tmp_path / "path", "opensmt", "exit 1") + fake_solver(tmp_path / "path", "z3") + result = configure("-o", "-", path=tmp_path / "path") + assert f"opensmt: {broken} does not work (exit code 1, no output)\nopensmt: not found\n" in result.stderr + + +def test_configure_solvers_without_solvers(tmp_path): + result = configure("-o", str(tmp_path / "solvers.toml"), path=tmp_path) + assert result.returncode == 1 + assert "no SMT solver found" in result.stderr + assert not (tmp_path / "solvers.toml").exists() + + +def test_configure_solvers_downloads(tmp_path, monkeypatch): + # the known solvers replaced by a cvc5 whose release for this platform is a local archive, through a + # sitecustomize module + archive = tmp_path / "cvc5.tar.bz2" + with tarfile.open(archive, "w:bz2") as t: + data = b"#!/bin/sh\necho sat\n" + info = tarfile.TarInfo("cvc5/bin/cvc5") + info.size, info.mode = len(data), 0o755 + t.addfile(info, io.BytesIO(data)) + sha256 = hashlib.sha256(archive.read_bytes()).hexdigest() + site = tmp_path / "site" + site.mkdir() + (site / "sitecustomize.py").write_text(f""" +import sys +sys.path.insert(0, {os.path.join(REPO_ROOT, "src")!r}) +import dataclasses, solver_detection, solver_download +cvc5 = next(solver for solver in solver_detection.KNOWN_SOLVERS if solver.name == "cvc5") +release = solver_detection.Release("1.0", {archive.as_uri()!r}, {sha256!r}) +solver_detection.KNOWN_SOLVERS = (dataclasses.replace(cvc5, releases={{solver_download.platform_name(): release}}),) +""") + monkeypatch.setenv("PYTHONPATH", str(site)) + result = configure("-o", "-", "--download", path=tmp_path) + assert result.returncode == 0, result.stderr + assert f"cvc5: {tmp_path}/downloads/bin/cvc5\n" in result.stderr + assert f'path = "{tmp_path}/downloads/bin/cvc5"' in result.stdout + + result = configure("-o", "-", "--download", "yices2", path=tmp_path) + assert result.returncode == 2 + assert "no download of yices2 for this platform (available: cvc5)" in result.stderr diff --git a/tests/test_solver_download.py b/tests/test_solver_download.py new file mode 100644 index 0000000..cbe6cd2 --- /dev/null +++ b/tests/test_solver_download.py @@ -0,0 +1,97 @@ +"""Download of solver release binaries (configure-solvers --download), from local archives.""" + +import hashlib +import io +import os +import tarfile +import zipfile + +import pytest + +from solver_detection import KNOWN_SOLVERS, KnownSolver, Release +from solver_download import DownloadError, bin_dir, download, downloadable + +SOLVER = "#!/bin/sh\necho sat\n" + + +def tar_archive(path, members): + with tarfile.open(path, "w:bz2") as t: + for name, text in members.items(): + data = text.encode() + info = tarfile.TarInfo(name) + info.size, info.mode = len(data), 0o755 + t.addfile(info, io.BytesIO(data)) + return path + + +def zip_archive(path, members): + with zipfile.ZipFile(path, "w") as z: # without permissions, like the cvc5 release zips + for name, text in members.items(): + z.writestr(name, text) + return path + + +CVC5 = KnownSolver("cvc5", ("cvc5",), ("QF_LIA",)) + + +def release(archive, sha256=None): + return Release("1.0", archive.as_uri(), sha256 or hashlib.sha256(archive.read_bytes()).hexdigest()) + + +@pytest.mark.parametrize("archive", [tar_archive, zip_archive]) +def test_download_links_the_executable(tmp_path, archive): + path = archive(tmp_path / "cvc5.archive", {"cvc5-Linux/bin/cvc5": SOLVER, "cvc5-Linux/README": "readme"}) + link = download(CVC5, release(path), str(tmp_path / "solvers")) + assert link == os.path.join(bin_dir(str(tmp_path / "solvers")), "cvc5") + assert os.path.realpath(link) == str(tmp_path / "solvers" / "cvc5-1.0" / "cvc5-Linux" / "bin" / "cvc5") + assert os.access(link, os.X_OK) + assert not os.path.isabs(os.readlink(link)) # the directory can be moved + + +def test_download_keeps_an_existing_download(tmp_path): + path = tar_archive(tmp_path / "cvc5.tar.bz2", {"bin/cvc5": SOLVER}) + solvers = str(tmp_path / "solvers") + first = release(path) + download(CVC5, first, solvers) + path.unlink() # a second download would fail + assert download(CVC5, first, solvers) == os.path.join(bin_dir(solvers), "cvc5") + with pytest.raises(DownloadError): + download(CVC5, first, solvers, force=True) + + +def test_download_checks_the_sha256(tmp_path): + path = tar_archive(tmp_path / "cvc5.tar.bz2", {"bin/cvc5": SOLVER}) + with pytest.raises(DownloadError, match="sha256 .*, expected 0000"): + download(CVC5, release(path, sha256="0000"), str(tmp_path / "solvers")) + assert not (tmp_path / "solvers" / "cvc5-1.0").exists() + assert not (tmp_path / "solvers" / "bin").exists() + + +def test_download_needs_the_executable(tmp_path): + path = tar_archive(tmp_path / "cvc5.tar.bz2", {"bin/other": SOLVER}) + with pytest.raises(DownloadError, match="no cvc5 in the archive"): + download(CVC5, release(path), str(tmp_path / "solvers")) + + +def test_download_reports_unreachable_urls(tmp_path): + with pytest.raises(DownloadError, match="missing.zip"): + download(CVC5, Release("1.0", (tmp_path / "missing.zip").as_uri(), "0"), str(tmp_path / "solvers")) + + +def test_download_rejects_paths_outside_the_archive(tmp_path): + if not hasattr(tarfile, "data_filter"): + pytest.skip("tarfile filters need Python 3.11.4") + path = tar_archive(tmp_path / "cvc5.tar.bz2", {"../evil": "x", "bin/cvc5": SOLVER}) + with pytest.raises(DownloadError, match="cannot unpack"): + download(CVC5, release(path), str(tmp_path / "solvers")) + assert not (tmp_path / "evil").exists() + + +def test_releases_by_platform(): + assert list(downloadable("linux-x86_64")) == ["yices2", "cvc5", "opensmt"] + assert list(downloadable("linux-arm64")) == ["cvc5"] + assert downloadable("sunos-sparc") == {} + for solver in KNOWN_SOLVERS: + for r in solver.releases.values(): + assert r.url.startswith("https://github.com/") and len(r.sha256) == 64 + assert r.version in r.url diff --git a/tests/test_solver_processes.py b/tests/test_solver_processes.py index edbce2b..5ec2e49 100644 --- a/tests/test_solver_processes.py +++ b/tests/test_solver_processes.py @@ -12,7 +12,7 @@ from synth import Synthesizer FAKE = os.path.join(os.path.dirname(__file__), "fake_solver.py") -YICES = b"yices_smt2" +YICES = b"yices" # yices-smt2, or yices_smt2 in the SMT-COMP builds def incremental_fake(mode="sat"): diff --git a/tests/test_validation.py b/tests/test_validation.py index 20818f6..4e8c573 100644 --- a/tests/test_validation.py +++ b/tests/test_validation.py @@ -9,6 +9,7 @@ from complex.vector import Vector from conftest import BENCHMARKS from gates import GateSet +from solver_detection import KNOWN_SOLVERS, Detection, render from synth import Synthesizer GHZ = os.path.join(BENCHMARKS, "ghz/2.qasm") @@ -114,5 +115,9 @@ def test_custom_vectors_must_use_the_synthesis_representation(workdir): @pytest.mark.parametrize("solver", ["smtinterpol", "opensmt"]) def test_solver_without_nra_is_rejected_for_classic(workdir, solver): + # as configure-solvers configures it; the solver need not be installed, it is rejected before it runs + known = next(known for known in KNOWN_SOLVERS if known.name == solver) + config = workdir / "solvers.toml" + config.write_text(render([Detection(known, solver)])) with pytest.raises(ValueError, match=f"{solver} does not support QF_NRA"): - synthesize(solver=solver, complex_representation="Classic") + synthesize(solver=solver, complex_representation="Classic", solver_config=str(config))