guide-mutators.rst

Mutators

.. toctree::
   :maxdepth: 2
   :caption: Contents:

Possible input simplifications are generated by so-called mutators, the drivers of input minimization. Given an S-expression, they may perform small local changes, or introduce global minimizations on the input based on that expression.

Mutator classes must provide the following interface:

class Mutator:
    """Some simplification."""
    def filter(self, node):
        """Check if mutator can be applied to the given node.
         Default: ``True``.
        """
        return True

    def mutations(self, node):
        """Create a list of local mutations of the given node.
        Default: []
        """
        return []

    def global_mutations(self, node, input_):
        """Create a list of mutations of the whole input.
        Default: []
        """
        return []

    def __str__(self):
        """Return a description of this mutator.
        This is (also) used for the command line help message.
        """
        return "some simplification"

Each mutator implements a filter method, which checks if the mutator is applicable to the given S-expression. If it is, the mutator can be queried to suggest (a list of) possible local (mutations()) and global simplifications (global_mutations()).

Note

Mutators are not required to be equivalence or satisfiability preserving. They may extract semantic information from the input when needed, e.g., to infer the sort of a term, to query the set of declared or defined symbols, to extract indices of indexed operators, and more.

Method mutations() constructs local replacements for a given node. Method global_mutations() constructs global replacements for the whole input, given both a specific node and the current input. The concept of local mutations is pretty much self-explanatory, a node is replaced with a simpler node, for example, (neg (neg a)) is replaced with a. For global mutations, on the other hand, some node triggers a simplification that needs to be applied to the whole input at once. For example, when renaming variables or replacing constants that occur multiple times, or when simplifications require adding declarations of new symbols.

Note

Please refer to section :ref:`writing new mutators` for details on how to implement new mutators.

Below follows a list of all available mutators, grouped by their main concern: :ref:`generic mutators <generic mutators>` that apply mutations based on the node structure, :ref:`SMT-LIB mutators <SMT-LIB mutators>` that deal with certain SMT-LIB constructs, and mutators for individual SMT-LIB theories (:ref:`arithmetic <arithmetic mutators>`, :ref:`bit-vectors <bit-vector mutators>`, :ref:`boolean <boolean mutators>`, :ref:`floating-point arithmetic <floating-point mutators>` and :ref:`strings <string mutators>`).

How to Enable and Disable Mutators

By default, all mutators are enabled.

Mutators can be explicitly enabled with command line options of the form --<mutator>, and disabled with options of the form --no-<mutator>, for example, --no-eliminate-variables.

All mutators from a specific group can by enabled and disabled similarly with --<group> and --no-<group>, for example, --no-strings.

If you want to enable a single mutator or mutator group, combine disabling all mutators (--disable-all) with enabling a single mutator or group. For example, --disable-all --bool-de-morgan or --disable-all --strings).

Generic Mutators

.. automodule:: ddsmt.mutators_core

SMT-LIB Mutators

.. automodule:: ddsmt.mutators_smtlib

Arithmetic Mutators

.. automodule:: ddsmt.mutators_arithmetic

Bit-vector Mutators

.. automodule:: ddsmt.mutators_bv

Boolean Mutators

.. automodule:: ddsmt.mutators_boolean

Floating-Point mutators

.. automodule:: ddsmt.mutators_fp

String mutators

.. automodule:: ddsmt.mutators_strings

Writing New Mutators

If you need a certain simplification that is not covered by existing mutators, it's easy to add your own mutator. If it is of general interest, we'd be happy if you contribute it back to ddSMT. The following instructions aim to provide a guide on what needs to be done and what you should consider when adding a new mutator.

Generally, mutators are organized into mutators for general purpose (:ref:`generic <generic mutators>` and :ref:`SMT-LIB <smt-lib mutators>` mutators), and mutators for specific theories (:ref:`arithmetic <arithmetic mutators>`, :ref:`bit-vectors <bit-vector mutators>`, :ref:`boolean <boolean mutators>`, :ref:`floating-point arithmetic <floating-point mutators>` and :ref:`strings <string mutators>`).

1. Identify into which grou your new mutator fits best.
2. Determine if you need to have a global view on the input, or if local mutations of a single node suffice. Prefer local mutations over global mutations if possible.
3. Implement the mutator following these guidelines:

• Use the above Mutator class as a template.
• Add your code to the corresponding mutators_<group>.py file.
• Register your mutator in the get_mutators() function towards the end of the file.
• Make sure your mutator is reasonably fast.
• Make sure that your mutator (mostly) generates valid SMT-LIB constructs.
• Make sure to return a list of nodes.Node objects.
• If your mutator returns a large number of candidates, do not return them as a list from mutations() and global_mutations(). Instead use yield to turn your mutator into a generator.
• Add some unit tests in ddsmt/tests/). For your own sanity, test at least that it does what you expect and does not apply to unrelated nodes (i.e., filter() returns False).

Note

Try do identify and avoid possible mutation cycles. Introducing such cycles may result in non-termination.