pub fn definite_property_implications(premises: &[ProofExpr]) -> Vec<ProofExpr>Expand description
“The unique D-trip has property P.” Each single-∃ definite-description clue
∃x(D(x) ∧ … ∧ P(x)) whose anchor D is a SINGLETON grid value (it carries an
Exactly one … premise, so the description denotes a unique row) entails the
propagatable rule ∀t(D(t) → P(t)); when P is ALSO a singleton value the
biconditional ∀t(P(t) → D(t)) too — e.g. “the Florida trip is the hunting trip”
⇒ In(t,Florida) ↔ Hunt(t). Sound: a singleton value names a unique row, so any row
holding it IS that row and therefore carries the clue’s property. This replaces the
existential (whose sort-aware grounding still explodes to a row-disjunction) with
row-indexed implications the incremental solver propagates.
Structural only — singleton-ness is read from the Exactly one premises, never the
literal value names — so it is not specific to any one puzzle. Nested ∃x∃y
of-pair clues are left untouched (they ground to compound clauses the DPLL decides).