python - 无法在 Z3py 中设置 pdr_use_farkas 选项

Question

当我尝试将定点引擎设置为 PDR 并尝试设置 pdr_use_farkas 选项时，我收到了 unknown_parameter 错误。

特别是，我在定点对象上使用以下选项：

fp.set(engine='1',pdr_use_farkas=True,unbound_compressor=False,compile_with_widening=True)

这会导致错误：

z3.types.Z3Exception: "unknown parameter ':pdr-use-farkas'"

使用 set_option 也无济于事。我试过了

set_option(dl_engine='1')
set_option(dl_pdr_use_farkas=True)

我得到“未知选项”。

我在哪里犯错？

我正在使用 Z3 4.3.1 64 位。

Answer 1

The parameter names have changed between versions as newer versions include a name-space mechanism for parameter names. The Python API has a method for listing parameter descriptions: For example:

fp = Fixedpoint() 
print fp.param_descrs() 

prints the set of available parameters (permalink: rise4fun.com/Z3Py/r32)