Looking for practical examples of SMT Z3 usecases (like DbC) and open source alternative to Z3? [closed]

Question

I have got interested in and looking for practical examples of SMT Z3 usage (like DbC) with code and open source alternatives to this tool. So, in fact, I am interested in similar Z3 formal solving tools, but:

• it must be open source
• provide both low-level (API) and high-level (Text scripting) interaction
• support SMT-LIB
• suitable(usable) in tools/written in/for languages as Java, python, ruby, Vala, and not Haskell
• has stable (usable in practice) tools based on it, like design by contract (DbC), static type verification, etc.

According to SMT-LIB homepage (see bit.ly bundle for details) the list of 2010 SMT solvers is: "Alt-Ergo, Barcelogic, Beaver, Boolector , CVC3, DPT, MathSAT, OpenSMT, SatEEn, Spear, STP, SWORD, UCLID, veriT, Yices, Z3."

Please give any feedback on using any of them in practice (code examples are the best)?

Finally, any information on comparison of it with GHC possibilities would be useful, but only in case there is an implementation example (not a language "feature").

More quick information on Z3 here http://bit.ly/bundles/ewiger/1

Answer 1

To the best of my knowledge, CVC3 comes closest to your requirements, in that it:

1. Has a feature set that is similar to Z3's.
2. Has a BSD-style license
3. Is the underlying solver for a number of existing projects.

CVC3 has bindings for C++ and Java, and probably other languages. In general, I think the API is far more difficult to use than the (textual) input language. This has the added benefit that, if you stick with the SMT-LIB2 language, you may be able to switch to a different tool later on if it becomes necessary. A large sample of examples is available on the SMT-LIB website.