[ondrik]

The SMT solvers' paths and command-line arguments were hard-coded in Synthesizer.add_solvers, and the repository shipped about 100 MB of solver binaries in solvers/. Now:

• the solvers are configured in solvers.toml;
• ./configure-solvers writes that file for the solvers installed on the computer;
• ./configure-solvers --download first downloads some of them.

Neither the binaries nor solvers.toml are tracked any more.

Solver configuration (solvers.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 (formula sent through stdin)
logics = ["QF_LIA", "QF_NIA", "QF_NRA"]
# portfolio = false                   # keep -a portfolio from running it

• Loading: src/solver_config.py loads and validates the file. Unknown keys, wrong types, unknown logics, a missing file and invalid TOML each give a SolverConfigError that names the file and table. If the default file is missing, the error tells you to run configure-solvers.
• Which file is used: --solver-config FILE (CLI) or solver_config= (Python) wins over the MILQ_SOLVER_CONFIG environment variable, which wins over solvers.toml in the repository root.
• -a NAME accepts any configured solver, so adding a solver needs no code change. portfolio, gurobi and cbc are reserved names.
• Clearer errors: each of these now gives milq: error: ... and exit code 2:
  • an unknown solver;
  • a solver that doesn't support the formula's logic;
  • a portfolio with no solver for the logic.
• pySMT:
  • A second pySMT synthesis in the same process reuses the registered solver. If its command or logics differ, it raises a SolverConfigError instead.
  • The pySMT portfolio runs only the configured solvers from its list. Before, a solver that wasn't installed made it crash with "Cannot find solvers".
• dReal special case removed: selecting dreal used to switch FiveTuple formulas to QF_NRA, which made the encoding fail with "rescaling with wrong logic". Now -a dreal -c FiveTuple reports that dReal does not support QF_LIA.

./configure-solvers

• Search: it looks for yices-smt2/yices_smt2, cvc5, opensmt, smtinterpol, z3 and dreal, in this order of places:
  1. the -s DIR directories;
  2. the downloaded solvers;
  3. PATH;
  4. for dReal, also /opt/dreal/*/bin.
• Check: it keeps a solver only if it answers sat to a trivial formula of its first logic. For example, SMTInterpol without Java is reported and left out.
• Arguments and logics are those of the old solvers.toml. SMTInterpol has no QF_NRA, as decided in Don't register SMTInterpol for QF_NRA #100.
• Options:
  • -o FILE writes another file, and -o - prints to standard output;
  • an existing file is kept unless --force is given.
• Downloads: --download [yices2,cvc5,opensmt] first downloads release binaries from GitHub into solvers/ (gitignored):
  • versions: yices2 2.7.0, cvc5 1.3.1 and OpenSMT 2.9.2;
  • each archive is checked against the sha256 GitHub publishes for it, and its executable is linked into solvers/bin;
  • platforms: Linux x86-64 and macOS; on Linux arm64 only cvc5 is available;
  • a solver that is already downloaded is kept;
  • SMTInterpol and dReal have no release binaries to download.

Tests and CI

• Tests: the tests generate their own configuration the same way, from the solvers that are installed and downloaded. They pass it through MILQ_SOLVER_CONFIG, so they don't depend on the user's solvers.toml.
• New test files:
  • tests/test_solver_config.py covers loading, file precedence, validation, custom solvers, the portfolio, pySMT and the CLI;
  • tests/test_solver_detection.py and tests/test_solver_download.py cover detection and downloads. They use fake solvers and local file:// archives, so they need no network.
• CI runs ./configure-solvers --download -o - before the tests, so it runs them with yices2, cvc5, OpenSMT and z3.

Docs

docs/installation.md has a new solver table with install links and a "Solver configuration" section covering configure-solvers and --download. The README, docs/reference.md and docs/index.md are updated too.

🤖 Generated with Claude Code

https://claude.ai/code/session_0177AhE9SXm3iJ1KP8GTSk6o

[codecov]

Codecov Report

❌ Patch coverage is 96.66667% with 9 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
src/solver_download.py	89.9%	5 Missing and 2 partials ⚠️
src/solver_detection.py	98.1%	1 Missing and 1 partial ⚠️

📢 Thoughts on this report? Let us know!

[jkhav]

I was also thinking about swapping everything to configs - we can even extend these configs to full synthesis configs (all milq.py arguments prepared in .toml), gate-set defining + presets, setting custom portfolio of solvers. One open question is whether it would be useful to somehow nest configs -- e.g. portfolio.toml denotes some solvers of the portfolio manually, and some other solvers are added by referring to another config (this would also be useful for the full synthesis configs, which can refer to a gate-set config, solver config etc.)

[ondrik]

I was also thinking about swapping everything to configs - we can even extend these configs to full synthesis configs (all milq.py arguments prepared in .toml), gate-set defining + presets, setting custom portfolio of solvers. One open question is whether it would be useful to somehow nest configs -- e.g. portfolio.toml denotes some solvers of the portfolio manually, and some other solvers are added by referring to another config (this would also be useful for the full synthesis configs, which can refer to a gate-set config, solver config etc.)

good point, I'm still vibe-coding the basic functionality, we can build on top of that - changed to draft PR for now