Foundations and tool support for robust non-linear optimisation with transcendental functions through satisfiability modulo theories