Add support for Z3 minimization/maximization

[RyanGlScott]

Z3 supports (minimize ...) and (maximize ...) commands, as illustrated in this example. As far as I am aware, Z3 is the only solver that supports something like this at the moment, as other solvers would have to approximate this functionality with something like resolveBoundsSymBV (see #187). In fact, resolveBoundsSymBV is exactly why I'm opening this issue, as the test cases that I added for it run noticeably slower on Z3 than on, say, Yices or CVC4 (at least a couple of seconds slower). I'm wondering if using minimize/maximize could make things faster on Z3.

I'm imagining the API would look something like:

minimize, maximize :: SMTWriter h => WriterConn t h -> Expr t tp -> IO ()

This would need to be guarded behind a problem feature of some sort. SBV already supports something like this here.