Package org.ek9lang.compiler.symbolic
package org.ek9lang.compiler.symbolic
-
ClassDescriptionTHE shared reading of a constraint's literals as
magnitude + suffix— use this, do not re-derive it.Decides whether aconstrain asexpression can be satisfied by ANY value of its base type — a declaration-site check, needing nothing but the constraint and the base.Finds values a constrained type can actually hold, by PROBING the constraint rather than reading it — the recovery path for when every value we knew how to guess turned out to be inadmissible.THE shared fold of aconstrain asexpression into the inclusive numeric window[lo,hi]it narrows to — call this, do not re-derive it.The result of running the Symbolic/Contract engine (SymbolicEngine) over one construct (docs/tooling/EK9_SYMBOLIC_SCANNER_IMPLEMENTATION_SPEC.md §3/§4.4/§6).A concrete input that violates an obligation — the witness a developer can paste into a test.A branch proven dead (unreachable for every input) by a contradiction in its path condition.An obligation the engine proved cannot fail within the bounded model — the green✓entry.THE registry of "dangerous values" per obligation kind for the Symbolic/Contract engine — the single place that answers which concrete base-domain values would violate this obligation.The inter-procedural summary of a callable (docs/tooling/EK9_SYMBOLIC_SCANNER_IMPLEMENTATION_SPEC.md §3.4) — the facts about it a caller needs to reason across the call boundary without re-analysing its whole body.A singlerequireprecondition:param OP literal, keyed to the parameter's position so a call site can map it onto the matching argument.THE reader of guard CO-OCCURRENCE — which of a callable's parameters, or which FIELDS of one parameter, the code tests together.Parameters, or fields of one parameter, that a condition (and its enclosing conditions) test together, with the provenance needed to re-check it later.THE reader ofrequirepreconditions — use this, do not re-derive one.SINGLE THREADED The Layer-2 symbolic/contract verification pass (docs/tooling/EK9_SYMBOLIC_SCANNER_IMPLEMENTATION_SPEC.md §4.4).The Layer-2 symbolic engine of the Symbolic/Contract Scanner (M3/M4) — it turns "this construct carries undischarged obligations" (the M1 census verdict) into "here is the exact input that panics", or proves no such input exists within the bounded model (docs/tooling/EK9_SYMBOLIC_SCANNER_IMPLEMENTATION_SPEC.md §3/§11.2/§12).The bounded-model witness materialiser for the Symbolic/Contract scanner (M3): given an obligation expressed as a predicate over a candidate input, enumerate the representative value-classes of a type and return the first input that violates it — a concrete counterexample.A concrete counterexample: which value-class it came from, its EK9-source literal, and its value.