Add an option for reusing existing elements when possible

[salmans]

The core idea is to avoid introducing new elements to the model when possible. Here is an example for the simple case:

P('a);
exists x. P(x);

Razor currently builds the following model for this theory:

Domain: e#0, e#1
Elements: 'a -> e#0, 'sk#0 -> e#1
Facts: P(e#0), P(e#1)

However, it could reuse e#0 (denoting 'a in place of e#1 (denoting the existential quantifier). This would introduce an unnecessary identification between e#0 and e#1, resulting in a model that is not homomorphically minimal:

Domain: e#0
Elements: 'a -> e#0, 'sk#0 -> e#0
Facts: P(e#0)

However, this kind of element reuse often helps avoid constructing infinite models as for the case for the grandpa example.