z3 - Z3 のビットベクトル VS 整数

Question

固定小数点 phi(Real,Real, Int,Int,Int,Int) を使用して z3 を実装し、いくつかのルールを固定小数点に追加しました。と答えてくれましたが、Int 型を BitVector 型に変更すると、問題が解決せず、最終的に「タイムアウト」してしまいました。int の代わりに bitvector を使用すると高速になると思っていましたが、そうではありません。なぜですか?

Answer 1

DL_ENGINE=0 は、ボトムアップ データログ エンジンを呼び出します。有限テーブルを使用するため、テーブルのドメインでビットベクトルとブール値を処理します。
現在の 2 つのオプションは次のとおりです。

DL_ENGINE=0: use a Datalog engine for saturation. It works for finite domains.
DL_ENGINE=1: use a PDR engine.

http://rise4fun.com/z3py/tutorial/fixedpointsのチュートリアルでは、 これら 2 つのオプションを使用した例を示しています。

Answer 2

DL_ENGINE=1 を使用していると思います。これにより、現在純粋なブール変数と線形実数演算用にのみ調整されている PDR エンジンが呼び出されます (多くの場合、線形整数演算でも機能します)。