Solver API¶

The :solve module defines the platform-agnostic API for goal resolution: Solver, Solution, SolveOptions, Library/Runtime, and I/O Channels. It defines no resolution algorithm itself — that's the job of the implementation modules :solve-classic, :solve-streams, :solve-concurrent and :solve-problog, each providing a SolverFactory. This page documents the common surface all of them implement.

`Solver`¶

 * strategy, `:solve-concurrent`, `:solve-problog`) must honour. Everything a resolution strategy needs to read
 * while solving a goal -- loaded `it.unibo.tuprolog.solve.library.Library`/`Runtime`, [FlagStore], the two
 * [Theory] knowledge bases, I/O [it.unibo.tuprolog.solve.channel.Channel]s -- is exposed through
 * [ExecutionContextAware], which this interface extends.
 *
 * __Solvers are not immutable entities__. Their state may mutate as an effect of solving queries -- e.g. `assert`ing
 * a clause during resolution replaces the dynamic knowledge base with a new [Theory] instance. Between resolutions,
 * a solver's assets can only be swapped by deriving a new [Solver] via [copy], unless the concrete instance also
 * implements [MutableSolver].
 *
 * Instances are usually obtained from a [SolverFactory], several of which are reachable from the companion object,
 * e.g.:
 * ```kotlin
 * val solver = Solver.prolog.solverWithDefaultBuiltins()
 * val solutions = solver.solve(Struct.of("append", listA, listB, result))
 * ```
 *
 * @see MutableSolver
 * @see Solution
 * @see SolveOptions
 */
interface Solver : ExecutionContextAware {
    /** Shorthand for [solve] with `options` set to [SolveOptions.allLazilyWithTimeout] of [timeout]. */
    @JsName("solveWithTimeout")
    fun solve(
        goal: Struct,
        timeout: TimeDuration,
    ): Sequence<Solution> = solve(goal, SolveOptions.allLazilyWithTimeout(timeout))

    /** Shorthand for [solve] with [SolveOptions.DEFAULT] (i.e. all solutions, lazily, without a timeout). */
    @JsName("solve")
    fun solve(goal: Struct): Sequence<Solution> = solve(goal, SolveOptions.DEFAULT)

    /**
     * Solves [goal], returning a (possibly infinite) [Sequence] of [Solution]s, computed according to `options`.
     *
     * Whether solutions are computed as the sequence is consumed, or eagerly ahead of time, depends on
     * [SolveOptions.isLazy]; how many solutions are produced is capped by [SolveOptions.limit], and the overall
     * resolution process is capped in time by [SolveOptions.timeout].
     */
    @JsName("solveWithOptions")
    fun solve(
        goal: Struct,
        options: SolveOptions,
    ): Sequence<Solution>

Three families of methods trigger resolution of a Struct goal, differing in how solutions are collected:

solve(goal, options): Sequence<Solution> — lazily or eagerly yields solutions, depending on options.isLazy;
solveList(goal, options): List<Solution> — always eager (careful with infinite solution sets);
solveOnce(goal, options): Solution — eagerly returns the first solution only (options.setLimit(1)).

Overloads accepting a timeout: TimeDuration instead of options are shorthands built on SolveOptions.of(...).

Solver also extends ExecutionContextAware (see below) and exposes copy(...) / clone() to derive a new solver sharing/overriding specific pieces of state.

Obtaining a `Solver`¶

Solver's companion object exposes one SolverFactory per implementation:

Solver.prolog — the classic, SLD-resolution-based solver (:solve-classic; Solver.classic is a deprecated alias for the same factory);
Solver.problog — a probabilistic-logic-programming solver (:solve-problog);
Solver.concurrent — a solver that parallelizes resolution (:solve-concurrent);
Solver.streams — an experimental, more side-effect-free solver (:solve-streams); marked @Deprecated as not production-ready.

Each SolverFactory (it.unibo.tuprolog.solve.SolverFactory) provides defaultRuntime, defaultUnificator, defaultFlags, defaultStaticKb/defaultDynamicKb, default I/O channels, and factory methods solverOf(...), solverWithDefaultBuiltins(...), mutableSolverOf(...) and mutableSolverWithDefaultBuiltins(...) (the WithDefaultBuiltins variants add the standard-library Library — see Default predicates — on top of whatever Runtime you pass). newBuilder() returns a SolverBuilder for a more fluent, stepwise construction.

Solving a query¶

val solver = Solver.prolog.solverWithDefaultBuiltins()
val solutions = solver.solve(Struct.of("append", listA, listB, result))

`SolveOptions`¶

/**
 * Configuration for a single [Solver.solve] invocation: whether solutions are computed lazily or eagerly, how long
 * resolution may run for, how many solutions to cap at, and any implementation-specific extra knob.
 *
 * Instances are immutable; the `set*`/`add*` methods all return a new [SolveOptions] rather than mutating the
 * receiver. Build one via the companion's factories -- [allLazily], [someLazily], [allEagerly], [someEagerly], their
 * `...WithTimeout` variants, or the general [of] -- or start from [DEFAULT] and tweak it, e.g.
 * `SolveOptions.DEFAULT.setLimit(1)`.
 *
 * @see Solver.solve
 */
interface SolveOptions {
    /**
     * Whether [Solver.solve] should stream solutions on demand as the returned [Sequence] is consumed (`true`), or
     * compute the whole (bounded) solution set eagerly before returning (`false`, see [isEager]).
     */
    @JsName("isLazy")
    val isLazy: Boolean

