Package-level declarations

Types

Link copied to clipboard
abstract class AbstractEndState(val solution: Solution, val context: ClassicExecutionContext) : AbstractState, EndState

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.

Link copied to clipboard
abstract class AbstractState(val context: ClassicExecutionContext) : State

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.

Link copied to clipboard
interface EndState : State

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.solve.classic.SolutionIterator visits one of these, solution is what it hands back to the caller.

Link copied to clipboard

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).

Link copied to clipboard
interface State

One location of the :solve-classic finite-state machine: an explicit, inspectable representation of "where resolution currently is", carrying the ClassicExecutionContext it operates on.

Link copied to clipboard

"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.

Link copied to clipboard
data class StateEnd(val solution: Solution, val context: ClassicExecutionContext) : AbstractEndState

"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.

Link copied to clipboard

"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).

Link copied to clipboard

"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).

Link copied to clipboard

"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.

Link copied to clipboard

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.

Link copied to clipboard

"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.

Link copied to clipboard

"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.

Link copied to clipboard

"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.

Link copied to clipboard

"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

Link copied to clipboard

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.

Link copied to clipboard

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.

Link copied to clipboard

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

Link copied to clipboard

Casts every Clause in this sequence to a Rule.

Link copied to clipboard

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.

Link copied to clipboard
fun Term.toGoals(): Cursor<out Term>

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.

Link copied to clipboard

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

Link copied to clipboard

Converts each Clause to a Rule (see ensureRules) and wraps the result in a lazy Cursor.

Link copied to clipboard

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