Module consistency 

Multi-Property Consistency Checking

Check if a set of properties can all hold simultaneously. Conjoin all properties, check Z3 satisfiability. If UNSAT → extract minimal unsatisfiable subset (MUS). If SAT → check for vacuity and redundancy.

Structs

ConsistencyConfig

Configuration for spec consistency analysis.

ConsistencyReport

Full consistency analysis report.

LabeledFormula

A formula labeled with its source text for error reporting.

PairwiseConflict

A pair of formulas that cannot hold simultaneously.

RedundancyFinding

A formula that is logically entailed by the remaining formulas.

VacuityFinding

A formula whose implication antecedent can never be satisfied.

Enums

ConsistencyResult

Result of consistency checking (legacy API).

SatisfiabilityResult

Whether the conjunction of all formulas is satisfiable.

Functions

check_consistency

Check if a set of properties can all hold simultaneously (legacy API).

check_spec_consistency

Run full consistency analysis on a set of labeled formulas.