0

Q1: Z3 がさまざまなサブソルバーで費やした時間を照会することは可能ですか?

呼び出し(get-info :all-statistics)により、Z3 の全体的な実行時間が得られますが、個々のサブソルバーに分解したいと思います。

特に、算術関連のサブソルバーに費やされた時間、より正確には、統計grobnerとnonlinear-horner.


Q2:また、サブソルバーにタイムアウトを付けることは可能ですか?

チェックサットとサブソルバーごとにタイムアウトを定義して、Z3 がそのサブソルバーで費やすことができる時間を制限するようなものを想像できます。Z3 はn 個の異なるサブソルバーを繰り返し呼び出し、そのうちの 1 つの時間制限に達した場合は続行しますが、残りのn-1サブソルバーのみを使用します。

戦術のチュートリアルを読んで、これは実際には次のような方法で可能であるという印象を受けました。

(repeat
  (par-or
    (try-for <arithmetic-solvers> 500)
    <all-other-solvers>))

しかし、どのソルバーを使用すればよいかわかりませんでした。

4

1 に答える 1

1

Q1 の場合: いいえ、独自のタイマーを追加する必要があります。正確に何を数えるべきか、何を数えるべきでないかが明確ではないため、これは自明ではないと思います。

Q2: はい、独自のカスタム戦略/戦術を構築できます。par-or は並列を意味することに注意してください。つまり、提供されたタクティックを並列に実行しようとします。私たちが「ソルバー」と呼ぶものすべてに独自の戦術があるわけではないため、これには多少の調整が必要になる場合があります。このコンテキストでの「ソルバー」は、必ずしも「ソルバー」と呼ばれる Z3 C++ オブジェクトと同じではないことに注意してください。一部の「ソルバー」も SMT カーネルの不可欠な部分です。

于 2015-01-21T13:21:46.980 に答える