Add distinct() variadic function

Only Z3 supports this SMT-LIB 2.0 feature directly. For MathSAT5,
we use the C API to assert that terms are pair-wise not equal.