Retrascope

We need utility methods for Fortress expressions printing in an SMV format.

The most wanted use case is:

we have a collection of Fortress expressions: e[1], e[2], ... , e[n];
we want to produce and SMV file of the following structure (it is supposed to be so):

declarations(e[1])
...
declarations(e[n])
formula(e[1])
...
formula(e[n])

where i = 1, ... , n; declarations(e[i]) is a list of variable declarations that are used in e[i] expression; formula(e[i]) is an SMV equivalent for e[i] expression.