Download

Table of contents

1. Installation
2. How to run Maude-SE

We provide a zip file of Maude-SE (maude-se-linux.zip). This file contains the Maude-SE executable, examples, and an installation script. The structure of the zip file is as follows.

Currently, we provide the Maude-SE executable for Linux only. We will provide executables for MacOS later.

Installation

To install Maude-SE, unzip the maude-se-linux.zip file and go inside the unzipped directory.

~$ unzip maude-se-linux.zip && cd maude-se-linux

Use the following command to install prerequisites for Maude-SE.

~/maude-se-linux$ ./pre-requisite.sh

The script requires sudo priviledge to install some dependencies.

Install one of the Maude-SE Python wheels.

~/maude-se-linux$ pip install maude_se-0.0.1-cp3xx-cp3xx-linux_x86_64.whl

Replace xx with the version you want

Type the following command to test successful installation.

~/maude-se-linux$ maude-se -h

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

usage: maude-se [-h] [-s [SOLVER]] [file]

positional arguments:
  file                  input Maude file

optional arguments:
  -h, --help            show this help message and exit
  -s [SOLVER], -solver [SOLVER]
                        set an underlying SMT solver
                        * Supported solvers: {z3,yices,cvc5}
                        * Usage: -s z3
                        * Default: -s z3

We built and tested Maude-SE on Ubuntu 20.04.

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-linux$ maude-se ./smt-check-ex.maude -s yices

Internally, the script reads maude-se.maude as its prelude and then runs the input Maude file. The prelude contains two Maude-SE 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.