solve/it.unibo.tuprolog.solve.impl/AbstractSolver

AbstractSolver

abstract class AbstractSolver<E : ExecutionContext>(unificator: Unificator, libraries: Runtime, flags: FlagStore, initialStaticKb: Theory, initialDynamicKb: Theory, inputChannels: InputStore, outputChannels: OutputStore, trustKb: Boolean = false) : Solver

Base Solver implementation, factoring out the state-management concerns common to every resolution strategy (initializing and updating the current ExecutionContext, loading/partitioning the initial static and dynamic knowledge bases and running their directives, honouring SolveOptions.limit/SolveOptions.isEager) so that concrete solver modules (:solve-classic, :solve-streams, :solve-concurrent) only have to implement solveImpl (the actual resolution algorithm), initializeContext (to produce their own E subtype), and copy/clone.

Parameters

trustKb

if true, initialStaticKb/initialDynamicKb are assumed to have already been partitioned and their directives already run, skipping initializeKb.

Type Parameters

the concrete ExecutionContext subtype used by the resolution strategy.

Constructors

AbstractSolver

constructor(unificator: Unificator, libraries: Runtime, flags: FlagStore, initialStaticKb: Theory, initialDynamicKb: Theory, inputChannels: InputStore, outputChannels: OutputStore, trustKb: Boolean = false)

Properties

dynamicKb

override val dynamicKb: Theory

Dynamic Knowledge-base, that is a KB that can change executing goals

flags

override val flags: FlagStore

Enabled flags

inputChannels

override val inputChannels: InputStore

The currently open input channels

libraries

override val libraries: Runtime

Loaded libraries

operators

override val operators: OperatorSet

Loaded operators

outputChannels

override val outputChannels: OutputStore

The currently open output channels

standardError

open val standardError: OutputChannel<String>

Shortcut for the standard error channel defined in outputChannels. Returns null if the channel is closed

standardInput

open val standardInput: InputChannel<String>

Shortcut for the standard input channel defined in inputChannels. Returns null if the channel is closed

standardOutput

open val standardOutput: OutputChannel<String>

Shortcut for the standard output channel defined in outputChannels. Returns null if the channel is closed

staticKb

override val staticKb: Theory

Static Knowledge-base, that is a KB that can't change executing goals

unificator

override val unificator: Unificator

warnings

open val warnings: OutputChannel<Warning>

Shortcut for the warnings channel defined in outputChannels. Returns null if the channel is closed

Functions

clone

abstract override fun clone(): AbstractSolver<E>

Shorthand for copy without overriding anything, i.e. an identical (but distinct) Solver instance.

copy

abstract override fun copy(unificator: Unificator = this.unificator, libraries: Runtime = this.libraries, flags: FlagStore = this.flags, staticKb: Theory = this.staticKb, dynamicKb: Theory = this.dynamicKb, stdIn: InputChannel<String> = this.standardInput, stdOut: OutputChannel<String> = this.standardOutput, stdErr: OutputChannel<String> = this.standardError, warnings: OutputChannel<Warning> = this.warnings): AbstractSolver<E>

Creates a new Solver, sharing the same resolution strategy as this one, but with every explicitly-provided argument replacing the corresponding piece of state; arguments left unspecified default to this solver's current value. Useful to derive variants of a solver overriding just a few "mutable aspects" (e.g. redirecting stdOut while keeping everything else identical).

equals

open operator override fun equals(other: Any?): Boolean

hashCode

open override fun hashCode(): Int

solve

open fun solve(goal: Struct): Sequence<Solution>

Shorthand for solve with SolveOptions.DEFAULT (i.e. all solutions, lazily, without a timeout).

open fun solve(goal: Struct, timeout: TimeDuration): Sequence<Solution>

Shorthand for solve with options set to SolveOptions.allLazilyWithTimeout of timeout.

override fun solve(goal: Struct, options: SolveOptions): Sequence<Solution>

Solves goal, returning a (possibly infinite) Sequence of Solutions, computed according to options.

solve

fun Solver.solve(maxDuration: TimeDuration = TimeDuration.MAX_VALUE, scopedContext: Scope.() -> Struct): Sequence<Solution>

Solves the goal built by scopedContext within a fresh, empty Scope (useful to build the goal Struct using scoped variables inline), capping resolution to maxDuration.

solveList

open fun solveList(goal: Struct): List<Solution>

Shorthand for solveList with SolveOptions.DEFAULT.

open fun solveList(goal: Struct, options: SolveOptions): List<Solution>

Eagerly solves goal and collects every produced Solution into a List. Unlike solve, this always computes solutions eagerly regardless of SolveOptions.isLazy -- be mindful of goals with infinite (or very large) solution sets, which will make this method never return (or exhaust memory).

open fun solveList(goal: Struct, timeout: TimeDuration): List<Solution>

Shorthand for solveList with options set to SolveOptions.allLazilyWithTimeout of timeout.

solveOnce

open fun solveOnce(goal: Struct): Solution

Shorthand for solveOnce with SolveOptions.someLazily of 1.

open fun solveOnce(goal: Struct, options: SolveOptions): Solution

Solves goal and eagerly returns its first Solution only, regardless of options' SolveOptions.limit (which is overridden to 1 via SolveOptions.setLimit).

open fun solveOnce(goal: Struct, timeout: TimeDuration): Solution

Shorthand for solveOnce with a timeout, and a limit of 1 solution.

toString

open override fun toString(): String