Verschiedene Theorem-Beweiser

Z3 ist ein SMT-Löser, d.h. er kann SAT-Formeln bezüglich verschiedener Theorien lösen. Als Eingabesprache verwendet Z3 den SMT-LIB 2.0 standard.

• Installiert von https://github.com/Z3Prover/z3
• Aufruf: /opt/provers/z3/bin/z3
• Version: 4.4.2
• Dokumentation: Tutorial

• Installiert von http://cvc4.cs.nyu.edu/downloads/
• Aufruf: /opt/provers/cvc4/bin/cvc4
• Version: 1.4
• Dokumentation: http://cvc4.cs.nyu.edu/wiki/User_Manual
• Tutorials: http://church.cims.nyu.edu/wiki/Tutorials

• arbeitet auf einer Variante der Prädikatenlogik 1. Stufe mit polymorphen Typen
• bereitgestellte Theorien: Lineare Arithmetik auf rationalen und Integerzahlen, Arrays, Tupel, Records, induktive Datentypen, Bitvektoren
• Quantoren
• interaktives Text-basiertes Interface
• C++ API
• Modell-Generierung

• Entpacken des Archivs (Source tarball)
• libantlr3c installieren: über das bereitgestelle Skript contrib/get-antlr-3.4
• Konfigurieren ./configure –prefix <Zielpfad>
• Bauen mittels make und im Zielverzeichnis installieren make install

• Installiert von http://yices.csl.sri.com/cgi-bin/yices2-newnewlicense.cgi?file=yices-2.4.2-x86_64-unknown-linux-gnu-static-gmp.tar.gz
• Aufrufe:
  • /opt/provers/yices/bin/yices (Yices-Sprache)
  • /opt/provers/yices/bin/yices-smt (SMT-LIB 1.0)
  • /opt/provers/yices/bin/yices-smt2 (SMT-LIB 2.0)
  • /opt/provers/yices/bin/yices-sat (DIMACS-Format)
• Version: 2.4.2
• Dokumentation: http://yices.csl.sri.com/yices2-documentation.html (verschiedene Veröffentlichungen und das Yices manual)

• bereitgestellte Theorien: Uninterpretierte Funktionssymbole, lineare Arithmetik über reellen und Integerzahlen, Bitvektoren, skalare Typen und Tupel
• Solver für vier verschiedene Eingabeformate
  • Yices-Spezifikationssprache
  • SMT-LIB 1.0
  • SMT-LIB 2.0
  • DIMACS

• Archiv entpacken
• Installationsskript ./install-yices <Installationsverzeichnis> ausführen

• Installiert von http://mathsat.fbk.eu/download.html
• Aufruf: /opt/provers/mathsat/bin/mathsat
• Version: 5.3.10
• Dokumentation: http://mathsat.fbk.eu/documentation.html

• bereitgestellte Theorien: Uninterpretierte Funktionssymbole, lineare Arithmetik, Bitvektoren, Arrays
• Modell- und Beweis-Generierung
• inkrementelle Arbeitsweise

• Archiv entpacken
• Inhalte ins Zielverzeichnis kopieren