python中z3求解器的超时答案

【问题标题】：timeout for z3 solver in pythonpython中z3求解器的超时
【发布时间】：2015-02-05 07:23:53
【问题描述】：

我在为求解器设置超时时遇到问题：

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 不是其中的一部分。我看了一下this post，但问题不一样。据我了解，参数应该是可以接受的，只是在稳定版本中可能永远不会发生超时，但编译应该没有问题。

无论如何我安装了不稳定的分支，问题仍然存在。

【问题讨论】：

你能试试“soft_timeout”选项吗？计划将此选项重命名为“超时”，但这尚未完成，因为可能与其他选项发生冲突/不一致。

标签： z3 z3py

【解决方案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'

【讨论】：

根据stackoverflow.com/questions/60841582/timeout-for-z3-optimize，超时时无法得到最知名的解决方案。