I'm writing a function that will identify when a dropped object will hit the ground. It starts at some highness-value y with some initial velocity y0. It takes gravity acceleration (9.81m/s) into account and tries to determine a dt at which y == 0.
The code (below) works fine to determine at what point the mass will hit the ground. However, I had to find out the hard way that I have to use Solver and not Optimize. (result: unknown). Can somebody explain the reason for this? Shouldn't optimize also be able to find a solution? (obviously there is only one in this scenario)
Here's my code:
from z3 import * vy0, y0 = Reals("vy0 y0") # initial velocity, initial position dt, vy, y = Reals("dt vy y") # time(s), acceleration, velocity, position solver = Solver() # Optmize doesn't work, but why? solver.add(vy0 == 0) solver.add(y0 == 3) solver.add(dt >= 0) # time needs to be positive solver.add(vy == vy0 - 9.81 * dt) # the velocity is initial - acceleration * time solver.add(y == y0 + vy/2 * dt) # the position changes with the velocity (s = v/2 * t) solver.add(y == 0) # solver.minimize(dt) # Optmize doesn't work, but why? print(solver.check()) print(solver.model()) 
