Maude

The following Python packages have been uploaded to [PyPI](https://pypi.org/project/maude), and they can be installed with `pip install --upgrade maude`.

`.whl` files can also be directly installed with `pip` for the matching Python version (2.7, 3.6, 3.7, 3.8, 3.9, and 3.10).

New features
------------

* New method `Term.apply` to apply rules with an interface similar to `metaXapply`. The term is applied any rule with the given label (or any executable rule if `None` is given instead) according to an optional initial substitution and optional depth bounds. The result is an iterator over the results of the rule application (not reduced, although this may change in the future), the matching substitutions, the matching contexts, and the applied rules. Matching contexts are provided as functions that return the original term with the matched subterm replaced by its argument.
* `Term.match` can now be used to match anywhere and not only on top. This method is now given two additional arguments `minDepth` and `maxDepth` to arbitrary limit matching by depth. By default, `minDepth` is 0 and `maxDepth` is -1 or 0 depending on the value of `withExtension`. The constant `maude.UNBOUNDED` can be used for `maxDepth`.
* New methods `Term.isVariable` and `Term.getVarName` to check whether a term is a variable and to get its name (`getVarName` will return null if the term is not a variable).
* New method `Symbol.isAssoc` to check whether a symbol is associative.
* `Term.search` receives a new keyword argument `strategy` to control the search using a strategy (experimental feature).

Improvements
------------
* Update to Maude alpha136.
* New global function `setRandomSeed` to set the random generator seed at any time.
* Condition fragments obtained from functions in Python are objects of the specific subclass (`EqualityCondition`, `RewriteCondition`, ...) instead of the generic `ConditionFragment`.


Bug fixes
---------

* The condition argument passed to `Term.match` and `Term.search` was destroyed after the completion of these operations, yielding dangling pointers at the user side. Moreover, if the condition belonged to a module statement, the module would be corrupted.
* Missing `hasCondition` and `getCondition` methods in `StrategyDefinition`.
* Partial substitutions (where some variables in the term are not defined by the substitution) caused the library to crash.
* `Module.upStrategy` returned malformed metarepresentations in some cases.

Non-backward compatible changes
-------------------------------

* Iterating through the result of `Term.match` in Python provides a pair of `Substitution` and `Context` instead of only a `Substitution`.
* Assignments in `Substitution` can no longer be accessed by index. Its method `var` has been removed, and `value` now receives a variable instead of an index.

The following Python packages have been uploaded to [PyPI](https://pypi.org/project/maude), and they can be installed with `pip install --upgrade maude`.

`.whl` files can also be directly installed with `pip` for the matching Python version (2.7, 3.6, 3.7, 3.8 and 3.9).

Update to Maude alpha133
------------------------

The Maude version used by the library is now [Maude alpha133](https://github.com/SRI-CSL/Maude/releases/tag/Alpha133). Since the bugs fixed since Maude 3.1 may affect the potential users of the library, it has been packaged with the latest release despite not being stable. However, using the stable version or a different compatible alpha version is still possible, by replacing the `libmaude.so` (Linux), `libmaude.dylib` (macOS) or `libmaude.dll` (Windows) and the `.maude` files in the package directory with that version.

New features
------------

* New method `getMetadata` to obtain the free text `metadata` attribute on `MembershipAxiom`, `Equation`, `Rule`, `RewriteStrategy`, `StrategyDefinition` and the declarations of a `Symbol`. The quotation marks surrounding this text are only trimed in Python, Lua and Java for the moment.
* New method `getLineNumber` to obtain the line number information as printed by Maude on module statements.


Improvements
------------
* In previous versions, the methods `findSort` and `findSymbol` of `Module` expected all special characters in the name to be escaped by backquotes, which is now optional.
* Object to string conversions are now reentrant.


Bug fixes
---------

* Bug fixes in the methods `rewrite`, `frewrite`, `erewrite`, `srewrite` of `Term`, and in `StrategyRewriteGraph`.
* Fixed several memory leaks. ⚠ Warning: memory errors are more likely now when are objects used outside their lifetimes (this mainly affects substitutions returned by searches, which should not survive its iterator).

The following Python packages have been uploaded to [PyPI](https://pypi.org/project/maude), and they can be installed with `pip install --upgrade maude`.

`.whl` files can also be directly installed with `pip` for the matching Python version (2.7, 3.6, 3.7, 3.8 and 3.9).

The following Python packages have been uploaded to [PyPI](https://pypi.org/project/maude), and they can be installed with `pip install --upgrade maude`.

`.whl` files can be directly installed too with `pip` for the matching Python version (2.7, 3.6, 3.7 or 3.8).

Non-backward compatible changes
-------------------------------

* `Module.downModule` is moved to `maude.downModule`, since no module object is required for this operation.

New features
------------

* New metalevel-related functions `Module.downTerm` and `Module.upTerm` to convert back and forth between metarepresented and object-level entities.
* `ModelCheckResult` includes a new field `nrBuchiStates` with the number of states of the Büchi automaton for the negated LTL property.
* `RewriteGraph` and `StrategyRewriteGraph` have a new method `getNrRewrites` to obtain the total number of rewrites spent in extending the rewrite graph.
* Equality testing method `equal` for `Sort`, `Kind`, `Symbol` and `Term`. In Python, the `==` operator can be used as a synomyn of `equal`, and `<=` as `Sort.leq` for subsort inclusion.
* Terms representing integers and floating-point numbers can be converted to their corresponding types of the external programming language using the methods `Term.toInt` and `Term.toFloat`. Integers not fitting in the host type are truncated, and other terms are converted to zero. In Python, the builtin `float` and `int` functions can be used.
* New method `Term.check` to check SMT formulae. Its result is one of the strings `sat`, `unsat` or `undecided`, like in the homonym command, or `None` if the term is not a SMT one.
* New method `Term.prettyPrint` for a more controlled pretty printing of terms, using the `maude.PRINT_*` flags.

Bug fixes
---------

* The strategy passed to `StrategyRewriteGraph` is copied to avoid illegal access when the graph is destroyed.

Experimental features
---------------------

* New feature to define in the external language the behavior of selected Maude operators against equational and rule rewriting. This is achieved using Maude special operators, which are marked by the `special` attribute and whose behavior is defined in the C++ code of the interpreter, instead of equationally or with rules. Here, external languages may extend the `Hook` class with a custom `run` method that get executed when the special symbol is reduced or rewritten.

The following Python packages have been uploaded to [PyPI](https://pypi.org/project/maude), and they can be installed with `pip install --upgrade maude`.

`.whl` files can be directly installed too with `pip` for the matching Python version (2.7, 3.6, 3.7 or 3.8).

Non-backward compatible changes
-------------------------------

+ `StateTransitionGraph` is renamed to `RewriteGraph` and `StrategyTranstionGraph` to `StrategyRewriteGraph`.

New features
------------

* Unification via `Module.unify` and variant unification via `Module.variant_unify`. Both methods receive the unification problem as a list of pairs of terms.
* Variant generation with `Term.get_variants`.
* Narrowing search using `Term.vu_narrow`.
* `Substitution` is extended with two new methods: `instantiate(term)` to instantiate terms, and `find(variableName, sort=None)` to find the value of a variable in a substitution by its name and sort.
* Syntactic sugar for building terms using `Symbol.makeTerm`: `f.makeTerm([t1, t2])` can be written as `f(t1, t2)`.

Bug fixes
---------

* A bug in the `modelCheck` methods that may cause bad results and crashes.
* A mismatched `libmaude.so` version in the 0.3 build may cause unexpected behavior and crashes.

The following Python packages have been uploaded to [PyPI](https://pypi.org/project/maude), and they can be installed with `pip install --upgrade maude`.

`.whl` files can be directly installed too with `pip` for the matching Python version (2.7, 3.6, 3.7 or 3.8).

Non-backward compatible changes
-------------------------------

* Maude-internal vectors returned by observer methods (`Module.getSorts`...) are now read-only.
* `Term.match` receives a Python list of condition fragments instead of an internal vector.
* `Symbol.domainComponent` is renamed to `Symbol.domainKind`.

New features
------------

* [Documentation](https://fadoss.github.io/maude-bindings).
* Terms can be constructed and destructured: `Term.arguments` to iterate their arguments, `Symbol.makeTerm` to build terms, `Module.findSort` and `findSymbol` to find symbols and sorts in a module.
* Access to the Maude LTL model checker and its extension for strategy-controlled systems: `modelCheck` method in `StateTransitionGraph` and `StrategyTransitionGraph`.
* `Module.downStrategy` and `Module.downModule` to get module and strategy expression objects from their metarepresentations.
* Additional methods in some other classes: operator declarations in `Symbol`, sorts in `Kind`...
* The random seed for the `RANDOM` module can now be set in the `maude.init` function.


Bug fixes
---------

* Internal errors in `Term.search` and `StrategyTransitionGraph`.
* `Sort.leq` only worked for symbols in the same kind.