#ifndef __FORMULA_H__
#define __FORMULA_H__

#include <string>
#include <vector>
#include <map>
#include <iostream>
#include <iterator>
using namespace std;

#include "relacija.h"
extern map<string, Relacija*> relacije;

class Argument {
 public:
    virtual int vrednost(map<string, int>& supstitucija) = 0;
};

class ArgumentPromenljiva : public Argument {
 public:
    ArgumentPromenljiva(const string& ime) 
	: _ime(ime) {
    }

    virtual int vrednost(map<string, int>& supstitucija) {
	map<string, int>::const_iterator it = supstitucija.find(_ime);
	if (it == supstitucija.end()) {
    	    cerr << "Error: free variable " << _ime  << endl;
	    exit(EXIT_FAILURE);
	}
	return it->second;
    }
 private:
    string _ime;
};

class ArgumentKonstanta : public Argument {
 public:
    ArgumentKonstanta(int vrednost) 
	: _vrednost(vrednost) {
    }

    virtual int vrednost(map<string, int>& supstitucija) {
	return _vrednost;
    }
    
 private:
    int _vrednost;
};

class Formula {
 public:
    virtual ~Formula() {}
    virtual bool vrednost(map<string, int>& supstitucija) = 0;
};

class Atom : public Formula {
 public:
    Atom(const string& ime, const vector<Argument*>& argumenti) 
	: _imeRelacije(ime), _argumenti(argumenti) {
    }
    
    ~Atom() {
	vector<Argument*>::iterator it;
	for (it = _argumenti.begin(); it != _argumenti.end(); it++) {
	    delete *it;
	}
    }

    virtual bool vrednost(map<string, int>& supstitucija) {
	vector<int> vrednosti;
	vector<Argument*>::const_iterator it;
	for (it = _argumenti.begin(); it != _argumenti.end(); it++) {
	    vrednosti.push_back((*it)->vrednost(supstitucija));
	}
	map<string, Relacija*>::const_iterator relit = relacije.find(_imeRelacije);
	if (relit == relacije.end()) {
	    cerr << "Error: relation " << _imeRelacije << " not defined" << endl;
	    exit(EXIT_FAILURE);
	}
	return relit->second->uRelaciji(vrednosti);
    }
 private:
    string _imeRelacije;
    vector<Argument*> _argumenti;
};

class Jednakost : public Formula {
 public:
    Jednakost(Argument* arg1, Argument *arg2) 
	: _arg1(arg1), _arg2(arg2) {
    }

    ~Jednakost() {
	delete _arg1;
	delete _arg2;
    }

    virtual bool vrednost(map<string, int>& supstitucija) {
	int v1 = _arg1->vrednost(supstitucija);
	int v2 = _arg2->vrednost(supstitucija);
	return v1 == v2;
    }
 private:
    Argument* _arg1, *_arg2;
};

class BinarniOperator : public Formula {
 protected:
    BinarniOperator(Formula* op1, Formula* op2) 
	: _op1(op1), _op2(op2) {
    }
    
    ~BinarniOperator() {
	delete _op1;
	delete _op2;
    }
    
    virtual bool vrednost(map<string, int>& supstitucija) {
	return primeniOperator(_op1->vrednost(supstitucija), _op2->vrednost(supstitucija));
    }

    virtual bool primeniOperator(bool v1, bool v2) = 0;

 private:
    Formula *_op1, *_op2;
};

class Disjunkcija : public BinarniOperator {
 public:
    Disjunkcija(Formula* f1, Formula* f2) 
	: BinarniOperator(f1, f2) 
	{}
    virtual bool primeniOperator(bool v1, bool v2) {
	return v1 || v2;
    }
};

class Konjunkcija : public BinarniOperator {
 public:
    Konjunkcija(Formula* f1, Formula* f2) 
	: BinarniOperator(f1, f2) 
	{}
    virtual bool primeniOperator(bool v1, bool v2) {
	return v1 && v2;
    }
};

class Implikacija : public BinarniOperator {
 public:
    Implikacija(Formula* f1, Formula* f2) 
	: BinarniOperator(f1, f2) 
	{}
    virtual bool primeniOperator(bool v1, bool v2) {
	return (!v1) || v2;
    }
};

class Negacija : public Formula {
 public:
    Negacija(Formula* op) 
	: _op(op) {
    }

    ~Negacija() {
	delete _op;
    }

    virtual bool vrednost(map<string, int>& supstitucija) {
	return !_op->vrednost(supstitucija);
    }
 private:
    Formula *_op;
};

class ZaSvaki : public Formula {
 public:
    ZaSvaki(const string& imePromenljive, const set<int>& domen, Formula* op) 
	: _imePromenljive(imePromenljive), _domen(domen), _op(op) {
    }

    ~ZaSvaki() {
	delete _op;
    }

    virtual bool vrednost(map<string, int>& supstitucija) {
	set<int>::const_iterator it;
	for (it = _domen.begin(); it != _domen.end(); it++) {
	    supstitucija[_imePromenljive] = *it;
	    if (!(_op->vrednost(supstitucija)))
		return false;
	}
	return true;
    }
    
 private:
    string _imePromenljive;
    set<int> _domen;
    Formula *_op;
};

class Postoji : public Formula {
 public:
    Postoji(const string& imePromenljive, const set<int>& domen, Formula* op) 
	: _imePromenljive(imePromenljive), _domen(domen), _op(op) {
    }

    ~Postoji() {
	delete _op;
    }

    virtual bool vrednost(map<string, int>& supstitucija) {
	set<int>::const_iterator it;
	for (it = _domen.begin(); it != _domen.end(); it++) {
	    supstitucija[_imePromenljive] = *it;
	    if (_op->vrednost(supstitucija))
		return true;
	}
	return false;
    }
    
 private:
    string _imePromenljive;
    set<int> _domen;
    Formula *_op;
};

#endif
