Hi Shiyu,
On 18/02/2013 23:08, Shiyu Dong wrote:
Daniel has mentioned that he did something so that klee can be
separated from
STP(http://www.mail-archive.com/[email protected]/msg00030.html).
Yes, right now STP is not tightly integrated with KLEE anymore; a recent
patch by Hristina has removed a remaining dependency on STP arrays (see
http://llvm.org/viewvc/llvm-project?rev=166214&view=rev for details).
So integrating a new solver should be easy now.
So I want to ask in what language does klee represent the constraints
and passing them to the solver? Is it in still in readable language
such as SMT or CVC, or some lower level representation?
KLEE uses its own expression language internally (documented at
http://test.minormatter.com/~ddunbar/klee-doxygen/index.html and
http://klee.llvm.org/KQuery.html), and is constructing equivalent
STP expressions just before invoking STP.
Last question about the big picture of klee, in order to have a
better understanding about how klee deals with constraints, what
part of the code should I pay more attention to?
Look in lib/Expr and lib/Solver.
BTW, we currently have support for multiple constraint solvers
internally, and we might be able to make this extension available
relatively soon (email me directly for more details).
Best,
Cristian
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
