module/name パラメーターは、主に Z3 のコマンドライン バージョン用です。
グローバル パラメータは、最初に 1 回設定することを意図しており、その後のすべての呼び出しで有効になります。このパラメーター設定スキームを新しい戦略/目標/ソルバー/戦術/プローブ インターフェイスと共に導入しました。これは、戦術のさまざまな構成が必要であり、Z3_params オブジェクトが主にそのために使用されることを意図しているためです。たとえば、Z3_tactic_using_params は、Z3_params オブジェクトのオプションに基づいて別の戦術を再構成した新しい戦術を作成します。
ただし、API を使用してタクティックを作成する場合、モジュールはありません (作成したタクティックは Z3 内部の「パラメーター モジュール」には存在しません)。たとえば、戦略のチュートリアル (ここを参照) では、次のように戦術が構築され、適用されます。
(check-sat-using (then (using-params simplify :arith-lhs true :som true)
normalize-bounds
lia2pb
pb2bv
bit-blast
sat))
そのため、パラメーター "arith-lhs" と "som" が簡約器に対して有効になります。コマンドラインでは、同じオプションが「rewriter」モジュールにあります。つまり、コマンド ラインでrewriter.arith_lhs=true
有効にすると、simplifier が呼び出されるたびに有効になります。
タクティクスのリストとそれが認識するパラメーターのリストは、実行することで取得できます (Windows、Linux それぞれ)。
echo (help-tactic) | z3 -in -smt2
echo "(help-tactic)" | z3 -in -smt2
注意すべきもう 1 つのことは、Z3_params オブジェクトのパラメーターはまったくチェックされないことです。つまり、偽のパラメーター名を提供することが可能であり、Z3 は文句を言ったり警告を発したりせず、戦術は単にそのパラメーターを無視します。
パラメータ名の:
前にあるのは、SMT2 フォーマットの基礎である Lisp の残りです。たとえば、ここを参照してください: Common Lisp でコロンが変数に先行する理由。これらは、SMT2 入力言語を使用する場合にのみ必要です。したがって、SMT2 コマンド
(set-option :timeout 2000)
コマンドラインパラメータと同等であることを意味します
timeout=2000
質問ではタイムアウト パラメータが明示的に言及されているため、最近、OSX でのタイムアウト処理に問題が発生したため、最新の修正プログラムを入手する必要がある可能性があります。もちろん、まだ見つかっていないバグが他にもある可能性があります。
C API では、この関数Z3_global_param_set
を使用してグローバル パラメータを設定し、デフォルトのモジュール パラメータを設定します。これらのパラメーターはZ3_context
、後で作成されるすべてのオブジェクト (つまり、pp.decimal) によって共有され、組み込みの戦術の 1 つが適用される場合に使用されます。