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

[Andrew Santosa]

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 <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