On 18 April 2016 at 12:20, Fabrizio Biondi <fabrizio.bio...@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. _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
