pub struct DatumSet { /* private fields */ }Expand description
The set of integer values of ONE datum that a conjunction of comparison terms leaves open — an interval with holes, or a pinned point.
This is the arithmetic shared by every question of the form “can this gate
ever open, and at what value?”: Gate::contradiction asks it per gate,
and the compiler’s cast-ladder solver asks it per clause while also
refusing sibling terms (DatumSet::forbid). It lives here, on the gate,
because a gate is the object class the question is about — a copy beside
each asking verb is how two answers to one question start disagreeing.
Determinism (ADR-0006): DatumSet::pick returns one canonical member, a
pure function of the constraint set.
Implementations§
Source§impl DatumSet
impl DatumSet
Sourcepub fn require(&mut self, op: CompareOp, value: i32)
pub fn require(&mut self, op: CompareOp, value: i32)
Intersect with the values that SATISFY op value.
Sourcepub fn forbid(&mut self, op: CompareOp, value: i32)
pub fn forbid(&mut self, op: CompareOp, value: i32)
Intersect with the values that VIOLATE op value — the negation of
DatumSet::require, spelled once so the two can never disagree about
what a term means.
Sourcepub fn min(&self) -> Option<i32>
pub fn min(&self) -> Option<i32>
The smallest value in the set, or None when it is unbounded below
or empty.
The question a price asks: what is the least balance at which this gate
opens? It is the same arithmetic Self::pick does — an interval with
holes, stepped past — asked from the bottom, so the purchase rule
(DW0901) and the satisfiability verdict cannot disagree about what a
term means. equals pins, and a pin is its own floor.
Sourcepub fn max(&self) -> Option<i32>
pub fn max(&self) -> Option<i32>
The largest value in the set, or None when it is unbounded above or
empty — the mirror of Self::min, which is what a refusal arm’s
ceiling is read from.
Sourcepub fn pick(&self) -> Option<i32>
pub fn pick(&self) -> Option<i32>
A deterministic member of the set, or None when the set is empty —
which is the satisfiability verdict.
Complete without enumeration games: an interval-with-holes is nonempty
iff a member exists within holes.len() + 1 steps of a bound (or of 0
when unbounded both ways), because each step is only ever excluded by a
distinct hole.