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()).


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.


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.


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 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.


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.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))``


(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.

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.

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

  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).


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