Symbolically minimise function with z3

minimise_function_z3.py

# Remember to install z3 with `python -m pip install z3-solver` (instead of
# `python -m pip install z3`) !

import z3
import numpy as np

f = lambda x: (x - 2) * (x - 3) * (x - 4)
x = z3.Real("x")
y = z3.Real("y")
z = z3.Real("z")
s = z3.Solver()
x_valid = z3.And(x > 2, x < 4)
s.add(z3.ForAll([x], z3.Implies(x_valid, f(y) >= f(x))))
s.add(z3.ForAll([x], z3.Implies(x_valid, f(z) <= f(x))))
s.add(z3.And(y > 2, y < 4))
s.add(z3.And(z > 2, z < 4))
res = s.check()
print(res)

if str(res) == "sat":
    m = s.model()
    print(m, m[x], m[y], m[z])
    print(3 - 1 / np.sqrt(3))
    print(3 + 1 / np.sqrt(3))

# >>> sat
# >>> [y = 2.4226497308?, z = 3.5773502691?] None 2.4226497308? 3.5773502691?
# >>> 2.4226497308103743
# >>> 3.5773502691896257