[klee-dev] Question about interface and constraint solving in klee

[Cristian Cadar]

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/klee-dev@imperial.ac.uk/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