Hi, On 11 June 2017 at 17:20, Awanish <[email protected]> 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. _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
