Class ConstraintSatisfiability

java.lang.Object
org.ek9lang.compiler.symbolic.ConstraintSatisfiability
public final class ConstraintSatisfiability extends Object
Decides whether a constrain as expression can be satisfied by ANY value of its base type — a declaration-site check, needing nothing but the constraint and the base.

A constrained type no value can inhabit is dead by construction: every constructor of it Panics, every variable of it is permanently unset, and no test, caller or code path can ever exercise it. That is not a style matter to warn about, it is a program that cannot do what it says — so where it can be PROVEN, it is an error, in keeping with EK9 eliminating a bug category rather than discouraging it.

🔑 Proof, never suspicion — and the asymmetry is the whole design. A missed case costs nothing but a later runtime Panic the developer would have got anyway. A false positive REJECTS A PROGRAM THAT WORKS, which is strictly worse. So every route below returns "unsatisfiable" only from a proof, and everything else — an unfamiliar operator, a literal that will not construct, a base whose ordering is not modelled — answers "cannot tell". This mirrors the doctrine stated in parseAndCompile/constrainedTypes/TautologyConstrainedNegative.ek9.

This is deliberately NOT the search. ConstraintValueSearch probes for a value and may come back empty; that means "this bounded search found no witness", which is a completely different claim from "no witness exists". Only the proofs here may raise an error, and the search result must never be substituted for one.

Two proofs today, both requiring a pure and-tree — under an or a failing branch proves nothing about the other:

  • Empty window. The and-tree folds to [lo,hi] with lo > hi. 🔑 This is DISCRETE reasoning: ConstraintWindows narrows > k to k + 1, which is why it is Integer-only. > 0 and < 1 admits nothing over Integer and admits 0.5 over Float, so applying the same fold to a continuous base would reject working code.
  • Pinned value fails. A leaf == L forces every satisfying value to be L, so if the whole constraint provably FAILs at L, nothing satisfies it. Base-type agnostic, because the verdict comes from the same reflective evaluator that powers E08260 — it catches == 5 and > 10, == "abc" and contains "z" and == 5 and == 7 with one rule.

  • Method Details

    • admitsNoValue

      public static boolean admitsNoValue(String baseTypeFqn, ConstraintExpr constraint)
      Whether no value of baseTypeFqn can possibly satisfy constraint.
      Parameters:
      baseTypeFqn - the constrained base type's fully qualified name, may be null
      constraint - the constraint model, may be null
      Returns:
      true only when unsatisfiability is PROVEN; false whenever it is satisfiable OR undecided

    • whyNoValue

      public static String whyNoValue(String baseTypeFqn, ConstraintExpr constraint)
      A human-readable proof for the error message, or null when the constraint is not provably empty. Kept beside the decision so the two can never describe different things.
      Parameters:
      baseTypeFqn - the constrained base type's fully qualified name
      constraint - the constraint model
      Returns:
      the reason, or null