z3 - Z3 中的位向量 VS 整数

Question

我使用定点 phi(Real,Real, Int,Int,Int,Int) 实现了一个 z3，并在定点中添加了一些规则。它给了我一个答案，但是，当我将 Int 类型更改为 BitVector 类型时，它无法解决问题，最后“超时”。我曾认为使用 bitvector 而不是 int 会更快，但是，这是不正确的，为什么？

Answer 1

我猜你正在使用 DL_ENGINE=1。这会调用 PDR 引擎，该引擎目前仅适用于纯布尔变量和线性实数算术（通常也适用于线性整数算术）。

Answer 2

DL_ENGINE=0 调用自下而上的数据记录引擎。它使用有限表，因此它处理表域中的位向量和布尔值。
当前的两个选项是：

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上的教程 说明了使用这两个选项的示例。