<div dir="ltr"><div><pre style="white-space:pre-wrap;color:rgb(0,0,0)"><font face="arial, helvetica, sans-serif">I'm happy to announce a new release of SBV (v6.0); a library for seamlessly integrating SMT solvers with Haskell:</font></pre><pre style="white-space:pre-wrap;color:rgb(0,0,0)">      <a href="https://hackage.haskell.org/package/sbv" style="font-family:arial,sans-serif">http://hackage.haskell.org/package/sbv</a></pre></div><div>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:</div><div><br></div><div>            <a href="http://hackage.haskell.org/package/sbv-6.0/docs/Data-SBV.html#g:44">http://hackage.haskell.org/package/sbv-6.0/docs/Data-SBV.html#g:44<br></a></div><div><br></div><div>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.</div><div><br></div><div>(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 <a href="https://github.com/Z3Prover/z3">github</a>.)</div><div><br></div><div>A few basic examples:</div><div><ul><li><a href="https://hackage.haskell.org/package/sbv-6.0/docs/Data-SBV-Examples-Optimization-LinearOpt.html">Basic linear optimization over reals</a><br></li><li><a href="https://hackage.haskell.org/package/sbv-6.0/docs/Data-SBV-Examples-Optimization-Production.html">Workshop product allocation</a><br></li><li><a href="https://hackage.haskell.org/package/sbv-6.0/docs/Data-SBV-Examples-Optimization-VM.html">Allocating virtual-machines in data-centers</a><br></li></ul><div>This release also comes with a number of other changes/features, including support for user given tactics, mainly aimed for advanced users. See <a href="https://hackage.haskell.org/package/sbv-6.0/changelog">here</a> for details.</div></div><div><br></div><div>Bug reports, as always, are most welcome.</div><div><br></div><div>-Levent.</div></div>