Module matching_loop

smt_scope::analysis::analysis

Module matching_loop 

Source

Structs§

CollectedBlame
GenIdx
GeneralisedBlame
MatchingLoop
MlAnalysis
MlAnalysisInfo
MlData
MlGraph
MlLeaves
MlLinkInfo
MlNodeInfo
MlOutput
MlSigCollection
Collection of instantiations all with the same ML signature, grouped by generalisations along with a set of unknown generalisations.
MlSigIdx
MlSignature
SimpIdx

Enums§

InstParent
For each pattern in the matched pattern, where did the blamed term come from? This will rule out a chain of instantiations which always requires new terms as each instantiation will have a different InstParent. Instantiation chains which all depend on a single term will have the same InstParent.
MLGraphEdge
MLGraphNode
MlLinkLeaf
RecurrenceKind

Constants§

MIN_MATCHING_LOOP_LENGTH
MIN_SUSPICIOUS_CHAIN_LENGTH

Type Aliases§

MlEndNodes
MlExplanation