以下代码在 8 次迭代后终止(实际上应该迭代 14 次),为什么?
代码编码了一个线性混合自动机,它应该运行指定的迭代次数,但没有。
from z3 import *
x,t,t1,t2,x_next=Reals ('x t t1 t2 x_next')
location=[None]
location='off'
x=20
t1=0
s=Solver()
#set_option(precision=10)
k=14
for i in range(k):
print location
if location=='off':
s.add((10*x_next)>=(3*t1)-(3*t2)+(10*x),(10*x_next)<=(10*x)-(t2-t1),x_next>=18,(t2-t1)>0)
elif location=='on':
s.add(10*x_next>=(t2-t1)+(10*x),(5*x_next)<=(5*x)+(t2-t1),x_next<=22,(t2-t1)>0)
if [location=='off' and x_next<19] :
location='on'
elif [location=='on' and x_next>21]:
location='off'
if s.check()==unsat:
break
m=s.model()
#print s.check()
print i
print location
print s.model()
print "value of x_next"
print m[x_next].as_decimal(10)
x=m[x_next]
t1=m[t2]
最佳答案
程序停止,因为在迭代 8 后断言集不可满足,并且在循环中您有以下语句:
if s.check()==unsat:
break
在第一次迭代中添加断言:
10*x_next <= 200 - t2 - 0
在最后一次迭代中,您添加:
10*x_next >= t2 - Q(40,3) + 10*Q(56,3),
t2 - Q(40,3) > 0
其中,命令 Q(a, b)
用于创建有理数 a/b
。
即t1
是 40/3
和x
是 56/3
在迭代 8 时。
上述三种说法均不能成立。前两个意味着t2 <= 40/3
,最后一个 t2 > 40/3
.
顺便说一句,以下说法似乎不正确。也就是说,我不认为它反射(reflect)了你的意图。请注意,这是正交问题。
if [location=='off' and x_next<19] :
表达式x_next<19
计算结果不为 True
或False
。它创建 Z3(符号)表达式 x_next < 19
。我相信,您想评估这个表达式在模型中是否成立 m
。如果是这种情况,您应该写:
if location=='off' and is_true(m.evaluate(x_next<19)) :
命令m.evaluate(t)
计算表达式 t
在模型中m
。结果是 Z3 表达式。函数is_true(t)
返回True
如果t
Z3 表达式是否为真。
关于python - z3 python代码中的错误,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/11829579/