For a short overview of KLEE's solver architecture, you might also like
to refer to this paper:
https://srg.doc.ic.ac.uk/publications/klee-multisolver-cav-13.html
Best,
Cristian
On 10/06/17 04:40, Andrew Santosa wrote:
Dear Qingyang,
Perhaps you may want to first look the comments in SolverImpl.h. For this, you
can generate
the doxygen documentation in the following way:
make doxygen
The documentation for SolverImpl class should be here:
docs/doxygen/html/classklee_1_1SolverImpl.html
Regarding the variety of solver classes, perhaps others can explain it better,
but here is what I know. These are structured in a proxy chain, starting at the
top level with TimingSolver. Each level provides extra solver functionality and
acts as a proxy to the lower level, for example, TimingSolver provides solver
timeout functionality to its client, and acts as a proxy to a lower level
solver.
CachingSolver provides result caching functionality to its client to enhance
performance, and acts as a proxy to a lower level solver. Please refer to
constructSolverChain function in ConstructSolverChain.cpp to see how this chain
is built. At the bottom of this proxy chain is any one of the "core" solvers,
which
is either STPSolver, Z3Solver, or MetaSMTSolver, that interfaces with external
solvers
(check the -solver-backend option in klee -help). Perhaps what you want to do
is to
add another core solver class to interface with your external solver. You can
probably
use STPSolver, STPSolverImpl, Z3Solver, Z3SolverImpl as examples for this.
Best,
Andrew
On Friday, 9 June 2017, 10:11, Cx Qingyang <[email protected]> wrote:
Hi,
I want to add a new solver to klee,but i am confused about the structure of
klee.As i know computeInitialValues in SolverImpl.h is the method to solve the
constraints,but the other method like computeValidity computeTruth,i don't konw
the use of the methods.
And the true solver should be STP,but there are some other solver like
CachingSolver.cpp CexCachingSolver.cpp,i don't know the use of them.Is there a
paper introduce the structure of klee?Wish your
reply,thanks!_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
