Hi Eric,
Yes, you are right, that part could be optimised as you say. If you
have such a patch, I would be happy to review it and incorporate it into
the mainline.
Best,
Cristian
On 22/01/15 21:29, [email protected] wrote:
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
_______________________________________________
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
