Solver
General type for logic solvers, i.e. any entity capable of solving some logic query -- provided as a Struct -- according to some logic, implementing one or more inference rule, via some resolution strategy.
A Solver is deliberately strategy-agnostic: this module defines no resolution algorithm at all, only the contract that every implementation (:solve-classic's SLD-NF resolution, :solve-streams's side-effect-free 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.Channels -- 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. asserting 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.:
val solver = Solver.prolog.solverWithDefaultBuiltins()
val solutions = solver.solve(Struct.of("append", listA, listB, result))See also
Inheritors
Properties
The currently open input channels
Loaded operators
The currently open output channels
Shortcut for the standard error channel defined in outputChannels. Returns null if the channel is closed
Shortcut for the standard input channel defined in inputChannels. Returns null if the channel is closed
Shortcut for the standard output channel defined in outputChannels. Returns null if the channel is closed
Shortcut for the warnings channel defined in outputChannels. Returns null if the channel is closed
Functions
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).
Shorthand for solve with SolveOptions.DEFAULT (i.e. all solutions, lazily, without a timeout).
Shorthand for solve with options set to SolveOptions.allLazilyWithTimeout of timeout.
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.
Shorthand for solveList with SolveOptions.DEFAULT.
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).
Shorthand for solveList with options set to SolveOptions.allLazilyWithTimeout of timeout.
Shorthand for solveOnce with SolveOptions.someLazily of 1.
Solves goal and eagerly returns its first Solution only, regardless of options' SolveOptions.limit (which is overridden to 1 via SolveOptions.setLimit).
Shorthand for solveOnce with a timeout, and a limit of 1 solution.