This version brings optimization features to SBV, where arithmetic goals can be minimized or maximized. The algorithms employed are particularly suitable for linear-optimization problems, over bounded/unbounded integers and reals. Multiple objective functions with optimization priorities are also supported:
Objective values that assume their optimal values at infinity and epsilon are also supported, allowing the user to express arbitrary combinations of goals. Furthermore, soft-goals (i.e., those that can be violated with a user-specified penalty) are included as well. Such goals can be used to expressed "nice-to-have" constraints, for instance as they appear in classic scheduling problems.
(Optimization is currently only supported by the z3-backend, and leverages the features of the z3 SMT solver. Please make sure you get a fresh copy of it from
github.)
A few basic examples:
This release also comes with a number of other changes/features, including support for user given tactics, mainly aimed for advanced users. See
here for details.
Bug reports, as always, are most welcome.
-Levent.