Metadata-Version: 2.1
Name: maude-se
Version: 0.0.4
Summary: Maude SMT Extension
Author-Email: Geunyeol Yu <maude-se@postech.ac.kr>
License: GPLv3
Classifier: Intended Audience :: Science/Research
Classifier: Programming Language :: Python
Classifier: Programming Language :: Python :: 3
Classifier: Topic :: Scientific/Engineering
Classifier: Operating System :: MacOS
Classifier: Operating System :: POSIX :: Linux
Project-URL: Homepage, https://maude-se.github.io
Project-URL: Bug tracker, https://github.com/postechsv/maude-se/issues
Project-URL: Documentation, https://maude-se.github.io
Project-URL: Source code, https://github.com/postechsv/maude-se
Requires-Python: <3.15,>=3.10
Requires-Dist: pyyaml
Requires-Dist: z3-solver==4.13.0.0; extra == "z3"
Requires-Dist: cvc5==1.4.0; extra == "cvc5"
Requires-Dist: yices==1.1.6; extra == "yices"
Requires-Dist: yices-solver==2.6.5.post24; extra == "yices"
Requires-Dist: z3-solver==4.13.0.0; extra == "all-solvers"
Requires-Dist: cvc5==1.4.0; extra == "all-solvers"
Requires-Dist: yices==1.1.6; extra == "all-solvers"
Requires-Dist: yices-solver==2.6.5.post24; extra == "all-solvers"
Provides-Extra: z3
Provides-Extra: cvc5
Provides-Extra: yices
Provides-Extra: all-solvers
Description-Content-Type: text/markdown

# MaudeSE

MaudeSE extends [Maude](https://github.com/SRI-CSL/Maude) with SMT solving. It
supports satisfiability checks and symbolic search, with Python connectors for
Z3, Yices2, and cvc5. You can also write a connector for another solver.

## Install and run

The upcoming release supports Python 3.10–3.14 on macOS and Linux. Install
MaudeSE with Z3, its default solver:

```sh
python3 -m pip install 'maude-se[z3]'
```

This command applies after the upcoming release is published. Until then,
build and test the current source as described in [INSTALL.md](INSTALL.md).

This installs both MaudeSE and the Z3 Python package. The connectors and
converters are included in MaudeSE; the extra installs the solver package.

From a checkout of this repository, open one of the included examples:

```sh
maude-se examples/smt-check-ex.maude -s z3
```

At the `MaudeSE>` prompt, run `check in SIMPLE : X:Integer > 4 using QF_LRA .`;
the result should be `sat`.

To use Yices2 or cvc5 instead, install `maude-se[yices]` or `maude-se[cvc5]`
and select it with `-s yices` or `-s cvc5`. See the
[installation guide](INSTALL.md) for existing installations, standalone
executables, and source builds.

## Documentation

The [MaudeSE documentation](https://maude-se.github.io) covers commands,
examples, and the connector interface.
