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.