[jkhav]

Replaces the custom Logger with the stdlib logging module and a small src/timing.py. CLI now decides where output goes: by default it prints only the result, the phase times and the circuit.

Fixes #86
Part of #87 (fixes F41; F65, the simulator stats, is still open)
Refs #76 (logging only: F14, F32)

What this resolves

#86, F34: every Synthesizer truncated ./synth.log

• Synthesizer() no longer opens a file. Only the CLI configures logging (logging.basicConfig in milq).
• The nested RUS recovery synthesizer can't wipe the main run's log any more, and no file handles leak.

#86, F75: unused verbosity, warnings never reached the console

• Warnings, e.g. Gurobi stopping with "cost not proven minimal", always reach the console.
• Logger.verbosity is replaced by a working --verbose flag (see below).
• Synthesizer.stats (a duplicate of the times) is removed.

#87, F41: wrong phase timings

• Incremental mode: the encoding clock restarts at every depth, so encoding no longer includes earlier solves.
• basic, binary, topdown and bottomup now record encoding time. They used to report 0.
• pareto-incremental: worker processes send back their solving and parsing times, which used to be lost, and the parent adds them up.
• encoding + solving + parsing + updating <= full now holds in every mode.

#76 (logging only, behaviour unchanged)

• F14: the log says Solver returned UNKNOWN or UNSAT instead of UNKNOWN/UNSAT.
• F14: a pySMT solver exception is logged as a warning. It's still treated as UNSAT.
• F32: the MILP model error is a logged warning instead of a print to std

Timings

• timing.timed(name) is a context manager that adds to a process-wide times dict. A phase that raises still counts.

• Each synthesis() stores its own times in synthesizer.times, with the solving and updating. This replaces synthesizer.logger.get_times().

• Nested syntheses are handled, so a RUS recovery synthesis can run in-process later:

  • Only the outermost run resets the totals. A nested run, in-process or ie outer run's totals.
  • Its synthesizer.times holds only its own share.

• synthesis(output_qasm=None) is the new default: no files are written. When no ouput_qasm is set, the formula etc. is written into tmp, which is then removed after the synthesis ends, and all the output is on stdout.

Flags	Log
none	no log; warnings on stderr
--log [PATH]	INFO log in the file (synth.log by default); warnings
--verbose	INFO and DEBUG log on stdout, before the result
--log --verbose	INFO and DEBUG log in the file

• -o is optional. Without it, the circuit is only printed.

• Gurobi: the license banner and "Set parameter" lines no longer go to stdout, for both -s gurobi and -s milp -a gurobi. They appear in the log when there is one.

• Full suite: 518 passed.

[codecov]

Codecov Report

❌ Patch coverage is 94.24460% with 8 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
src/generator.py	88.9%	2 Missing and 2 partials ⚠️
src/pareto.py	57.1%	3 Missing ⚠️
src/synth.py	98.6%	1 Missing ⚠️

📢 Thoughts on this report? Let us know!