mirror of
https://git.freebsd.org/ports.git
synced 2025-06-07 13:50:38 -04:00
25 lines
453 B
Python
25 lines
453 B
Python
# example from https://ericpony.github.io/z3py-tutorial/guide-examples.htm
|
|
|
|
from z3 import Reals, set_option, solve
|
|
|
|
|
|
d, a, t, v_i, v_f = Reals('d a t v__i v__f')
|
|
|
|
equations = [
|
|
d == v_i * t + (a*t**2)/2,
|
|
v_f == v_i + a*t,
|
|
]
|
|
|
|
# Given v_i, t and a, find d
|
|
problem = [
|
|
v_i == 0,
|
|
t == 4.10,
|
|
a == 6
|
|
]
|
|
|
|
solve(equations + problem)
|
|
|
|
# Display rationals in decimal notation
|
|
set_option(rational_to_decimal=True)
|
|
|
|
solve(equations + problem)
|