Is optimization / maximization supported?

[SteveElp]

The C++ bindings seem to support optimizations (e.g., maximize/minimize).

But how could we use that?

using Z3

# how do we use these?
methods(maximize)  # ==> 2 methods for "maximize"
methods(minimize)  # ==> 2 methods for "minimize"

(Another thing which would be helpful are 'soft constraints', which Z3 should also support.)

I love the Z3 bindings and I hope to use it extensively.

[ahumenberger]

The Z3 repo contains examples for the C++ API which you can translate into Julia code. For instance, the optimization example from https://github.com/Z3Prover/z3/blob/7eb05dd952a2f5de1d4be09436a97651c85dba18/examples/c%2B%2B/example.cpp#L1024 would translate to the following Julia code:

c = Context()
opt = Optimize(c)
p = Params(c)
set(p, "priority", "pareto")
set(opt, p)
x = int_const(c, "x")
y = int_const(c, "y")
add(opt, and(10 >= x, x >= 0))
add(opt, and(10 >= y, y >= 0))
add(opt, x+y <= 11)
h1 = maximize(opt, x)
h2 = maximize(opt, y)
while true
  if Z3.sat == check(opt)
    println("x: $(lower(opt, h1))\t y: $(lower(opt, h2))")
  else
    break
  end
end

Soft constraints can also be added via Optimize::add which accepts a weight as an argument (see https://github.com/Z3Prover/z3/blob/59d8895d1583496f53205ea4dc81b1b91295fbb3/src/api/c%2B%2B/z3%2B%2B.h#L2851).