Package-level declarations
Types
Common base of the two terminal EndStates (StateEnd and StateHalt). By default there is no further transition from here (computeNext throws); StateEnd overrides this to loop back into StateBacktracking when ClassicExecutionContext.hasOpenAlternatives is true, which is what makes it a resumable terminal, unlike StateHalt, the one true sink of the machine.
Common base of every :solve-classic State: wraps computeNext with a shared timeout check, so no concrete state has to implement SolveOptions.timeout handling itself.
A State reached because of a ResolutionException -- either StateException (still looking for an enclosing catch/3) or StateHalt (no handler was found, or the exception reached the root context).
One location of the :solve-classic finite-state machine: an explicit, inspectable representation of "where resolution currently is", carrying the ClassicExecutionContext it operates on.
"Backtracking", the central hub of the state machine: if ClassicExecutionContext.choicePoints is empty (or exhausted), moves to StateEnd emitting a negative solution; otherwise it walks the choice-point queue's pathToRoot for the nearest choice point that still has an alternative, restores that saved execution-context lineage (see it.unibo.tuprolog.solve.classic.ChoicePointContext.backtrack), and resumes at either StatePrimitiveExecution or StateRuleExecution, depending on which kind of alternative was pending.
"End": a resumable terminal -- a solution (positive or negative) has just been emitted, but if ClassicExecutionContext.hasOpenAlternatives is true, computeNext loops back into StateBacktracking rather than truly stopping. This is what makes Solver.solve's lazy Sequence of it.unibo.tuprolog.solve.Solutions work: pulling the next item from the sequence is exactly what triggers this transition. Never times out (isTimeout is always false), since it is reached only after a solution has already been produced.
"Exception": reached whenever a primitive's response, or an ISO error raised mid-resolution, carries an exception rather than a substitution. Climbs the execution-context stack (context.parent, one frame at a time, mirroring the paper's "search for a catch/3 frame") looking for a currently-executing catch(Goal, Catcher, Recovery) whose Catcher unifies with the exception's content. If found, the recovery goal becomes the new goal stream and the machine resumes at StateGoalSelection; if the root context is reached without a match, it moves to StateHalt with the exception attached to the emitted solution (an internal it.unibo.tuprolog.solve.exception.error.MessageError is converted to a public it.unibo.tuprolog.solve.exception.error.SystemError at that point).
"Goal Selection", the entry point of every resolution step: decides what to do with ClassicExecutionContext.goals. Three cases: no goals left and no parent context -> emit the current substitution as a solution and move to StateEnd; no goals left but a parent exists -> pop the stack, carrying the child's substitution (filtered down to variables the parent still cares about, via ClassicExecutionContext.isVariableInteresting) into the parent, and loop back into StateGoalSelection for the parent's remaining goals; goals remain -> move to StatePrimitiveSelection (after recording the current goal's variables as relevant, if TrackVariables is ON).
"Halt": the one true sink of the state machine, reached only via an uncaught exception (no catch/3 matched it all the way up to the root context, or a timeout occurred). Unlike StateEnd, there is no transition back out of it -- resolution truly stops here, with Solution.halt wrapping exception.
Bootstrap State, with no counterpart in the formal paper (whose initial configuration is stipulated rather than computed): resets context into a fresh root frame for ClassicExecutionContext.query -- goals from the query, empty rule/primitive cursors and choice points, no substitution, depth = 0 -- and immediately moves to StateGoalSelection, the actual entry point of every subsequent step.
"Primitive Execution": consumes exactly one response from the current primitive's response stream (ClassicExecutionContext.primitives). A successful response merges its substitution and returns to StateGoalSelection; an empty stream moves to StateBacktracking; an exceptional response moves to StateException.
"Primitive Selection": looks up a Primitive for the current goal's (functor, arity) signature among the loaded libraries. If found, builds a child ClassicExecutionContext, invokes the primitive, and moves to StatePrimitiveExecution with the resulting response cursor already attached as a choice point; if not found, falls through to StateRuleSelection. A malformed goal -- an unbound variable, or a term that isn't callable (not a it.unibo.tuprolog.core.Struct) -- short-circuits straight to StateException here, before any lookup is attempted.
"Rule Execution": pops the first candidate it.unibo.tuprolog.core.Rule from ClassicExecutionContext.rules and unifies its head with the current goal. On success, the rule's body (with the goal's substitution already applied) becomes the new goal stream and the machine moves back to StateGoalSelection; on failure, it moves to StateBacktracking.
"Rule Selection", the clause-resolution counterpart of StatePrimitiveSelection, and where several ISO special cases live: true/! succeed without touching the knowledge base at all (! additionally triggers cut, see below); fail/false, and goals that don't exist anywhere, move to StateBacktracking or StateException depending on the Unknown flag (error/fail/warning); the general case queries the static/dynamic knowledge bases and the libraries' own theories, freshCopy()s the matching clauses to rename variables apart, and moves to StateRuleExecution with the fresh rule stream as a new choice point.
Functions
Solve.Response analogue of appendRulesAndChoicePoints, recording a it.unibo.tuprolog.solve.classic.ChoicePointContext.Primitives instead.
Attaches rules as this context's ClassicExecutionContext.rules cursor and records a matching it.unibo.tuprolog.solve.classic.ChoicePointContext.Rules onto ClassicExecutionContext.choicePoints, so the remaining candidates (if any) can be retried later on backtracking.
Pushes a new child frame onto the execution-context stack for the current goal, becoming its own ClassicExecutionContext.goals.
Combines createChild and appendPrimitivesAndChoicePoints: how StatePrimitiveSelection moves into a primitive call.
Combines createChild and appendRulesAndChoicePoints: the usual way StateRuleSelection moves into a non-tail rule call.
Last-call-optimization counterpart of createChild: reuses the current frame for the current goal (incrementing ClassicExecutionContext.depth without growing the ClassicExecutionContext.parent chain), used by StateRuleSelection for tail calls to avoid an unbounded execution-context stack.
Combines replaceWithChild and appendRulesAndChoicePoints: how StateRuleSelection moves into a last-call-optimized (tail) rule call.
Builds the Solve.Request passed to a Primitive's solve from this context, goal and signature, at startTime.
Converts each Clause to a Rule (see ensureRules) and wraps the result in a lazy Cursor.
Flattens a (possibly nested) , /2 tuple of goals into the sequence of its leaves, depth-first.