我正在使用可用的pythonz3api并使用相当标准的代码打印出SAT模型。在
我将省去无关的部分(Full Example Here),不管这是什么大局:
for bits in range(HIGH, LOW, -1):
var1, var2 ... varn = BitVecs('var1 var2 ... varn', bits)
s = Solver();
s.add(...)
...
if(s.check() == sat):
print "Sat, %d," %(bits),
m = s.model()
for d in m.decls():
print "%s," % (d.name()),
print " "
print "ASSIGN, %d," %(bits),
for d in m.decls():
print "%s," % (m[d]),
else:
print "NotSat, %d," %(bits),
print " "
break
print " "
我得到的结果是这样的(95%的时间):
^{pr2}$但这种情况是伪随机发生的(它只发生在特定的问题上,但每次都会在同一点重复出现):
Sat, HIGH, VAR1, VAR2, VAR3 ... VARn
ASSIGN, HIGH, VAL1, VAL2, VAL3 ... VALn
Sat, HIGH-1, VAR1, VAR2
此时,python继续无休止地运行。在
如有任何想法或建议,我们将不胜感激。在
你放在上面链接里的脚本没有问题。只是很难解决
bits=6
的实例。 这可能是不能满足的,但Z3将需要很长的时间来证明它。 我把我得到的输出附在帖子的末尾。 如果系统中的输出被截断,您可以尝试使用在每次迭代的最后。它将强制Python将结果刷新为标准输出。 当Z3不能在x毫秒内解决问题时,也可以使用超时来中断它。例如,要将超时设置为60秒,您应该在
^{pr2}$s = Solver()
之后包含以下命令当达到超时时,Z3将返回}。{cd4}可能是你决定暂停。
您还可以强制Z3显示详细的消息。你可以用它们来检查是不是死了。要启用详细消息,我们应该包括
^{3}$unknown
,而不是{Z3将显示许多信息,例如:
以下是您的脚本在我的机器上生成的输出:
相关问题 更多 >
编程相关推荐