4

Python をインストールせずに posix API を提供するシステムで Z3 を実行することは可能ですか?

新しいバージョン 4.3 では、ビルド プロセス (scripts/mk_make.py) で既に python を使用しているのを見てきました。4.1 のような古いバージョンはどうですか? Pythonなしでposixで実行することは想像できますか?

4

1 に答える 1

2

お使いのシステムでPythonを使用できませんか？

Pythonは、Z3コードベースの一部を自動的に生成するために常に使用されていました。最初のソースコードリリースには、自動生成されたコードが含まれています。実際、当時、私たちはpython + sed + awk+grepの組み合わせを使用してコードのこれらの部分を生成していました。最初のリリースのもう1つの問題は、Windows（+ Visual Studio）のビルドシステムが他のプラットフォームのビルドシステムとは完全に異なっていたことです。LinuxおよびOSX用のMakefileは、VisualStudioProjectファイルから派生しました。一部のユーザーは、LinuxおよびOSXのビルドシステムに関する問題も報告し始めました。したがって、これらの問題を減らし、ビルドシステムを統一するために、Python（およびPythonのみ）を使用して次のことを行うことにしました。

  • コードを自動的に生成します（さまざまな言語のバインディング、APIロギングサポートなど）
  • システムの要件を確認してください
  • Makefileを生成する
  • そして他の形式の自動化

Pythonは、ほとんどのシステム（posixに準拠していないシステムでも）で機能するため、私たちにとって非常に魅力的です。ポータブルスクリプトを簡単に書くことができます。さらに、切り替えを行った後、より多くのプラットフォームでZ3をコンパイルできます。Windows、Linux（Mint、Ubuntu、Suseなど）、OSX、Cygwin、およびFreeBSDで正常にコンパイルされました。「不安定な」（別名working-in-progress）ブランチでは、autoconfも必要なくなり、Pythonを使用してすべてのシステム固有の構成を行います。Z3をビルドするには、Python、C ++コンパイラ（Visual Studio C ++、g++またはclang++）、ar（Windows以外のプラットフォームの場合）、make（またはnmake）が必要です。これは非常に小さな要件のセットです。Pythonは、デフォルトでほとんどのプラットフォームで使用できます。

そうは言っても、Pythonの要件を削除することは可能ですか？はい、そうですが、Pythonを別のものに置き換える必要があります。上記のすべてのタスクを実行できるようにする何か。http://z3.codeplex.com/SourceControl/changeset/view/0c1f2a82818aのディレクトリscriptsを見てください。これらすべての自動化スクリプトを、サポートするすべてのプラットフォームで使用できるものに移植する必要があります。

于 2012-11-30T16:54:02.040 に答える