2

私はいくつかの単純化の一般性をテストしています（主に：有向部分数量詞のインスタンス化）。したがって、単純化の有無にかかわらず、smtCompの「AUFLIA-p」セクションでベンチマークのコレクションを実行しました。副作用をできるだけ少なくするために、（ユーザー提供の）パターンなしでZ3を実行することに興味があります。

「AUFLIA-p」セクションでいくつかのベンチマークを調べましたが、なぜこのセクションのベンチマークにパターンが含まれているのか疑問に思います。パターンを無効にするオプションを使用して、このセクションでZ3を実行した可能性があります。最近、いくつかのベンチマークからパターンを削除したところ、劇的なパフォーマンスの低下が見られました。

質問：
「AUFLIA-p」セクションと「AUFLIA + p」セクションに違いはありますか？
（ユーザー提供の）パターンを無視するようにZ3に指示するにはどうすればよいですか？

よろしく、
Aboubakr Achraf El Ghazi

4

1 に答える 1

2

AUFLIA-pとAUFLIA+pの違いは、前者にはパターンが含まれていませんが、後者にはパターンが含まれていることです。ただし、SMTLIBには、AUFLIAと呼ばれるベンチマークのカテゴリが1つだけあります。（一部）これらのベンチマークには、SMTCOMP中にツールを実行する前に削除されるパターンが含まれています。たとえば、スクランブルされていないベンチマークとスクランブルされたベンチマークを比較します。前者にはパターンが含まれていますが、後者には含まれていません。

パターンの削除は、ベンチマークスクランブラーを介して行われると思います。

于 2012-09-11T14:59:55.480 に答える