GhostQ is distributed under the terms of the GNU GPL v3.
Unfortunately, the source code is rather messy at the moment. The above versions of GhostQ no longer support non-prenex input (except the old 2010 version).
The GhostQ executable can be built by running make. There is a script battery02.sh that runs a few test inputs and compares to the expected output.
The GhostQ executable reads its input in a special GhostQ input format. There are scripts
qcir-conv.py that convert QDIMACS and prenex QCIR to the GhostQ format. The Gallery versions also have scripts
solver-*.sh that run the solver.
Converting a large, deeply-nested QCIR formula may fail if there is insufficient stack space. This can be fixed by increasing the stack limit before running the converter (e.g., by running "ulimit -S -s unlimited" in Bash).
The output of GhostQ is in a formula format that allows subformulas to be named and then referred to again by name. For example, in the below formula, the subformula "or(x1, x2)" is named "$1" and then referred to again by that name:
A parser for this format is in fmla.cpp. Recent versions of GhostQ also support an option "-write-qcir" to write output in the QCIR format. (An older draft of this format, limited to prenex only, is also available: qcir.pdf, qcir.tex.)