Конечно .. Вот один из способов:
from z3 import *
a, b, c, x, y, z = Ints('a b c x y z')
print simplify(a*b*c*x + a*b*c*y + a*b*z, hoist_mul=True)
Это печатает:
a*b*(c*(x + y) + z)
, что именно то, что вы ищете.
И для вашего следующий вопрос, как я нашел аргумент hoist_cmul=True? Просто запустите:
help_simplify()
в ответ на приглашение Python, и в нем будут перечислены все параметры, которые simplify принимает.
Обратите внимание, что в общем случае вы не должны рассчитывать на то, что упрощатель даст вам. Он в основном основан на heuristi c, и при наличии других терминов то, что вы получаете, может не соответствовать ожидаемому. (Конечно, это все равно будет эквивалентное выражение.) Нет понятия «простейшего», когда речь идет о арифметических c выражениях, и то, что вы считаете простым и то, что z3 считает простым, может не совпадать.