CaseDecisionDag class
A helper class for building a decision DAG (directed acyclic graph) for case statement exhaustiveness analysis.
The DAG is "built" from a set of case statement clauses, where each clause is an integral constant value.
The DAG is used to determine if a set of clauses covers all possible input values for a given case expression bit width, as well as to identify overlapping and redundant clauses for issuing diagnostics.
Constructors, destructors, conversion operators
-
CaseDecisionDag(std::
span<const SVInt> clauses, uint32_ t bitWidth, bool wildcardX, uint32_ t maxSteps = UINT32_MAX) - Constructs a new case decision DAG.
Public functions
- auto isExhaustive() const -> bool
- Indicates whether the DAG is exhaustive, meaning that all possible input values are covered by the case statement clauses.
Public variables
- flat_hash_set<ClauseIndex> unreachableClauses
- Contains the indices of clauses that are never reachable because some earlier clause subsumes it.
-
flat_hash_set<std::
pair<ClauseIndex, ClauseIndex>> overlappingClauses - Contains pairs of indices that overlap, meaning that some inputs match both clauses.
-
std::
optional<SVInt> counterexample - If the DAG is not exhaustive, this contains a counterexample that demonstrates a value that is not covered by any of the clauses.
- bool gaveUp
- If true, analyzing the case clauses took more than maxSteps and so the analysis was halted.
Variable documentation
flat_hash_set<std::
Contains pairs of indices that overlap, meaning that some inputs match both clauses.
Clauses that are deemed unreachable are not included here.
std::
If the DAG is not exhaustive, this contains a counterexample that demonstrates a value that is not covered by any of the clauses.
Otherwise, this is empty.