[klee-dev] Add new solver like dreal to backend of klee

[Dan Liew]

Hi,

On 9 April 2017 at 04:21, Cx Qingyang <qingyangcx2015 at gmail.com> wrote:
> Thanks very much.Actually i need to add Z3 to the backend of klee-fp which
> is an extension of klee.I think the method is similar.But i still confused
> about the structure of klee,like the use of metaSMT.Z3 has been directly add
> to klee without metaSMT,why not use the metaSMT?

IIRC metaSMT doesn't support floating point constraints. I have not
confirmed this but I prefer to work with Z3 directly anyway. Z3 has a
very powerful API that allows customising many internal options and
allows custom tactics to be built.

I'm aware of klee-fp. However I should warn you (so that you don't
waste time doing this) that I (and another research institution) have
already extended KLEE with floating point support using Z3. We intend
to open source our implementations in the very near future.

> And is there a way to fast
> understand klee,besides directly reading the source code?Looking forward to
> your reply.

"Fast" really depends on what sort of person you are. I find walking
through an execution in a debugger like gdb very helpful.

Also. Please don't forget to CC the mailing list.

HTH,
Dan.