BinaryReduction
Constants
EraseNode
MergeWithChildren
ReplaceByChild
ReplaceByVariable
SortChildren
CheckSatAssuming
EliminateVariable
InlineDefinedFuns
IntroduceFreshVariable
LetElimination
LetSubstitution
RemoveAnnotation
RemoveRecursiveFunction
SimplifyLogic
SimplifyQuotedSymbols
SimplifySymbolNames
ArithmeticNegateRelation
ArithmeticSimplifyConstant
ArithmeticSplitNaryRelation
ArithmeticStrengthenRelation
BVNormalizeConstants
BVConcatToZeroExtend
BVDoubleNegation
BVElimBVComp
BVEvalExtend
BVExtractConstants
BVExtractZeroExtend
BVIteToBVComp
BVReflexiveNand
BVSimplifyConstants
BVTransformToBool
BVZeroExtendPredicate
BVReduceBW
BVMergeReducedBW
BvMergeExtend
BoolDeMorgan
BoolDoubleNegation
BoolEliminateFalseEquality
BoolEliminateImplication
BoolNegateQuantifier
BoolXOREliminateBinary
BoolXORRemoveConstant
RemoveConstructor
RemoveDatatype
RemoveDatatypeIdentity
FPShortSort
SeqNthUnit
StringSimplifyConstant
StringReplaceAll
StringIndexOfNotFound
StringContainsToConcat
--cross-check
result_differs.py
let
This guide covers some more advanced topics of using ddSMT.