これは、Ubuntu Online、Fedora Online、Windows オンライン エミュレーター、または MAC OS オンライン エミュレーターなどの複数の無料オンライン ワークステーションの 3 つを使用して、OnWorks 無料ホスティング プロバイダーで実行できるコマンド zXNUMX です。
プログラム：
NAME
z3 - Microsoft Research の最先端の定理証明ツール
SYNOPSIS
z3 [オプション] [-ファイル:]ファイル
DESCRIPTION
このマニュアルページでは、 z3
z3 Z3 は、Microsoft Research が提供する最先端の定理証明装置です。 使用できるのは、
3 つ以上の理論に対する論理式の充足可能性をチェックします。 ZXNUMX が提供するのは、
いくつかの一般的なため、ソフトウェア分析および検証ツールに非常に適しています。
ソフトウェアの構築は、サポートされている理論に直接マップされます。
入力 形式でアーカイブしたプロジェクトを保存します．
-smt SMT 入力形式にはパーサーを使用します。
-smt2 SMT 2 入力形式のパーサーを使用します。
氏 データログ入力形式にはパーサーを使用します。
-ディマック
DIMACS 入力形式のパーサーを使用します。
-ログ Z3 ログ入力形式にはパーサーを使用します。
-に 標準入力から数式を読み取ります。
その他
-h | -?
使用状況情報を出力します。
-バージョン
Z3 のバージョン番号を出力します。
-v:レベル
冗長に、どこで冗長レベルです。
-nw 警告メッセージを無効にします。
-p Z3 グローバル (およびモジュール) パラメーターを表示します。
-pd Z3 グローバル (およびモジュール) パラメーターの説明を表示します。
-pm:名前
ディスプレイ Z3 モジュールパラメーター。
-pp:名前
場合は、Z3 パラメータの説明を表示します。 が提供されていない場合は、すべてのモジュール名
記載されています。
-- 残りの引数はすべて、入力ファイル名の一部であるとみなされます。 このオプション
Z3 は、-foo.smt2 などの奇妙な名前のファイルを読み取ることができます。
その他
-T:タイムアウト
タイムアウトを秒単位で設定します。
-t:タイムアウト
ソフトタイムアウトをミリ秒単位で設定します。 現在のクエリのみを強制終了します。
-メモリ:メガバイト
仮想メモリの消費量の制限を設定します。
出力
-st 統計を表示します。
設定
グローバルパラメータとモジュールパラメータはコマンドラインで設定できます。 完全に実行するには「z3 -p」を使用します。
グローバルパラメータとモジュールパラメータのリスト。
param_name=値
グローバルパラメータを設定します。
module_name.param_name=値
モジュールのパラメータを設定します。
onworks.net サービスを使用して z3 オンラインを使用する
