48 lines
848 B
Python
48 lines
848 B
Python
#!/usr/bin/env python3
|
|
|
|
from z3 import *
|
|
|
|
s = Solver()
|
|
|
|
x = Real('x')
|
|
Dx = Real('Dx')
|
|
y = Real('y')
|
|
Dy = Real('Dy')
|
|
z = Real('z')
|
|
Dz = Real('Dz')
|
|
t0 = Real('t0')
|
|
eqT0 = t0 >= 0
|
|
eq0x = x + Dx * t0 == (-2 * t0) + 19
|
|
eq0y = y + Dy * t0 == (1 * t0) + 13
|
|
eq0z = z + Dz * t0 == (-2 * t0) + 30
|
|
t1 = Real('t1')
|
|
eqT1 = t1 >= 0
|
|
eq1x = x + Dx * t1 == (-1 * t1) + 18
|
|
eq1y = y + Dy * t1 == (-1 * t1) + 19
|
|
eq1z = z + Dz * t1 == (-2 * t1) + 22
|
|
t2 = Real('t2')
|
|
eqT2 = t2 >= 0
|
|
eq2x = x + Dx * t2 == (-2 * t2) + 20
|
|
eq2y = y + Dy * t2 == (-2 * t2) + 25
|
|
eq2z = z + Dz * t2 == (-4 * t2) + 34
|
|
#solve for x, y, z, Dx, Dy, Dz, t1, t2, t3.
|
|
|
|
|
|
s.add(eqT0,
|
|
eq0x,
|
|
eq0y,
|
|
eq0z,
|
|
eqT1,
|
|
eq1x,
|
|
eq1y,
|
|
eq1z,
|
|
eqT2,
|
|
eq2x,
|
|
eq2y,
|
|
eq2z)
|
|
|
|
if s.check() == sat:
|
|
print("Solution:", s.model())
|
|
else:
|
|
print("No solution found")
|