#ifndef __WP__
#define __WP__
#include <string>
#include <vector>
#include <utility>
#include <set>
#include <algorithm>
#include "CatomSim.hxx"
using namespace std;

typedef enum {
	no,maybe,yes
} TriState;

class WPObject {};

class WPManager;

class BoolExp: public WPObject {	
public:
	virtual void propagate(string name,CatomSim *catom,WPManager *wm) = 0;
	virtual TriState isSatisfied() = 0;
	virtual int minExtent(string name) = 0;
	virtual int maxExtent(string name) = 0;
	virtual BoolExp *clone() = 0;
	virtual set<string> watchedVariables() { return set<string>(); }
	virtual ~BoolExp() {}
	virtual bool isValidCandidate(map<CatomSim*,set <CatomSim *> > &neighbors, 
																vector<pair<string,CatomSim*> > &names,
																CatomSim *candidate,const string &slotName) = 0;
};

class RVal: public WPObject {
public:
	int value;
	virtual void propagate(string name,CatomSim *catom,WPManager *wm) = 0;
	virtual TriState isSatisfied() = 0;
	virtual int minExtent(string name) = 0;
	virtual int maxExtent(string name) = 0;
	virtual RVal *clone() = 0;
	virtual set<string> watchedVariables() { return set<string>(); }
	virtual ~RVal() {}
	virtual bool isValidCandidate(map<CatomSim*,set <CatomSim *> > &neighbors, 
																vector<pair<string,CatomSim*> > &names,
																CatomSim *candidate,const string &slotName) = 0;
};

class CatomRef: public WPObject {
public:
	int temporalOffset;
	string name;
	CatomRef(const char *n) {
		name = n;
		temporalOffset = 0;
	}
	virtual ~CatomRef() {}
	virtual CatomRef *clone() {
		CatomRef *newRef = new CatomRef(name.c_str());
		newRef->temporalOffset = temporalOffset;
		return newRef;
	}
};

class CatomVar: public RVal {
	CatomRef *catomref;
	string var;
public:
	bool filled;
	CatomVar(CatomRef *c,const char *v) {
		var = v;
		catomref = c;
		filled = false;
		value = 0;
	}
	virtual ~CatomVar() {
		delete catomref;
	}
	virtual void propagate(string name,CatomSim *catom,WPManager *wm);
	virtual TriState isSatisfied() {
		if (filled) return yes;
		else return maybe;
	}
	virtual int minExtent(string name) {
		if (name == var) {
			return (catomref->temporalOffset < 0)? catomref->temporalOffset : 0;
		}
		else return 0;
	}
	virtual int maxExtent(string name) {
		if (name == var) {
			return (catomref->temporalOffset > 0)? catomref->temporalOffset : 0;
		}
		else return 0;
	}
	virtual CatomVar *clone() {
		CatomVar *cv = new CatomVar(catomref->clone(),var.c_str());
		cv->filled = filled;
		cv->value = value;
		return cv;
	}
	virtual set<string> watchedVariables() { 
		set<string> s; 
		s.insert(var); 
		return s;
	}
	virtual bool isValidCandidate(map<CatomSim*,set <CatomSim *> > &neighbors, 
																vector<pair<string,CatomSim*> > &names,
																CatomSim *candidate,const string &slotName) {return true;}
};

class Number : public RVal {
public:
	Number(int val) {value = val;}
	virtual ~Number() {}
	virtual void propagate(string name,CatomSim *catom,WPManager *wm){}
	virtual TriState isSatisfied() {return yes;}
	virtual int minExtent(string name) { return 0; }
	virtual int maxExtent(string name) { return 0; }
	virtual Number *clone() {return new Number(value);}
	virtual bool isValidCandidate(map<CatomSim*,set <CatomSim *> > &neighbors, 
																vector<pair<string,CatomSim*> > &names,
																CatomSim *candidate,const string &slotName) {return true;}
};

