[klee-dev] Some questions about SMT solvers

[Fabrizio Biondi]

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

> > 3. I prefer more comments in the code rather than separate documentation.
> I think it depends on the type of documentation.  I agree that in many
> cases, it makes sense to just add comments in the code, which can also
> be displayed in HTML form via doxygen.  However, I would welcome a
> tutorial-style separate document on how to add a new solver to the chain.

Ok, I'll try to write something down when I have some time.

Thank you,
  Fabrizio