Struct ConsistencyConfig 

pub struct ConsistencyConfig {
    pub timeout_ms: u64,
    pub temporal_bound: u32,
    pub check_vacuity: bool,
    pub check_redundancy: bool,
    pub check_pairwise: bool,
}

Configuration for spec consistency analysis.

Fields

timeout_ms: u64

Z3 timeout per query in milliseconds.

temporal_bound: u32

BMC bound for temporal unrolling (used by orchestrator, not by Z3 checks).

check_vacuity: bool

Whether to check for vacuous implications.

check_redundancy: bool

Whether to check for redundant formulas.

check_pairwise: bool

Whether to identify pairwise conflicts (only runs when UNSAT).

Trait Implementations

impl Clone for ConsistencyConfig

fn clone(&self) -> ConsistencyConfig

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for ConsistencyConfig

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for ConsistencyConfig

fn default() -> Self

Returns the “default value” for a type.