CODEWITHSUNDEEP
pythonz3
hafizul asad
hafizul asad

Reputation: 527

Z3 code not running for specified number of iterations

This code runs for only i=4, but if location is uninitialized, it runs for i=19????? location=BoolVal(False) location is initialized here

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)

Upvotes: 4

Views: 116

Answers (1)

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

The short answer is: the formula you add in the command s.add(...) is unsatisfiable at iteration 4. At the beginning of iteration 4, we have that x is 19 and location is False. By replacing x and location in the formula, we have that:

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

After simplifying the formula above we have:

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

To show the unsatisfiability of this formula, let us consider the following two cases: location_next is True, or location_next is False.

  1. location_next is True. Then, x_next < 19 must also be True. Moreover, the first argument of the Or is False. Thus, formula is satisfiable only if we can make the second argument True. This is not the case, since the following is unsatisfiable:

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

    The first two inequalities imply that x_next >= 19.

  2. location_next is False. Then x_next >= 19 must be True. By a similar argument, the formula is satisfiable only if we can make the first argument of the Or True. This is also not possible, since the following is unsatisfiable:

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

    The first two inequalities imply that x_next < 19.

Remark: you did not update the value of location using location_next in the end of the loop. You do it for x, but not for location. This is an orthogonal problem. I was expecting a statement such as:

location=m[location_next]

Upvotes: 2

Related Questions