A second pySMT synthesis in the same process fails with SolverRedefinitionError #90

Bug: in one Python process, every pySMT synthesis after the first fails, even with a new Synthesizer for each run:

pysmt.exceptions.SolverRedefinitionError: Solver opensmt already defined

Reproduction (master at 1af733c, src/ on the module path):

from synth import Synthesizer

for _ in range(2):
    Synthesizer().synthesis(qasm_file="benchmarks/ghz/2.qasm", vectors="all", solving="pysmt", solver="z3",
                            mode="incremental", complex_representation="FiveTuple")

The first call returns the Bell circuit and the second raises. Basic mode, or yices2 after z3, fail the same way.

Cause: on every pySMT synthesis, Synthesizer.add_solvers() registers opensmt, yices2, smtinterpol, cvc5 and dReal as generic solvers in pySMT's global environment (add_one_solver). This happens even when the synthesis uses z3, which pySMT has built in. pySMT keeps registrations for the whole process and refuses to register a name it already has.

How much it matters: only the Python API offers pySMT (-s has no pysmt), but notebooks, benchmark loops and test suites run several syntheses in one process. The docs' advice to create a new Synthesizer for every run doesn't help, because the state is pySMT's, not the Synthesizer's.

Fix: draft PR #55 already handles this: it reuses a registered solver when its command and logics are the same, and raises SolverConfigError otherwise. One thing to keep in mind when fixing #61, though:

• The fix for pySMT incremental mode fails #61 passes the incremental flags to pySMT, so a solver's command differs between incremental and basic mode.
• Configure SMT solvers in solvers.toml, generated by configure-solvers #55's check would then make a basic synthesis after an incremental one (or the other way round) raise.
• Registering each command under its own name, or giving each synthesis a fresh pySMT environment, would avoid that.

Found while working on #89.