class
CaseDecisionDagA 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:: pair<ClauseIndex, ClauseIndex>> slang:: analysis:: CaseDecisionDag:: overlappingClauses
Contains pairs of indices that overlap, meaning that some inputs match both clauses.
Clauses that are deemed unreachable are not included here.
std:: optional<SVInt> slang:: analysis:: CaseDecisionDag:: counterexample
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.