Installation of Z3 on a posix system without pytho

2019-06-26 13:30发布

问题:

Is it possible to get Z3 running on a system providing posix API without having python installed?

I have seen the new version 4.3 uses python already in the build-process (scripts/mk_make.py). Whats about older versions like 4.1? Is it imaginable to get it to run on posix without python?

回答1:

Is Python not available in your system?

Python was always used to automatically generate some parts of the Z3 code base. In the first source code release, we have included the automatically generated code. Actually, at that time, we were using a combination of python + sed + awk + grep to generate these parts of the code. Another problem with the first release is that the build system for Windows (+ Visual Studio) was completely different from the build system for the other platforms. The Makefiles for Linux and OSX were derived from Visual Studio Project files. Some users also started to report problems with the build system for Linux and OSX. So, to reduce these problems and have a uniform build system, we decided to use python (and python only) to:

  • Automatically generate code (for bindings for different languages, API logging support, etc)
  • Check the system for requirements
  • Generate the Makefiles
  • And any other form of automation

Python is very attractive for us because it works in most systems (even non posix compliant ones). We can easily write portable scripts. Moreover, after we made the switch, we can compile Z3 in more platforms. We successfully compiled it on Windows, Linux (Mint, Ubuntu, Suse, etc), OSX, Cygwin, and FreeBSD. In the "unstable" (aka working-in-progress) branch, we don't even require autoconf anymore, we use python to do all system specific configuration. To build Z3, we just need: python, C++ compiler (Visual Studio C++, g++ or clang++), ar (on non-windows platform), make (or nmake). This is very small set of requirements. Python is available in most platforms by default.

That being said, is it possible to remove the python requirement? Yes, it is, but it would have to replace python with something else. Something, that would allows us to perform all tasks described above. Take a look in the directory scripts at http://z3.codeplex.com/SourceControl/changeset/view/0c1f2a82818a, we would have to port all these automation scripts to something that can be used on all platforms we support.



标签: z3