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 <[email protected]> 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 <[email protected]> > 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 > [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
