pub enum Predicate {
True,
False,
Approximate {
marker: String,
paths: BTreeSet<String>,
sound_subset: Vec<Guard>,
},
Guard(Guard),
Not(Box<Predicate>),
And(Vec<Predicate>),
Or(Vec<Predicate>),
}Expand description
Typed Boolean formula recovered from template control flow.
Variants§
True
Formula that holds for every input.
False
Formula that holds for no input.
Approximate
A control condition whose exact relation could not be lowered.
The paths remain available for diagnostics and conservative attribution, but consumers must not turn this marker into a narrowing schema condition.
Fields
sound_subset: Vec<Guard>Guards whose conjunction IMPLIES the real condition (a sound subset). Usable only in POSITIVE polarity where firing less often is safe — a fail-arm’s outer condition — never through a negation, which would invert the containment. Empty when no bounded strengthening was recognized.
Guard(Guard)
Exactly lowerable atomic guard.
Not(Box<Predicate>)
Logical negation of a predicate.
And(Vec<Predicate>)
Conjunction of every enclosed predicate.
Or(Vec<Predicate>)
Disjunction of the enclosed predicates.
Implementations§
Source§impl Predicate
impl Predicate
Sourcepub fn truthy_path(path: impl Into<String>) -> Self
pub fn truthy_path(path: impl Into<String>) -> Self
Creates an atomic truthiness predicate for a values path.
Sourcepub fn approximate(marker: impl Into<String>, paths: BTreeSet<String>) -> Self
pub fn approximate(marker: impl Into<String>, paths: BTreeSet<String>) -> Self
Marks an unlowerable condition without inventing a relation between its paths.
Sourcepub fn approximate_with_sound_subset(
marker: impl Into<String>,
paths: BTreeSet<String>,
sound_subset: Vec<Guard>,
) -> Self
pub fn approximate_with_sound_subset( marker: impl Into<String>, paths: BTreeSet<String>, sound_subset: Vec<Guard>, ) -> Self
Marks an unlowerable condition that still admits a bounded sound
strengthening: guards hold only in states where the real condition
holds too.
Sourcepub fn all(predicates: Vec<Self>) -> Self
pub fn all(predicates: Vec<Self>) -> Self
Normalizes a conjunction, collapsing empty and singleton formulas.
Sourcepub fn negated(&self) -> Self
pub fn negated(&self) -> Self
Returns the logical complement without retaining redundant double negation.
Sourcepub fn is_trivial(&self) -> bool
pub fn is_trivial(&self) -> bool
Reports whether the predicate is the constant true or false formula.
Sourcepub fn contains_approximation(&self) -> bool
pub fn contains_approximation(&self) -> bool
Whether this predicate contains a condition that could not be lowered exactly. Returns every values path referenced by the formula.
Sourcepub fn value_paths(&self) -> BTreeSet<String>
pub fn value_paths(&self) -> BTreeSet<String>
Returns every values path referenced by the formula.
Sourcepub fn with_context_predicates(self) -> Vec<Self>
pub fn with_context_predicates(self) -> Vec<Self>
Expands header predicates into the context-selection facts active in their bodies.
Sourcepub fn conditionally_optional_paths(&self) -> BTreeSet<String>
pub fn conditionally_optional_paths(&self) -> BTreeSet<String>
Returns values paths whose branch structure permits them to be absent.
Sourcepub fn contract_guards(&self) -> Vec<Guard>
pub fn contract_guards(&self) -> Vec<Guard>
Projects this formula into the contract guard vocabulary.
Sourcepub fn contract_guards_are_exact(&self) -> bool
pub fn contract_guards_are_exact(&self) -> bool
Whether Self::contract_guards represents this predicate
EXACTLY: the flattened guard conjunction selects the same states.
Negations distribute by De Morgan down to negatable guard leaves;
a negation reaching a leaf the vocabulary cannot flip flattens to
NOTHING, which an And flatten would silently drop — a fail
conjunction missing such a conjunct negates into states the
validator never rejects, so callers keep those conjuncts as raw
predicates instead.
Sourcepub fn contract_guard_stack(predicates: &[Self]) -> Vec<Guard>
pub fn contract_guard_stack(predicates: &[Self]) -> Vec<Guard>
Projects a predicate stack into a deduplicated guard conjunction.