[klee-dev] meaning of description of the getValue method

[Sumit Kumar]

Hi Andrew,

Thanks for the explanation. It has helped me understand better.
Also, thanks a lot for the correction. It is indeed in
include/klee/Solver.h. I will be more careful next time. :)

--
Thanks and Regards,
Sumit

On 24 April 2016 at 19:16, Andrew Santosa <santosa_1999 at yahoo.com> wrote:

> Hi Sumit,
>
> I think that comment and declaration are in include/klee/Solver.h and not
> Solver.cpp.
>
> My rough understanding is as follows. A Query object is a data structure
> containing
> a list of "constraints" and an "expression" (expr field). I think Query
> objects are typically
> used to query the solver for the validity of "constraints" =>
> "expression". However, in getValue(),
> in case "constraints" is satisfiable, the procedure uses a satisfying
> assignment of
> it to evaluate "expression" into a constant, which is the "result"
> argument of getValue(),
> and then getValue() returns "true".
>
> Best,
> Andrew
>
>
>
> On Sunday, 24 April 2016, 17:53, Sumit Kumar <sumit686215 at gmail.com>
> wrote:
>
>
> Hi All,
>
> Can anyone please explain me the meaning of following description of the
> getValue method described in Solver.cpp:
>
>     ///getValue - Compute one possible value for the given expression.
>     ///
>     /// \param [out] result - On success, a value for the expression in
> some
>     /// satisfying assignment.
>     ///
>     /// \return True on success.
>     bool getValue(const Query&, ref<ConstantExpr> &result);
>
> --
> Thanks and Regards,
> Sumit
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
>
>
-------------- next part --------------
HTML attachment scrubbed and removed