Enum Predicate 

pub enum Predicate {
    True,
    False,
    Approximate {
        marker: String,
        paths: BTreeSet<String>,
        role: ApproximationRole,
        sound_subset: Option<Box<Predicate>>,
    },
    Guard(Guard),
    Not(Box<Predicate>),
    And(Vec<Predicate>),
    Or(Vec<Predicate>),
}

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

marker: String

Stable description of the expression shape that could not be lowered.

paths: BTreeSet<String>

Values paths mentioned by the unlowerable expression.

role: ApproximationRole

Whether the subset describes ordinary execution or returned-value selection.

sound_subset: Option<Box<Predicate>>

A predicate that 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.

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

impl Predicate

pub fn truthy_path(path: impl Into<String>) -> Self

Creates an atomic truthiness predicate for a values path.

pub fn invalid_kind_path(path: impl Into<String>) -> Self

Creates the exact predicate for Sprig’s kindIs "invalid" over a values path.

pub fn approximate(marker: impl Into<String>, paths: BTreeSet<String>) -> Self

Marks an unlowerable condition without inventing a relation between its paths.

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.

pub fn approximate_with_sound_predicate( marker: impl Into<String>, paths: BTreeSet<String>, sound_subset: Self, ) -> Self

Marks an unlowerable condition with a typed predicate that implies it.

pub fn approximate_output_selection( marker: impl Into<String>, paths: BTreeSet<String>, sound_subset: Self, ) -> Self

Marks an inexact returned-value selection with a typed predicate that proves when the candidate supplies the result.

pub fn all(predicates: Vec<Self>) -> Self

Normalizes a conjunction, collapsing empty and singleton formulas.

pub fn negated(&self) -> Self

Returns the logical complement without retaining redundant double negation.

pub fn normalize_boolean(self) -> Self

Canonicalizes an exact Boolean formula without distributive expansion.

Opaque approximate predicates are returned unchanged. Exact formulas use a bounded decision diagram internally and fall back to the input formula if neither normal form stays bounded.

pub fn exactly_implies(&self, consequent: &Self) -> bool

Reports whether this exact Boolean formula entails consequent.

Opaque approximations never prove entailment. The bounded decision diagram may also abstain when either formula exceeds its limits.

pub fn is_trivial(&self) -> bool

Reports whether the predicate is the constant true or false formula.

pub fn contains_approximation(&self) -> bool

Whether this predicate contains a condition that could not be lowered exactly.

pub fn value_paths(&self) -> BTreeSet<String>

Returns every values path referenced by the formula.

pub fn with_context_predicates(self) -> Vec<Self>

Expands header predicates into the context-selection facts active in their bodies.

pub fn conditionally_optional_paths(&self) -> BTreeSet<String>

Returns values paths whose branch structure permits them to be absent.

pub fn contract_guards(&self) -> Vec<Guard>

Projects this formula into the contract guard vocabulary.

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.

pub fn contract_guard_stack(predicates: &[Self]) -> Vec<Guard>

Projects a predicate stack into a deduplicated guard conjunction.

pub fn map_value_paths<F>(self, map: &mut F) -> Self

where F: FnMut(&str) -> String,

Rewrites every values path carried by this formula.

Trait Implementations

impl Clone for Predicate

fn clone(&self) -> Predicate

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Predicate

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

Formats the value using the given formatter.

impl Eq for Predicate

impl From<Guard> for Predicate

fn from(guard: Guard) -> Self

Converts to this type from the input type.

impl Hash for Predicate

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)

where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl Ord for Predicate

fn cmp(&self, other: &Predicate) -> Ordering

This method returns an Ordering between self and other.

fn max(self, other: Self) -> Self

where Self: Sized,

Compares and returns the maximum of two values.

fn min(self, other: Self) -> Self

where Self: Sized,

Compares and returns the minimum of two values.

fn clamp(self, min: Self, max: Self) -> Self

where Self: Sized,

Restrict a value to a certain interval.

impl PartialEq for Predicate

fn eq(&self, other: &Predicate) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl PartialOrd for Predicate

fn partial_cmp(&self, other: &Predicate) -> Option<Ordering>

This method returns an ordering between self and other values if one exists.

fn lt(&self, other: &Rhs) -> bool

Tests less than (for self and other) and is used by the < operator.

fn le(&self, other: &Rhs) -> bool

Tests less than or equal to (for self and other) and is used by the <= operator.

fn gt(&self, other: &Rhs) -> bool

Tests greater than (for self and other) and is used by the > operator.

fn ge(&self, other: &Rhs) -> bool

Tests greater than or equal to (for self and other) and is used by the >= operator.

impl StructuralPartialEq for Predicate