CODEWITHSUNDEEP
z3polynomial-mathz3py
w00d
w00d

Reputation: 5596

z3 simplify to polynomial form

How can I use z3 to print a complex function of (x) in polynomial form ? The simplify function print something nasty:

-1/120*(-5 + x)*(-4 + x)*(-3 + x)*(-2 + x)*(-1 + x) +
1/12*x*(-5 + x)*(-4 + x)*(-3 + x)*(-2 + x) +

Upvotes: 1

Views: 226

Answers (1)

Juan Ospina
Juan Ospina

Reputation: 1347

One possible solution using Z3Py

x = Real('x')
y = (-1/120)*(-5+x)*(-4+x)*(-3+x)*(-2+x)*(-1+x)
z = (1/12)*(-5+x)*(-4+x)*(-3+x)*(-2+x)
w = y + z
print simplify(simplify(w, som=True), mul_to_power=True)

and the corresponding output is

120 + -274*x + 225*x**2 + -85*x**3 + 15*x**4 + -1*x**5

Upvotes: 1

Related Questions