Configure SMT solvers in solvers.toml, generated by configure-solvers

.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
 

.gitignore

@@ -11,3 +11,7 @@ excel/
 
 coverage.xml
 .coverage
+
+# written by ./configure-solvers
+/solvers.toml
+/solvers/

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,22 +69,23 @@ 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
 
 ```
 - 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)

codecov.yml

@@ -27,7 +27,6 @@ coverage:
 ignore:
   - "tests/**"
   - "benchmarks/**"
-  - "solvers/**"
 
 comment:
   layout: "condensed_header, diff, files"

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)

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

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.

docs/reference.md

@@ -17,7 +17,8 @@ $ ./milq [options] <qasm_file>
 | `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 2<sup>q</sup> amplitudes in the chosen representation: