Тайм-аут для решателя z3 в python

Question

У меня проблемы с установкой таймаута для моего решателя:

s = Solver()
encoding = parse_smt2_file("ex.smt2")
s.add(encoding)

s.set("timeout", 600)
solution = s.check()

но я получаю следующую ошибку

Traceback (most recent call last): 
File "/Users/X/Documents/encode.py", line 145, in parse_polyedra("file") 
File "/Users/X/Documents/encode.py", line 108, in parse_polyedra s.set("timeout",1) File "/Users/X/z3/build/z3.py", line 5765, in set Z3_solver_set_params(self.ctx.ref(), self.solver, p.params) 
File "/Users/X/z3/build/z3core.py", line 3969, in Z3_solver_set_params raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err)) 
Z3Exception: unknown parameter 'timeout'

Появляется список юридических параметров, но timeout не является частью этого. Я посмотрел на этот пост, но проблема не та. Насколько я понимаю, параметр должен быть принят, просто в стабильной версии таймаут может никогда не произойти, но не должно быть проблем для компиляции.

В любом случае я установил нестабильную ветку и проблема не исчезла.

Answer 1

Я смог использовать опцию тайм-аута (и это фактически тайм-ауты и возвращает самое известное решение в случае оптимизации) со следующими версиями:

Python 2.7.9 (default, Mar  1 2015, 12:57:24) 
[GCC 4.9.2] on linux2
Type "help", "copyright", "credits" or "license" for more information.
>>> import z3
>>> s = z3.Solver()
>>> s.set("timeout", 600)
>>> z3.get_version_string()
'4.4.2'