Download
Table of contents
We provide Python wheels for Maude-SE through our GitHub repository. Please visit https://github.com/maude-se/maude-se/releases/tag/v0.0.1 and download. The followings are the currently available wheels provided on the release page.
| File | Description |
| maude_se-0.0.1-cp38-cp38-linux_x86_64.whl | A Python 3.8 wheel of Maude-SE for Linux |
| maude_se-0.0.1-cp39-cp39-linux_x86_64.whl | A Python 3.9 wheel of Maude-SE for Linux |
| maude_se-0.0.1-cp310-cp310-linux_x86_64.whl | A Python 3.10 wheel of Maude-SE for Linux |
| maude_se-0.0.1-cp311-cp311-linux_x86_64.whl | A Python 3.11 wheel of Maude-SE for Linux |
| maude_se-0.0.1-cp312-cp312-linux_x86_64.whl | A Python 3.12 wheel of Maude-SE for Linux |
| maude_se-0.0.1-cp38-cp38-macosx_14_0_arm64.whl | A Python 3.8 wheel of Maude-SE for MacOS |
| maude_se-0.0.1-cp39-cp39-macosx_14_0_arm64.whl | A Python 3.9 wheel of Maude-SE for MacOS |
| maude_se-0.0.1-cp310-cp310-macosx_14_0_arm64.whl | A Python 3.10 wheel of Maude-SE for MacOS |
| maude_se-0.0.1-cp311-cp311-macosx_14_0_arm64.whl | A Python 3.11 wheel of Maude-SE for MacOS |
| maude_se-0.0.1-cp312-cp312-macosx_14_0_arm64.whl | A Python 3.12 wheel of Maude-SE for MacOS |
We also provide a zip file (maude-se.zip). This file contains examples and an installation script. The structure of the zip file is as follows.
| File | Description |
|---|---|
| requirements.txt | A list of required Python packages for MaudeSE |
| api-test.py | Example usages of the Maude-SE Python API |
| api-test.maude | A Maude file used by api-test.py |
| smt-check-ex.maude | A Maude file containing examples for metaSmtCheck function |
| smt-search-ex.maude | A Maude file containing examples for metaSmtSearch2 function |
Prerequisite
Maude-SE supports various SMT solvers such as Z3, CVC4, CVC5, and Yices. Maude-SE provides connections to their Python bindings. Among these solvers, The Yices Python binding requires the Yices executable to be installed.
Please follow the instructions of https://github.com/SRI-CSL/yices2 to install the Yices executable.
Installation
To install Maude-SE, unzip the maude-se.zip file and go inside the unzipped directory.
~$ unzip maude-se.zip && cd maude-se
Use the following command to install required Python packages for Maude-SE.
~/maude-se$ pip install -r requirements.txt
Install one of the Maude-SE Python wheels.
~/maude-se$ pip install maude_se-0.0.1-cp<YOUR-PYTHON-VERSION>-cp<YOUR-PYTHON-VERSION>-<YOUR-OS>.whl
Type the following command to test successful installation.
~/maude-se$ maude-se -h
If the installation was successful, you can see the following message.
usage: maude-se [-h] [-s [SOLVER]] [-no-meta] [file]
positional arguments:
file input Maude file
options:
-h, --help show this help message and exit
-s [SOLVER], -solver [SOLVER]
set an underlying SMT solver
* Supported solvers: {z3,yices,cvc5}
* Usage: -s cvc5
* Default: -s z3
-no-meta no metaInterpreter
We built and tested Maude-SE on Ubuntu 20.04 and on M1 MacBook Pro.
How to run Maude-SE
You are now ready to run Maude-SE using the main script maude-se. The script takes an input Maude file and executes it. For example, you can run the example file smt-check-ex.maude with yices solver using the following command.
~/maude-se$ maude-se ./smt-check-ex.maude -s yices
The Maude-SE Python package contains smt-check.maude which includes two meta-level functions: metaSmtCheck and metaSmtSearch2. The metaSmtCheck function can check the satisfiability of SMT queries, as similar to metaCheck, but it can handle various theories (with uninterpreted functions) and generate satisfying assignments. The metaSmtSearch2 function can perform search using rewriting modulo SMT, similar to metaSmtSearch, but supports folding.
Currently, we do not support metaSimplify. We will update this later.