Может ли кто-нибудь сказать мне, как я могу реализовать задачу минимизации целых чисел, подобную приведенной ниже, с помощью Z3py? Как я могу определить для всех утверждений? Здесь все переменные int sort.
Есть ли в Z3 специальный решатель для решения такой проблемы? Если есть, то как я могу установить конфигурацию для этого решателя?
Спасибо
