[klee-dev] Getting path formula in dimacs format

[Dan Liew]

Hi,

On 11 June 2017 at 17:20, Awanish <avanis1994 at gmail.com> wrote:
> Hi,
>
> I want to get/convert path constraint into dimacs/SAT format. Is there any
> way to convert in the desired form?

No such feature exists in KLEE itself but I think it should still be
possible to get queries in the DIMACS format.

I had a quick grep of the STP code and there is some that suggests
that it can print DIMACS but this not exposed by its API. So I'm
guessing that you need to collect the queries from KLEE in some other
format (i.e. CVC or SMT-LIBv2) and then use STP's `--output-CNF` flag
on those queries.

Alternatively it would be possible to have KLEE get the DIMACS
directly if some modifications were made to Z3. I also grepped through
Z3's codebase quickly and it does have the capability to print DIMACS
but this is not exposed via their C API.
If you ask the Z3 developers to expose the ability to get DIMACS as a
string in their C API then it would be possible to teach KLEE to call
this API.

However Z3 doesn't always invoke its SAT solver (it sometimes uses its
more general SMT solver) so there will be cases where DIMACS is simply
not available. My guess is the right way to do this is have a C
function that works on a `Z3_goal` and only gives output if the goal
is in CNF form already. If that's something you want to do then open
an issue on the Z3 issue tracker on GitHub stating very clearly what
you would like.

HTH,
Dan.