Domáca úloha č.2

1. Vytvorte funkciu Tableaux my_tableaux();, ktorá vráti korektné a úplné tableaux, ktoré je rozšírením tabla zadaného nižšie. Funkcia má teda splniť nasledovné podmienky.

   
   	Variable x{'x'}, y{'y'}, z{'z'};
   	Predicate P{'P'};
   	Tableaux zadanie; 
   	{
   	    auto x00 = &zadanie;
   	    auto x01 = emplace_next (x00, SPlus , 1, true , Nand(P(x), Nand(P(y), P(z))) );
   	    auto x02 = emplace_next (x01, SPlus , 2, true , Nand(P(z), Nand(Nand(P(x),P(y)), Nand(P(z),P(y)))) ); 
   	    auto x03 = emplace_next (x02, SPlus , 3, true , Nand(Nand(P(z), P(z)), Nand(P(y), P(z))) );
   	    auto x04 = emplace_next (x03, SPlus , 4, false, Nand(P(x), P(y)) );
       }
   	Tableaux riesenie = my_tableaux();
   	assert(is_correct(riesenie));
   	assert(is_closed(riesenie));
   	assert(is_subtableaux(zadanie, riesenie));
   

   Knižnica je pomerne striktná ohľadom toho, čo sú korektné pravidá pre NAND. Je k dispozícii pravidlo ALFA a pravidlo Beta, pričom pri pravidle beta musí poradie formúl v riadku zodpovedať poradiu vo formule. Presné znenie pravidiel si buď odvoďte (prídite na to ako by mali vyzerať) a overte si že funkcia is_correct to chápe rovnako. Alternatívne, odkukajte pravidlá z implementácie is_correct. Podotýkam, že funkcia my_tableaux má fungovať iba presne pre toto jedno tableaux, preto asi bude iba obsahovať definíciu správneho tabla a žiadne algoritmy. Riešenie tohoto príkladu je prípustné odovzdať nie ako program ale len ako textový súbor s požadovaným tablom.
2. Vytvorte funkciu std::vector<std::vector<int>> nandformulatoCNF(std::vector<Formula> formuly), ktorá prekonvertuje množinu formúl obsahujúcu iba NANDy a predikátové atómy do konjunktívnej normálnej formy (vo formáte ako v DÚ1). Vytvorte funkciu bool nandformulaSAT(std::vector<Formula> formuly), ktorá použije togasat na vyriešenie splniteľnosti vytvorenej konjunktívnej normálnej formy.
3. Vytvorte funkciu bool extendTableaux(Tableaux &tabl). Táto funkcia dostane na vstup tablo, ktore obsahuje iba S+ riadky a pokúsi sa ho rozšíriť na korektné uzavreté tablo. V prípade úspechu, vráti true a zmodifikuje tablo predané referenciou, inak vráti false a tablo môže byť zmenené akokoľvek. Formuly v table budú obsahovať iba logické spojky Nand a predikátové atómy.