Z3Explanation

The Z3 automated theorem prover is developed by Microsoft Research in Redmond (dB08). It and Simplify are the primary theorem provers of the Boogie reasoning framework. Z3 is released in binary-only form. The most recent releases are only built for the Microsoft Windows operating system. An older, out-of-date release was built for Linux to conform to the SMT-LIB competition's rules.

Z3 is a very powerful modern prover, thus it has been "bridged" into the MOBIUS Prover API as well. It supports the Simplify and SMT-LIB concrete syntaxes, as well as its own.

Whereas Z3 only runs on the Microsoft Windows platform, the Mobius PVE runs on all modern platforms, including Apple's OS X and UNIX variants like Linux, Solaris, etc. We wish to support as many modern theorem provers as possible within the Mobius PVE, but supporting Z3 on non-Windows systems is a non-trivial task.

Recently Z3 has been tested running within the Wine runtime (Win08) on Intel-based systems running Linux. This mechanism (spawning Z3 within Wine, communication via piped datastreams, etc.) is now built into the MOBIUS Automated Prover API.

In theory, such a mechanism will work on all Intel-based Wine runtimes, like those available for other UNIX variants and OS X. In addition, we plan on experimenting with executing Z3 within a virtualized Microsoft Windows installation (e.g. using Parallels or VMware, (both of which are used for Mobius PVE development and testing) on OS X on Intel.

Version: 1 Time: Mon Mar 31 13:25:48 2008 Author: dcochran (dcochran) IP: 193.1.132.32