Z3::Optimize
Inherits Z3::Checkable < Reference < Object
A solver with objectives. Everything Solver does with assertions it does too,
plus #maximize, #minimize and #assert_soft - soft constraints being the ones
Z3 is allowed to break, paying their weight when it does, which is MaxSAT.
Z3's objective value readers aren't bound, so read the maximised term out of the
model rather than expecting one from #maximize, which answers the objective's
index the way Z3 does.
Constructors
Instance methods
tracker is a Bool const standing in for expr, and it's what shows up in
#unsat_core if the solver blames this assertion
A constraint Z3 may break, at the cost of weight. The weight is a String
because that's Z3's own interface to it.
Parses SMT-LIB2 and adds its assertions on top of whatever's already asserted,
the same way Solver#from_string does - except that this parser knows
(maximize ...), (minimize ...) and (assert-soft ...) too, so a string can
bring objectives along with its assertions.
A hint at which value to try for a variable first, the same warm start
Solver.simple takes - but Bool and Bitvec only.
Z3's optimizer gets arithmetic ones wrong in both directions: an Int hint is
dropped by its elim_01 preprocessing before the search ever sees it, and a Real
hint which does arrive comes back out of that preprocessing scaled, so an Optimize
with an objective can answer with a model that fails its own assertions. Those two
raise here rather than being passed through; Solver.simple honours arithmetic
warm starts correctly and is where one belongs until Z3 is fixed.