solve/it.unibo.tuprolog.solve/MutableSolver

MutableSolver

General type for mutable logic Solvers. MutableSolvers differ from Solvers in that they expose public methods for letting clients affect the state of the solver -- e.g. affecting the KB -- while no resolution process is ongoing.

This is a distinct concern from the state changes a Solver performs on itself while resolving a single query (e.g. assertz/1 executed as a goal): those are expressed as it.unibo.tuprolog.solve.sideffects.SideEffects attached to a primitive's response, not through this interface. MutableSolver instead lets client code reconfigure a solver from the outside, in between resolutions.

Obtain one via SolverFactory.mutableSolverOf / SolverFactory.mutableSolverWithDefaultBuiltins, or SolverBuilder.buildMutable.

Types

Companion

object Companion

Properties

dynamicKb

abstract val dynamicKb: Theory

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

flags

abstract val flags: FlagStore

Enabled flags

inputChannels

abstract val inputChannels: InputStore

The currently open input channels

libraries

abstract val libraries: Runtime

Loaded libraries

operators

abstract val operators: OperatorSet

Loaded operators

outputChannels

abstract 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

abstract val staticKb: Theory

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

unificator

abstract 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

appendDynamicKb

abstract fun appendDynamicKb(theory: Theory)

Appends theory's clauses to this solver's dynamic knowledge base, keeping the existing ones.

appendStaticKb

abstract fun appendStaticKb(theory: Theory)

Appends theory's clauses to this solver's static knowledge base, keeping the existing ones.

assertA

abstract fun assertA(clause: Clause)

Prepends clause to the dynamic knowledge base, as asserta/1 would.

abstract fun assertA(fact: Struct)

Prepends fact, treated as a fact (a clause with an empty body), to the dynamic knowledge base.

assertZ

abstract fun assertZ(clause: Clause)

Appends clause to the dynamic knowledge base, as assertz/1 would.

abstract fun assertZ(fact: Struct)

Appends fact, treated as a fact (a clause with an empty body), to the dynamic knowledge base.

clone

abstract override fun clone(): MutableSolver

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): MutableSolver

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

loadDynamicClauses

open fun loadDynamicClauses(clauses: Iterable<Clause>)

open fun loadDynamicClauses(clauses: Sequence<Clause>)

open fun loadDynamicClauses(vararg clauses: Clause)

Replaces this solver's dynamic knowledge base with a Theory indexing clauses.

loadDynamicKb

abstract fun loadDynamicKb(theory: Theory)

Replaces this solver's dynamic knowledge base with theory.

loadLibrary

abstract fun loadLibrary(library: Library)

Loads library into this solver's Runtime, adding it to the currently loaded libraries.

loadStaticClauses

open fun loadStaticClauses(clauses: Iterable<Clause>)

open fun loadStaticClauses(clauses: Sequence<Clause>)

open fun loadStaticClauses(vararg clauses: Clause)

Replaces this solver's static knowledge base with a Theory indexing clauses.

loadStaticKb

abstract fun loadStaticKb(theory: Theory)

Replaces this solver's static knowledge base with theory.

resetDynamicKb

abstract fun resetDynamicKb()

Empties this solver's dynamic knowledge base.

resetStaticKb

abstract fun resetStaticKb()

Empties this solver's static knowledge base.

retract

abstract fun retract(clause: Clause): RetractResult<Theory>

Removes the first clause in the dynamic knowledge base unifiable with clause, as retract/1 would.

abstract fun retract(fact: Struct): RetractResult<Theory>

Removes the first clause in the dynamic knowledge base whose head unifies with fact.

retractAll

abstract fun retractAll(clause: Clause): RetractResult<Theory>

Removes every clause in the dynamic knowledge base unifiable with clause, as retractall/1 would.

abstract fun retractAll(fact: Struct): RetractResult<Theory>

Removes every clause in the dynamic knowledge base whose head unifies with fact.

setFlag

abstract fun setFlag(flag: NotableFlag)

Sets flag to its default term value, as reported by NotableFlag.defaultTerm.

abstract fun setFlag(flag: Pair<String, Term>)

Sets the Prolog flag identified by flag's first component to its second component.

abstract fun setFlag(name: String, value: Term)

Sets the Prolog flag named name to value in this solver's it.unibo.tuprolog.solve.flags.FlagStore.

setRuntime

abstract fun setRuntime(libraries: Runtime)

Replaces this solver's whole Runtime of loaded libraries with libraries.

setStandardError

abstract fun setStandardError(stdErr: OutputChannel<String>)

Replaces this solver's standard error channel with stdErr.

setStandardInput

abstract fun setStandardInput(stdIn: InputChannel<String>)

Replaces this solver's standard input channel with stdIn.

setStandardOutput

abstract fun setStandardOutput(stdOut: OutputChannel<String>)

Replaces this solver's standard output channel with stdOut.

setWarnings

abstract fun setWarnings(warnings: OutputChannel<Warning>)

Replaces this solver's warnings channel with warnings.

solve

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

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

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

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

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

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

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.

unloadLibrary

abstract fun unloadLibrary(library: Library)

Removes library from this solver's Runtime.