yices_new_uninterpreted_term does not produce an uninterpreted term

[disteph]

There's a corner case I've just discovered: If the type is the unit type (scalar type of cardinality 1), yices_new_uninterpreted_term returns the unique inhabitant of the type. It's satisfiability-preserving, but not ideal. In particular, yices_subst_term will then complain if you try to substitute what you thought was an uninterpreted term (but is actually this constant) by an expression of type unit. In a model, I suspect the value for what the user thought was an uninterpreted term may also be missing, because the uninterpreted term never existed in the first place (to be checked). Obviously, there's little point introducing uninterpreted terms of type unit, perhaps even less substituting them, but the user code may be generic over Yices types, so now we're pushing onto the user the burden to do a case analysis on the type, for an optimization that isn't documented.

@BrunoDutertre : Did the trick provide speed-ups? If we want to keep it, we may want to do a case analysis in yices_subst_term so that it doesn't complain but instead ignores the substitution on type unit, trying to pretend there is actually an uninterpreted term of type unit even if internally there isn't. And perhaps make sure a value is returned in the model for an uninterpreted term of type unit? Any thoughts?

[BrunoDutertre]

This was an optimization but it now looks like a mistake. Not many people use unit types anyway so I'm not sure the speedup is that important. It would be simpler to treat uninterpreted symbols of unit types the same as for other types. The only issue is making sure that we handle terms of unit types properly in the e-graph or in internalize_to_eterm (I.e., for every uninterpreted term X of unit type, we have to assert X = or just convert all terms of unit types to the unique inhabitant in the internalize code).