apollo-backend/eu.yeger.apollo.shared.model.fol/Operator/Binary

Binary

sealed class Binary : Operator(source)

Represents a binary FOL operator.

Author

Jan Müller

Parameters

name

The name of this binary operator.

Inheritors

And

Implication

BiImplication

Types

And

class And(val firstOperand: Formula, val secondOperand: Formula) : Operator.Binary

Represents a conjunction operator.

BiImplication

class BiImplication(val firstOperand: Formula, val secondOperand: Formula) : Operator.Binary

Represents a bi-implication operator.

Implication

class Implication(val firstOperand: Formula, val secondOperand: Formula) : Operator.Binary

Represents an implication operator.

class Or(val firstOperand: Formula, val secondOperand: Formula) : Operator.Binary

Represents a disjunction operator.

Properties

firstOperand

val firstOperand: Formula

The first/left operand of this binary operator.

name

val name: String

The name of the entity.

secondOperand

val secondOperand: Formula

The second/right operand of this binary operator.

Functions

fullCheck

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

Recursively evaluate all subformulas, including redundant checks.

getRawString

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

Returns raw String representation of this binary operator.

partialCheck

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

Recursively evaluate some subformulas, excluding redundant checks.

toString

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.