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