Agregar solver Z3 a la deteccion de interseccion de dominios

Para poder extender la deteccion de dominios a funciones de N variables debemos utilizar un solver para poder verificar que las distintas condiciones dadas en las funciones por partes no satisfagan ningun modelo al definir la funcion, es decir que no se intersecten.

Edit: Agrego dependencia z3 para integracion con binario Z3