ddSMT
v2.0.2
ddSMT: Delta Debugging for SMT-LIBv2
Installation
Quickstart
How to run ddSMT
How Behavior is Compared with the Golden Run
Full Option Listing
User Guide
Minimization Strategies
The
ddmin
Strategy
The
hierarchical
Strategy
The
hybrid
Strategy
Mutators
How to Enable and Disable Mutators
Generic Mutators
SMT-LIB Mutators
Arithmetic Mutators
Bit-vector Mutators
Boolean Mutators
Datatype Mutators
Floating-Point mutators
String mutators
Writing New Mutators
Common Scenarios
Debugging Unsoundness
Using Option
--cross-check
Using Wrapper Script
result_differs.py
Debugging Performance Issues
Eliminate
let
Binders
How to Speed Up Delta Debugging
How to Identify Which Side is The Bottleneck
The Solver Side is Slow
The ddSMT Side is Slow
Developer Guide
Performance Profiling
Reading profiling data
Contributing
FAQ
References
ddSMT
»
Index
Edit on GitHub
Index
A
|
B
|
C
|
D
|
E
|
F
|
I
|
L
|
M
|
R
|
S
A
ArithmeticNegateRelation (class in ddsmt.mutators_arithmetic)
ArithmeticSimplifyConstant (class in ddsmt.mutators_arithmetic)
ArithmeticSplitNaryRelation (class in ddsmt.mutators_arithmetic)
ArithmeticStrengthenRelation (class in ddsmt.mutators_arithmetic)
B
BinaryReduction (class in ddsmt.mutators_core)
BoolDeMorgan (class in ddsmt.mutators_boolean)
BoolDoubleNegation (class in ddsmt.mutators_boolean)
BoolEliminateFalseEquality (class in ddsmt.mutators_boolean)
BoolEliminateImplication (class in ddsmt.mutators_boolean)
BoolNegateQuantifier (class in ddsmt.mutators_boolean)
BoolXOREliminateBinary (class in ddsmt.mutators_boolean)
BoolXORRemoveConstant (class in ddsmt.mutators_boolean)
BVConcatToZeroExtend (class in ddsmt.mutators_bv)
BVDoubleNegation (class in ddsmt.mutators_bv)
BVElimBVComp (class in ddsmt.mutators_bv)
BVEvalExtend (class in ddsmt.mutators_bv)
BVExtractConstants (class in ddsmt.mutators_bv)
BVExtractZeroExtend (class in ddsmt.mutators_bv)
BVIteToBVComp (class in ddsmt.mutators_bv)
BVMergeReducedBW (class in ddsmt.mutators_bv)
BVNormalizeConstants (class in ddsmt.mutators_bv)
BVReduceBW (class in ddsmt.mutators_bv)
BVReflexiveNand (class in ddsmt.mutators_bv)
BVSimplifyConstants (class in ddsmt.mutators_bv)
BVTransformToBool (class in ddsmt.mutators_bv)
BVZeroExtendPredicate (class in ddsmt.mutators_bv)
C
CheckSatAssuming (class in ddsmt.mutators_smtlib)
Constants (class in ddsmt.mutators_core)
D
ddsmt.mutators_arithmetic
module
ddsmt.mutators_boolean
module
ddsmt.mutators_bv
module
ddsmt.mutators_core
module
ddsmt.mutators_datatypes
module
ddsmt.mutators_fp
module
ddsmt.mutators_smtlib
module
ddsmt.mutators_strings
module
E
EliminateVariable (class in ddsmt.mutators_smtlib)
EraseNode (class in ddsmt.mutators_core)
F
FPShortSort (class in ddsmt.mutators_fp)
I
InlineDefinedFuns (class in ddsmt.mutators_smtlib)
IntroduceFreshVariable (class in ddsmt.mutators_smtlib)
L
LetElimination (class in ddsmt.mutators_smtlib)
LetSubstitution (class in ddsmt.mutators_smtlib)
M
MergeWithChildren (class in ddsmt.mutators_core)
module
ddsmt.mutators_arithmetic
ddsmt.mutators_boolean
ddsmt.mutators_bv
ddsmt.mutators_core
ddsmt.mutators_datatypes
ddsmt.mutators_fp
ddsmt.mutators_smtlib
ddsmt.mutators_strings
R
RemoveAnnotation (class in ddsmt.mutators_smtlib)
RemoveConstructor (class in ddsmt.mutators_datatypes)
RemoveDatatype (class in ddsmt.mutators_datatypes)
RemoveDatatypeIdentity (class in ddsmt.mutators_datatypes)
RemoveRecursiveFunction (class in ddsmt.mutators_smtlib)
ReplaceByChild (class in ddsmt.mutators_core)
ReplaceByVariable (class in ddsmt.mutators_core)
S
SeqNthUnit (class in ddsmt.mutators_strings)
SimplifyLogic (class in ddsmt.mutators_smtlib)
SimplifyQuotedSymbols (class in ddsmt.mutators_smtlib)
SimplifySymbolNames (class in ddsmt.mutators_smtlib)
SortChildren (class in ddsmt.mutators_core)
StringContainsToConcat (class in ddsmt.mutators_strings)
StringIndexOfNotFound (class in ddsmt.mutators_strings)
StringReplaceAll (class in ddsmt.mutators_strings)
StringSimplifyConstant (class in ddsmt.mutators_strings)
Read the Docs
v: v2.0.2
Versions
master
stable
v2.0.2
v2.0.1
Downloads
On Read the Docs
Project Home
Builds