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 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.
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
.
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 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).
Identify into which grou 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/
). For your own sanity, test at least that it does what you expect and 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.