Operator

Represents an FOL operator.

Jan Müller

name

The name of this operator.

Types

sealed class Binary : Operator

Represents a binary FOL operator.

sealed class Unary : Operator

Represents an unary FOL operator.

The name of the entity.

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

Recursively evaluate all subformulas, including redundant checks.

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

Returns a raw String representation of an FOLEntity. This method should not be called directly, as it does not include brackets and dots.

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

Recursively evaluate some subformulas, excluding redundant checks.

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.