Module Terms.ConditionSource

This uses the structure of the dominator tree as conditions. It observes the fact that we never perform intersection on arbitrary conditions, as conditions represent set of paths, we either assume a new condition or join existing ones.

A dummy Condition, which creates a new int each time.

Condition using Cudd binary-decision diagrams.