无法在Z3py中设置pdr\u use\u farkas选项

Question

当我尝试将fixedpoint引擎设置为PDR，并尝试设置PDR\u use\u farkas选项时，我得到了一个未知的\u参数错误。你知道吗

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

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

这会导致错误：

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

使用setu选项也没有帮助。我试过了

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

我得到了“未知的选择”。你知道吗

我哪里出错了？你知道吗

我用的是Z3 4.3.1 64位。你知道吗

Answer 1

参数名在不同版本之间发生了变化，因为较新版本包含了参数名的名称空间机制。Python API有一个列出参数描述的方法：例如：

fp = Fixedpoint() 
print fp.param_descrs() 

打印可用参数集（permalink:rise4开心网/Z3Py/r32)你知道吗