3

z3 -p最新の (不安定な) Z3 で実行すると、モジュールごとにグループ化されたパラメーターのリストが表示されます。指示は次のとおりです。

To set a module parameter, use <module-name>.<parameter-name>=value
Example:  pp.decimal=true

一般に、これらの命令はどのように C API に変換されますか? 現在のドキュメントでは、「グローバル」構成を扱う API 呼び出しのセット( など) と、 などの型をZ3_set_param_value中心に構築された別のオブジェクト固有の呼び出しのセットがあるようです。Z3_paramsZ3_solver_set_params

Z3_set_param_value特に、任意のモジュールの任意のパラメーターをグローバルに設定するために使用できるかどうか疑問に思っていました。他の StackOverflow の回答Z3_paramsでは、グローバル パラメータに対してもオブジェクトの使用が宣伝されていますがtimeout(またはそうでしょうか?)、この API が構文:timeoutにどのようにマップされるかは明確ではありません。module.parameter=value

4

1 に答える 1

4

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 つが適用される場合に使用されます。

于 2014-07-03T12:50:14.653 に答える