Hi Jingde, For your question on tracking SolverImpl - you may want to look at the constructSolverChain function. KLEE uses chain of solvers, so when a query is made, it is passed through the chain, not necessarily directly to the STP (although probably this can be set this way). This is why sometimes some of the interface functions are defined in more than one place. For example, one of "solvers" in the chain can do logging of queries that go to STP.
Hope that helps, Tomek On 19/11/13 13:56, Paul Marinescu wrote: > You're probably looking for TimingSolver::getInitialValues > > Paul > > On 19/11/13 04:40, jingde liu wrote: >> Hi, >> I want to seed a solution to evaluate the constraints of an >> ExecutionState ignore the expr. In klee, evaluate(ExecutionState, expr, >> Validity) evaluates the result of the expr (constraints--> expr), but >> now I only care about the satisfiability of the constraints. Another >> problem I faced is that I don't know how to track into the functions of >> SolverImpl, when I track the program it stop at the virtual declaration. >> >> Cheers, >> Jingde >> >> >> _______________________________________________ >> 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
