Clean up interpretation code

[nancyday]

The code for interpretations needs to be reviewed along with the unapplies for every transformer. (Note that a flag is supplied to Z3 to avoid it returning definitions as part of the instance.)