python中z3求解器的超时 [英] timeout for z3 solver in python
问题描述
我在为求解器设置超时时遇到问题:
s = Solver()编码 = parse_smt2_file("ex.smt2")s.add(编码)s.set("超时", 600)解决方案 = s.check()
但我收到以下错误
回溯(最近一次调用最后一次):文件/Users/X/Documents/encode.py",第 145 行,在 parse_polyedra("file")文件/Users/X/Documents/encode.py",第 108 行,在 parse_polyedra s.set("timeout",1) 文件/Users/X/z3/build/z3.py",第 5765 行,在集合中Z3_solver_set_params(self.ctx.ref(), self.solver, p.params)文件/Users/X/z3/build/z3core.py",第 3969 行,在 Z3_solver_set_params 中引发 Z3Exception(lib().Z3_get_error_msg_ex(a0, err))Z3Exception:未知参数超时"
出现合法参数列表,但 timeout
不是其中的一部分.我看了一下这篇文章,但问题不一样.据我了解,参数应该是可以接受的,只是稳定版可能不会超时,但是编译应该没有问题.
无论如何我安装了不稳定的分支并且问题仍然存在.
我能够使用以下版本的超时选项(它实际上超时,并在优化的情况下返回最著名的解决方案):
>
Python 2.7.9(默认,2015 年 3 月 1 日,12:57:24)[GCC 4.9.2] 在 linux2 上输入帮助"、版权"、信用"或许可"以获取更多信息.>>>进口z3>>>s = z3.Solver()>>>s.set("超时", 600)>>>z3.get_version_string()'4.4.2'
I have problems setting a timeout for my solver:
s = Solver()
encoding = parse_smt2_file("ex.smt2")
s.add(encoding)
s.set("timeout", 600)
solution = s.check()
but I get the following error
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'
A list of legal parameters appears, but timeout
is not part of it. I took a look to this post, but the problem is not the same. As far as I understand, the parameter should be accepted, it is just that in the stable version the timeout may never happens, but there should not be problems to compile.
Anyway I installed the unstable branch and the problem persist.
I was able to use the timeout option (and it actually timeouts, and returns the best known solution in the case of optimization) with the following versions:
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'
这篇关于python中z3求解器的超时的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!