python – Z3代码没有运行指定的迭代次数

2019年8月4日 187次阅读

此代码仅运行i = 4,但如果位置未初始化,则运行i = 19 ?????

 location = BoolVal(False)位置在此处初始化

from z3 import *
x,t,t1,t2,x_next=Reals ('x t t1 t2 x_next')
location,location_next=Bools('location location_next')

x=20
#t1=0
t=0
location=BoolVal(False)
#set_option(precision=10)
k=20


for   i in range(k):
  s=Solver()

  s.add(Or(And((10*x_next)>=(3*t1)-(3*t2)+(10*x),(10*x_next)<=(10*x)-(t2-t1),x_next>=18,(t2-t1)>0,Not(location_next)),
           And((10*x_next)>=(t2-t1)+(10*x),(5*x_next)<=(5*x)+(t2-t1),x_next<=22,(t2-t1)>0,location_next)),
            location_next==If(And(Not(location),x_next<19),True,If(And(location,x_next>21),False,location)))


  print i
  print s.check()
  if s.check()==unsat:
      break

  m=s.model()
  x=m[x_next]
  #t1=m[t2]


  print m[x_next].as_decimal(10)

最佳答案 简短的回答是：在命令s.add(…)中添加的公式在迭代4中是不可满足的.

在迭代4的开始,我们得到x是19并且location是False.

通过替换公式中的x和位置,我们得到：

[Or(And(10*x_next >= 3*t1 - 3*t2 + 190,
        10*x_next <= 190 - t2 + t1,
        x_next >= 18,
        t2 - t1 > 0,
        Not(location_next)),
    And(10*x_next >= t2 - t1 + 190,
        5*x_next <= 95 + t2 - t1,
        x_next <= 22,
        t2 - t1 > 0,
        location_next)),
 location_next ==
 If(And(Not(False), x_next < 19),
    True,
    If(And(False, x_next > 21), False, False))]

简化上述公式后,我们有：

[Or(And(10*x_next >= 190 + 3*t1 - 3*t2,
           10*x_next <= 190 - t2 + t1,
           x_next >= 18,
           t2  - t1 > 0,
           Not(location_next)),
       And(10*x_next >= 190 + t2 - t1,
           5*x_next <= 95 + t2 - t1,
           x_next <= 22,
           t2 - t1 > 0,
           location_next)),
    location_next == x_next < 19]

为了显示该公式的不可满足性,让我们考虑以下两种情况：location_next为True,或location_next为False.

> location_next为True.然后,x_next< 19也必须是真的.而且,Or的第一个参数是假的.因此,只有当我们可以使第二个参数为True时,公式才是可满足的.情况并非如此,因为以下内容不可满足： 10 * x_next> = 190 t2-t1,5 * x_next< = 95 t2-t1,x_next< 19 前两个不等式意味着x_next> = 19.
> location_next为False.然后x_next> = 19必须为True.通过类似的论证,只有当我们能够得到Or True的第一个参数时,公式才是可满足的.这也是不可能的,因为以下是不可满足的：

10 * x_next< = 190-t2 t1,t2-t1> 0,19< = x_next 前两个不等式意味着x_next< 19.
备注：您没有在循环结束时使用location_next更新位置值.你是为x做的,但不是为了位置.这是一个正交问题.我期待着如下声明：

location=m[location_next]
点赞