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

Closed. This question does not meet Stack Overflow guidelines. It is not currently accepting answers.

---

We don’t allow questions seeking recommendations开发者_如何学编程 for books, tools, software libraries, and more. You can edit the question so it can be answered with facts and citations.

Closed 8 years ago.

Improve this 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

---

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.

---

You've asked about opensource alternatives to Z3:

According to SMT-Wikipedia at 2011-08, we have:

Based on these measures, it appears that the most vibrant, well-organized projects are OpenSMT, STP and CVC4.

I'm just checking this stuff - so far, all three seems reasonable, plus older CVC -> I mean CVC3.