无法在 Z3py 中设置 pdr_use_farkas 选项答案

【问题标题】：Cannot set pdr_use_farkas option in Z3py无法在 Z3py 中设置 pdr_use_farkas 选项
【发布时间】：2013-09-06 11:05:13
【问题描述】：

当我尝试将定点引擎设置为 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 位。

【问题讨论】：

参数名称在版本之间发生了变化，因为较新的版本包括参数名称的命名空间机制。 Python API 有一个列出参数描述的方法：例如： fp = Fixedpoint() print fp.param_descrs() 打印可用参数集（永久链接：rise4fun.com/Z3Py/r32）

【解决方案1】：

版本之间的参数名称已更改，因为较新的版本包含用于参数名称的名称空间机制。 Python API 有一个列出参数描述的方法：例如：

fp = Fixedpoint() 
print fp.param_descrs()

打印一组可用参数（永久链接：rise4fun.com/Z3Py/r32）

【讨论】：