Невозможно установить параметр pdr_use_farkas в Z3py

Question

Когда я пытаюсь установить механизм фиксированной точки в PDR, и я пытаюсь установить параметр pdr_use_farkas, я получаю сообщение об ошибке unknown_parameter.

В частности, я использую следующие параметры на объекте fixedpoint:

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 64bit.

Answer 1

Имена параметров были изменены между версиями, поскольку более новые версии включают механизм имен для имен параметров. Python API имеет метод для перечисления описания параметров: Например:

fp = Fixedpoint() 
print fp.param_descrs() 

печатает набор доступных параметров (Permalink: rise4fun.com/Z3Py/r32)