Package-level declarations

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 PrologExecutionContext.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-prolog State: wraps computeNext with a shared timeout check, so no concrete state has to implement SolveOptions.timeout handling itself.

A State that carries an emitted Solution (StateEnd, reached on a positive or negative solution, or StateHalt, reached on an uncaught exception). Every time it.unibo.tuprolog.argumentation.core.engine.SolutionIterator visits one of these, solution is what it hands back to the caller.

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-prolog finite-state machine: an explicit, inspectable representation of "where resolution currently is", carrying the PrologExecutionContext it operates on.

"Backtracking", the central hub of the state machine: if PrologExecutionContext.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.argumentation.core.engine.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 PrologExecutionContext.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 PrologExecutionContext.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 PrologExecutionContext.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 PrologExecutionContext.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 (PrologExecutionContext.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 PrologExecutionContext, 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 PrologExecutionContext.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, resolves the goal with the matching clauses (see ClauseResolver: renamed apart, or as stored with the unificator of arg2p), and moves to StateRuleExecution with the resolutions as a new choice point.

The indexes of the immutable theories a solver resolves with (arg2p): the libraries of each module and the static theory, the last ones met, by identity. A solver keeps them for all its resolutions, and shares them with the solvers its resolutions create (for sub-goals, modules), which run in the same thread: the indexes need no synchronization, and the resolutions of solvers in other threads have indexes of their own.

Records a it.unibo.tuprolog.argumentation.core.engine.ChoicePointContext.Rules onto PrologExecutionContext.choicePoints whose alternatives resolve the current goal of this context on backtracking (arg2p): for the frames whose first alternative is not a clause (see ControlConstruct)

Solve.Response analogue of appendRulesAndChoicePoints, recording a it.unibo.tuprolog.argumentation.core.engine.ChoicePointContext.Primitives instead.

Attaches rules as this context's PrologExecutionContext.rules cursor and records a matching it.unibo.tuprolog.argumentation.core.engine.ChoicePointContext.Rules onto PrologExecutionContext.choicePoints, so the remaining candidates (if any) can be retried later on backtracking.

This exception, raised by the code of a primitive, as a resolution exception (arg2p): a Kotlin exception becomes a system_error, which catch/3 can handle, rather than crashing the resolution

Pushes a new child frame onto the execution-context stack for the current goal, becoming its own PrologExecutionContext.goals (arg2p: currentGoal is the current goal with the substitution applied, when the caller already has it)

Combines createChild and appendRulesAndChoicePoints: the usual way StateRuleSelection moves into a non-tail rule call.

The answers of a primitive, an error raised computing one of them becoming an answer raising it (arg2p): the engine computes an answer ahead (to know whether the call leaves alternatives), but the error is only raised if the resolution backtracks into it, as an error of that answer

Last-call-optimization counterpart of createChild: reuses the current frame for the current goal (incrementing PrologExecutionContext.depth without growing the PrologExecutionContext.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.

The context an error raised in this one is reported in: the nearest one that is not throw/1

The goals of the body of a clause, as toGoals: none for true, the body of a fact (arg2p)

Turns this term into the Cursor of goals StateGoalSelection iterates over: unfoldGoals flattens conjunctions, and every variable goal is wrapped into call(X) so it goes through the ISO callability check before execution.

Builds the Solve.Request passed to a Primitive's solve from this context, goal and signature, at startTime.

Flattens a (possibly nested) , /2 tuple of goals into the sequence of its leaves, depth-first.