In an answer to this question, Leonardo posts a link to "Exact nonlinear optimization on demand". This sounds like nonlinear optimization will be (or is?) supported by vZ. In the paper "νZ - An Optimizing SMT Solver", the abstract says:
νZ provides a portfolio of approaches for solving linear optimization problems over SMT formulas, MaxSMT, and their combinations.
This again sounds like nonlinear optimizations are out of scope at the moment.
I played around with this smt2 code:
(set-option :pp.decimal true)
(set-option :produce-models true)
(declare-fun x () Real)
(declare-fun y () Real)
(assert (= y (+ 1 (^ (- x 1) 2.0))))
(assert (and (<= (- 3.0) x) (< x 3.0)))
(assert (and (<= (- 3.0) y) (< y 3.0)))
(minimize y)
(check-sat)
(get-value (x y))
(exit)
As an answer I get this response:
unknown
(objectives
(y ((* (- 1) oo) oo))
)
((x 0.0)
(y 2.0))
So I guess, that nonlinear functions are indeed not supported by vZ.
Are there plans in doing so?
