[klee-dev] Some questions about SMT solvers

[Fabrizio Biondi]

> > 1) I have noticed that computeValidity returns 0 (Unknown) a lot. This is
> > an
> > example:
> 
> Your example is missing from the e-mail.
> 
> > Since in the example above there is no constraint on word number 6 and the
> > query is on word number 6, I would expect the solver to return 1 (True),
> > meaning that there exists a model satisfying the query under the
> > constraints. Is my understanding of what 'validity' and 'invalid' mean
> > wrong?
> 
> Yes your understanding is incorrect here.
> 
> See the comments on the ``computeValidity(...)`` method [1].
> 
> You are confusing validity and satisfiability which are two different
> but related concepts. Validity is in general concerned with some
> formula being true for all possible variable substitutions whereas
> satisfiability is in general concerned with some formula being true
> for at least one variable substitution.
> 
> In KLEE a ``Query`` object is made up of a "query expression" and a
> set of constraints.
> 
> The ``computeValidity()`` method computes the value of
> 
> ∀ X : C(X) → Q(X)
> 
> which is either true (valid) or false (invalid). Here X is a set of
> free variables, C is the set of constraints conjuncted that may use
> the free variables and Q is the "query expression" which may use the
> free variables.
> 
> This is equivalent to
> 
> ¬ ∃ X : C(X) ∧ ¬ Q(X)

Thanks, this was very helpful. I understand now.

> > 2) I have noticed that KLEE does not simplify SMT statements much, I guess
> > this is because it expects the underlying SMT solver (STP or Z3) to take
> > care of the simplification. However, is the simplified version of the
> > constraints obtained from the solver and used in the rest of the symbolic
> > execution?
> 
> Ideally KLEE should simplify expressions as much as possible to try to
> avoid expressions from growing large as execution continues.
> We assume that the underlying SMT solver can do some simplification
> but currently for Z3 we are missing an opportunity to do further
> simplificiation
> because Z3 exposes an API (Z3_simplify()) which we aren't currently using.
> 
> See [2]. I think it would be useful to investigate doing this.
> 
> > Allow me to elaborate. I have some large set of constraints C, and I query
> > the solver for e.g. its validity. The solver internally simplifies C to a
> > smaller set C', computes its validity, and answers. Does KLEE henceforth
> > use
> > C' as its set of constraints for that trace, or does it use C?
> 
> KLEE continues to use C. Even so are you assuming that C' and C are
> equivalent or equisatisifiable?
> The SMT solver and KLEE are currently decoupled from each other so
> this is unlikely to change any time soon.
 
Yes, I am assuming they are equivalent or at least equisatisfiable. I will investigate a little into this. 
 
> [1] https://github.com/klee/klee/blob/master/include/klee/SolverImpl.h#L60
> [2] https://github.com/klee/klee/blob/master/lib/Solver/Z3Builder.cpp#L416
> 
> Hope that helps,
> Dan.

It does! Thank you again,
   Fabrizio