UFBVクエリでZ3を実行しています。現在、クエリには2つの呼び出しが含まれていますcheck-sat。push 1直後に置くとcheck-sat、Z3は30秒でクエリを解決します。私が何も入れていない場合、つまりそれらの間に何も入れずpush 1に2つの呼び出しがある場合、Z3は200秒でそれを解決します。面白い。特定の理由または単なる偶然の一致？check-satpush 1
1103 次
1 に答える
7
Z3 3.xには、戦術と戦術に基づく「戦略仕様言語」があります。それが進行中であるので、私はまだそれを「宣伝」していません。基本的な考え方は、このスライドデッキで説明されています。ロジックごとに異なる組み込み戦略があります。戦略は、「閉世界」仮定を使用する変換を適用する可能性があるため、通常、増分解決をサポートしていません。たとえば、0-1線形整数演算をSATにマップする変換があります。Z3は、ユーザーがインクリメンタルソルバー（複数のcheck-satコマンドやpushコマンドなどpop）を「望んでいる」ことを検出すると、汎用ソルバーに切り替わります。将来のバージョンでは、Z3の動作を制御するためのより多くの機能を提供する予定です。
ところで、2つの連続(check-sat) (check-sat)したコマンドがある場合、Z3は必ずしもインクリメンタルモードに入るとは限りません。assert2つの呼び出しの間にorpushコマンドがある場合にのみ入力されます。
ここで、クエリの形式が：(check-sat) <assertions> (check-sat)であり、2番目のクエリの形式が。であるとします(check-sat) <assertions> (push) (check-sat)。どちらの場合も、Z3は2番目にインクリメンタルモードになります(check-sat)。ただし、動作は同じではありません。インクリメンタルソルバーは、アサートされた数式を内部形式に「コンパイル」し、pushコマンドが実行された場合、その動作に影響を与えます。たとえば、ユーザースコープがない場合にのみ、バイナリ句のより効率的なエンコーディングを使用します。ユーザースコープとは、つまり、コマンドの数push-コマンドの数ですpop。これは、より効率的なエンコーディングで使用されるデータ構造に効率的な元に戻す/反転操作がないためです。
于 2012-02-03T17:06:34.177 に答える