Installing Z3 on a posix system without python?

Is it possible to run Z3 on a system providing a posix API without installing python?

I saw that the new version 4.3 uses python already in the build process (scripts / mk_make.py). What are older versions like 4.1? Is it possible to get it to work on posix without python?

+4
source share
1 answer

Is Python unavailable on your system?

Python has always been used to automatically create some parts of the Z3 code base. In the first release of the source code, we included automatically generated code. In fact, at that time we used a combination of python + sed + awk + grep to generate these pieces of code. Another issue with the first release is that the build system for Windows (+ Visual Studio) was completely different from the build system for other platforms. Makefiles for Linux and OSX were obtained from Visual Studio project files. Some users also started reporting issues with the build system for Linux and OSX. So, to reduce these problems and have a single build system, we decided to use only python (and only python) for:

  • Automatic code generation (for bindings for different languages, support for API logging, etc.)
  • Check your system for compliance.
  • Creating Makefiles
  • And any other form of automation

Python is very attractive to us because it works on most systems (even incompatible with them). We can easily write portable scripts. Moreover, after we made the switch, we can compile Z3 on other platforms. We successfully compiled it on Windows, Linux (Mint, Ubuntu, Suse, etc.), OSX, Cygwin, and FreeBSD. In the "unstable" branch (the so-called working in the process), we do not even require autoconf, we use python to complete the entire system configuration. To build Z3, we just need: python, a C ++ compiler (Visual Studio C ++, g ++ or clang ++), ar (on a windowless platform), make (or nmake). This is a very small set of requirements. By default, Python is available on most platforms.

As the saying goes, is it possible to remove a python requirement? Yes, it is, but you need to replace python with something else. Something that would allow us to complete all the tasks described above. Take a look at the scripts directory at http://z3.codeplex.com/SourceControl/changeset/view/0c1f2a82818a , we would have to transfer all these automation scripts to what can be used on all platforms supported by us.

+2
source

All Articles