Class PathCondition

java.lang.Object

org.ek9lang.compiler.phase5.flow.PathCondition

public final class PathCondition
extends Object

The relational path condition accumulated along a control-flow path — an orthogonal structure that sits beside ConstraintState and records facts between symbolic term names (e.g. lo <= hi), which the per-value lattice cannot express.

It carries a set of relational PathCondition.Facts and answers one question: is this fact-set self-contradictory? A branch whose accumulated facts are isUnsatisfiable() is dead — unreachable for every input — which is exactly how the symbolic engine discharges an obligation guarded by a require/if that cannot hold together with the branch it guards. Example 6: require lo <= hi then if lo > hi → {lo<=hi, lo>hi} unsat → the if body is dead.

Contradiction detection is solver-free: a purely syntactic, pairwise operator conflict over facts on the same term pair, handling aligned (a op b vs a op' b) and mirrored (a op b vs b op' a) pairs. This is deliberately just enough for the 2-fact dead-branch class; transitive/arithmetic reasoning is a later extension (see the residual-hardening notes in the spec §11.2). Snapshot-based so branch hooks can push a copy on entry and discard it on exit without a mutable-aliasing hazard.

Proven by spikes S3/S3c (see EK9_SYMBOLIC_SCANNER_SPIKE_REFERENCE.md §4.3): the AST→facts walker emits these facts by reading operator+operands off the relational nodes, with no hand-fed facts (perturbation-verified).

Nested Class Summary

Nested Classes

Modifier and Type	Class	Description
static final record	PathCondition.Fact	A single relational fact between two term names, e.g.

Constructor Summary

Constructors

Constructor	Description
PathCondition()

Method Summary

Modifier and Type	Method	Description
void	addFact(SymbolicTermValue left, String op, SymbolicTermValue right)	Add a relational fact between two symbolic terms.
String	contradictionReason()	A human-readable "a ∧ b unsat" reason for the first contradiction, or null if satisfiable.
List<PathCondition.Fact>	facts()	The accumulated facts (immutable view).
boolean	isUnsatisfiable()	True when the fact-set is self-contradictory — i.e.
PathCondition	snapshot()	An independent copy — used to branch a path condition without aliasing the parent's fact list.

Methods inherited from class Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Details

PathCondition

public PathCondition()

Method Details

addFact

public void addFact(SymbolicTermValue left,
 String op,
 SymbolicTermValue right)

Add a relational fact between two symbolic terms.

snapshot

public PathCondition snapshot()

An independent copy — used to branch a path condition without aliasing the parent's fact list.

facts

public List<PathCondition.Fact> facts()

The accumulated facts (immutable view).

isUnsatisfiable

public boolean isUnsatisfiable()

True when the fact-set is self-contradictory — i.e. this path/branch is dead for every input.

contradictionReason

public String contradictionReason()

A human-readable "a ∧ b unsat" reason for the first contradiction, or null if satisfiable.