base on The Z3 Theorem Prover # Z3 Z3 is a theorem prover from Microsoft Research. It is licensed under the [MIT license](LICENSE.txt). If you are not familiar with Z3, you can start [here](https://github.com/Z3Prover/z3/wiki#background). Pre-built binaries for stable and nightly releases are available from [here](https://github.com/Z3Prover/z3/releases). Z3 can be built using [Visual Studio][1], a [Makefile][2] or using [CMake][3]. It provides [bindings for several programming languages][4]. See the [release notes](RELEASE_NOTES.md) for notes on various stable releases of Z3. [](https://microsoft.github.io/z3guide/) ## Build status | Azure Pipelines | Code Coverage | Open Bugs | Android Build | WASM Build | Windows Build | Pyodide Build | | --------------- | --------------|-----------|---------------|------------|---------------|---------------| | [](https://dev.azure.com/Z3Public/Z3/_build/latest?definitionId=1&branchName=master) | [](https://github.com/Z3Prover/z3/actions/workflows/coverage.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/wip.yml) |[](https://github.com/Z3Prover/z3/actions/workflows/android-build.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/wasm.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/Windows.yml) | [](https://github.com/Z3Prover/z3/actions/workflows/pyodide.yml) <a href="https://github.com/z3prover/z3/pkgs/container/z3">Docker image</a>. [1]: #building-z3-on-windows-using-visual-studio-command-prompt [2]: #building-z3-using-make-and-gccclang [3]: #building-z3-using-cmake [4]: #z3-bindings ## Building Z3 on Windows using Visual Studio Command Prompt 32-bit builds, start with: ```bash python scripts/mk_make.py ``` or instead, for a 64-bit build: ```bash python scripts/mk_make.py -x ``` then: ```bash cd build nmake ``` Z3 uses C++20. The recommended version of Visual Studio is therefore VS2019. ## Building Z3 using make and GCC/Clang Execute: ```bash python scripts/mk_make.py cd build make sudo make install ``` Note by default ``g++`` is used as the C++ compiler if it is available. If you would prefer to use Clang change the ``mk_make.py`` invocation to: ```bash CXX=clang++ CC=clang python scripts/mk_make.py ``` Note that Clang < 3.7 does not support OpenMP. You can also build Z3 for Windows using Cygwin and the Mingw-w64 cross-compiler. To configure that case correctly, make sure to use Cygwin's own python and not some Windows installation of Python. For a 64 bit build (from Cygwin64), configure Z3's sources with ```bash CXX=x86_64-w64-mingw32-g++ CC=x86_64-w64-mingw32-gcc AR=x86_64-w64-mingw32-ar python scripts/mk_make.py ``` A 32 bit build should work similarly (but is untested); the same is true for 32/64 bit builds from within Cygwin32. By default, it will install z3 executable at ``PREFIX/bin``, libraries at ``PREFIX/lib``, and include files at ``PREFIX/include``, where ``PREFIX`` installation prefix is inferred by the ``mk_make.py`` script. It is usually ``/usr`` for most Linux distros, and ``/usr/local`` for FreeBSD and macOS. Use the ``--prefix=`` command line option to change the install prefix. For example: ```bash python scripts/mk_make.py --prefix=/home/leo cd build make make install ``` To uninstall Z3, use ```bash sudo make uninstall ``` To clean Z3 you can delete the build directory and run the ``mk_make.py`` script again. ## Building Z3 using CMake Z3 has a build system using CMake. Read the [README-CMake.md](README-CMake.md) file for details. It is recommended for most build tasks, except for building OCaml bindings. ## Building Z3 using vcpkg vcpkg is a full platform package manager, you can easily install libzmq with vcpkg. Execute: ```bash git clone https://github.com/microsoft/vcpkg.git ./bootstrap-vcpkg.bat # For powershell ./bootstrap-vcpkg.sh # For bash ./vcpkg install z3 ``` ## Dependencies Z3 itself has few dependencies. It uses C++ runtime libraries, including pthreads for multi-threading. It is optionally possible to use GMP for multi-precision integers, but Z3 contains its own self-contained multi-precision functionality. Python is required to build Z3. To build Java, .Net, OCaml, Julia APIs requires installing relevant tool chains. ## Z3 bindings Z3 has bindings for various programming languages. ### ``.NET`` You can install a nuget package for the latest release Z3 from [nuget.org](https://www.nuget.org/packages/Microsoft.Z3/). Use the ``--dotnet`` command line flag with ``mk_make.py`` to enable building these. See [``examples/dotnet``](examples/dotnet) for examples. ### ``C`` These are always enabled. See [``examples/c``](examples/c) for examples. ### ``C++`` These are always enabled. See [``examples/c++``](examples/c++) for examples. ### ``Java`` Use the ``--java`` command line flag with ``mk_make.py`` to enable building these. See [``examples/java``](examples/java) for examples. ### ``OCaml`` Use the ``--ml`` command line flag with ``mk_make.py`` to enable building these. See [``examples/ml``](examples/ml) for examples. ### ``Python`` You can install the Python wrapper for Z3 for the latest release from pypi using the command: ```bash pip install z3-solver ``` Use the ``--python`` command line flag with ``mk_make.py`` to enable building these. Note that it is required on certain platforms that the Python package directory (``site-packages`` on most distributions and ``dist-packages`` on Debian based distributions) live under the install prefix. If you use a non standard prefix you can use the ``--pypkgdir`` option to change the Python package directory used for installation. For example: ```bash python scripts/mk_make.py --prefix=/home/leo --python --pypkgdir=/home/leo/lib/python-2.7/site-packages ``` If you do need to install to a non standard prefix a better approach is to use a [Python virtual environment](https://virtualenv.readthedocs.org/en/latest/) and install Z3 there. Python packages also work for Python3. Under Windows, recall to build inside the Visual C++ native command build environment. Note that the ``build/python/z3`` directory should be accessible from where python is used with Z3 and it depends on ``libz3.dll`` to be in the path. ```bash virtualenv venv source venv/bin/activate python scripts/mk_make.py --python cd build make make install # You will find Z3 and the Python bindings installed in the virtual environment venv/bin/z3 -h ... python -c 'import z3; print(z3.get_version_string())' ... ``` See [``examples/python``](examples/python) for examples. ### ``Julia`` The Julia package [Z3.jl](https://github.com/ahumenberger/Z3.jl) wraps the C API of Z3. A previous version of it wrapped the C++ API: Information about updating and building the Julia bindings can be found in [src/api/julia](src/api/julia). ### ``Web Assembly`` / ``TypeScript`` / ``JavaScript`` A WebAssembly build with associated TypeScript typings is published on npm as [z3-solver](https://www.npmjs.com/package/z3-solver). Information about building these bindings can be found in [src/api/js](src/api/js). ### Smalltalk (``Pharo`` / ``Smalltalk/X``) Project [MachineArithmetic](https://github.com/shingarov/MachineArithmetic) provides Smalltalk interface to Z3's C API. For more information, see [MachineArithmetic/README.md](https://github.com/shingarov/MachineArithmetic/blob/pure-z3/MachineArithmetic/README.md) ## System Overview  ## Interfaces * Default input format is [SMTLIB2](http://smtlib.cs.uiowa.edu) * Other native foreign function interfaces: * [C++ API](https://z3prover.github.io/api/html/namespacez3.html) * [.NET API](https://z3prover.github.io/api/html/namespace_microsoft_1_1_z3.html) * [Java API](https://z3prover.github.io/api/html/namespacecom_1_1microsoft_1_1z3.html) * [Python API](https://z3prover.github.io/api/html/namespacez3py.html) (also available in [pydoc format](https://z3prover.github.io/api/html/z3.html)) * [Rust](https://github.com/prove-rs/z3.rs) * C * OCaml * [Julia](https://github.com/ahumenberger/Z3.jl) * [Smalltalk](https://github.com/shingarov/MachineArithmetic/blob/pure-z3/MachineArithmetic/README.md) (supports Pharo and Smalltalk/X) ## Power Tools * The [Axiom Profiler](https://github.com/viperproject/axiom-profiler-2) currently developed by ETH Zurich ", Assign "at most 3 tags" to the expected json: {"id":"6331","tags":[]} "only from the tags list I provide: [{"id":77,"name":"3d"},{"id":89,"name":"agent"},{"id":17,"name":"ai"},{"id":54,"name":"algorithm"},{"id":24,"name":"api"},{"id":44,"name":"authentication"},{"id":3,"name":"aws"},{"id":27,"name":"backend"},{"id":60,"name":"benchmark"},{"id":72,"name":"best-practices"},{"id":39,"name":"bitcoin"},{"id":37,"name":"blockchain"},{"id":1,"name":"blog"},{"id":45,"name":"bundler"},{"id":58,"name":"cache"},{"id":21,"name":"chat"},{"id":49,"name":"cicd"},{"id":4,"name":"cli"},{"id":64,"name":"cloud-native"},{"id":48,"name":"cms"},{"id":61,"name":"compiler"},{"id":68,"name":"containerization"},{"id":92,"name":"crm"},{"id":34,"name":"data"},{"id":47,"name":"database"},{"id":8,"name":"declarative-gui "},{"id":9,"name":"deploy-tool"},{"id":53,"name":"desktop-app"},{"id":6,"name":"dev-exp-lib"},{"id":59,"name":"dev-tool"},{"id":13,"name":"ecommerce"},{"id":26,"name":"editor"},{"id":66,"name":"emulator"},{"id":62,"name":"filesystem"},{"id":80,"name":"finance"},{"id":15,"name":"firmware"},{"id":73,"name":"for-fun"},{"id":2,"name":"framework"},{"id":11,"name":"frontend"},{"id":22,"name":"game"},{"id":81,"name":"game-engine "},{"id":23,"name":"graphql"},{"id":84,"name":"gui"},{"id":91,"name":"http"},{"id":5,"name":"http-client"},{"id":51,"name":"iac"},{"id":30,"name":"ide"},{"id":78,"name":"iot"},{"id":40,"name":"json"},{"id":83,"name":"julian"},{"id":38,"name":"k8s"},{"id":31,"name":"language"},{"id":10,"name":"learning-resource"},{"id":33,"name":"lib"},{"id":41,"name":"linter"},{"id":28,"name":"lms"},{"id":16,"name":"logging"},{"id":76,"name":"low-code"},{"id":90,"name":"message-queue"},{"id":42,"name":"mobile-app"},{"id":18,"name":"monitoring"},{"id":36,"name":"networking"},{"id":7,"name":"node-version"},{"id":55,"name":"nosql"},{"id":57,"name":"observability"},{"id":46,"name":"orm"},{"id":52,"name":"os"},{"id":14,"name":"parser"},{"id":74,"name":"react"},{"id":82,"name":"real-time"},{"id":56,"name":"robot"},{"id":65,"name":"runtime"},{"id":32,"name":"sdk"},{"id":71,"name":"search"},{"id":63,"name":"secrets"},{"id":25,"name":"security"},{"id":85,"name":"server"},{"id":86,"name":"serverless"},{"id":70,"name":"storage"},{"id":75,"name":"system-design"},{"id":79,"name":"terminal"},{"id":29,"name":"testing"},{"id":12,"name":"ui"},{"id":50,"name":"ux"},{"id":88,"name":"video"},{"id":20,"name":"web-app"},{"id":35,"name":"web-server"},{"id":43,"name":"webassembly"},{"id":69,"name":"workflow"},{"id":87,"name":"yaml"}]" returns me the "expected json"