Binary

class Binary(val name: String, val firstTerm: Term, val secondTerm: Term, val isInfix: Boolean) : Relation(source)

Represents a binary FOL relation.

Jan Müller

name

The name of this binary relation.

Constructors

constructor(name: String, firstTerm: Term, secondTerm: Term, isInfix: Boolean)

Creates an Binary relation with the given name.

The first/left Term of this binary relation.

Indicates that this binary relation has infix-notation.

The name of the entity.

The second/right Term of this binary relation.

open override fun fullCheck(graph: Graph, symbolTable: SymbolTable, variableAssignments: Map<String, Node>, shouldBeModel: Boolean): ModelCheckerTrace

Checks if the Nodes which firstTerm and secondTerm evaluate to are part of this Relation.

open override fun getRawString(variableAssignments: Map<String, Node>): String

Returns raw String representation of binary relation.

open override fun partialCheck(graph: Graph, symbolTable: SymbolTable, variableAssignments: Map<String, Node>, shouldBeModel: Boolean): ModelCheckerTrace

Checks if the Nodes which firstTerm and secondTerm evaluate to are part of this Relation.

override fun toString(): String

Returns a String representation with no variable assignments and no brackets or dot at root level.

fun toString(variableAssignments: Map<String, Node>, wrap: Boolean): String

Returns a String representation with no variable assignments and optional brackets or dot at root level.