Take advantage of previous computations via filters/pushouts

[kris-brown]

If enumerating models of a theory that simply adds constraints to a previous theory that has been enumerated, then we can get models merely by filtering previous results.

If a theory is expressible as a pushout of two other theories, then enumerating its models is just the database join of the enumerations of the smaller theories (which should often be easier to compute).

These should be implemented. Are there other tricks that can take advantage of the structure of theories?