    /** The negation of [isLazy]: `true` if solutions are computed eagerly, ahead of consuming the sequence. */

isLazy / isEager — controls whether solve() streams solutions on demand or computes eagerly;
timeout: TimeDuration — max execution duration (SolveOptions.MAX_TIMEOUT by default);
limit: Int — caps the number of returned solutions (SolveOptions.ALL_SOLUTIONS, i.e. -1, by default);
customOptions: Map<String, Any> — implementation-specific extra knobs.

Instances are built via the companion's factories: allLazily(), someLazily(limit), allEagerly(), someEagerly(limit), their ...WithTimeout(...) variants, or the general of(lazy, timeout, limit, customOptions). SolveOptions.DEFAULT is allLazily().

`Solution`¶

Every solution is one of three sealed subtypes of Solution:

Solution.Yes — successful; substitution: Substitution.Unifier, solvedQuery: Struct are non-nullable;
Solution.No — the goal failed; substitution is Substitution.Fail, solvedQuery is null;
Solution.Halt — resolution was aborted by an exception; carries exception: ResolutionException.

All three share query: Struct (the original goal), isYes/isNo/isHalt, asYes()/asNo()/asHalt() (nullable casts), whenIs(yes = ..., no = ..., halt = ...) for exhaustive pattern matching, and valueOf(variable) to read a binding directly off the solution. Construct them via Solution.yes(...), Solution.no(...), Solution.halt(...).

See Errors and exceptions for ResolutionException and its hierarchy.

`ExecutionContextAware`¶

Both Solver and the internal ExecutionContext (visible to primitives while they run) expose the same set of "mutable aspects" of a resolution process:

interface ExecutionContextAware : UnificationAware {
    /** Loaded libraries */
    @JsName("libraries")
    val libraries: Runtime

    /** Enabled flags */
    @JsName("flags")
    val flags: FlagStore

    /** Static Knowledge-base, that is a KB that *can't* change executing goals */
    @JsName("staticKb")
    val staticKb: Theory

    /** Dynamic Knowledge-base, that is a KB that *can* change executing goals */
    @JsName("dynamicKb")
    val dynamicKb: Theory

    /** Loaded operators */
    @JsName("operators")
    val operators: OperatorSet

    /** The currently open input channels */
    @JsName("inputChannels")
    val inputChannels: InputStore

    /** The currently open output channels */
    @JsName("outputChannels")
    val outputChannels: OutputStore

libraries: Runtime — the loaded libraries (see Libraries);
flags: FlagStore — an immutable map of Prolog flags (name → Term), including implementation-defined NotableFlags (name, defaultTerm, admissibleValues);
staticKb / dynamicKb: Theory — the two knowledge bases a solver draws clauses from; only dynamicKb can be altered by assert/retract during resolution;
operators: OperatorSet — currently known Prolog operators;
inputChannels / outputChannels — InputStore/OutputStore maps of named Channels, with standardInput, standardOutput, standardError and warnings as convenience shortcuts to the well-known ones.

`MutableSolver`¶

MutableSolver extends Solver with methods to alter its state between resolutions: loadLibrary/unloadLibrary, setRuntime, loadStaticKb/loadDynamicKb/appendStaticKb/appendDynamicKb/resetStaticKb/resetDynamicKb, assertA/assertZ, retract/retractAll, setFlag, and setStandardInput/setStandardOutput/setStandardError/ setWarnings. Obtain one via mutableSolverOf(...) / mutableSolverWithDefaultBuiltins(...) on any SolverFactory.

During resolution itself, state changes (asserting a clause, loading a library, altering a flag...) are instead expressed as SideEffects attached to a primitive's Solve.Response — see Primitives and functions.

Channels¶

I/O with a Solver is abstracted through Channel<T> (it.unibo.tuprolog.solve.channel), generic in the type of element it carries:

InputChannel<T> — read(), peek(), available, isOver; built via InputChannel.of(generator), InputChannel.of(string), or the default InputChannel.stdIn();
OutputChannel<T> — write(value), flush(); built via OutputChannel.of(consumer), or the defaults OutputChannel.stdOut(), OutputChannel.stdErr(), OutputChannel.warn(): OutputChannel<Warning>.

Both extend Channel<T>, which supports addListener/removeListener/clearListeners (registering Listener<T?> callbacks invoked on every element transiting the channel) and close()/isClosed. A Solver's channels are collected into InputStore/OutputStore (Map<String, Channel<*>>-like containers), reachable via Solver.inputChannels / Solver.outputChannels.

See Solver design for the rationale behind the immutable-context, side-effect-list architecture.

Solver API¶

Solver¶

Obtaining a Solver¶

Solving a query¶

SolveOptions¶

Solution¶

ExecutionContextAware¶

MutableSolver¶