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
containinga list of "constraints" and an "expression" (expr field). I think
Query objects are typicallyused 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
