¿Busca ejemplos prácticos de Usecases SMT Z3 (como DBC) y alternativa de código abierto a Z3? [cerrado

Question

Me he interesado y buscando ejemplos prácticos de uso de SMT Z3 (como DBC) con código y alternativas de código abierto a esta herramienta. Entonces, de hecho, estoy interesado en herramientas de resolución formales Z3 similares, pero:

• Debe ser de código abierto
• Proporcionar interacción de bajo nivel (API) y de alto nivel (secuencia de comandos de texto)
• Apoyo a SMT-LIB
• adecuado (utilizable) en herramientas/escritos en/para idiomas como Java, Python, Ruby, Vala y no Haskell
• tiene herramientas estables (utilizables en la práctica) basadas en ella, como el diseño por contrato (DBC), verificación de tipo estático, etc.

Según la página de inicio SMT-LIB (ver bit.ly Bundle para más detalles) La lista de SMT Solvers 2010 es: "Alt-ergo, Barcelogic, Beaver, Boolector, CVC3, DPT, Mathsat, Opensmt, Sateen, Spear, STP, Sword, Uclid, Verit, Yices, Z3 ".

Por favor, otorgue algún comentario sobre el uso de cualquiera de ellos en la práctica (los ejemplos de código son los mejores).

Finalmente, cualquier información sobre la comparación de TI con posibilidades de GHC sería útil, pero solo en caso de que haya un ejemplo de implementación (no una "característica" de lenguaje).

Más información rápida sobre Z3 aquí http://bit.ly/bundles/ewiger/1

Answer 1

Que yo sepa, CVC3 se acerca más a sus requisitos, en eso:

1. Tiene un conjunto de características que es similar a Z3.
2. Tiene un Licencia de estilo BSD
3. Es el solucionador subyacente para varios proyectos existentes.

CVC3 tiene fijación para C ++ y Java, y probablemente otros idiomas. En general, creo que la API es mucho más difícil de usar que el (textual) idioma de entrada. Esto tiene el beneficio adicional de que, si se queda con el lenguaje SMT-LIB2, es posible que pueda cambiar a una herramienta diferente más adelante si es necesario. Una gran muestra de ejemplos está disponible en el Sitio web de SMT-LIB.

Answer 2

Has preguntado sobre las alternativas de Opensource a Z3:

De acuerdo a Smt-wikipedia En 2011-08, tenemos:

Según estas medidas, parece que los proyectos más vibrantes y bien organizados son OpenSMT, STP y CVC4.

Solo estoy revisando estas cosas, hasta ahora, las tres parecen razonables, además de CVC más antiguo -> Me refiero a CVC3.