solve-classic/it.unibo.tuprolog.solve.classic

Package-level declarations

Types

abstract class AbstractClassicSolver(unificator: Unificator = Unificator.default, libraries: Runtime = Runtime.empty(), flags: FlagStore = FlagStore.empty(), initialStaticKb: Theory = Theory.empty(unificator), initialDynamicKb: Theory = MutableTheory.empty(unificator), inputChannels: InputStore = InputStore.fromStandard(), outputChannels: OutputStore = OutputStore.fromStandard(), trustKb: Boolean = false) : AbstractSolver<ClassicExecutionContext>

Base implementation of every :solve-classic it.unibo.tuprolog.solve.Solver/it.unibo.tuprolog.solve.MutableSolver (ClassicSolver and MutableClassicSolver, both internal, are the only two concrete subclasses; instances are normally obtained through ClassicSolverFactory, which is what Solver.prolog/Solver.classic resolve to).

ChoicePointContext

sealed class ChoicePointContext

One node of the :solve-classic choice-point queue: a saved point in the proof search that it.unibo.tuprolog.solve.classic.fsm.StateBacktracking can resume from, chained to its parent to form the full lineage of choice points recorded since the query started (see pathToRoot).

ClassicExecutionContext

data class ClassicExecutionContext(val procedure: Struct? = null, val unificator: Unificator = Unificator.default, val libraries: Runtime = Runtime.empty(), val flags: FlagStore = FlagStore.empty(), val staticKb: Theory = Theory.empty(unificator), val dynamicKb: MutableTheory = MutableTheory.empty(unificator), val operators: OperatorSet = getAllOperators(libraries, staticKb, dynamicKb).toOperatorSet(), val inputChannels: InputStore = InputStore.fromStandard(), val outputChannels: OutputStore = OutputStore.fromStandard(), val customData: CustomDataStore = CustomDataStore.empty(), val substitution: Substitution.Unifier = Substitution.empty(), val query: Struct = Truth.TRUE, val goals: Cursor<out Term> = Cursor.empty(), val rules: Cursor<out Rule> = Cursor.empty(), val primitives: Cursor<out Solve.Response> = Cursor.empty(), val startTime: TimeInstant, val maxDuration: TimeDuration = TimeDuration.MAX_VALUE, val choicePoints: ChoicePointContext? = null, val parent: ClassicExecutionContext? = null, val depth: Int = 0, val step: Long = 0, val relevantVariables: Set<Var> = emptySet()) : ExecutionContext

One frame of the :solve-classic execution-context stack: a substitution, the streams of remaining goals, candidate Rules and candidate primitive responses, plus a parent link. Frames chain into their parent rather than living in a separate stack container, so the parent chain (see pathToRoot) is the call stack -- ordinary heap-allocated data rather than native JVM/JS stack frames, which is what lets Prolog resolution of arbitrarily deep recursive programs run as an explicit, non-recursive it.unibo.tuprolog.solve.classic.fsm.State loop instead of unbounded host-language recursion.

ClassicSolverFactory

object ClassicSolverFactory : SolverFactory

The SolverFactory for :solve-classic, 2P-Kt's ISO-standard, SLD-NF resolution engine.

MutableSolutionIterator

interface MutableSolutionIterator : SolutionIterator

A SolutionIterator that can hijack a state transition, i.e. substitute the State the machine actually moves into for the one it would otherwise have computed.

SolutionIterator

interface SolutionIterator : Iterator<Solution>

Drives the :solve-classic finite-state machine, one State.next step at a time, and turns every visited end-state (see it.unibo.tuprolog.solve.classic.fsm.EndState) into an emitted Solution.

Functions

appendPrimitives

fun ChoicePointContext?.appendPrimitives(alternatives: Cursor<out Solve.Response>, executionContext: ClassicExecutionContext? = null): ChoicePointContext

Chains a new ChoicePointContext.Primitives recording alternatives onto this (null meaning "the root").

appendRules

fun ChoicePointContext?.appendRules(alternatives: Cursor<out Rule>, executionContext: ClassicExecutionContext? = null): ChoicePointContext

Chains a new ChoicePointContext.Rules recording alternatives onto this (null meaning "the root").

nextDepth

fun ChoicePointContext?.nextDepth(): Int

The ChoicePointContext.depth a new choice point chained onto this one (or null, for the root) would have.