handler fdReell {

    class java.lang.Double;
    class DIntv;

    constraint reInt(java.lang.Double,DIntv);
    constraint leq(java.lang.Double,java.lang.Double);
    constraint add(java.lang.Double,java.lang.Double,java.lang.Double);
    constraint sub(java.lang.Double,java.lang.Double,java.lang.Double);
    constraint mult(java.lang.Double,java.lang.Double,java.lang.Double);
    constraint div(java.lang.Double,java.lang.Double,java.lang.Double);


    rules {
        variable DIntv Xi;
        variable DIntv Yi;
        variable DIntv Zi;
        variable DIntv Xineu;
        variable DIntv Yineu;
        variable DIntv Zineu;
        variable DIntv Xi2;
        variable DIntv Yi2;
        variable DIntv Zi2;
        variable java.lang.Double X;
        variable java.lang.Double Y;
        variable java.lang.Double Z;

        // Konkretisieren
        if (DIntv.isNumber(Xi)) { reInt(X,Xi) } ==>
        { X=DIntv.getNumber(Xi) } konkret;

        // Widerspruch
        if (DIntv.isEmpty(Xi)) { reInt(X,Xi) } <=>
        { false } leeresIntervall;

        // Schnitt
        if(Zi=DIntv.intersect(Xi,Yi) ) { reInt(X,Xi) && reInt(X,Yi) } <=>
        { reInt(X,Zi) } durchschnitt;

        // Kleinergleich
        if( DIntv.leq(Xi,Yi) ) { leq(X,Y) && reInt(X,Xi) && reInt(Y,Yi)} <=>
        { true } kgDisjunkt;

        { leq(X,Y) && leq (Y,X) } <=>
        { X=Y } kgAntisym;

        { leq(X,Y) &\& leq(X,Y) } <=>
        { true } idempotenz;

        { leq(X,Y) && reInt(X,Xi) && reInt(Y,Yi) } ==>
        { Zi=DIntv.kgSchnitt(Xi,Yi) && reInt(X,Zi) && reInt(Y,Zi) } kgSchnitt;


        // Addition x+y=z
        if (    Yi2=DIntv.negate(Yi) &&
                Xi2=DIntv.negate(Xi) &&
                Xineu=DIntv.add(Zi,Yi2) &&
                Yineu=DIntv.add(Zi,Xi2) &&
                Zineu=DIntv.add(Xi,Yi) &&
                DIntv.not6eq(Xi,Xineu,Yi,Yineu,Zi,Zineu) )
        { add(X,Y,Z) && reInt(X,Xi) && reInt(Y,Yi) && reInt(Z,Zi) } ==>
        {
                reInt(X,Xineu) && reInt(Y,Yineu) && reInt(Z,Zineu)
        } addition;


        // Subtraktion x-y=z
        { sub(X,Y,Z) } <=> { add(Z,Y,X) } subtraktion;


        // Multiplikation x*y=z
        if (
                Zi2=DIntv.mult(Xi,Yi) &&
                Yi2=DIntv.div(Zi,Xi,Yi) &&
                Xi2=DIntv.div(Zi,Yi,Xi) &&
                DIntv.not6eq(Xi,Xi2,Yi,Yi2,Zi,Zi2) &&
                Xineu=DIntv.intersect(Xi,Xi2) &&
                Yineu=DIntv.intersect(Yi,Yi2) &&
                Zineu=DIntv.intersect(Zi,Zi2)
           )
        { mult(X,Y,Z) &\& reInt(X,Xi) && reInt(Y,Yi) && reInt(Z,Zi) } <=>
        {
                reInt(X,Xineu) && reInt(Y,Yineu) && reInt(Z,Zineu)
        } multiplikation;

        // Division x/y=z
        { div(X,Y,Z) } <=> { mult(Y,Z,X) } division;

    }

    goal add_X_Y_Z {
        variable java.lang.Double X, Y, Z;
        reInt(X, new DIntv(2.0, 5.0)) &&
        reInt(Y, new DIntv(3.0, 4.0)) &&
        reInt(Z, new DIntv(1.0, 7.0)) &&
        add(X, Y, Z)
    }//end of add_X_Y_Z


    goal mult_X_Y_Z {
        variable java.lang.Double X, Y, Z;
        reInt(X, new DIntv(-2.0, 3.0)) &&
        reInt(Y, new DIntv(-3.0, 4.0)) &&
        reInt(Z, new DIntv(7.0, 12.0)) &&
        mult(X, Y, Z)
    }//end of mult_X_Y_Z
}