Existential

Represents an existential FOL quantifier.

Jan Müller

variable

The BoundVariable of this existential quantifier.

operand

The operand of this existential quantifier.

Constructors

constructor(variable: BoundVariable, operand: Formula)

Creates an Existential quantifier with the given variable and operand.

The name of the entity.

The operand of this quantifier.

The BoundVariable of this quantifier.

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

Checks all possible variable assignments.

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

Returns raw String representation of this quantifier.

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

Checks all possible variable assignments, until one is positive.

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.