Evaluate the constraints without expr

[jingde liu]

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

[Paul Marinescu]

You're probably looking for TimingSolver::getInitialValues

Paul

Post by jingde liu
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

[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

Post by Paul Marinescu
You're probably looking for TimingSolver::getInitialValues
Paul

Post by jingde liu
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
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev