Editing Diagrams/Dev/Constraints (section)

== What other libraries did you consider?  Why sbv? ==
* See mailing list discussion: https://groups.google.com/forum/#!topic/diagrams-discuss/DPaSbHqp4N4
* After that, I had more discussion with cmears: http://ircbrowse.net/browse/diagrams?events_page=1386
* Summary: Many solvers were considered, sourced from googling "constraint solving library" and from going through Hackage. Most of the "solvers" were limited to linear constraints. Two were not: SMT solvers, and GECODE. The haskell bindings (monadiccp-gecode) for gecode are basically unmaintained, as told to me by the listed maintainer. SMT solvers are being actively researched by various people (Microsoft, SRI International, etc.) and show no signs of going away. Sbv is a well-maintained binding that abstracts over the SMT solvers (using SMTLIB, a well-defined format). Z3 in particular seems to be developing nonlinear solving techniques, and there was a research project that used a combination of Z3 and Mathematica to solve extremely complex systems. It also supported the SMTLIB format. My conclusion was thus that sbv is/was going to be around for a while, and will (through the efforts of the SMT solver people) gain many useful constraint-solving algorithms, so it was a good library to use.