4

このコードは に対してのみ実行されます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)
4

1 に答える 1

2

簡単な答えは次のとおりです。コマンドに追加した式はs.add(...)、反復 4 では満足できません。反復 4 の開始時には、xis19とlocationis がありFalseます。式のと を置き換えるxと、次のようになります。location

[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]

この式が満たされないことを示すために、次の 2 つのケースを考えてみましょlocation_nextうlocation_next。

  1. location_next真です。次に、x_next < 19True にする必要があります。さらに、 の最初の引数Orは False です。したがって、数式は、2 番目の引数を True にできる場合にのみ充足可能です。以下は満足できないため、これは当てはまりません。

    10*x_next >= 190 + t2 - t1, 5*x_next <= 95 + t2 - t1, x_next < 19

    最初の 2 つの不等式は、x_next >= 19.

  2. location_nextは偽です。次にx_next >= 19、True にする必要があります。同様の議論により、最初の引数をOrTrue にすることができる場合にのみ、式は満足されます。これも、次の条件が満たされないため、不可能です。

    10*x_next <= 190 - t2 + t1, t2 - t1 > 0, 19 <= x_next

    最初の 2 つの不等式は、x_next < 19.

注意:ループの最後でlocationusingの値を更新していません。location_nextあなたはのためにそれをしますが、のためxにはしませんlocation。これは直交問題です。私は次のような声明を期待していました。

location=m[location_next]
于 2012-08-07T16:58:07.183 に答える