Struct ConditionModel 

pub struct ConditionModel {
    pub conditions: HashMap<String, ConditionExpr>,
    pub parameters: HashMap<String, ParameterInfo>,
    pub mutex_groups: Vec<MutexGroup>,
    pub implications: Vec<Implication>,
    /* private fields */
}

Fields

conditions: HashMap<String, ConditionExpr>

parameters: HashMap<String, ParameterInfo>

mutex_groups: Vec<MutexGroup>

implications: Vec<Implication>

Implementations

impl ConditionModel

pub fn from_ir( ir: &TemplateIR, parameters: &HashMap<String, ParameterInfo>, pseudo_overrides: &PseudoParameterOverrides, mappings: &MappingData, ) -> Self

pub fn is_satisfiable(&self, assumptions: &[(String, bool)]) -> bool

Decides whether the given condition assumptions can hold simultaneously.

A condition is a pure function of the template’s parameters, pseudo-parameters, and mappings, so the assumptions hold exactly when some assignment of concrete values to the parameters they read makes every assumed condition take its assumed value. The search is over those parameter assignments, which is why its cost tracks how many independent inputs a template really has rather than how many conditions are layered over them.

On inputs that exhaust a search budget this degrades to a conservative true (assume satisfiable). Whether that conservative answer adds or suppresses a diagnostic depends on how each caller uses the result, so “conservative” is not safe in one fixed direction. The callers below are examples, not an exhaustive list:

• Used directly (conditions_compatible, resources_compatible, and the scenario-reachability filters in resolve_scenarios_json and the schema validator) a conservative true treats two conditions as able to coexist / a scenario as reachable, so it keeps a pair or scenario a full search might have eliminated - at worst surfacing an extra (false-positive) diagnostic.
• Used negated to prove unreachability (find_unreachable_branches, which emits when !is_satisfiable(branch_assumptions)) a conservative true makes the branch look reachable and therefore suppresses an unreachable-branch diagnostic - a false negative, the opposite direction.
• Used negated to prove implication (condition_implies, i.e. !is_satisfiable(a = true, b = false); the conditional-reference guard uses the same shape) a conservative true flips the result to “does not imply”, which can surface an extra (false-positive) diagnostic.

All of these occur only on adversarial inputs that exhaust the budget; valid templates resolve well within budget and are unaffected. Reaching a budget is recorded (see Self::budget_exhausted_queries) so a curtailed analysis is reported rather than silently narrowing what validation proves.

A condition the parameters cannot decide - one comparing a value the model cannot resolve, or sitting on a reference cycle - is treated as compatible with any assumption about it, the same conservative direction.

pub fn satisfiability(&self, assumptions: &[(String, bool)]) -> Satisfiability

Decides satisfiability without conflating a budget-curtailed search with an exact satisfiable result. Proof-producing callers must require Satisfiability::Satisfiable; callers that use satisfiability only as a conservative reachability guard can continue using Self::is_satisfiable.

pub fn is_satisfiable_in_region( &self, assumptions: &[(String, bool)], region: &str, ) -> bool

Like Self::is_satisfiable, but with the target region pinned as the only candidate value for the AWS::Region pseudo-parameter - a per-region satisfiability query that asks whether a condition can hold in that region, not whether the region could be anything. Used by the region-availability check so a resource guarded by a condition that cannot hold in the target region (e.g. !Equals [AWS::Region, other-region]) is correctly treated as never created there - even when no explicit --region override pins the pseudo-parameter globally (where it stays a free variable to avoid false unreachable-branch diagnostics).

pub fn satisfiability_budget_exhausted(&self) -> bool

Whether this model has spent its cumulative satisfiability search budget. Callers that drive many queries (the pairwise compatibility pass) check this to stop early once further queries would only return the conservative answer.

pub fn sat_iterations_used(&self) -> u64

Cumulative satisfiability search steps consumed by this model so far.

pub fn budget_exhausted_queries(&self) -> Vec<String>

pub fn conditions_compatible(&self, cond_a: &str, cond_b: &str) -> bool

pub fn condition_implies(&self, cond_a: &str, cond_b: &str) -> bool

pub fn resources_compatible( &self, cond_a: Option<&str>, cond_b: Option<&str>, ) -> bool

pub fn get(&self, name: &str) -> Option<&ConditionExpr>

pub fn names(&self) -> impl Iterator<Item = &str>

pub fn tautological_equals(&self) -> Vec<(String, bool)>

pub fn referenced_params(&self) -> Vec<String>

pub fn register_inline(&mut self, name: String, expr: ConditionExpr)

pub fn register_inline_batch( &mut self, items: impl IntoIterator<Item = (String, ConditionExpr)>, )

Registers many inline conditions at once, recomputing the derived mutex groups and implications a single time. Registering a large batch through register_inline would recompute them per insertion (quadratic).

pub fn register_rule_implications( &mut self, arena: &Arena, rules: &[(String, NodeRef, Vec<NodeRef>)], )

pub fn undefined_condition_refs(&self) -> Vec<(String, String)>

pub fn invalid_condition_bodies(&self) -> Vec<String>

Names of top-level conditions whose body does not produce a boolean (e.g. a bare Fn::Ref), for the not-a-boolean condition diagnostic. Synthetic conditions (__-prefixed) are excluded - they are never user-visible. Returned sorted for deterministic diagnostic ordering.

pub fn detect_cycles(&self) -> Vec<Vec<String>>

pub fn detect_equivalent_conditions(&self) -> Vec<(String, String)>

Trait Implementations

impl Debug for ConditionModel

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

Formats the value using the given formatter.