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 mutatorddsmt.mutators_core.EraseNode
.If
self.ident
is set, only nodes with the identifier specified asself.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 asself.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
(useinc
for substitution with smaller, anddec
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 regularcheck-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 byzero_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 azero_extend
by pushing thezero_extend
to the outside and reducing the bit-width, if possible.
- class ddsmt.mutators_bv.BVIteToBVComp
Replace an
ite
of bit-width one withbvcomp
.
- 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
andzero_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.
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
bydistinct
.
- 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 datatypeA
with a constructorC
that has the selectors
. NestingC
ands
like(s (C x))
returnsx
unchanged and we can thus usually replace this expression byx
.
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)
tot
.
- class ddsmt.mutators_strings.StringSimplifyConstant
Replace a string constant by a shorter constant.
- class ddsmt.mutators_strings.StringReplaceAll
Replace
str.replace_all
bystr.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()
andglobal_mutations()
. Instead useyield
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()
returnsFalse
).
Note
Try do identify and avoid possible mutation cycles. Introducing such cycles may result in non-termination.