This provides a new function that can be used to evaluate formulas under
partial knowledge about the individual variables’ assignments.
This will be useful for testing whether formulas or subformulas become
trivial under specific interpretations.
This implements a function for retrieving the return type of terms, that
is, both the domain to which the expression evaluates to as well as
whether it’s an empty, unit, or general set with multiple values.