> > 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 _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
