[klee-dev] `MustBeTrue` and `evaluate` methods in solver.

[Yuzhou Fang]

I occasionally found some comments for `evaluate` and `mustBeTrue` methods
in "include/klee/Solver/Solver.h".
The explanations are clear and make much sense.
For `evaluate`, the function will determine if the expression is
"expression is provably true, provably false or neither."
That says the `UNKNOWN` result indicates the expression could be either sat
or unsat, so for such a situation, klee needs to fork the state.

Please refer to the source code
https://github.com/klee/klee/blob/master/include/klee/Solver/Solver.h.


On Mon, Aug 26, 2024 at 4:50 AM Nguyễn Gia Phong <cnx at loang.net> wrote:

> On 2024-08-25 at 20:34-07:00, Yuzhou Fang wrote:
> > On 2024-08-25 at 22:23+09:00, Nguyễn Gia Phong wrote:
> > > SMT solver could give up on the constraint, hence the unknown result.
> >
> > I'm still quite confused by the situations when solvers will give up.
> > Does it mean the constraints are too hard for solvers to solve?
>
> Yes, and also the caller (KLEE) limits the resources (e.g. memory and time)
> in each evaluation because the goal is not solving a constraint precisely,
> but rather to explore many paths effectively.
>
> On 2024-08-25 at 20:34-07:00, Yuzhou Fang wrote:
> > it seems like `UNKNOWN` indicates the constraints could be
> > either sat or unsat, but I'm not sure about that (just kind of guess).
> > Could you share more thoughts on this? Thanks!
>
> I also understand it in such literal sense.  The SMT-LIB standard
> doesn't seem to specify anything further than "unknown" means "not
> known."
>
-------------- next part --------------
HTML attachment scrubbed and removed