QCNF2Z3 is a set of scripts that enable invoking Z3 on QDIMACS instances. The scripts do not do anything clever; it is really mainly just a mechanical translation. See more detailed description.
qcnf2z3.py --- qdimacs to smt2 conversion script (potentially negates the formula)
runz3 --- run on a qdimacs file and simulate a qbf solver output
example.qcnf ---
example.smt2
(C) 2012 Mikolas Janota
qcnf2z3 is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
qcnf2z3 is free for noncommercial use.
Last updated: Feb 04, 2013 21:07:48 PM |