[ondrik]

Removes the pySMT backend (synthesis(solving="pysmt")) and the PySMT requirement.

Why: the backend was reachable only from Python (the CLI's -s never offered it), and it had four open bugs. The SMT-LIB backend (-s smt) drives the same solvers through solvers.toml.

Closes #61, closes #90, closes #92, closes #93.

Changes

• src/generator.py: all mode == "pysmt" branches are removed. The default mode is now smtlib.
• src/synth.py:
  • solving accepts only smt, milp or gurobi; "pysmt" raises ValueError.
  • The generic-solver registration and the Portfolio/Solver setup are removed.
• src/parser.py: the branches that read pySMT model values (is_true(), constant_value()) are removed. The other backends give bool, int, float or str.
• src/complex/*.py: unused pySMT imports are removed.
• requirements.txt: PySMT is dropped. z3-solver stays, because its z3 binary is one of the solvers CI detects.

Tests

• Removed: the tests of the backend itself:
  • test_pysmt_* in test_solver_config.py, test_solver_errors.py and test_solver_processes.py
  • test_float_k_reaches_pysmt_as_an_integer
• Ported to the SMT-LIB generator with z3: three tests used pySMT's z3 only to check the encoding. They now use the new z3_generator() and z3_check() helpers in conftest.py:
  • the adjoint-pair constraints in test_generator.py
  • filter_model in test_pareto.py
  • Vector.to_real in test_simulator.py
• Local run with import pysmt blocked: 780 passed and 3 failed. The 3 failures are the cvc5-parametrized tests, which fail only because cvc5 isn't installed on that machine (Invalid solver: cvc5). CI downloads cvc5.

🤖 Generated with Claude Code

https://claude.ai/code/session_0177AhE9SXm3iJ1KP8GTSk6o

[codecov]

Codecov Report

❌ Patch coverage is 61.36364% with 17 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
src/generator.py	59.0%	8 Missing and 8 partials ⚠️
src/synth.py	80.0%	0 Missing and 1 partial ⚠️

📢 Thoughts on this report? Let us know!