tents.idp

/*
 * tents.idp
 * Olivier Van den Eede & Dylan Van Assche
 */

vocabulary V {
    // Types
    type Rij isa int
    type Kolom isa int
    type Aantal isa int
    
    // Relaties
    Tenten(Rij, Kolom) 		// Vak is een tent
    Bomen(Rij, Kolom) 		// Vak is een boom
    
    // Getallen naast het speelveld
    AantalPerRij(Rij): Aantal
    AantalPerKolom(Kolom): Aantal
    
 	// Tent verbonden aan boom   
    Verbonden(Rij, Kolom, Rij, Kolom) // Tent rij, Tent kolom, Boom rij, Boom kolom
 
    // Welke vakken liggen diagonaal naast elkaar
    BurenDiagonaal(Rij, Kolom, Rij, Kolom)
    
    // Welke vakken liggen Horizontaal en Verticaal naast elkaar
    BurenHV(Rij, Kolom, Rij, Kolom)
}

structure Voorbeeld: V {
    // 5x5 vierkant, max aantal tenten = 2 per rij of kolom
    Rij = {1 .. 5}
    Kolom = {1 .. 5}
    
    // Rij en kolom starten vanaf 1 in de linkerbovenhoek
    AantalPerRij = {
        1 -> 2;
      	2 -> 0;
        3 -> 2;
        4 -> 0;
        5 -> 1;
    }
    
    AantalPerKolom = {
        1 -> 2;
        2 -> 0;
        3 -> 1;
        4 -> 0;
        5 -> 2;
    }
    
   	Bomen = {
        1,2;
        2,5;
        3,2;
        3,4;
        4,5;
    }
}

structure Medium: V {
    // 8x8 vierkant
    Rij = {1 .. 8}
    Kolom = {1 .. 8}
    
    // Rij en kolom starten vanaf 1 in de linkerbovenhoek
    AantalPerRij = {
        1 -> 2;
      	2 -> 1;
        3 -> 1;
        4 -> 2;
        5 -> 0;
        6 -> 3;
        7 -> 0;
        8 -> 3;
    }
    
    AantalPerKolom = {
        1 -> 1;
      	2 -> 2;
        3 -> 1;
        4 -> 2;
        5 -> 2;
        6 -> 1;
        7 -> 2;
        8 -> 1;
    }
    
   	Bomen = {
        1,2;
        1,8;
        2,7;
        3,2;
        3,4;
        4,6;
        5,8;
        6,2;
        6,4;
        7,2;
        7,6;
        8,3;
    }
}

structure Moeilijk: V {
    // 8x8 vierkant
    Rij = {1 .. 8}
    Kolom = {1 .. 8}
    
    // Rij en kolom starten vanaf 1 in de linkerbovenhoek
    AantalPerRij = {
        1 -> 3;
      	2 -> 1;
        3 -> 1;
        4 -> 0;
        5 -> 2;
        6 -> 1;
        7 -> 1;
        8 -> 3;
    }
    
    AantalPerKolom = {
        1 -> 2;
      	2 -> 1;
        3 -> 2;
        4 -> 1;
        5 -> 1;
        6 -> 2;
        7 -> 1;
        8 -> 2;
    }
    
   	Bomen = {
        1,2;
        1,7;
        2,3;
        3,4;
        3,8;
        4,2;
        5,6;
        6,3;
        7,3;
        7,7;
        8,2;
        8,5;
    }
}


theory T: V {
     
    /** Een tent wordt verbonden met een boom **/
	// Als een tent en boom verbonden zijn, moeten ze buren zijn.
    !rb, kb, rt, kt: Verbonden(rt, kt, rb, kb) => 
    												Tenten(rt, kt) & 
    												Bomen(rb, kb) & 
    												(BurenHV(rt, kt, rb, kb) | BurenHV(rb, kb, rt, kt)).
    
    // Elke boom mag maximum verbonden zijn met 1 tent
    !rb kb: Bomen(rb,kb) => (#{rt[Rij], kt[Kolom]: Tenten(rt,kt) & Verbonden(rt, kt, rb, kb)} = 1).
    
    // Elke tent mag maximim verbonden zijn met 1 boom
    !rt kt: Tenten(rt,kt) => (#{rb[Rij], kb[Kolom]: Bomen(rb,kb) & Verbonden(rt, kt, rb, kb)} = 1).
    
    
    
    /** evenveel tenten als bomen **/
    // Dit is niet nodig omdat de getallen naast elke rij of kolom dit reeds aangeven
    #{r[Rij], k[Kolom]: Tenten(r,k)} = #{r[Rij], k[Kolom]: Bomen(r,k)}.
    
    
    
    /** De getallen geven aan hoeveel tenten er in de gegeven rij of kolom mogen staan **/
    !r[Rij]: AantalPerRij(r) = #{k[Kolom]: Tenten(r, k)}.
    !k[Kolom]: AantalPerKolom(k) = #{r[Rij]: Tenten(r, k)}.
    
    
    
    /** Tenten mogen elkaar niet raken **/
    // Definieer wat een buur is
    {
        !r1, r2, k1, k2: BurenHV(r1, k1, r2, k2) <- ((r1 = r2+1) & (k1 = k2)).	// Niet raken verticaal
        
		!r1, r2, k1, k2: BurenHV(r1, k1, r2, k2) <- ((r1 = r2)   & (k1 = k2+1)).	// Niet raken horizontaal
        
        !r1, r2, k1, k2: BurenDiagonaal(r1, k1, r2, k2) <- ((r1 = r2-1) & (k1 = k2-1)).	// Niet op Hoofddiagonaal
        !r1, r2, k1, k2: BurenDiagonaal(r1, k1, r2, k2) <- ((r1 = r2+1) & (k1 = k2+1)).
        
        !r1, r2, k1, k2: BurenDiagonaal(r1, k1, r2, k2) <- ((r1 = r2+1) & (k1 = k2-1)).	// Niet op 2de diagonaal
        !r1, r2, k1, k2: BurenDiagonaal(r1, k1, r2, k2) <- ((r1 = r2-1) & (k1 = k2+1)).
    }
    
    // Tenten mogen geen buren zijn
    !r1, r2, k1, k2: Tenten(r1, k1) & Tenten(r2, k2) => ~BurenHV(r1, k1, r2, k2) & ~BurenDiagonaal(r1, k1, r2, k2).
}

procedure main() {
    stdoptions.nbmodels = 5
    printmodels(modelexpand(T, Moeilijk))
    //printmodels(modelexpand(T, Medium))
    //printmodels(modelexpand(T, Voorbeeld))
}