milq exits 0 on failure and prints tracebacks for user errors #85

Medium. milq returns exit status 0 when synthesis fails, its option defaults conflict (-s smt with the default -a gurobi), only SolverError is caught so routine mistakes print tracebacks, and the -d help text is misleading.

Found in a code review of master at 66b41d9. Every item below was reproduced; the IDs (F1, G2, ...) are the review's.

Items: F39, F40, F79

F39

milq exits with status 0 when synthesis fails

Location: milq:61 · severity: medium

When synthesis returns res=False (no circuit within --max-depth, unsat in basic or other modes, Pareto timeout before any point), the CLI prints 'synthesis failed' on stdout and exits 0. Only SolverError exits with 1. Scripts and benchmark harnesses cannot tell success from failure by exit status, and a circuit.qasm from an earlier run may still be on disk.

Reproduction. for f in *.qasm; do ./milq $f --max-depth 5 && collect_result; done treats every failure as success and collects stale circuit.qasm files.

$ milq two.qasm -s smt -a yices2 --max-depth 1 (needs 2 gates) -> 'synthesis failed', exit=0.

Suggested fix. After printing 'synthesis failed' (preferably to stderr), call sys.exit(1) or a distinct code (e.g. 3 for 'no circuit within the bounds'), and document the exit codes.

F40

CLI option defaults conflict (-s smt with default -a gurobi), only SolverError is caught, and numeric options are not validated, so routine user errors print tracebacks

Location: milq:24 · severity: medium

-a defaults to 'gurobi' regardless of -s, so milq file.qasm -s smt always fails (likewise -s gurobi -a cbc, -s milp -a yices2). The validation in Synthesizer.synthesis raises ValueError, which milq does not catch (milq:56 catches only SolverError); missing input files (FileNotFoundError), -o in a missing directory, --max-depth 0, NotImplementedError, GurobiError (license limits) and RuntimeError from status checks all end in tracebacks. -d, -T and -A accept negative values (-m basic -d -1 -> IndexError on weights[0]). The -f help still says '(use with dreal solver)' while the docs say it is for -ap. PR #55 makes -a free-form but keeps default='gurobi' and still catches only SolverError/SolverConfigError.

Reproduction. A new user runs ./milq bench.qasm -s smt and gets a 15-line traceback ending in 'ValueError: Invalid solver: gurobi' instead of a usage message. milq nonexist.qasm -s smt -a yices2 prints a FileNotFoundError traceback.

$ milq two.qasm -s smt -> File src/synth.py, line 956, in synthesis: ValueError: Invalid solver: gurobi, exit=1.
$ milq nonexist.qasm -s smt -a yices2 -> FileNotFoundError traceback.
differential t.py 'h q[0];' mode=basic d=-1 -> IndexError: list index out of range.

Suggested fix. Default -a to None and pick per backend (smt -> yices2, milp -> cbc, gurobi -> gurobi); check -s/-a combinations after parse_args with parser.error() (exit 2). Wrap the call in main() with except (ValueError, OSError, RuntimeError, NotImplementedError, SolverError, GurobiError): print 'milq: error: ...' to stderr and exit non-zero. Use argparse type checks for non-negative integers, validate d >= 0 in synthesis(), and fix the -f help.

F79

CLI help for -d is misleading and --max-depth is silently ignored in fixed-depth modes

Location: milq:33 · severity: low

-d's help says 'number of allowed gates', but in the default incremental mode d only sizes preallocated states and does not bound the result (docs/reference.md correctly says 'number of layers for the fixed-depth modes'). Conversely, --max-depth is read only in the incremental branch (synth.py:1144), and basic/binary/topdown/bottomup accept it without effect or warning.

Reproduction. milq x.qasm -s smt -a yices2 -d 3 can return a 5-gate circuit; milq x.qasm -m basic --max-depth 2 encodes the input's full gate count.

milq:33 help='number of allowed gates'; synth.py:1138-1145: max_depth only used in the incremental/pareto branch.

Suggested fix. Change the help to 'number of layers for basic/binary/topdown/bottomup', and warn or reject --max-depth outside the incremental modes and -d inside them.