[klee-dev] Add a new solver to klee

[Cristian Cadar]

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