Binary

interface Binary<out This : Tree, Tree : TreeNode<Tree>> : TreeNode<Tree>

Common interface for binary operators.

Properties

left	`abstract val left: Tree` The child of this element which is the root of the left subtree.
right	`abstract val right: Tree` The child of this element which is the root of the right subtree.

Inherited Properties

node	`abstract val node: Tree` The object which holds the actual data in the tree.

Functions

copy	`abstract fun copy(left: Tree = this.left, right: Tree = this.right): This` Create a copy of the original object but optionally replace the left or right child element.

Extension Functions

fold

fun <Tree : TreeNode<Tree>, R> TreeNode<Tree>.fold(atom: Tree.() -> R, unary: Unary<*, Tree>.(R) -> R, binary: Binary<*, Tree>.(R, R) -> R): R

Standard tree fold. You can provide transformation operations for atoms, unary and binary nodes.

map

fun <Tree : TreeNode<Tree>> TreeNode<Tree>.map(atom: Tree.() -> Tree = { this }, unary: Unary<Tree, Tree>.(Tree) -> Tree = { this.copy(inner = it) }, binary: Binary<Tree, Tree>.(Tree, Tree) -> Tree = { left, right -> this.copy(left, right)}): Tree

Change tree structure while preserving tree type. You can provide transformation operations for atoms, unary and binary nodes. The only requirement is that operations don't change the type of the tree.

Inheritors

Add	`data class Add : Expression, Binary<Add, Expression>` Addition: A + B
And	`data class And : DirFormula, Binary<And, DirFormula>` Logical conjunction. A path will match this restriction only if it matches both left and right restrictions.
And	`data class And : Formula, Binary<And, Formula>` Logical conjunction. A state satisfies this formula if it satisfies both left and right.
Div	`data class Div : Expression, Binary<Div, Expression>` Division: A / B
Equals	`data class Equals : DirFormula, Binary<Equals, DirFormula>` Logical equivalence. A path will match this restriction either when it matches both left and right restriction or none of them.
Equals	`data class Equals : Formula, Binary<Equals, Formula>` Logical equivalence. A state satisfies this formula if it does not satisfy neither left nor right or if it satisfies both.
Exists	`data class Exists : Formula, Binary<Exists, Formula>` First-order exists operator. Specifies that there exists a state in bound, such that when substituted for name, the target formula is valid at the inspected state.
ForAll	`data class ForAll : Formula, Binary<ForAll, Formula>` First-order forall operator. Specifies that for all states in bound substituted for name, the target formula is valid at inspected state.
Implies	`data class Implies : DirFormula, Binary<Implies, DirFormula>` Logical implication. A path will match this restriction only if does not match the left restriction or matches both left and right restriction.
Implies	`data class Implies : Formula, Binary<Implies, Formula>` Logical implication. A state satisfies this formula if it does not satisfy left or if it satisfies both left and right.
Mul	`data class Mul : Expression, Binary<Mul, Expression>` Multiplication: A * B
Or	`data class Or : DirFormula, Binary<Or, DirFormula>` Logical disjunction. A path will match this restriction only if it matches any of the left and right restrictions.
Or	`data class Or : Formula, Binary<Or, Formula>` Logical disjunction. A state satisfies this formula if it satisfies any of the left and right formulas.
Sub	`data class Sub : Expression, Binary<Sub, Expression>` Subtraction: A - B
Until	`data class Until : Formula, Binary<Until, Formula>` Temporal until (U) operator. A state satisfies until if the paths specified by the quantifier match the direction and always satisfy the path formula until the eventually, the reach formula is satisfied.