| | | Multi-Valued Variables |
There is an alternate method for using multi-valued variables. This is to extend the notion of a context to allow for membership in a set of values. That is, a context could be a conjunction of terms of the form X in S where S is a set of values. The original version of equality of the form X=v is the same as X in {v}. Splitting can be done more efficiently as there is only one residual confactor for each split. Effectively we treat a multiset of confactors as a unit.
There are examples where this representation can be much more efficient, but it makes the algorithm much more complicated to explain. There are also examples where the binary splitting is less efficient as it needs more splits to get the same result.
| | | Multi-Valued Variables |