theory/it.unibo.tuprolog.theory/TheoryFactory

TheoryFactory

interface TheoryFactory : UnificationAware

A factory of Theory/MutableTheory instances, all sharing the same backing data structure (e.g. indexed or listed, see IndexedTheoryFactory and ListedTheoryFactory) and, by default, the same unificator.

This exists so that code building many theories (e.g. a solver library loading several source files) can depend on "a way of making theories" without hard-coding which concrete implementation — indexed or listed — gets used; swapping IndexedTheoryFactory for ListedTheoryFactory (or vice versa) changes every theory the factory produces without touching the calling code.

Inheritors

Properties

unificator

abstract val unificator: Unificator

Functions

copy

abstract fun copy(unificator: Unificator): TheoryFactory

Returns a factory equivalent to this one, but using the given unificator as its default.

emptyMutableTheory

open fun emptyMutableTheory(): MutableTheory

Creates an empty MutableTheory using this factory's unificator.

abstract fun emptyMutableTheory(unificator: Unificator): MutableTheory

Creates an empty MutableTheory using the given unificator.

emptyTheory

open fun emptyTheory(): Theory

Creates an empty Theory using this factory's unificator.

abstract fun emptyTheory(unificator: Unificator): Theory

Creates an empty Theory using the given unificator.

mutableTheoryOf

open fun mutableTheoryOf(clauses: Iterable<Clause>): MutableTheory

open fun mutableTheoryOf(clauses: Sequence<Clause>): MutableTheory

open fun mutableTheoryOf(vararg clauses: Clause): MutableTheory

Creates a MutableTheory containing the given clauses, using this factory's unificator.

abstract fun mutableTheoryOf(unificator: Unificator, vararg clauses: Clause): MutableTheory

abstract fun mutableTheoryOf(clauses: Iterable<Clause>, unificator: Unificator): MutableTheory

abstract fun mutableTheoryOf(clauses: Sequence<Clause>, unificator: Unificator): MutableTheory

Creates a MutableTheory containing the given clauses, using the given unificator.

theoryOf

open fun theoryOf(clauses: Iterable<Clause>): Theory

open fun theoryOf(clauses: Sequence<Clause>): Theory

open fun theoryOf(vararg clauses: Clause): Theory

Creates a Theory containing the given clauses, using this factory's unificator.

abstract fun theoryOf(unificator: Unificator, vararg clauses: Clause): Theory

abstract fun theoryOf(clauses: Iterable<Clause>, unificator: Unificator): Theory

abstract fun theoryOf(clauses: Sequence<Clause>, unificator: Unificator): Theory

Creates a Theory containing the given clauses, using the given unificator.