[klee-dev] Evaluate the constraints without expr

[Tomasz Kuchta]

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
>> 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