Compitino 1 a.a. 2018-19 - turno 1

/* ESEMPIO
n_ele = 22
lim1, lim2, lim3 = 5,3,3 (prodotto >= n_ele)
A (visto a 3 dimensioni):
1  2  3
11 20 20  <---
11 8  12

10 11 12
20 12 15  <---
16 20 18

19 20 21
22        <---

np=3
P:
11 12 20

H-Fetta selezionata: 1  (7 elementi), nell'esempio le righe sono
                                      indicate con <---
OUTPUT ATTESO:
start
pattern rimasto 20
La H-fetta 1 e' diventata:
20 20 20 15 22
end
*/

//SVOLTO DA LUCA VERONESE PER L'INCONTRO TUTORATO DEL GIORNO 09/04/2020
#include<iostream>
using namespace std;

int dimHFetta(int i, int n_ele, int lim2, int lim3);
//POST=(restituisce la dimensione della h-fetta i)

// PRE=(index indica l'indice dell'elemento della H-fetta di cui si vuole la distanza dal primo elmento della H-fetta)
int pos(int index, int lim2, int lim3);
//POST=(restituisce la distanza in X tra il primo elemento di una
//H-fetta e l’elemento index di quella H-fetta)

void Stampa(int* inizioHF, int bene, int lim2, int lim3);

