z3Opt оптимизировать нелинейную функцию с помощью qfnra-nlsat

Question

Я пытаюсь использовать z3Opt для оптимизации реальной нелинейной функции, но и для простых случаев, как следующий один

http://rise4fun.com/Z3Opt/JbaU

результата является не то, что ожидается. Это как z3, это совсем не оптимизирует ... кто-нибудь может помочь мне понять?

Answer 1

Оптимизация нелинейных функций на данный момент не поддерживается, поэтому по результатам не дается никаких гарантий. Вероятно, было бы лучше, если бы решатель вернул неизвестный (а не сидел) для этого случая, что я должен изучить.