Jaa

Making use of F#'s math libraries together with Z3

  • Artikkeli

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.

Comments