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 <qingyangcx2...@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@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev