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. The script qcir-conv.py attempts to reverse-engineer QDIMACS to prenex QCIR or to the GhostQ format. The script qcir-to-gq.sh converts a QCIR file 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).
For formulas with free variables, 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.)