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.
Note that (exists x in A : B) is semantically equivalent to (exists x : ((at x: A) && B)).
However, we allow the in syntax because it is much more readable and can yield interesting
performance optimisations.
Warning: name must usually be a free name (not assigned yet).
| <init> |
Exists(name: String, bound: Formula, target: 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. |
| bound |
val bound: Formula
The bound formula which limits the states considered for substitution |
| left |
val left: Formula
The child of this element which is the root of the left subtree. |
| name |
val name: String
The name that should be substituted in the target formula. |
| right |
val right: Formula
The child of this element which is the root of the right subtree. |
| target |
val target: Formula
The target formula which is subject to substitution |
| node |
open val node: Formula
Formula is also the node in the tree, so |
| copy |
fun copy(left: Formula, right: Formula): Exists
Create a copy of the original object but optionally replace the left or right child element. |
| toString |
fun toString(): String
Return string which uniquely represents this formula and can be parsed to create an equivalent object. |