Infer logic type from expression

[elsoroka]

If we implement the SMT-LIB logic definitions, this would allow Satisfiability.jl to infer the best logic type for a given SAT problem. Some SAT solvers will do this themselves (Z3), but others (CVC5) want to receive an explicit (set-logic _) command. Currently, users must provide this command explicitly when solvers require it, so it would be nice to have an infer_logic function that figures out the appropriate type.