Hi, On 9 April 2017 at 04:21, Cx Qingyang <qingyangcx2...@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. _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev