1

たとえば、smtLib ファイル 'encoding.smt' があります。ここで、Ubuntu マシンで特定のタイムアウトとメモリ割り当てを使用して、z3 (スタンドアロン exe) でこのファイルを実行したいと考えています。お気に入り ：

$./z3 encoding.smt 240(sec) 6(GB)

Z3ダウンロードページからubuntu 32ビットzipファイルをダウンロードしました。私は今何をしなければなりませんか？「bin」フォルダーに z3 アプリケーションがあります。Ubuntu で Z3py スクリプトを書きたい場合、環境変数を変更する必要がありますか?

誰でも両方の手順を教えてもらえますか (指定されたタイムアウトとメモリを使用してスタンドアロン Z3 で.smtファイルを実行し、指定されたタイムアウトとメモリで z3py スクリプトから .smt ファイルを実行します)

ご提案ありがとうございます

4

1 に答える 1

0

これらのオプションは、それぞれ および と呼ばれtimeoutますmemory_max_size。Python インターフェイスでは、次のように設定できます。

set_option(timeout='60')
set_option(memory_max_size='1000')

(グローバルおよびモジュール) オプションのリストは、 を実行して取得できますz3 -p。これらのオプションは、コマンド ラインでも設定できます。

z3 encoding.smt2 timeout=60 memory_max_size=1000
于 2013-12-13T13:50:06.233 に答える