25 lines
643 B
Python
25 lines
643 B
Python
|
#!/usr/bin/env python3
|
||
|
|
|
||
|
|
from z3 import *
|
||
|
|
|
||
|
|
rx, ry, rz = Ints('rx ry rz')
|
||
|
|
rvx, rvy, rvz = Ints('rvx rvy rvz')
|
||
|
|
t0, t1, t2 = Ints('t0 t1 t2')
|
||
|
|
answer = Int('answer')
|
||
|
|
|
||
|
|
solve(
|
||
|
|
rx + t0 * rvx == 225415405941969 + t0 * 23,
|
||
|
|
ry + t0 * rvy == 400648127977931 + t0 * -204,
|
||
|
|
rz + t0 * rvz == 79201130433258 + t0 * 617,
|
||
|
|
|
||
|
|
rx + t1 * rvx == 353783687623292 + t1 * -80,
|
||
|
|
ry + t1 * rvy == 138575899489956 + t1 * 156,
|
||
|
|
rz + t1 * rvz == 318416438572569 + t1 * 21,
|
||
|
|
|
||
|
|
rx + t2 * rvx == 215751176267772 + t2 * -120,
|
||
|
|
ry + t2 * rvy == 376619563956940 + t2 * 126,
|
||
|
|
rz + t2 * rvz == 230133299986253 + t2 * -352,
|
||
|
|
|
||
|
|
answer == rx + ry + rz,
|
||
|
|
)
|