[klee-dev] Independent Solver

[eric.rizzi at huskers.unl.edu]

Sorry for the barrage of emails.


I have a question about how the IndependentSolver handles calls to computeInitialValues().  The other 3 functions for this phase of the Solver (computeValues, computeTruth, and computeValidity) do some type of independence analysis.  The goal, it seems, is to only pass forward the expressions that are directly related to the newest part of the state.


With computeInitialValues(), however, the entire query is forwarded without any analysis at all.  This seems to be suboptimal since every previous call only evaluated (and therefore cached) pieces of the query.  Therefore, by not breaking the query down, the cached information can not be easily utilized.


What I would instead expect is the solver splitting the query up into smaller factors.  It would then forward each of these pieces, one by one, to the next solver instance.  Once all the pieces had been evaluated, it could then recombine the answers from each in order to get a complete answer.  It seems that taking this approach would greatly increase the chances that the following stages (cache or cex) will hit, avoiding a SMT call.


My question is, is this intuition correct, and, if not, what am I missing.

Thanks,

Eric Rizzi
-------------- next part --------------
HTML attachment scrubbed and removed