[klee-dev] Add a new solver to klee

[Andrew Santosa]

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 <qingyangcx2015 at gmail.com> 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
klee-dev at imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev