List of all items

Structs

• BigRational
• BigUint
• F64Ord
• FxHashMap
• FxHashSet
• Graph
• IString
• NonMaxU32
• NonMaxUsize
• StringTable
• TiVec
• analysis::AllAnalyses
• analysis::AssignData
• analysis::CdclAnalysis
• analysis::DirectDep
• analysis::InstGraph
• analysis::InstsInfo
• analysis::LogInfo
• analysis::MatchesInfo
• analysis::ProblemBehaviour
• analysis::ProblemBehaviours
• analysis::ProofAnalysis
• analysis::QuantPatInfo
• analysis::QuantRedundancy
• analysis::QuantifierAnalysis
• analysis::QuantsInfo
• analysis::RawEdgeIndex
• analysis::RawNodeIndex
• analysis::RedundancyAnalysis
• analysis::VisibleEdgeIndex
• analysis::VisibleNodeIndex
• analysis::analysis::Analysis
• analysis::analysis::OrderingAnalysis
• analysis::analysis::cost::DefaultCost
• analysis::analysis::cost::ProofCost
• analysis::analysis::depth::DefaultDepth
• analysis::analysis::matching_loop::CollectedBlame
• analysis::analysis::matching_loop::GenIdx
• analysis::analysis::matching_loop::GeneralisedBlame
• analysis::analysis::matching_loop::MatchingLoop
• analysis::analysis::matching_loop::MlAnalysis
• analysis::analysis::matching_loop::MlAnalysisInfo
• analysis::analysis::matching_loop::MlData
• analysis::analysis::matching_loop::MlGraph
• analysis::analysis::matching_loop::MlLeaves
• analysis::analysis::matching_loop::MlLinkInfo
• analysis::analysis::matching_loop::MlNodeInfo
• analysis::analysis::matching_loop::MlOutput
• analysis::analysis::matching_loop::MlSigCollection
• analysis::analysis::matching_loop::MlSigIdx
• analysis::analysis::matching_loop::MlSignature
• analysis::analysis::matching_loop::SimpIdx
• analysis::analysis::next_nodes::NextInstsInit
• analysis::analysis::proof::ProofInitialiser
• analysis::analysis::reconnect::BwdReachableAnalysis
• analysis::analysis::reconnect::ReachNonDisabled
• analysis::analysis::reconnect::ReachVisible
• analysis::analysis::reconnect::ReconnectAnalysis
• analysis::analysis::reconnect::ReconnectData
• analysis::analysis::reconnect::ReconnectEdge
• analysis::analysis::reconnect::ReconnectFrom
• analysis::raw::Depth
• analysis::raw::GraphStats
• analysis::raw::Neighbors
• analysis::raw::NextNodes
• analysis::raw::Node
• analysis::raw::ProofReach
• analysis::raw::RawEdgeIndex
• analysis::raw::RawInstGraph
• analysis::raw::RawIx
• analysis::raw::RawNodeIndex
• analysis::raw::WalkNeighbors
• analysis::subgraph::Subgraph
• analysis::subgraph::Subgraphs
• analysis::subgraph::VisitBox
• analysis::visible::VisibleEdgeIndex
• analysis::visible::VisibleInstGraph
• analysis::visible::VisibleIx
• analysis::visible::VisibleNode
• analysis::visible::VisibleNodeIndex
• display_with::DisplayConfiguration
• display_with::DisplayCtxt
• display_with::DisplayWrapperData
• display_with::DisplayWrapperEmpty
• display_with::VarName
• formatter::BindPowerPair
• formatter::ChildIndex
• formatter::ChildPath
• formatter::ChildRange
• formatter::DeParse
• formatter::FallbackFormatter
• formatter::Formatter
• formatter::FormatterConst
• formatter::MatchResult
• formatter::Matcher
• formatter::MatcherConst
• formatter::ParseError
• formatter::ParseErrorConst
• formatter::RegexMatcher
• formatter::SubFormatterRepeat
• formatter::SubFormatterRepeatConst
• formatter::SubFormatterRepeatSeparator
• formatter::SubFormatterSingle
• formatter::SubFormatterString
• formatter::TermDisplay
• formatter::TermDisplayConst
• formatter::TermDisplayContext
• items::Assignment
• items::BitVec
• items::Blame
• items::BoundVars
• items::Cdcl
• items::CdclBacklink
• items::CdclIdx
• items::Conflict
• items::ENode
• items::ENodeIdx
• items::EqGivenIdx
• items::EqTransIdx
• items::Equality
• items::Fingerprint
• items::GraphIdx
• items::InstIdx
• items::Instantiation
• items::Justification
• items::LitIdx
• items::Literal
• items::Match
• items::MatchIdx
• items::PatVec
• items::PatternIdx
• items::ProofIdx
• items::ProofStep
• items::ProofStepKindIter
• items::QuantIdx
• items::QuantPat
• items::QuantPatVec
• items::Quantifier
• items::StackFrame
• items::StackIdx
• items::Term
• items::TermId
• items::TermIdToIdxMap
• items::TermIdx
• items::TimeRange
• items::TransitiveExpl
• items::TransitiveExplSegment
• parsers::AsyncParser
• parsers::ReaderState
• parsers::StreamParser
• parsers::z3::ParseErrors
• parsers::z3::Z3Parser
• parsers::z3::cdcl::CdclTree
• parsers::z3::cdcl::DeadBranch
• parsers::z3::cdcl::Literals
• parsers::z3::egraph::EGraph
• parsers::z3::egraph::Equalities
• parsers::z3::egraph::Graph
• parsers::z3::egraph::SimplePath
• parsers::z3::egraph::TransEqStopWalker
• parsers::z3::inst::InstData
• parsers::z3::inst::Insts
• parsers::z3::smt2::Event
• parsers::z3::smt2::EventLog
• parsers::z3::stack::Stack
• parsers::z3::synthetic::DefStIdx
• parsers::z3::synthetic::SynthIdx
• parsers::z3::synthetic::SynthTerm
• parsers::z3::synthetic::SynthTerms
• parsers::z3::terms::TermStorage
• parsers::z3::terms::Terms

