[klee-dev] Some questions about SMT solvers

[Dan Liew]

On 18 April 2016 at 12:20, Fabrizio Biondi <fabrizio.biondi at inria.fr> wrote:
>> > 1. Your example is missing from your email, but I think validity in KLEE
>> > means that any valuation is a model (as in model theory). Whereas it
>> > seems your understanding of validity (some valuations are models) is
>> > more commonly known as satisfiability.
>> Indeed, that' correct.
>
> Thanks, it's clearer now. Sorry for the missing example, but it seems you guys got the question right anyway :).
>
>> > 2. I don't recall ever seeing KLEE extracts more information from the
>> > solver other than satisfiability decision. Perhaps others would know more.
>> KLEE does several constraint simplification and optimisation passes, but
>> does not extract any information from the solver other than
>> satisfiability/validity results and solutions/counterexamples.
>
> I see. Does this not mean that possibly the solver is asked to simplify the same constraints over and over? I am assuming the simplifications don't over- or underapproximate the constraints, of course.

This might be the case. However we don't have a good way right now of
communicating the solver's expression simplifications to KLEE right
now. We have only recently added Z3 support which can simplify
expressions for us on demand but use of this hasn't been investigated
yet.

In the case of Z3 simplification would be simpler if we used the
solver's expression language for constraints but currently we use
KLEE's own language for several reasons:

* Independence from a particular solver implementation. This allows to
support STP, Z3 and MetaSMT
* The semantics of KLEE's Expression language and the solver's
expression language aren't exactly the same. The reason for this is
that KLEE's expression language closely models LLVM's instructions.