Mutators

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 Writing New Mutators for details on how to implement new mutators.

Below follows a list of all available mutators, grouped by their main concern: generic mutators that apply mutations based on the node structure, SMT-LIB mutators that deal with certain SMT-LIB constructs, and mutators for individual SMT-LIB theories (arithmetic, bit-vectors, boolean, floating-point arithmetic and 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 --<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

class ddsmt.mutators_core.BinaryReduction

Binary reduction on the top level node.

This mutator mimics what strategy ddmin achieves when applying mutator ddsmt.mutators_core.EraseNode.

If self.ident is set, only nodes with the identifier specified as self.ident are considered.

Note

This mutator is always disabled for strategy ddmin.

class ddsmt.mutators_core.Constants

Replace given node with a default value of the same sort.

Default values are defined in ddsmt.smtlib.get_default_constants().

class ddsmt.mutators_core.EraseNode

Erase given node.

If self.ident is set, only nodes with the identifier specified as self.ident are considered.

class ddsmt.mutators_core.MergeWithChildren

Merge given node with one of its children.

This mutator can only be applied to n-ary operations like and or +.

class ddsmt.mutators_core.ReplaceByChild: Replace given node with one of its children.

class ddsmt.mutators_core.ReplaceByVariable: Replace given node with an existing variable of the same type.

Note

Replacing variables with other variables potentially introduces cycles. To avoid this, for leaf nodes we only allow substitutions with variables that are lexicographically smaller (default) or larger than the leaf mode. Configure with option --replace-by-variable-mode (use inc for substitution with smaller, and dec for substition with larger variables).

class ddsmt.mutators_core.SortChildren: Sort the children of a given node by size (count of sub-nodes).

SMT-LIB Mutators

class ddsmt.mutators_smtlib.CheckSatAssuming

Replace check-sat-assuming with a regular check-sat.

This discards any assumptions provided to check-sat-assuming.

class ddsmt.mutators_smtlib.EliminateVariable

Eliminate variables that occur as children of equalities.

Globally replace every leaf node from an equality with every other node from the same equality. For example, for (= x (* a b) (+ c d)), x is replaced with either (* a b) or (+ c d).

class ddsmt.mutators_smtlib.InlineDefinedFuns: Explicitly inline a defined function.

class ddsmt.mutators_smtlib.IntroduceFreshVariable: Replace a term by a fresh variable of the same sort.

class ddsmt.mutators_smtlib.LetElimination: Substitute a let expression with its body.

class ddsmt.mutators_smtlib.LetSubstitution: Substitute a variable bound by a let binder into the nested term.

class ddsmt.mutators_smtlib.RemoveAnnotation: Remove an annotation (! t ...) from a term.

class ddsmt.mutators_smtlib.RemoveRecursiveFunction: Remove a function from a recursive function definition.

class ddsmt.mutators_smtlib.SimplifyLogic: Replace the logic specified in (check-logic ...) with a simpler one.

class ddsmt.mutators_smtlib.SimplifyQuotedSymbols: Turn a quoted symbol into a simple symbol.

class ddsmt.mutators_smtlib.SimplifySymbolNames

Simplify variable names.

This only has cosmetic impact except for cases where variable names are compared/ordered lexicographically (it may enable, for example, the application of mutator ddsmt.mutators_core.ReplaceByVariable).

Arithmetic Mutators

class ddsmt.mutators_arithmetic.ArithmeticNegateRelation

Replace a negated relation by the corresponding inverse relation.

For example, (not (< a b)) is replaced with (>= a b).

class ddsmt.mutators_arithmetic.ArithmeticSimplifyConstant

Replace a constant with a simpler constant.

We consider constants that are smaller (in value) or with fewer decimal places as simpler.

class ddsmt.mutators_arithmetic.ArithmeticSplitNaryRelation

Split an n-ary relation into the conjunction of multiple relations.

This assumes that the relation symbol is transitive.

class ddsmt.mutators_arithmetic.ArithmeticStrengthenRelation

Replace a relation by a stronger relation.

For example, >= is replaced by >.

Bit-vector Mutators

class ddsmt.mutators_bv.BVNormalizeConstants: Normalize bit-vector constants to be represented using the (_ bvN M) notation.

class ddsmt.mutators_bv.BVConcatToZeroExtend: Replace a concat with zero by zero_extend.

class ddsmt.mutators_bv.BVDoubleNegation: Eliminate double bit-vector negations.

class ddsmt.mutators_bv.BVElimBVComp

Replace equality over bvcomp and constant with a regular equality.

For example, (= (bvcomp a b) #b1) is replaced with (= a b).

class ddsmt.mutators_bv.BVEvalExtend: Evaluate a bit-vector (sign|zero)_extend if it is applied to a constant or another (sign|zero)_extend.

class ddsmt.mutators_bv.BVExtractConstants: Evaluate a bit-vector extract if it is applied to a constant.

class ddsmt.mutators_bv.BVExtractZeroExtend: Simplify an extract of a zero_extend by pushing the zero_extend to the outside and reducing the bit-width, if possible.

class ddsmt.mutators_bv.BVIteToBVComp: Replace an ite of bit-width one with bvcomp.

class ddsmt.mutators_bv.BVReflexiveNand: Replace a reflexive bvnand by bitwise negation.

class ddsmt.mutators_bv.BVSimplifyConstants: Replace a bit-vector constant with a simpler constant of smaller value.

class ddsmt.mutators_bv.BVTransformToBool

Turn bit-vector operators into Boolean operators.

For example, transform (= bv1 (bvor X Y)) into (or (= bv1 X) (= bv1 Y)).

class ddsmt.mutators_bv.BVZeroExtendPredicate

Eliminate zero_extend when both operands of an equality, disequality or inequality are zero extended.

For example, transform (= ((_ zero_extend 2) a) ((_ zero_extend 2) b)) into (= a b), and (= ((_ zero_extend 2) a) ((_ zero_extend 4) b)) into (= a ((_ zero_extend 2 b))).

class ddsmt.mutators_bv.BVReduceBW

Reduce the bit-width of a variable by introducing an extract and zero_extend on that variable.

For example, (declare-const v (_ BitVec 32)) is transformed into

(declare-const _v (_BitVec 1))
(define-fun v () (_ BitVec 32) ((_ zero_extend 31) _v))

class ddsmt.mutators_bv.BVMergeReducedBW

Merge previous bit-width reductions of the form.

(declare-const __w (_BitVec MM))
(define-fun _w () (_ BitVec Y) ((_ zero_extend N) __w))
(define-fun w () (_ BitVec X) ((_ zero_extend M) _w))``

into

(declare-const __w (_BitVec MM))
(define-fun _w () (_ BitVec Y) ((_ zero_extend N) __w))
(define-fun w () (_ BitVec X) ((_ zero_extend M+N) __w))

Obsolete define-fun expressions will be removed later on.

class ddsmt.mutators_bv.BvMergeExtend

Merge nested zero_extend/sign_extend terms.

For example, ((_ zero_extend 5) ((_ zero_extend 4) x)) is transformed into ((zero_extend 9) x).

Boolean Mutators

class ddsmt.mutators_boolean.BoolDeMorgan: Use de Morgans rules to push negations inside.

class ddsmt.mutators_boolean.BoolDoubleNegation: Eliminate double negations.

class ddsmt.mutators_boolean.BoolEliminateFalseEquality

Replace an equality with false by a negation.

For example, transform (= false X) into (not X).

class ddsmt.mutators_boolean.BoolEliminateImplication: Replace (possibly n-ary) implications by disjunctions.

class ddsmt.mutators_boolean.BoolNegateQuantifier: Push negations inside quantifiers.

class ddsmt.mutators_boolean.BoolXOREliminateBinary: Eliminate binary xor by distinct.

class ddsmt.mutators_boolean.BoolXORRemoveConstant: Eliminate constant children from xor.

Datatype Mutators

class ddsmt.mutators_datatypes.RemoveConstructor: Remove a single datatype constructor.

class ddsmt.mutators_datatypes.RemoveDatatype: Remove a datatype from a recursive datatype declaration.

class ddsmt.mutators_datatypes.RemoveDatatypeIdentity: Remove a datatype constructor and selector that are nested to function as the identify. For (declare-datatype (A 0) ((C (s A)))) we have the datatype A with a constructor C that has the selector s. Nesting C and s like (s (C x)) returns x unchanged and we can thus usually replace this expression by x.

Floating-Point mutators

class ddsmt.mutators_fp.FPShortSort

Replace long sort names with short names.

(_ FloatingPoint 5 11)   --> Float16
(_ FloatingPoint 8 24)   --> Float32
(_ FloatingPoint 11 53)  --> Float64
(_ FloatingPoint 15 113) --> Float128

String mutators

class ddsmt.mutators_strings.SeqNthUnit: Simplify (seq.nth (seq.unit t) 0) to t.

class ddsmt.mutators_strings.StringSimplifyConstant: Replace a string constant by a shorter constant.

class ddsmt.mutators_strings.StringReplaceAll: Replace str.replace_all by str.replace.

class ddsmt.mutators_strings.StringIndexOfNotFound: Replace str.indexof by special value (- 1) indicating that the substring was not found.

class ddsmt.mutators_strings.StringContainsToConcat: Replace str.contains by concatenation.

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 (generic and SMT-LIB mutators), and mutators for specific theories (arithmetic, bit-vectors, boolean, floating-point arithmetic and strings).

Identify into which group your new mutator fits best.
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.
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/). 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., filter() returns False).

Note

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