Dies ist der Befehl z3, der beim kostenlosen Hosting-Anbieter OnWorks mit einer unserer zahlreichen kostenlosen Online-Workstations wie Ubuntu Online, Fedora Online, dem Windows-Online-Emulator oder dem MAC OS-Online-Emulator ausgeführt werden kann
PROGRAMM:
NAME/FUNKTION
z3 – ein hochmoderner Theorembeweis von Microsoft Research
ZUSAMMENFASSUNG
z3 [Optionen] [-file:]Datei
BESCHREIBUNG
Diese Handbuchseite dokumentiert kurz die z3 Befehl.
z3 Z3 ist ein hochmoderner Theorembeweis von Microsoft Research. Es kann verwendet werden
Überprüfen Sie die Erfüllbarkeit logischer Formeln über eine oder mehrere Theorien. Z3 bietet eine
überzeugende Ergänzung für Software-Analyse- und Verifizierungstools, da mehrere gängig sind
Software-Konstrukte werden direkt in unterstützte Theorien abgebildet.
Eingang Format
-smt Verwenden Sie den Parser für das SMT-Eingabeformat.
-smt2 Verwenden Sie den Parser für das SMT 2-Eingabeformat.
Herr Verwenden Sie einen Parser für das Datalog-Eingabeformat.
-dimacs
Verwenden Sie den Parser für das DIMACS-Eingabeformat.
-Log Verwenden Sie den Parser für das Z3-Protokolleingabeformat.
-in Lesen Sie die Formel aus der Standardeingabe.
Weitere Anwendungsbereiche
-h | -?
Druckt die Nutzungsinformationen.
-Ausführung
Gibt die Versionsnummer von Z3 aus.
-v:Ebene
Seien Sie ausführlich, wo ist der Ausführlichkeitsgrad.
-nw Warnmeldungen deaktivieren.
-p Zeigt globale Z3-Parameter (und Modulparameter) an.
-PD Zeigt globale Z3-Parameterbeschreibungen (und Modulbeschreibungen) an.
-pm:Name
Z3-Modul anzeigen Parameter.
-pp:Name
Z3-Parameterbeschreibung anzeigen, falls nicht angegeben, dann alle Modulnamen
sind aufgelistet.
-- Bei allen übrigen Argumenten wird davon ausgegangen, dass sie Teil des Eingabedateinamens sind. Diese Option
Ermöglicht Z3 das Lesen von Dateien mit seltsamen Namen wie: -foo.smt2.
Ressourcen
-T:Zeitüberschreitung
Legen Sie das Timeout (in Sekunden) fest.
-t:Zeitüberschreitung
Stellen Sie den Soft-Timeout ein (in Millisekunden). Es beendet nur die aktuelle Abfrage.
-Speicher: Megabyte
Legen Sie eine Grenze für den virtuellen Speicherverbrauch fest.
Ausgang
-st Statistiken anzeigen.
Parameter Einstellung
Globale und Modulparameter können in der Befehlszeile eingestellt werden. Verwenden Sie für den Abschluss „z3 -p“.
Liste der globalen und Modulparameter.
param_name=Wert
Zum Einstellen globaler Parameter.
module_name.param_name=Wert
Zum Einstellen von Modulparametern.
Verwenden Sie z3 online über die Dienste von onworks.net
