Suchen Sie nach praktischen Beispielen für SMT Z3 -Usecasen (wie DBC) und Open -Source -Alternative zu Z3? [abgeschlossen

Question

Ich habe mich für praktische Beispiele für die SMT Z3 -Nutzung (wie DBC) mit Code und Open -Source -Alternativen zu diesem Tool interessiert und nach SMT Z3 -Nutzung gesucht. Tatsächlich interessiere ich mich also für ähnliche Z3 -formale Lösungswerkzeuge, aber:

• Es muss Open Source sein
• Stellen Sie sowohl Low-Level- (API) als auch hochrangige Interaktion (Text Scripting) bereit
• Unterstützen Sie SMT-Lib
• Geeignet (nutzbar) in Tools/geschrieben in/für Sprachen als Java, Python, Ruby, Vala und nicht Haskell
• hat stabile (in der Praxis verwendbare) Tools basierend darauf, wie Design nach Vertrag (DBC), statische Typüberprüfung usw.

Laut SMT-Lib-Homepage (siehe Bit.ly-Bundle für Details) lautet die Liste der SMT Solver von 2010: "Alt-Engo, Barcelogic, Biber, Boolector, CVC3, DPT, Mathsat, OpenMT, Sateen, Spear, STP, Sword, Uclid, Verit, Yices, Z3. "

Bitte geben Sie Feedback zur Verwendung eines von ihnen in der Praxis (Code -Beispiele sind die besten)?

Schließlich wären alle Informationen zum Vergleich mit GHC -Möglichkeiten nützlich, aber nur für den Fall, dass es ein Implementierungsbeispiel gibt (keine Sprache "Funktion").

Weitere schnelle Informationen zu Z3 hier http://bit.ly/bundles/ewiger/1

Answer 1

Nach meinem besten Wissen kommt CVC3 Ihren Anforderungen am nächsten, da dies:

1. Hat ein Feature -Set, das den Z3 ähnelt.
2. Hat ein Lizenz im BSD-Stil
3. Ist der zugrunde liegende Löser für eine Reihe bestehender Projekte.

CVC3 hat Bindungen Für C ++ und Java und wahrscheinlich andere Sprachen. Im Allgemeinen denke ich, dass die API weitaus schwieriger ist als die (Text) Eingabesprache. Dies hat den zusätzlichen Vorteil, dass Sie, wenn Sie sich bei der SMT-LIB2-Sprache halten, möglicherweise später zu einem anderen Tool wechseln können, wenn dies erforderlich ist. Eine große Stichprobe von Beispielen ist auf dem verfügbar SMT-LIB-Website.

Answer 2

Sie haben nach OpenSource -Alternativen zu Z3 gefragt:

Entsprechend SMT-Wikipedia Bei 2011-08 haben wir:

Basierend auf diesen Maßnahmen scheint es, dass die lebendigsten, gut organisierten Projekte OpenMT, STP und CVC4 sind.

Ich überprüfe nur dieses Zeug - bisher scheinen alle drei vernünftig, plus älterer CVC -> Ich meine CVC3.