pub struct GuardDnf(/* private fields */);Expand description
Disjunction of conjunctions of typed predicates.
Construction removes impossible conjunctions and normalizes exact complementary resolution, absorption, and deduplication.
Implementations§
Source§impl GuardDnf
impl GuardDnf
Sourcepub fn unconditional() -> Self
pub fn unconditional() -> Self
Returns the formula that accepts every input.
Sourcepub fn from_conjunction(predicates: impl IntoIterator<Item = Predicate>) -> Self
pub fn from_conjunction(predicates: impl IntoIterator<Item = Predicate>) -> Self
Builds a normalized DNF from one predicate conjunction.
Sourcepub fn from_guards(guards: impl IntoIterator<Item = Guard>) -> Self
pub fn from_guards(guards: impl IntoIterator<Item = Guard>) -> Self
Builds a normalized DNF from one guard conjunction.
Sourcepub fn from_guard_disjunction(
conjunctions: impl IntoIterator<Item = impl IntoIterator<Item = Guard>>,
) -> Self
pub fn from_guard_disjunction( conjunctions: impl IntoIterator<Item = impl IntoIterator<Item = Guard>>, ) -> Self
Builds a normalized DNF from guard conjunction alternatives.
Sourcepub fn from_contract_predicate_disjunction(
conjunctions: impl IntoIterator<Item = impl IntoIterator<Item = Predicate>>,
) -> Self
pub fn from_contract_predicate_disjunction( conjunctions: impl IntoIterator<Item = impl IntoIterator<Item = Predicate>>, ) -> Self
Project typed predicate branches to the contract-expressible guard vocabulary while retaining their disjunction as one row condition.
Sourcepub fn from_contract_predicate_disjunction_preserving_evidence(
conjunctions: impl IntoIterator<Item = impl IntoIterator<Item = Predicate>>,
) -> Self
pub fn from_contract_predicate_disjunction_preserving_evidence( conjunctions: impl IntoIterator<Item = impl IntoIterator<Item = Predicate>>, ) -> Self
Retain projected alternatives until their downstream evidence payloads can be compared; early resolution can erase a nullable or strict arm.
Sourcepub fn from_contract_predicate_conjunction(
predicates: impl IntoIterator<Item = Predicate>,
) -> Self
pub fn from_contract_predicate_conjunction( predicates: impl IntoIterator<Item = Predicate>, ) -> Self
Projects one predicate conjunction into contract guards.
Sourcepub fn normalize_conditional_guard_disjunction(
conjunctions: impl IntoIterator<Item = impl IntoIterator<Item = ConditionalGuard>>,
) -> Vec<Vec<ConditionalGuard>>
pub fn normalize_conditional_guard_disjunction( conjunctions: impl IntoIterator<Item = impl IntoIterator<Item = ConditionalGuard>>, ) -> Vec<Vec<ConditionalGuard>>
Canonicalizes a disjunction of conditional-guard conjunctions.
Sourcepub fn from_disjunction(
conjunctions: impl IntoIterator<Item = impl IntoIterator<Item = Predicate>>,
) -> Self
pub fn from_disjunction( conjunctions: impl IntoIterator<Item = impl IntoIterator<Item = Predicate>>, ) -> Self
Builds and minimizes a DNF from predicate conjunction alternatives.
Sourcepub fn is_unconditional(&self) -> bool
pub fn is_unconditional(&self) -> bool
Reports whether the formula accepts every input.
Sourcepub fn disjuncts(&self) -> &BTreeSet<BTreeSet<Predicate>>
pub fn disjuncts(&self) -> &BTreeSet<BTreeSet<Predicate>>
Returns normalized predicate conjunctions in stable order.
Sourcepub fn guard_conjunctions(&self) -> Vec<Vec<Guard>>
pub fn guard_conjunctions(&self) -> Vec<Vec<Guard>>
Projects each predicate conjunction into serializable contract guards.
Sourcepub fn single_guard_conjunction(&self) -> Option<Vec<Guard>>
pub fn single_guard_conjunction(&self) -> Option<Vec<Guard>>
Returns the sole projected guard conjunction, if exactly one exists.
Sourcepub fn conjoined(&self, other: &Self) -> Self
pub fn conjoined(&self, other: &Self) -> Self
Returns the conjunction of this formula and other.
Sourcepub fn conjoined_with_guards(
&self,
guards: impl IntoIterator<Item = Guard>,
) -> Self
pub fn conjoined_with_guards( &self, guards: impl IntoIterator<Item = Guard>, ) -> Self
Conjoins this formula with one guard conjunction.
Sourcepub fn union_preserving_disjuncts(&mut self, other: Self)
pub fn union_preserving_disjuncts(&mut self, other: Self)
Adds alternatives without absorbing subsets that may carry distinct evidence.
Sourcepub fn union_absorbing(&mut self, other: Self)
pub fn union_absorbing(&mut self, other: Self)
Union conditions after their evidence payloads are known to be
equal, re-normalizing so duplicate and subsumed disjuncts are
absorbed (unlike Self::union_preserving_disjuncts).