Installation

MaudeSE can be installed in two ways: (i) as a Python package, or (ii) as a standalone executable. If you are looking for an older version, you can find it here.

Note

The standalone executable tightly integrates with its underlying SMT solver at the C++ level, and is more efficient than the Python package. However, its connector and converter cannot be extended or customized at the Python level.

MaudeSE Python Package

Wheel Installation

Use pip to install the latest version of the MaudeSE Python package from PyPi.

$ pip install maude-se

Important

Python version 3.8 or newer is required.

You can also manually install the MaudeSE wheel that matches your operating system (macOS or Linux) and machine architecture (arm64 or x86_64) from our GitHub repository:

https://github.com/postechsv/maude-se/releases

$ pip install ./maude_se-<MAUDE_SE_VERSION>-cp<PYTHON_VERSION>-cp<PYTHON_VERSION>-<OS>_<ARCH>.whl

Release	Published At	Wheels
v0.0.3	2025-06-08	maude_se-0.0.3-cp310-cp310-macosx_13_0_x86_64.whl maude_se-0.0.3-cp310-cp310-macosx_14_0_arm64.whl maude_se-0.0.3-cp310-cp310-manylinux_2_28_x86_64.whl maude_se-0.0.3-cp311-cp311-macosx_13_0_x86_64.whl maude_se-0.0.3-cp311-cp311-macosx_14_0_arm64.whl maude_se-0.0.3-cp311-cp311-manylinux_2_28_x86_64.whl maude_se-0.0.3-cp312-cp312-macosx_13_0_x86_64.whl maude_se-0.0.3-cp312-cp312-macosx_14_0_arm64.whl maude_se-0.0.3-cp312-cp312-manylinux_2_28_x86_64.whl maude_se-0.0.3-cp313-cp313-macosx_13_0_x86_64.whl maude_se-0.0.3-cp313-cp313-macosx_14_0_arm64.whl maude_se-0.0.3-cp313-cp313-manylinux_2_28_x86_64.whl maude_se-0.0.3-cp38-cp38-macosx_13_0_x86_64.whl maude_se-0.0.3-cp38-cp38-macosx_14_0_arm64.whl maude_se-0.0.3-cp38-cp38-manylinux_2_28_x86_64.whl maude_se-0.0.3-cp39-cp39-macosx_13_0_x86_64.whl maude_se-0.0.3-cp39-cp39-macosx_14_0_arm64.whl maude_se-0.0.3-cp39-cp39-manylinux_2_28_x86_64.whl

Smoke Test

Use the following command to test successful installation.

$ maude-se -h

If the installation was successful, you can see the following message.

usage: maude-se [-h] [-cfg CONFIG] [-s SOLVER] [-no-meta] [file]

positional arguments:
file                  input Maude file

options:
-h, --help            show this help message and exit
-cfg CONFIG, -config CONFIG
                        a directory to a configuration file (default: "config.yml")
-s SOLVER, -solver SOLVER
                        solver name
-no-meta              no metaInterpreter

SMT Solvers

MaudeSE is shipped with connectors and converters for integrating various SMT solvers (Z3, Yices2, and CVC5), but not containing the solvers. You need to download SMT solvers and their Python bindings by yourself.

For example, if you want to use MaudeSE with Z3, use the following command to install the Z3 Python package along with all required dependencies:

$ pip install z3-solver

Tip

You can also connect other SMT solvers to MaudeSE by implementing the MaudeSE generic interface. See Generic Interface.

Standalone Executable

Currently, we provide standalone executables for macOS and Linux, statically linked with Z3.

Release	Published At	Executables
v0.0.3	2025-06-08	maude_se_z3-0.0.3-macosx-arm64.zip maude_se_z3-0.0.3-macosx-x86_64.zip maude_se_z3-0.0.3-manylinux-x86_64.zip

Note

Standalone executables for Yices2 and CVC5 will be updated soon.