only print pair datatype def if emitted smt-lib code will use it

[dominicmkennedy]

There was this todo in smt-printer the code for a while:
# TODO: check for usage of pairs in the program to not always print this
where smt-printer would always put this datatype decl in emitted smt-lib code:
(declare-datatypes ((Pair 2)) ((par (X Y) ((pair (first X) (second Y))))))

I wanted to use some other solvers including bitwuzla, which doesn't support declare-datatypes, so this line prevents any of those solvers from running even if the resulting code doesn't include any pairs. so by adding a small check to see if the mlir even has a smt.utils.pair in it, we can conditionally emit the datatype decl, without breaking any functionality, while allowing more compatibility with solvers other than z3