unify/it.unibo.tuprolog.unify/Equation

Equation

sealed class Equation : TermConvertible, Castable<Equation>

An equation between two logic Terms, lhs = rhs, as built and progressively simplified while computing a Substitution (see AbstractUnificator).

LHS stands for Left-Hand side and RHS stands for Right-Hand side, of the Equation. Every Equation falls into exactly one of five shapes, reflected by this sealed class' subtypes and the corresponding is/as/castTo member triples (isIdentity/asIdentity/castToIdentity and so on):

Identity — both sides are already equal (a no-op for unification purposes);
Assignment (further split into LeftAssignment and RightAssignment) — one side is a Var that could be bound to the other side, turning the equation into a Substitution entry;
Comparison — both sides are non-variable, non-equal terms still to be decomposed further (e.g. two structs with the same functor/arity, to be compared argument-wise);
Contradiction — both sides are irreconcilably different, signaling unification failure.

Instances are normally created through the factory functions in the companion object, which classify a pair of Terms into the appropriate subtype rather than requiring callers to pick one manually.

Inheritors

Types

Assignment

abstract class Assignment(val lhs: Term, val rhs: Term) : Equation

An equation assigning a Var to a Term, regardless of which side (lhs or rhs) the Var is on.

Companion

object Companion

Equation companion object

Comparison

data class Comparison(val lhs: Term, val rhs: Term) : Equation

An equation comparing Terms, possibly different

Contradiction

data class Contradiction(val lhs: Term, val rhs: Term) : Equation

A contradicting equation, trying to equate non equal Terms

Identity

data class Identity(val lhs: Term, val rhs: Term) : Equation

An equation of identical Terms

LeftAssignment

data class LeftAssignment(val lhs: Var, val rhs: Term) : Equation.Assignment

An equation stating Var = Term

RightAssignment

data class RightAssignment(val lhs: Term, val rhs: Var) : Equation.Assignment

An equation stating Term = Var

Properties

isAssignment

open val isAssignment: Boolean

Whether this Equation is an Assignment (either LeftAssignment or RightAssignment).

isComparison

open val isComparison: Boolean

Whether this Equation is a Comparison, i.e. still needs decomposing into sub-equations.

isContradiction

open val isContradiction: Boolean

Whether this Equation is a Contradiction, i.e. represents unification failure.

isIdentity

open val isIdentity: Boolean

Whether this Equation is an Identity, i.e. an equation between already-equal terms.

isLeftAssignment

open val isLeftAssignment: Boolean

Whether this Equation is a LeftAssignment, i.e. shaped as Var = Term.

isRightAssignment

open val isRightAssignment: Boolean

Whether this Equation is a RightAssignment, i.e. shaped as Term = Var.

lhs

open val lhs: Term

The left-hand side of the equation

rhs

open val rhs: Term

The right-hand side of the equation

Functions

apply

@JvmOverloads

fun apply(substitution: Substitution, equalityChecker: (Term, Term) -> Boolean = Term::equals): Equation

Applies given substitution to the Equation left-hand and right-hand sides, returning the new Equation

open fun <U : Equation> as(): U?

asAssignment

open fun asAssignment(): Equation.Assignment?

This Equation as an Assignment, or null if isAssignment is false.

asComparison

open fun asComparison(): Equation.Comparison?

This Equation as a Comparison, or null if isComparison is false.

asContradiction

open fun asContradiction(): Equation.Contradiction?

This Equation as a Contradiction, or null if isContradiction is false.

asIdentity

open fun asIdentity(): Equation.Identity?

This Equation as an Identity, or null if isIdentity is false.

asLeftAssignment

open fun asLeftAssignment(): Equation.LeftAssignment?

This Equation as a LeftAssignment, or null if isLeftAssignment is false.

asRightAssignment

open fun asRightAssignment(): Equation.RightAssignment?

This Equation as a RightAssignment, or null if isRightAssignment is false.

castTo

open fun <U : Equation> castTo(): U

castToAssignment

fun castToAssignment(): Equation.Assignment

This Equation as an Assignment. @throws ClassCastException if isAssignment is false.

castToComparison

fun castToComparison(): Equation.Comparison

This Equation as a Comparison. @throws ClassCastException if isComparison is false.

castToContradiction

fun castToContradiction(): Equation.Contradiction

This Equation as a Contradiction. @throws ClassCastException if isContradiction is false.

castToIdentity

fun castToIdentity(): Equation.Identity

This Equation as an Identity. @throws ClassCastException if isIdentity is false.

castToLeftAssignment

fun castToLeftAssignment(): Equation.LeftAssignment

This Equation as a LeftAssignment. @throws ClassCastException if isLeftAssignment is false.

castToRightAssignment

fun castToRightAssignment(): Equation.RightAssignment

This Equation as a RightAssignment. @throws ClassCastException if isRightAssignment is false.

clone

abstract fun clone(lhs: Term = this.lhs, rhs: Term = this.rhs): Equation

Creates a copy of this Equation, of the same concrete subtype, with lhs and/or rhs replaced.

swap

fun swap(): Equation

Creates a new Equation with lhs and rhs swapped, reclassifying it accordingly (see of).

toAssignmentPair

open fun toAssignmentPair(): Pair<Var, Term>

The (variable, term) pair this Equation assigns, i.e. its Var side paired with the other side.

toContradiction

fun toContradiction(): Equation.Contradiction

Turns this Equation into a Contradiction with the same lhs and rhs, regardless of its actual shape.

toPair

open fun toPair(): Pair<Term, Term>

This Equation's lhs and rhs, as a Pair.

toSubstitution

open fun toSubstitution(): Substitution

The single-binding Substitution this Equation amounts to, i.e. its Var side unified with the other side.

toTerm

open override fun toTerm(): Struct

Converts this Equation to its logical representation, the binary Struct lhs = rhs.