[klee-dev] Independent Solver

[Cristian Cadar]

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, eric.rizzi at huskers.unl.edu 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
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>