int main()
{
    int X[400], P[20], hf;      //gli elementi di P vanno cercati in H-fetta hf di X
    int n_ele, nP;              //n° elementi inizializzati in X e in P
    int lim1, lim2, lim3;       //n° di strati, righe, colonne di X

    cin >> n_ele;
    for(int i = 0; i < n_ele; i++) {    //riempimento X[0..n_ele-1]
        cin >> X[i];
    }

    cin >> lim1 >> lim2 >> lim3 >> nP;
    if(n_ele > lim1 * lim2 * lim3) {    //la correttezza richiede n_ele <= lim1*lim2*lim3
        n_ele = lim1 * lim2 * lim3;
    }
    for(int i = 0; i < nP; i++) {       //riempimento P[0..nP-1]
        cin >> P[i];
    }


    cout << "start" << endl;
    cin >> hf;                          //selezione H-fetta da trattare
    int dimH = dimHFetta(hf, n_ele, lim2, lim3);
    int* inizioHF = X + (hf * lim3);    //inizio H-fetta da trattare (=inizio riga hf di strato 0)
    int matchCount =0;                  //ultimo elemento di P ad essere stato trovato tra primi i elementi di vH-Fetta
    /*PRE= i==0 && matchCount ==0
    && X è array con n_ele elementi inizializzati, dove n_ele <= lim1*lim2*lim3
    && vH-Fetta ha dimH elementi inizializzati
    && Pattern ha nP elementi inizializzati
    */

    for (int i=0; i<dimH; i++) {
        /*R = (0<=i<=dimH)
         *&& (tra i primi i elementi di vH-Fetta sono stati trovati nell'ordine tutti gli elementi di P[0..matchCount-1])
         *&& (primi i-matchCount elementi di H-Fetta sono ottenuti eliminando nell'ordine ogni elemento di P[0..matchCount-1] dai primi i elementi di vH-Fetta)
         */
        /*N.B.'sono stati trovati nell'ordine' non significa anche "contigui"
            dunque se matchCount = 3, P[0..matchCount-1] = {2,5,3}
            allora i primi i elementi di vH-Fetta sono (prima seq. di interi) 2 (seconda seq. di int) 5 (terza seq.) 3 (quarta seq.)
            e primi i - matchCount elementi di H-Fetta = (prima seq. ) (seconda seq.) (terza seq.) (quarta seq.)
            dove prima seq. può contenere 5,3; seconda seq. può contenere 2,3; terza seq può contenere 2,5; quarta seq. può contenere 2,5,3
        */
        int k = pos(i,lim2,lim3);
        if (matchCount == nP || inizioHF[k] != P[matchCount]) {
            int h = pos(i-matchCount,lim2,lim3);
            inizioHF[h] = inizioHF[k];
        } else {
            matchCount++;
        }
        /*PROVA DI CORRETTEZZA:
    1- INIZIALIZZAZIONE (dimostriamo PRE => R)
        i==0 && match==0
      =>  (0<=i<=dimH) banalmente vera
        i==0 && match==0 => (tutti gli elementi di P[0..matchCount-1] sono presenti nello stesso ordine tra i primi i elementi di vH-Fetta)
      => banalmente vera (P[0..matchCount-1] e primi i elementi di vH-Fetta sono entrambi vuoti)
        i==0 && match==0 => (primi 0 elementi di H-Fetta corrispondono a primi 0 elementi [...] tra i quali abbiamo eliminato 0 elementi [...])
      => vera

        abbiamo dimostrato PRE => (i==0 && matchCount==0) => (parte1 && parte2 && parte3 di R) == R

    2- INVARIANZA  (R && cond => R)
        (0<=i<=dimH) && (i<dimH)
      => (0<=i+1<=dimH)

        assumendo parte2 e parte3 dell'invariante si ha che la parte2 e la parte3 valgono all'inizio dell'iterazione successiva qualunque ramo venga preso.
        DIMOSTRAZIONE:
        se valgono parte2 && parte3 && cond
    se matchCount == nP (ramo if, 1° caso)
            il pattern è già stato consumato.

            L'invariante assieme a matchCount == nP afferma che tra i primi i elementi di vH-Fetta sono già contenuti nell'ordine TUTTI gli elementi
            del pattern, non rimangono altri elementi del pattern da cercare da i+1-esimo elemento di vH-fetta in poi.

            Dunque sono vere:
            -parte2 di R in i+1:
                i primi i+1 elementi di vH-Fetta includono primi i elementi di vH-Fetta, tra i quali sono stati trovati
                tutti gli elementi di P[0..(matchCount)-1]. Inoltre tra i primi i+1 elementi di vH-Fetta non sono
                stati trovati nuovi elementi del pattern rispetto a iter. precedente (non ce ne sono più!)
            -parte3 di R in i+1:
                non essendoci altri elementi del pattern da cercare oltre ai primi i elementi di vH-Fetta, si ha che aggiungendo
                i+1-esimo elemento di vH-Fetta agli i-matchCount elementi di H-Fetta questa corrisonde ancora alla sequenza
                ottenuta eliminando nell'ordine ogni elemento di P[0..(matchCount)-1] dai primi i+1 elementi di vH-Fetta.

            Abbiamo dimostrato che in questo caso vale parte2 && parte3 di R in (i+1).
            Al termine dell'iterazione si incrementa i per mantenere invariante in iterazione successiva.
            Ora dobbiamo ripetere dimostrazione per i restanti casi.

    se matchCount < nP && inizioHF[k] != P[matchCount] (ramo if, 2° caso)
            i+1-esimo elemento di vH-Fetta è UGUALE a P[matchCount], allora matchCount non viene incrementato

        Dimostriamo con uno pseudo-formalismo che la sequenza {P[0..matchCount-1]} è CONTENUTA nell'ordine IN {primi i+1 elementi di vH-fetta}
        Nel seguente pseudo-formalismo si abusa della notazione insiemistica ( {} indicano una sequenza e U indica concatenazione ),
         si scrive una sola frase per riga e si scrive a lato del connettivo/operatore una giustificazione

            {P[0..matchCount-1]}
        CONTENUTO ORDINATAMENTE IN (hyp: parte2 di R, che abbbiamo assunto vero)
            {primi i elementi di vH-fetta}
        CONTENUTO ORDINATAMENTE IN
            {primi i+1 elementi di vH-fetta}

            per affermare che vale la parte3 di R in iterazione successiva occorre affermare che
        {primi i+1-matchCount elementi di H-Fetta} == {seq. ottenuta eliminando [...] P[0..matchCount-1] dai primi i+1 elementi di vH-Fetta}
            dimostriamo questa proprietà facendo uso di alcune ipotesi (invariante ed esecuzione istruzioni del ciclo)

            {primi i+1-matchCount elementi di H-Fetta}
        == (a seguito di assegnamento dell'i+1-esimo elemento di vH-Fetta in i+1-matchCount elementi di H-Fetta)
            {primi i-matchCount elementi di H-Fetta} U {i+1-esimo elemento di vH-Fetta}
        == (hyp: parte3 di R)
            {seq. ottenuta eliminando [...] P[0..matchCount-1] dai primi i elementi di vH-Fetta} U {i+1-esimo elemento di vH-Fetta}
        == (hyp: i+1-esimo elemento di vH-Fetta != P[matchCount], ovvero la condizione del ramo)
            {seq. ottenuta eliminando [...] P[0..matchCount-1] dai primi i+1 elementi di vH-Fetta}

            Per proprietà transitiva di == e di CONTENUTO (ordinatamente) IN abbiamo ottenuto le affermazioni delle
            righe 134 e 145, ovvero quelle che dovevamo ottenere per affermare parte2 e parte3 di R con i+1 al posto di i.
            Al termine dell'iterazione si incrementa i per mantenere invariante in iterazione successiva.

    se  matchCount < nP && inizioHF[k] == P[matchCount]
            i+1-esimo elemento di vH-Fetta è UGUALE a P[matchCount], allora matchCount viene incrementato al fine di mantenere R in iter. successiva

            Bisogna dimostrare:
            R && cond && (matchCount < nP && inizioHF[k] == P[matchCount])
          =>
            {primi i+1-(matchCount+1) elementi di H-Fetta}=={seq. ottenuta eliminando P[0..matchCount] dai primi i+1 elementi di vH-Fetta} &&
            && {P[0..matchCount]} contenuto ordinatamente in {primi i+1 elementi di vH-fetta}

      Dimostrazione R && cond && (matchCount < nP && inizioHF[k] == P[matchCount])=> parte2 (con i+1 al posto di i)

            {P[0..matchCount]}
        ==
            {P[0..matchCount-1]} U {P[matchCount]}
        CONTENUTO ORDINATAMENTE IN (hyp: parte2 di R)
            {primi i elementi di vH-fetta} U {P[matchCount]}
        CONTENUTO ORDINATAMENTE IN (hyp: i+1-esimo elemento di vH-Fetta == P[matchCount], condizione del ramo in cui ci troviamo)
            {primi i+1 elementi di vH-fetta}

      Dimostrazione R&& cond && matchCount<nP && inizioHF[k]==P[matchCount] => parte3 (con i+1 al posto di i)
            {primi i+1-(matchCount+1) elementi di H-Fetta}
        == (dall'aritmetica i+1-(matchCount+1) == i-matchCount)
            {primi i-matchCount elementi di H-Fetta}
        == (hyp: parte3 di R)
            {seq. ottenuta eliminando P[0..matchCount-1] dai primi i elementi di vH-Fetta}
        == (i+1-esimo elemento di vH-Fetta == P[matchCount]; dunque seq. ottenuta eliminando P[0..matchCount] dai primi i+1 elementi di vH-Fetta non contiene i+1-esimo elemento di vH-Fetta)
            {seq. ottenuta eliminando P[0..matchCount] dai primi i+1 elementi di vH-Fetta}

        Abbiamo dimostrato anche in questo caso parte2 e parte3 R con i+1 e matchCount+1, ovvero l'affermazione di righe 164-167.

        Oltre a i, in questo caso si incrementa anche matchCount per mantenere invariante all'inizio di iter. successiva

    ALLA FINE ABBIAMO OTTENUTO che SE SI ENTRA NEL CICLO (vale R && cond)
     parte2 e parte3 DI R valgono all'inizio dell'iterazione successiva qualunque ramo venga preso.
    Ricordandoci che in righe 105-106 abbiamo dimostrato che se vale R && cond vale parte1 in iterazione successiva,
     siamo riusciti a dimostrare R && cond => (parte1 && parte2 && parte3 di R[i+1]) == R[i+1]

    3- TERMINAZIONE (R && !cond => POST)
        (0<=i<=dimH) && !(i<dimH) => i==dimH

        POST1 e POST2 (prima e seconda parte di POST) si ottengono sostituendo dimH a i in parte2 e parte3 di R

        (tra i primi i elementi di vH-Fetta sono stati trovati nell'ordine tutti gli elementi di P[0..matchCount-1])
            && i==dimH && vH-Fetta aveva dimH elementi
    =>  (in vH-Fetta sono stati trovati nell'ordine tutti gli elementi di P[0..matchCount-1])

        (primi i-matchCount elementi di H-Fetta sono ottenuti eliminando nell'ordine ogni elemento di P[0..matchCount-1] dai primi i elementi di vH-Fetta) && i==dimH
    => (primi dimH-matchCount elementi di H-Fetta sono ottenuti eliminando nell'ordine ogni elemento di P[0..matchCount-1] dai primi i elementi di vH-Fetta)

    ABBIAMO DIMOSTRATO  R && !cond => POST1 && POST2 == POST


    POST=(tutti gli elementi di P[0..matchCount-1] erano presenti nello stesso ordine in vH-Fetta)
        &&  (dimH-matchCount elementi più a sinistra di H-Fetta = vH-Fetta a cui è stata eliminata la sequenza P[0..matchCount-1], a partire da sinistra)

    */
    }
    if (matchCount == nP) {
        cout << "pattern consumato tutto";
    } else {
        cout << "pattern rimasto ";
        for (int i = matchCount; i < nP; i++) {
            cout << P[i] << ' ';
        }
    }
    cout << "\nLa H-fetta " << hf << " e' diventata:" << endl;
    Stampa(inizioHF, dimH - matchCount, lim2, lim3);
    cout << "end" << endl;
    return 0;
}

int dimHFetta(int hf, int n_ele, int lim2, int lim3) {
    int nsp = n_ele / (lim2 * lim3);    //numero strati pieni
    int eus = n_ele % (lim2 * lim3);    //elementi dell'ultimo strato
    int rpus = eus / lim3;              //(numero) righe piene ultimo strato
    int ur = eus % lim3;                //(numero di elementi nell') ultima riga

    int dimH = lim3 * nsp;              //lunghezza minima di una H-fetta (se hf > rpus)
    if (hf < rpus) {
        dimH += lim3;
    } else if (hf == rpus) {
        dimH += ur;
    }

    return dimH;
}

int pos(int index, int lim2, int lim3) {
    return (index/lim3)*lim2*lim3 + (index%lim3);
}

void Stampa(int* inizioHF, int dim, int lim2, int lim3) {
    for (int i = 0; i < dim; i++) {
        int b = pos(i, lim2, lim3);
        cout << inizioHF[b] << ' ';
    }
    cout << endl;
}