Uputstvo za koriscenje:
-----------------------

Fajl fol.hpp sadrzi minimalni kod sa vezbi dovoljan za predstavljanje
bilo iskaznih bilo formula prvog reda. Implementirano je prikazivanje
formula (poboljsano, tako da se zagrade koje nisu neophodne
izostavljaju).

Formule se kreiraju tako sto se koristi klasa FormulaDatabase
(singleton klasa, tj. postoji jedinstvena instanca). Slicno vazi za
termove (klasa TermDatabase). Na primer:

Term x = TermDatabase::getTermDatabase().makeVariableTerm("X");
Formula p = FormulaDatabase::getFormulaDatabase().makeAtom("p", { x });
Formula q = FormulaDatabase::getFormulaDatabase().makeAtom("q", { x });
Formula p_and_q = FormulaDatabase::getFormulaDatabase().makeAnd(p, q);

cout << p_and_q << endl;


Na ovaj nacin je obezbedjeno potpuno deljenje zajednickih podizraza
(baza termova/formula proverava da li takav izraz vec postoji u bazi i
ne kreira ga ponovo, vec vraca deljeni pokazivac na
postojeci. Takodje, termovi/formule se automatski brisu iz baze kada
se unisti poslednji deljeni pokazivac).

NAPOMENA: Formule i termovi se mogu uporedjivati na jednakost prostim
poredjenjem deljenih pokazivaca (tj. operatorom ==). Ovo je zato sto
je garantovano da ne postoje dve ili vise identicnih kopija nekog
terma u memoriji. 

VAZNO: ne koristiti equalTo() za uporedjivanje na jednakost, vec
operator == nad deljenim pokazivacima (tip Term i tip Formula).

Za detalje pogledati odgovarajuci interfejs klasa FormulaDatabase i
TermDatabase.

Fajl parser.ypp sadrzi ulazni fajl za Bison. Prevodjenje ovog fajla
vrsi se komandom:

bison -d -o parser.cpp parser.ypp

cime se kreiraju fajlovi parser.cpp i parser.hpp

Fajl lexer.lpp sadrzi ulazni fajl za Flex. Prevodjenje ovog fajla vrsi
se komandom:

flex -o lexer.cpp lexer.lpp

Nakon toga treba samo u Vas projekat da ubacite fajlove parser.cpp,
parser.hpp, lexer.cpp, fol.cpp i da prevedete *.cpp fajlove. Detalje
komandi mozete videti u prilozenom Makefile-u. U Vase *.cpp fajlove
treba dodati #include "fol.hpp" da bi se videle definisane klase. Fajl
"fol.hpp" mozete dopunjavati po zelji dodatnim funkcionalnostima.

Fajl main.cpp predstavlja primer programa: poziva yyparse(), a zatim
ispisuje formulu. Funkcija yyparse() nakon sto isparsira formulu sa
ulaza smesta pokazivac na kreiranu formulu u globalnu varijablu
parsed_formula. Nakon toga main() funkcija (ili bilo koja druga) moze
preko tog pokazivaca pristupiti formuli.

Sintaksa koju parser prihvata: 

1) <symbol> je bilo koji identifikator (kao u C-u) koji pocinje malim slovom.
2) <var> je bilo koji identifikator (kao u C-u) koji pocinje velikim slovom.
3) <term> je:
   3a) <var>			-- varijabla
   3b) <symbol>			-- konstanta
   3c) <symbol>(<term_seq>)	-- slozeni term

4) <atomic_formula> je:
   4a) true			-- kljucna rec koja oznacava "Te"
   4b) false			-- kljucna rec koja oznacava "Ne-Te"
   4c) <symbol>			-- iskazna varijabla
   4d) <symbol>(<term_seq>)	-- slozeni atom
   4e) <term> = <term>  	-- jednakost
   4f) <term> ~= <term> 	-- razlicitost

5) <term_seq> je :
   5a) <term>			-- jedan term
   5b) <term1>,...,<termn>	-- sekvenca termova razdvojenih zarezima
   
6) <formula> je:
   6a) <formula> <=> <formula>	-- ekvivalencija
   6b) <formula> => <formula>	-- implikacija
   6c) <formula> | <formula>    -- disjunkcija
   6d) <formula> & <formula>    -- konjunkcija
   6e) ~<formula>  		-- negacija
   6f) !<var>. <formula>	-- univerzalni kvantifikator
   6g) ?<var>. <formula>	-- egzistencijalni kvantifikator
   6h) <atomic_formula>
   6i) (<formula>)		-- zagrade oko formula su dozvoljene
7) <ulaz> je oblika:
   <formula>;

Dakle, simbol ';' se koristi kao terminator ulaza. Kvantifikatori
imaju najnizi prioritet. Ukoliko je kvantifikovana formula podformula
neke druge formule, tada se ona mora navesti u zagradama. Na primer,
dozvoljeno je:

!X.!Y.p(X,Y)  -- kvantifikatori su vodeci veznici 

ali nije dozvoljeno:

q | !X.!Y.p(X,Y)   -- kvantifikovana formula je podformula

vec mora da stoji:

q | (!X.!Y.p(X,Y))  -- OK: kvantifikovana podformula je u zagradama


Binarni operatori imaju nizi prioritet od unarnih. Binarni operatori &
i | su levo asocijativni, dok su operatori => i <=> desno
asocijativni.  Medju binarnim operatorima, najvisi prioritet ima &, a
zatim |, => i <=>.  Jedini unarni operator je negacija ~. Zagrade se
mogu koristiti oko izraza kako bi se promenio prioritet operatora
(mogu se koristiti i kada nisu neophodne).

Beline se ignorisu. 