blob: c1cfe30916af70cd71212c4c5946cebb9bef4022 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
# 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)
|
