Skip to content

Solver Design: Why Solvers Look the Way They Do

See Solver API for the full method-by-method listing of Solver, Solution, and friends. This page is about the shape of that API: what a solver actually is under the hood, what state it carries, and why that state is split the way it is. Understanding this is a prerequisite for understanding The state-machine solver, which is one concrete way of driving this state to a solution.

A solver is strategy-agnostic on purpose

The :solve module defines Solver, Solution, ExecutionContext, Library, FlagStore, and Channel without committing to how resolution is actually carried out. That is a deliberate split: :solve-classic implements ISO-standard SLD-NF resolution as an explicit finite-state machine (see state-machine.md); :solve-streams implements a different, more minimalistic side-effect-free strategy over the same Solver contract. Both are interchangeable from client code's point of view — Solver.classic() and Solver.streams() return the same Solver interface — because everything a resolution strategy needs to read and mutate while solving a goal is factored out into ExecutionContext, not hardwired into Solver itself.

 * An interface representing the Solver execution context, containing important information that determines its
 * behaviour.
 *
 * An [ExecutionContext] is a [Solver]'s entire mutable state, reified as an immutable value: the current
 * [substitution], the [logicStackTrace], [customData], and (via [ExecutionContextAware]) the unificator, libraries,
 * flags, both knowledge bases, and I/O channels. It is what
 * [it.unibo.tuprolog.solve.primitive.Solve.Request]s/[it.unibo.tuprolog.solve.primitive.Solve.Response]s carry
 * around, letting [it.unibo.tuprolog.solve.primitive.Primitive]s and
 * [it.unibo.tuprolog.solve.function.LogicFunction]s observe (and, via [apply]/[update], derive new versions of) the
 * state of the resolution they're running within, without depending on any concrete resolution strategy.
 *
 * Because each of these pieces of state is itself an immutable data structure, "mutating" an [ExecutionContext]
 * always means producing a new instance (e.g. [update] or [apply]) rather than changing this one in place -- which
 * keeps every intermediate state snapshot-able, a property resolution strategies rely on for backtracking.
 *
 * Resolution strategies (e.g. `:solve-classic`'s state-machine solver) are free to extend this interface with
 * whatever extra bookkeeping they personally need; code written against the generic [ExecutionContext] keeps
 * working regardless of which concrete strategy produced the instance.
 *
 * @see Solver
 * @see ExecutionContextAware
 */
interface ExecutionContext :
    ExecutionContextAware,
    Durable {
    /** The current procedure being executed, or `null` if none is (e.g. at the very start of resolution) */
    @JsName("procedure")
    val procedure: Struct?

An ExecutionContext is the solver's entire mutable state, reified as a value: the current substitution, the call stack trace, custom data, and (via createSolver/update) the unificator, libraries, flags, both knowledge bases, and channels. Every resolution strategy is free to extend this with whatever bookkeeping it personally needs (:solve-classic's ClassicExecutionContext adds the goal/rule/primitive cursors and the choice-point stack described in state-machine.md) — but any code written against the generic ExecutionContext interface keeps working regardless of which concrete strategy produced it.

The "mutable aspects" of a solver

Conceptually, every Solver carries five kinds of state that can meaningfully change during a resolution (this is the same list the old wiki page called out as the "mutable aspects of solvers", and it is worth preserving because it is the actual design rationale, not just an API inventory):

  • a set of libraries
  • a set of operators
  • a static and a dynamic knowledge base
  • a set of flags
  • an input and an output channel

Calling these "mutable" is slightly counter-intuitive given that 2P-Kt's data structures are immutable end-to-end (terms, substitutions, theories — see Clause databases and indexing). The resolution is: each of these five things is represented by an immutable data structure, but the solver's current one changes over the course of resolution by being replaced with a new instance (e.g. assertz/1 during resolution replaces the dynamic KB with a new Theory, it does not mutate the old one in place). This keeps every intermediate state snapshot-able and inspectable — which matters a great deal to a state-machine solver that needs to save and restore whole execution snapshots for backtracking — while still letting the running system evolve. A MutableSolver (see the Reference page) additionally allows external code to swap these assets in between resolutions, which is a distinct concern from the solver mutating its own state while resolving a single query.

Libraries: the unit of extensibility

 * Bundling all four kinds of extension together, rather than exposing four separate registration points on
 * [it.unibo.tuprolog.solve.Solver], is what makes it possible to ship a self-contained feature (e.g. `:io-lib`,
 * `:oop-lib`) as a single pluggable unit. Since more than one [Library] can be loaded into a `Runtime` at once,
 * [alias] is what lets clashing predicate indicators between libraries be resolved without either library needing
 * to know about the other (see [of] and its `alias` parameter).
 *
 * @see Runtime
 * @see it.unibo.tuprolog.solve.libraryOf
 * */
interface Library : Pluggable {
    /** The alias identifying this library */

A Library bundles everything a piece of built-in (or user-supplied) functionality needs to plug into a solver: operators, clauses (a Theory of "library predicates" written in Prolog itself), primitives (built-ins implemented in Kotlin — see state-machine.md for how these interact with resolution), and functions (arithmetic-style term-reducing helpers). Bundling all four together, rather than exposing four separate registration points on Solver, is what makes it possible to ship a self-contained feature (:io-lib, :oop-lib) as a single pluggable unit, and what makes AliasedLibrary meaningful: since more than one library can be loaded, aliasing is the mechanism that resolves clashing predicate indicators between libraries without either library needing to know about the other.

Flags: read-mostly, solver-scoped configuration

A Prolog flag is a named, valued switch — some standard (double_quotes, unknown), some implementation-specific — read via a FlagStore (an immutable String → Term map) and typed via NotableFlag subclasses (Unknown, DoubleQuotes, LastCallOptimization, TrackVariables, MaxArity, in it.unibo.tuprolog.solve.flags). Keeping flags as data (a map) rather than as scattered solver fields means the whole configurable surface of a solver is enumerable, snapshot-able as part of ExecutionContext, and equally settable whether the strategy is :solve-classic or :solve-streams.

Two of these flags are worth calling out because they visibly shape the state machine's behaviour, not just cosmetic solver output: Unknown controls what happens in Rule Selection when a goal's predicate does not exist at all (fail silently, raise an ExistenceError, or just warn — see StateRuleSelection.missingProcedure in the codebase), and LastCallOptimization lets the classic solver avoid growing the execution-context stack on genuine tail calls.

Channels: solver I/O without a fixed transport

/**
 * Base type abstracting a channel of communication of [T]-typed elements between a [it.unibo.tuprolog.solve.Solver]
 * and the outside world, without committing to a specific transport.
 *
 * This is what lets Prolog built-ins like `write/1`, `read/1`, or warning reporting talk to the outside world
 * uniformly whether the solver runs on the JVM (wrapping a `java.io.PrintStream`/`Reader`/`Writer`) or on JS
 * (wrapping `console.log`), since a built-in only ever depends on this abstraction, never on a concrete transport.
 * See [InputChannel] and [OutputChannel] for the two directions of communication, and
 * [it.unibo.tuprolog.solve.channel.ChannelStore] for how several named channels are held together by a solver.
 *
 * Every element transiting the channel (via [InputChannel.read]/[OutputChannel.write]) is broadcast to every
 * registered [Listener].
 */
interface Channel<T : Any> {
    /** Registers [listener] to be invoked with every element subsequently transiting this channel. */
    @JsName("addListener")

Prolog built-ins like write/1, read/1, or warning reporting need some way to talk to the outside world, but 2P-Kt runs on the JVM, on JS, and (via stdin()/stdout()/stderr()/warning() being expect/actual declarations) potentially other Kotlin targets with entirely different I/O primitives. Channel<T> genericizes over the payload type and stays deliberately minimal (listeners, open/close) so that a JVM stdout() can wrap a java.io.PrintStream while a JS one wraps console.log, and a Solver built-in only ever depends on the Channel abstraction. InputStore/OutputStore then let a solver hold several named channels at once (useful for asserting a Prolog stream term for format/3-style I/O redirection), rather than assuming a single stdin/stdout pair.

Why the split matters

None of these five aspects need to change type when the resolution strategy changes; they only need to change value as resolution proceeds. That is precisely what lets :solve-classic's finite-state-machine engine (described in detail in state-machine.md) and :solve-streams's alternative strategy share one Solver/ExecutionContext/Library/Solution vocabulary while disagreeing entirely on how a goal becomes a stream of solutions.