class Rectangle {

    /* système de coords
    y
    |
    |
    | (1,2)
    | (1,1) (2,1)
    ________>x
    */
    predicate positif(i:int)
    {
        i >= 0
    }

    var hauteur: int;
    var largeur: int;
    var emplacementX:int;
    var emplacementY:int;

    predicate isNeighbour(r1: Rectangle)
    reads r1
    reads this
        requires r1 != null;
    {
        (emplacementX+largeur)==r1.emplacementX || (emplacementY+hauteur)==r1.emplacementY
        || (r1.emplacementX+r1.largeur)==emplacementX || (r1.emplacementY+r1.hauteur)==emplacementY
    }

  method min(i: int, j: int) returns (m:int)
  {
    if(i<j) {
      m:=i;
    }
    else  {
      m:=j;
    }

  }

    /* un peu la même chose que avec canMerge, voir si r1 est a gauche,a droite, en bas ou au dessus
    pour déterminer le nouveau x et y */

    method merge(r1:Rectangle)
        returns (r2: Rectangle)
        requires r1!=null;
    ensures r2!=null
    {
    if hauteur == r1.hauteur && largeur==r1.largeur { //memes dimensions
              if(emplacementX == r1.emplacementX){
            var min := min(emplacementY,r1.emplacementY);
            r2:= new Rectangle(hauteur+r1.hauteur, largeur, emplacementX, min); //merge vertical
          }
          else{
            var min := min(emplacementX,r1.emplacementX);
            r2:= new Rectangle(hauteur, largeur + r1.largeur, min, emplacementY); //merge horizontal
          }
        }
    else{
      if largeur==r1.largeur {
               if emplacementY+hauteur == r1.emplacementY {
                    r2 :=new Rectangle(hauteur+r1.hauteur,largeur,emplacementX,emplacementY); /*au dessus*/
               }
               else{
                    r2 :=new Rectangle(hauteur+r1.hauteur,largeur,r1.emplacementX,r1.emplacementY); /* en dessous*/
               }
          }
          else{
               if emplacementX+largeur == r1.emplacementX {
                    r2:=new Rectangle(hauteur,r1.largeur+largeur,emplacementX,emplacementY); /* a droite*/
               }
               else {
                   r2:=new Rectangle(hauteur,r1.largeur+largeur,r1.emplacementX,r1.emplacementY); /*a gauche*/
               }
          }
    }

    }


    /* Si largeur et hauteur sont les mêmes ==> merge
     si largeur est la même==> que merge si le deuxième est dans la continuation de l'axe Y du premier ( est soit en dessous, soit au dessus)
     si hauteur est la même==> que merge si le deuxième est dans la continuation de l'axe X du premier ( est soit a gauche soit a droite)
     */

    method canMerge(r1: Rectangle) returns (canM: bool)
    requires r1!=null
    {
        assert r1 != null;
        if hauteur == r1.hauteur && largeur==r1.largeur {
              canM:=true; return;
        }
        else {
            if largeur==r1.largeur && (emplacementY+hauteur == r1.emplacementY || r1.emplacementY+r1.hauteur == emplacementY) {
               canM:=true; return;
            }
            else{
                if hauteur==r1.hauteur && (emplacementX+largeur == r1.emplacementX || r1.emplacementX+r1.largeur == emplacementX){
                    canM:=true; return;
                }
                else {canM:=false; return;}
            }
        }
    }

    constructor (h:int , l: int , x:int , y :int)
    modifies this
    {
        hauteur:=h;
        largeur:=l;
        emplacementX:=x;
        emplacementY:=y;
    }
}



class Couverture {

    var rectangles: array<Rectangle>;

    // Ceci est votre invariant de représentation.
    // C'est plus simple d'avoir ok() dans les pre et les posts que le le recoper à chaque fois.
    predicate ok()
        reads this,rectangles;
    {
        rectangles != null
    }

    constructor (qs: array<Rectangle>)
        requires qs != null
        modifies this
        ensures ok()
        ensures rectangles == qs
    {
        rectangles := qs;
    }

    method merge(i: int , j:int)
    requires ok()
    requires rectangles!=null
    requires 0<=i<rectangles.Length
    requires 0<=j<rectangles.Length
    requires rectangles[i]!=null
    requires rectangles[j]!=null
    requires rectangles.Length>2
    modifies rectangles
    {
            var r3 := rectangles[i].merge(rectangles[j]);
            rectangles[i] := r3;
            rectangles[j] := null;
    }

  method improve() returns (imp:bool)
      requires ok()
      modifies rectangles
  {
       var mod := false;
       var i:=0;
       var n := rectangles.Length;
       while i < n && rectangles != null && rectangles.Length>2 && !mod
            invariant 0 <= i <= n
       {
            if i < rectangles.Length && i >=0 && rectangles[i] != null {
              var j:=i+1;
              while j < n && rectangles != null && rectangles.Length>2 && !mod
                invariant 0 <= j <= n
              {
                  if i < rectangles.Length && i >=0 && j < rectangles.Length && j > 0 && rectangles[j] != null && rectangles[i] != null
                      && ((rectangles[i].emplacementX+rectangles[i].largeur)==(rectangles[j].emplacementY)
                        || (rectangles[i].emplacementY+rectangles[i].hauteur)==(rectangles[j].emplacementY)
                        || (rectangles[j].emplacementX+rectangles[j].largeur)==(rectangles[i].emplacementY)
                        || (rectangles[j].emplacementY+rectangles[j].hauteur)==(rectangles[i].emplacementY))
                  {
                      var mergeable := (rectangles[i]).canMerge(rectangles[j]);
                      if mergeable{
                          merge(i,j);
                          mod := true;
                      }

                  }
                  j := j+1;
              }
            }
            i := i+1;

       }
       imp:=mod;
    }

    method optimize()
        requires ok()
        modifies rectangles
    {
        var merged := true;
        var i := rectangles.Length + 1;
            while merged && i>=0 && rectangles != null
          decreases i
            {
                 merged:=improve();
                 i := i-1;
            }
    }

    method dump()
        requires ok()
    {
        var i := 0;
        var first := true;
        print "[ ";
        while i < rectangles.Length
        {
            if !first { print ", "; }
            if rectangles[i] !=null {
                 print "(";
                   print rectangles[i].emplacementX;
                   print ",";
                   print rectangles[i].emplacementY;
                 print ") --> ";
                 print rectangles[i].largeur;
                 print " / ";
                 print rectangles[i].hauteur;
            }
            else {print "null";}
            i := i + 1;
            first := false;
            print "\n";
        }
        print " ] \n";
    }
}
method Test(c: Couverture)
requires c!=null
requires c.ok()
modifies c, c.rectangles
{
  c.optimize();
  if c!= null && c.rectangles != null {c.dump();}
}
method Main()
{
    // Vous devez écrire ici trois tests de votre méthode optimize
     var g1 := new Rectangle(1,1,0,0);
     var g2 := new Rectangle(1,1,1,0);
     var g3 := new Rectangle(1,1,2,0);
     var g4 := new Rectangle(1,1,0,1);
     var g5 := new Rectangle(1,1,1,1);
     var g6 := new Rectangle(1,1,2,1);
     var g7 := new Rectangle(1,1,0,2);
     var g8 := new Rectangle(1,1,1,2);
     var g9 := null;

     var a := new Rectangle[9];
     a[0], a[1], a[2], a[3], a[4], a[5], a[6], a[7], a[8]:= g1,g2,g3,g4,g5,g6,g7,g8,g9;
     var couv := new Couverture(a);
     Test(couv);

}