class CompExp: public BoolExp {
	string op;
	CatomVar *lval;
	RVal *rval;
public:
	CompExp(CatomVar *l,const char *o,RVal *r) {
		lval = l;
		rval = r;
		op = o;
	}
	virtual ~CompExp() {
		delete lval;
		delete rval;
	}
	virtual void propagate(string name,CatomSim *catom,WPManager *wm){
		lval->propagate(name,catom,wm);
		rval->propagate(name,catom,wm);
	}
	virtual TriState isSatisfied() {
		if ((lval->isSatisfied() == yes) && (rval->isSatisfied() == yes)) {
			if (op == "==") {
				if (lval->value == rval->value) return yes;
				else return no;
			}
			else if (op == "!=") {
				if (lval->value != rval->value) return yes;
				else return no;
			}
			else if (op == ">=") {
				if (lval->value >= rval->value) return yes;
				else return no;
			}
			else if (op == "<=") {
				if (lval->value <= rval->value) return yes;
				else return no;
			}
			else if (op == ">") {
				if (lval->value > rval->value) return yes;
				else return no;
			}
			else if (op == "<") {
				if (lval->value < rval->value) return yes;
				else return no;
			}
			else {
				cout << "Unknown operator:" << op << endl;
				return yes;
			}
		}
		else return maybe;
	}
	virtual int minExtent(string name) {
		if (lval->minExtent(name) < rval->minExtent(name)) return lval->minExtent(name);
		else return rval->minExtent(name);
	}
	virtual int maxExtent(string name) {
		if (lval->maxExtent(name) > rval->maxExtent(name)) return lval->maxExtent(name);
		else return rval->maxExtent(name);
	}
	virtual CompExp *clone() {return new CompExp(lval->clone(),op.c_str(),rval->clone());}
	virtual set<string> watchedVariables() { 
		set<string> l = lval->watchedVariables(); 
		set<string> r = rval->watchedVariables(); 
		set<string> u;
		set_union(l.begin(),l.end(),r.begin(),r.end(),inserter(u,u.end()));
		return u;
		}
		virtual bool isValidCandidate(map<CatomSim*,set <CatomSim *> > &neighbors, 
																	vector<pair<string,CatomSim*> > &names,
																	CatomSim *candidate,const string &slotName) {return true;}
};

class AndExp: public BoolExp {
	BoolExp *lval;
	BoolExp *rval;
public:
	AndExp(BoolExp *l,BoolExp *r):lval(l),rval(r) {}
	virtual ~AndExp() {delete lval; delete rval;}	
	virtual void propagate(string name,CatomSim *catom,WPManager *wm){
		lval->propagate(name,catom,wm);
		rval->propagate(name,catom,wm);
	}
	virtual TriState isSatisfied() {
		if ((lval->isSatisfied() == yes) && (rval->isSatisfied() == yes)) return yes;
		else if ((lval->isSatisfied() == no) || (rval->isSatisfied() == no)) return no;
		else return maybe;
	}
	virtual int minExtent(string name) {
		if (lval->minExtent(name) < rval->minExtent(name)) return lval->minExtent(name);
		else return rval->minExtent(name);
	}
	virtual int maxExtent(string name) {
		if (lval->maxExtent(name) > rval->maxExtent(name)) return lval->maxExtent(name);
		else return rval->maxExtent(name);
	}
	virtual AndExp *clone() {return new AndExp(lval->clone(),rval->clone());}
	virtual set<string> watchedVariables() { 
		set<string> l = lval->watchedVariables(); 
		set<string> r = rval->watchedVariables(); 
		set<string> u;
		set_union(l.begin(),l.end(),r.begin(),r.end(),inserter(u,u.end()));
		return u;
		}
		virtual bool isValidCandidate(map<CatomSim*,set <CatomSim *> > &neighbors, 
																	vector<pair<string,CatomSim*> > &names,
																	CatomSim *candidate,const string &slotName) {
					return (lval->isValidCandidate(neighbors,names,candidate,slotName) &&
									rval->isValidCandidate(neighbors,names,candidate,slotName));
		}
};

class OrExp: public BoolExp {
	BoolExp *lval;
	BoolExp *rval;
public:
	OrExp(BoolExp *l,BoolExp *r):lval(l),rval(r) {}
	virtual ~OrExp() {delete lval; delete rval;}
	virtual void propagate(string name,CatomSim *catom,WPManager *wm){
		lval->propagate(name,catom,wm);
		rval->propagate(name,catom,wm);
	}
	virtual TriState isSatisfied() {
		if ((lval->isSatisfied() == no) && (rval->isSatisfied() == no)) return no;
		if ((lval->isSatisfied() == yes) || (rval->isSatisfied() == yes)) return yes;
		else return maybe;
	}
	virtual int minExtent(string name) {
		if (lval->minExtent(name) < rval->minExtent(name)) return lval->minExtent(name);
		else return rval->minExtent(name);
	}
	virtual int maxExtent(string name) {
		if (lval->maxExtent(name) > rval->maxExtent(name)) return lval->maxExtent(name);
		else return rval->maxExtent(name);
	}
	virtual OrExp *clone() {return new OrExp(lval->clone(),rval->clone());}	
	virtual set<string> watchedVariables() { 
		set<string> l = lval->watchedVariables(); 
		set<string> r = rval->watchedVariables(); 
		set<string> u;
		set_union(l.begin(),l.end(),r.begin(),r.end(),inserter(u,u.end()));
		return u;
		}
		virtual bool isValidCandidate(map<CatomSim*,set <CatomSim *> > &neighbors, 
																	vector<pair<string,CatomSim*> > &names,
																	CatomSim *candidate,const string &slotName) {
					return (lval->isValidCandidate(neighbors,names,candidate,slotName) &&
									rval->isValidCandidate(neighbors,names,candidate,slotName));
		}
};

