Module Operator.ConditionSource

We want a choose operation on sets (which normally selects an arbitrary elements in a set) but we want to tell whether two distinct choose(S) operations selected the same element or not.

For this we parameterized the choice function by a choice identifier: Two calls with the same identifier on the same set return the same value. This makes the choice function deterministic (but parameterized by an unknown value).

We also represent sets by decision trees: A union B is really "if(cond) A else B", where cond is a fresh condition variable (that we never use). Thus, a choice can viewed as a valuation of different condition variables. We can thus express that choise_c(S) is equal to one element in the set (we just don't know which one).

We want a choose operation on sets (which normally selects an arbitrary elements in a set) but we want to tell whether two distinct choose(S) operations selected the same element or not.

For this we parameterized the choice function by a choice identifier: Two calls with the same identifier on the same set return the same value. This makes the choice function deterministic (but parameterized by an unknown value).

We also represent sets by decision trees: A union B is really "if(cond) A else B", where cond is a fresh condition variable (that we never use). Thus, a choice can viewed as a valuation of different condition variables. We can thus express that choise_c(S) is equal to one element in the set (we just don't know which one).