Playground

Run AutoQ in your browser. This is the command-line tool itself, compiled to WebAssembly: it reads the same .hsl and OpenQASM files and prints the same output. Everything runs on your machine; nothing is uploaded.

Loading AutoQ…

Output

Notes

ver checks the circuit against the postcondition and prints [OK] or [failed]. ex prints the set of states after the circuit. eq compares the circuits in a.qasm and b.qasm and prints [equal] if they implement the same unitary up to a global phase; it reads the qubit count from an OpenQASM 2.0 qreg declaration. eq has its own files and examples; ver and ex share theirs, and edits are kept when you switch.
A while loop names its invariant file in a trailing comment, as in the While loop example. Every file in the tabs is available to the run under its tab name.
The first run downloads the WebAssembly module (it includes the Z3 solver). Later runs reuse it.
Runs use a single thread and the memory your browser allows a page, so the larger benchmarks from the papers may be slow or run out of memory here. Use the native build for those.
One difference from the native build: WebAssembly has no floating-point traps, so an arithmetic error that stops the native tool with SIGFPE continues here.
The file formats are described in the .hsl and OpenQASM documentation.