Making use of F#'s math libraries together with Z3
Byron Cook, of Terminator fame, has just been looking at using F# in conjunction with the Z3 theorem prover, a great new .NET and native component out of Microsoft Research Redmond.
Recent work on F#'s math libraries, together with the latest release of Z3 make for a pretty powerful mixture. In particular I find it interesting that its so easy to combine the polymorphic matrix code support together with the power of Z3. To play around with F#'s new matrix syntax and the new release of Z3 I decided to re-implement the rank function synthesis engine used within TERMINATOR. The result turned out to be so concise that I thought it would be interesting to the larger F# community. ...
At the high-level we're going to build a tool that takes in a mathematical relation represented as the conjunction of linear inequalities....
It's a really beautiful piece of work, and read all about it over on Byron's blog.
