Home · Installation · Usage · Reference

Command-line reference

milq: synthesis

$ ./milq [options] <qasm_file>

Option	Values	Default	Description
qasm_file	path	(required)	Input circuit (format).
-v, --vectors	all, zero, jamiolkowski, rus	all	Input states the circuits must agree on (details).
-s, --solving	smt, gurobi, milp	gurobi	Solving method (details).
-a, --solver	a solver from the solver configuration (as written by configure-solvers: yices2, cvc5, opensmt, smtinterpol, z3, dreal, those installed), portfolio, gurobi, cbc	yices2 for -s smt, cbc for -s milp, gurobi for -s gurobi	Solver; SMT solvers and portfolio require -s smt, cbc requires -s milp, and -s gurobi takes only gurobi.
--solver-config	path	$MILQ_SOLVER_CONFIG, else solvers.toml in the repository root	Solver configuration file; requires -s smt.
-c, --complex_representation	FiveTuple, Classic	FiveTuple	Representation of amplitudes.
-m, --mode	incremental, basic, bottomup, topdown, binary, pareto-incremental	incremental	Search mode (details).
-d, --depth	integer ≥ 0	input gate count	Number of layers for the fixed-depth modes (basic, binary, topdown, bottomup); rejected in the incremental modes.
-u, --up_to_global_phase	flag	off	Allow a global phase difference.
-ap, --approx	flag	off	Approximate synthesis.
-f, --fidelity_threshold	number in [0, 1]	1.0	Minimum average fidelity; requires -ap.
-T, --targets	integer ≥ 1	1	Number of target qubits; requires -v rus.
-A, --ancillas	integer ≥ 0	1	Number of ancilla qubits; requires -v rus. Targets and ancillas together need at least as many qubits as the input circuit.
-nm, --no_measurement	flag	off	Ignore end-of-circuit measurements in the input.
--max-depth	integer ≥ 0	no limit	Incremental modes: give up (synthesis failed, exit status 3) when no circuit with at most this many gates exists; rejected in the other modes.
-pt, --pareto_timeout	seconds > 0	36000	Time limit; requires -m pareto-incremental.
--log	path (optional)	no log	Write a detailed log of the run to this file; --log alone writes synth.log.
--verbose	flag	off	Print the detailed log, with debug messages (e.g. every Gurobi model variable), to stdout, or to the --log file if given.
-o, --output_qasm	path	none (printed only)	Also write the synthesized circuit to this file.
-b, --basis	cb	cb	Basis of the encoding; only the computational basis is available.

An option given outside the mode it applies to (-d, --max-depth, -f, -pt, -T, -A) is rejected instead of ignored.

Exit status:

Status	Meaning
0	a circuit was synthesized
1	error: missing input file, license limit, … (milq: error: ... on stderr), or a solver failure (synthesis failed: ...)
2	invalid options (usage message on stderr), or an SMT solver that the solver configuration lacks or that does not support the formula’s logic (milq: error: ... on stderr)
3	no circuit found: unsat, or none within --max-depth or -pt (synthesis failed on stderr)

cli/simulator.py: simulation

Prints the input and output vectors of a circuit in MILQ’s own representations. It is useful to see what the synthesizer will be asked to match.

$ python3 cli/simulator.py -v zero -c Classic benchmarks/ghz/2.qasm
[(1 + 0j), (0 + 0j), (0 + 0j), (0 + 0j)], k=0
[(0.7071067811865476 + 0.0j), (0.0 + 0.0j), (0.0 + 0.0j), (0.7071067811865476 + 0.0j)], k=0
--------------------------------

Option	Values	Default	Description
qasm_file	path	(required)	Input circuit.
-v, --vectors	all, zero, jamiolkowski, rus, matrix	all	Input states to simulate, or matrix for the whole unitary.
-c, --complex_representation	FiveTuple, Classic	FiveTuple	Representation of amplitudes. FiveTuple vectors are printed as tuples with the exponent k.
-T, --targets	integer ≥ 1	1	Target qubits; requires -v rus.
-A, --ancillas	integer ≥ 0	1	Ancilla qubits; requires -v rus.
-m, --meas	0 or 1	0	Outcome assumed for measurements in the circuit.

Python API

The synthesizer can also be called from Python, with src/ on the module path:

import sys
sys.path.insert(0, "path/to/milq/src")
from synth import Synthesizer

synthesizer = Synthesizer()
ok, circuit, _ = synthesizer.synthesis(
    qasm_file="benchmarks/ghz/3.qasm",
    vectors="all",
    solving="smt", solver="yices2",
    mode="incremental",
    complex_representation="FiveTuple",
    output_qasm="ghz3_opt.qasm",
)
print(ok)                               # True
print(circuit)                          # the circuit as OpenQASM 3.0
print(synthesizer.times)                # time per phase of the last synthesis, in seconds

Without output_qasm, no files are written: the circuit and the last formula go to a temporary directory that is removed when synthesis() returns.

The synthesizer logs through the standard logging module (loggers synth, generator, parser) and writes no log file of its own. To see its progress, configure logging, e.g. logging.basicConfig(level=logging.INFO).

The keyword arguments mirror the command-line options (vectors ↔ -v, solving ↔ -s, solver ↔ -a, mode ↔ -m, complex_representation ↔ -c, d ↔ -d, up_to_global_phase ↔ -u, approx ↔ -ap, fidelity_threshold ↔ -f, targets ↔ -T, ancillas ↔ -A, no_measurement ↔ -nm, max_depth ↔ --max-depth, pareto_timeout ↔ -pt, solver_config ↔ --solver-config). Three more are available only from Python:

• gate_set=GateSet([...]) (from gates), or just a list of gate names, restricts the gates the synthesized circuit may use. It is used as it is, also with vectors="rus": only without a gate_set does RUS mode add Clifford+T and weight by T-count (call set_t_optimal() on your gate set for that). The caller’s object is not changed.

• vectors="custom" with input_vectors and a qasm_file (or matrix, which requires complex_representation="Classic") synthesizes a circuit that agrees with the input circuit only on the given input states. With a matrix, the fixed-depth modes need d, since a matrix has no gate count. The expected outputs are simulated from the circuit, and q, d, the gate set and the measured qubits are taken from it unless passed explicitly. Each input state is a Vector (from complex.vector) with 2^q amplitudes in the chosen representation:

  from complex.fivetuple import FiveTuple
  from complex.vector import Vector
  
  plus_zero = Vector(q=4, generator=None, element_representation=FiveTuple, k=1)  # |0>|+>, amplitudes / sqrt(2)^k
  plus_zero[0] = FiveTuple.one(None)
  plus_zero[1] = FiveTuple.one(None)
  ok, circuit, _ = Synthesizer().synthesis(qasm_file="benchmarks/ghz/2.qasm", vectors="custom",
                                           input_vectors=[plus_zero], solving="smt", solver="yices2")
  print(circuit)  # h q[0]; on |0>|+>, the cx of the Bell circuit is not needed
  

• vectors="custom" together with vector_pairs, q, d and gate_set gives the (input, output) state pairs directly instead of a circuit.

Create a new Synthesizer for every run.