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: .. code-block:: python3 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 :code:`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 (:code:`mutations()`) and global simplifications (:code:`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 :code:`mutations()` constructs **local** replacements for a given **node**. Method :code:`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 :code:`node` is replaced with a simpler node, for example, :code:`(neg (neg a))` is replaced with :code:`a`. For `global mutations`, on the other hand, some :code:`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 ` that apply mutations based on the node structure, :ref:`SMT-LIB mutators ` that deal with certain SMT-LIB constructs, and mutators for individual SMT-LIB theories (:ref:`arithmetic `, :ref:`bit-vectors `, :ref:`boolean `, :ref:`floating-point arithmetic ` and :ref:`strings `). How to Enable and Disable Mutators ---------------------------------- By default, all mutators are enabled. Mutators can be explicitly enabled with command line options of the form :code:`--`, and disabled with options of the form :code:`--no-`, for example, :code:`--no-eliminate-variables`. All mutators from a specific group can by enabled and disabled similarly with :code:`--` and :code:`--no-`, for example, :code:`--no-strings`. If you want to enable a single mutator or mutator group, combine disabling all mutators (:code:`--disable-all`) with enabling a single mutator or group. For example, :code:`--disable-all --bool-de-morgan` or :code:`--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 Datatype Mutators ----------------- .. automodule:: ddsmt.mutators_datatypes 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 contributed 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 ` and :ref:`SMT-LIB ` mutators), and mutators for specific theories (:ref:`arithmetic `, :ref:`bit-vectors `, :ref:`boolean `, :ref:`floating-point arithmetic ` and :ref:`strings `). 1. Identify into which **group** 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 :code:`Mutator` class as a **template**. - **Add** your code to the corresponding :code:`mutators_.py` file. - **Register** your mutator in the :code:`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 :code:`nodes.Node` objects. - If your mutator returns a large number of candidates, do not return them as a list from :code:`mutations()` and :code:`global_mutations()`. Instead use :code:`yield` to turn your mutator into a **generator**. - Add some **unit tests** in :code:`ddsmt/tests/`). This way you can document what your mutator does, and ensure that it keeps working in the future. Also, test that it does not apply to unrelated nodes (i.e., :code:`filter()` returns :code:`False`). .. note:: Try do identify and **avoid** possible mutation **cycles**. Introducing such cycles may result in **non-termination**.