Enums

• BoxSlice
• Error
• FatalError
• analysis::PbKind
• analysis::analysis::matching_loop::InstParent
• analysis::analysis::matching_loop::MLGraphEdge
• analysis::analysis::matching_loop::MLGraphNode
• analysis::analysis::matching_loop::MlLinkLeaf
• analysis::analysis::matching_loop::RecurrenceKind
• analysis::raw::CdclEdge
• analysis::raw::EdgeKind
• analysis::raw::NodeKind
• analysis::raw::NodeState
• analysis::visible::VisibleEdge
• analysis::visible::VisibleEdgeKind
• display_with::SymbolReplacement
• formatter::ConversionError
• formatter::EitherError
• formatter::FallbackParseError
• formatter::FormatterError
• formatter::MatcherError
• formatter::MatcherKind
• formatter::MatcherKindConst
• formatter::SubFormatter
• formatter::SubFormatterConst
• formatter::TdcError
• items::CdclKind
• items::Coupling
• items::ENodeBlame
• items::EqualityExpl
• items::InstProofLink
• items::InstantiationKind
• items::JustificationKind
• items::MatchKind
• items::Meaning
• items::ProofStepKind
• items::QuantKind
• items::TermKind
• items::TermKindInner
• items::TheoryKind
• items::TimeRangeStatus
• items::TransitiveExplIter
• items::TransitiveExplSegmentKind
• items::VarNames
• parsers::ParseState
• parsers::z3::VersionInfo
• parsers::z3::egraph::Never
• parsers::z3::smt2::EventKind
• parsers::z3::synthetic::AnyTerm
• parsers::z3::synthetic::SynthTermKind

Traits

• analysis::analysis::cost::CostInitialiser
• analysis::analysis::depth::DepthInitialiser
• analysis::analysis::reconnect::ReachKind
• analysis::analysis::run::CollectInitialiser
• analysis::analysis::run::Initialiser
• analysis::analysis::run::TopoAnalysis
• analysis::analysis::run::TransferInitialiser
• analysis::raw::IndexesInstGraph
• display_with::DisplayWithCtxt
• formatter::DeParseTrait
• parsers::AsyncBufferRead
• parsers::AsyncCursorRead
• parsers::CursorRead
• parsers::FileRead
• parsers::IntoAsyncParser
• parsers::IntoStreamParser
• parsers::LogParser
• parsers::LogParserHelper
• parsers::z3::Z3LogParser
• parsers::z3::egraph::EqualityWalker
• parsers::z3::stack::HasFrame
• parsers::z3::synthetic::TermWalker
• parsers::z3::terms::HasTermId

Macros

• analysis::graph_idx
• graph_idx
• idx
• items::idx

Functions

• analysis::run_all

Type Aliases

• DiGraph
• FResult
• Result
• UnGraph
• analysis::analysis::matching_loop::MlEndNodes
• analysis::analysis::matching_loop::MlExplanation
• formatter::BindPower
• formatter::FormatterParseError
• formatter::MatcherParseError
• formatter::ResultConst
• formatter::ResultFormatterConst
• formatter::ResultMatcherConst
• formatter::TermDisplayContextParts
• items::EqGivenUse
• parsers::z3::AstSize
• parsers::z3::egraph::TransEqSimpleWalker

Constants

• analysis::analysis::matching_loop::MIN_MATCHING_LOOP_LENGTH
• analysis::analysis::matching_loop::MIN_SUSPICIOUS_CHAIN_LENGTH
• formatter::BINARY_OP
• formatter::CONTROL_CHARACTER
• formatter::DEFAULT_BIND_POWER
• formatter::DEFAULT_FORMATTER
• formatter::IF
• formatter::NEG
• formatter::QUANT_BIND
• formatter::SEPARATOR_CHARACTER
• formatter::S_EXPRESSION
• formatter::S_EXPRESSION_LEAF
• formatter::S_EXPRESSION_PATTERN
• formatter::TRIGGER
• formatter::UNARY_OP
• parsers::z3::smt2::M_PREDEF_NAMES