class NotExp: public BoolExp {
	BoolExp *val;
public:
	NotExp(BoolExp *v):val(v) {}
	virtual ~NotExp() {delete val;}
	virtual void propagate(string name,CatomSim *catom,WPManager *wm){val->propagate(name,catom,wm);}
	virtual TriState isSatisfied() {
		if (val->isSatisfied() == yes) return no;
		if (val->isSatisfied() == no) return yes;
		else return maybe;
	}
	virtual int minExtent(string name) {return val->minExtent(name);}	
	virtual int maxExtent(string name) {return val->maxExtent(name);}	
	virtual NotExp *clone() {return new NotExp(val->clone());}
	virtual set<string> watchedVariables() { 	return val->watchedVariables(); }
	virtual bool isValidCandidate(map<CatomSim*,set <CatomSim *> > &neighbors, 
																vector<pair<string,CatomSim*> > &names,
																CatomSim *candidate,const string &slotName) {
				return !(val->isValidCandidate(neighbors,names,candidate,slotName));
	}
};

class NeighborExp: public BoolExp {
	string lval;
	string rval;
public:
	NeighborExp(const char *l,const char *r) {
		lval = l;
		rval = r;
	}
	virtual ~NeighborExp() {}
	virtual void propagate(string name,CatomSim *catom,WPManager *wm){}
	virtual TriState isSatisfied() {return yes;}
	virtual int minExtent(string name) {return 0;}
	virtual int maxExtent(string name) {return 0;}
	virtual NeighborExp *clone() {return new NeighborExp(lval.c_str(),rval.c_str());}
	virtual set<string> watchedVariables() { return set<string>();}
	virtual bool isValidCandidate(map<CatomSim*,set <CatomSim *> > &neighbors, 
																vector<pair<string,CatomSim*> > &names,
																CatomSim *candidate,const string &slotName) {
			if ((lval!=slotName) && (rval != slotName))  return true; //if we don't use either name, then candidate is fine
			string &filledName = (lval==slotName) ? rval : lval; //get name of filled half of n(a,b)
			for (unsigned i = 0; i < names.size(); i++) {
				if (names[i].first == filledName) {
					return (neighbors[names[i].second].count(candidate) != 0); //is candidate in neighbor set of filledName?
				}
			}
			return false;
	}
};

class CatomList: public WPObject {
	public:
	vector<pair<string,CatomSim*> > names;
	CatomList() {}
	virtual ~CatomList() {}
	CatomList(const char *name) {
		pair<string,CatomSim *> newCatom(name,NULL);
		names.push_back(newCatom);
	}
	void addName(const char *name) {
		pair<string,CatomSim *> newCatom(name,NULL);
		names.push_back(newCatom);
	}
	bool isFull() {
		for (unsigned i =0; i < names.size(); i++) {
			if (!names[i].second) return false;
		}
		return true;
	}
	string nextSlot() {
		for (unsigned i =0; i < names.size(); i++) {
			if (!names[i].second) return names[i].first;
		}
		return string("");
	}
	virtual void propagate(string name,CatomSim *catom,WPManager *wm) {
		for (unsigned i =0; i < names.size(); i++) {
			if (names[i].first == name) {
				names[i].second = catom;
				return;
			}
		}
	}
	virtual CatomList *clone() {
		CatomList *newCL = new CatomList();
		newCL->names = names;
		return newCL;
	}
};

class Watchpoint: public WPObject {
public:
	CatomList *c_list;
	BoolExp *main_exp;
		Watchpoint(CatomList *l,BoolExp *b) {
			c_list = l;
			main_exp = b;
		}
		virtual ~Watchpoint() {
			delete c_list;
			delete main_exp;
		}
		bool isFull() {return c_list->isFull();}
		string nextSlot() {return c_list->nextSlot();}
		virtual void propagate(string name,CatomSim *catom,WPManager *wm) {
			c_list->propagate(name,catom,wm);
			main_exp->propagate(name,catom,wm);
		}
		virtual TriState isSatisfied() {return main_exp->isSatisfied();}
		virtual int minExtent(string name) {return main_exp->minExtent(name);}
		virtual int maxExtent(string name) {return main_exp->maxExtent(name);}
		virtual Watchpoint *clone() {return new Watchpoint(c_list->clone(),main_exp->clone());}
		set<string> watchedVariables() { return main_exp->watchedVariables();}
		virtual bool isValidCandidate(map<CatomSim*,set <CatomSim *> > &neighbors, 
																	vector<pair<string,CatomSim*> > &names,
																	CatomSim *candidate,const string &slotName) {
			return main_exp->isValidCandidate(neighbors,names,candidate,slotName);
		} 
};

Watchpoint *parseWP(string input);

#endif //__WP__
