/*
  *
  * stable_marriage.cpp :	Source c++ code solving "Stable Marriage Problem"
  * Implemented by : 		Psallidas Fotis (using naxos project implemented by Nikos Pothitos)
  * std code :			std06170
  * Project Reference:		Logic Programming Project 7.0
  *
  */
#include <naxos.h>
#include <iostream>
#include <fstream>
#include <string>
#include <algorithm>
#include "strtok.h"

using namespace std;
using namespace naxos;

extern "C"{
	#include <stdlib.h>
	#include <time.h>
}

//  Maps the given `name' to the corresponding (name)Index of the array with
//   men's or women's names.  Sets `isMan' accordingly.  Returns `false' if
//   the name was not found in neither array.

	bool
nameToId (string& name, NsDeque<string>& men, NsDeque<string>& women,
		bool& isMan, NsInt& nameIndex)
{
	nameIndex  =  find(men.begin(),men.end(),name) - men.begin();

	if ( nameIndex  !=  (signed int)men.size() )   {

		isMan  =  true;
		return  true;
	}

	nameIndex  =  find(women.begin(),women.end(),name) - women.begin();

	if ( nameIndex  !=  (signed int)women.size() )   {

		isMan  =  false;
		return  true;
	}

	return  false;
}



	int
main (int argc, char *argv[])
{
	unsigned int i,j;
	NsInt k,l;
	bool tr;
	NsProblemManager  pm;
	NsIntVarArray  POSSIBLE_WIFE,POSSIBLE_HUSBAND;
	bool solution_flag=false;
	try  {
		//  Checking input arguments.
		if ( argc  !=  2 )   {
			cerr << "Correct syntax is:\t" << argv[0]<< " <input_filename>\n";
			exit(EXIT_FAILURE);
		}
		//  Opening input filename, e.g. `stable_data.pl'.
		ifstream  file(argv[1]);
		if ( ! file )   {
			cerr << "Could not open `" << argv[1] << "'\n";
			exit(EXIT_FAILURE);
		}
		string  input, tok;
		NsDeque<string>  men, women;
		NsDeque< NsDeque<NsInt> >  manPrefersWoman, womanPrefersMan;
		//  Reading input file line by line.
		while ( getline(file,input) )    {
			StrTokenizer  tokens(input, "([,]).");
			tok  =  tokens.next();
			if ( tok  ==  "men" )    {
				while ( ! (tok = tokens.next()).empty() )
					men.push_back(tok);
					manPrefersWoman.resize( men.size() );
			}  else if ( tok  ==  "women" )    {
				while ( ! (tok = tokens.next()).empty() )
					women.push_back(tok);
					womanPrefersMan.resize( women.size() );
			}  else if ( tok  ==  "prefers" )    {
				bool   isMan;
				NsInt  nameIndex, preferredNameIndex;
				tok  =  tokens.next();
				if ( ! nameToId(tok,men,women,isMan,nameIndex) )   {
					cerr << "Unknown name `" << tok << "'\n";
					exit(EXIT_FAILURE);
				}
				if ( isMan )	manPrefersWoman[nameIndex].resize( women.size() );
				else		womanPrefersMan[nameIndex].resize( men.size() );
				NsInt  priority = 0;
				while ( ! (tok = tokens.next()).empty() )    {
					if ( ! nameToId(tok,men,women,isMan,preferredNameIndex) )   {
						cerr << "Unknown name `" << tok << "'\n";
						exit(EXIT_FAILURE);
					}
					if ( isMan )	womanPrefersMan[nameIndex][preferredNameIndex]  =  priority;
					else		manPrefersWoman[nameIndex][preferredNameIndex]  =  priority;
					++priority;
				}
			}  else if ( tok  !=  "" )    {
				cerr << "Unknown predicate `" << tok<< "'\n";
				exit(EXIT_FAILURE);
			}
		}
		file.close();

		/* Declare variables */
		/* Every woman has a correpsonding variable which is her possible husband */
		/* Every man has a correpsonding variable which is his possible wife */
		for (i=0;  i < men.size();  ++i) {
			POSSIBLE_WIFE.push_back( NsIntVar(pm, 0, men.size()-1) );
			POSSIBLE_HUSBAND.push_back( NsIntVar(pm, 0 ,men.size()-1) );
		}

		/* Basic Constraints */
		/* All variables must be different */
		pm.add( NsAllDiff(POSSIBLE_WIFE) );
		pm.add( NsAllDiff(POSSIBLE_HUSBAND) );

		NsIntVarArray vm,vw;
		for(i = 0 ; i < men.size() ; i++){
			vm.push_back(NsIntVar(pm,0,men.size()-1));
			vw.push_back(NsIntVar(pm,0,women.size()-1));
		}

		/*
 		 *	Now we want to declare the basic constraint which is.
 		 *	If we have a marriage M-W then this marriage is stable if
 		 *	M likes another woman(say W1) than W then W1 must like her husband A1 more than M and
 		 *	if W likes another man (say A2) than M then A2 must like her wife G2 more than W.
 		 *	To express something like that based on the csp declaration we have done till now 
 		 *	we take every possible combination of A-W (constants A-W) and say that
 		 *	if M likes her possible wife (which is his corresponded variable in SM variables) less than W ,
 		 *	then W must like her possible husband (which is her corresponded variable in SW variables)  more than M and
 		 *	if W likes her possible husband more than M then M must like his possible wife more than W.
 		 *	Schema virtualize 
 		 *			    N3
 		 *			 ------->
 		 *			M  	 W
 		 *			 <-------
 		 *			|   N4	 |
 		 *		     N1 |	 | N2
 		 *			|	 |
 		 *		       \ /      \ /
 		 *			`        `
 		 *			DM       DW
 		 *	Where:
 		 * 		N1 is how much man M likes his possible wife DM.
 		 *		N2 is how much woman W likes his possible husband DW.
 		 *		N3 is how much man M likes woman W.
 		 *		N4 is how much woman W like man M.
 		 *		So the constraints we can declare now are:
 		 *		N1 > N3 => N2 < N4 and N2 > N4 => N1 < N3.
 		 *	This gets done for every possible combination of M-W.
 		 *	
 		 *	Till now everything seems good but there is also something
 		 * 	we have to declare.If M-W is a marriage then also W-M is a marriage.
 		 *	This can be expressed by declaring than 
 		 *		M == DW <=> W == DM [look schema]
 		 *	This is also gets done for every possible combination of W-M.
 		 */
		NsInt N3,N4;
		for(i = 0 ; i < men.size() ; i++){
			nameToId(men[i],men,women,tr,k);
			pm.add( vm[i] == manPrefersWoman[k][POSSIBLE_WIFE[i]]);
			for(j = 0 ; j < women.size() ; j++){			
				nameToId(women[j],men,women,tr,l);
				N3 = manPrefersWoman[k][l];
				N4 = womanPrefersMan[l][k];
				pm.add( vw[j] == womanPrefersMan[l][POSSIBLE_HUSBAND[j]] );
				pm.add( NsIfThen(vm[i] > N3,vw[j] < N4) );
				pm.add( NsIfThen(vw[j] > N4,vm[i] < N3) );
				pm.add( NsEquiv(l == POSSIBLE_WIFE[i],k == POSSIBLE_HUSBAND[j]) );
			}
		}

		double starttime,endtime;
		starttime = clock();
		pm.addGoal( new NsgLabeling(POSSIBLE_WIFE) );


		/* 
	 	 *	 Solve stable marriage problem by labeling Possible_Wifes. 
		 *	 Because of the constraint that iff A-G is a marriage then G-A is also a marriage
		 *	 Possible_Husbands variables will be filled concurrently.
		 *
		 */

		while (pm.nextSolution() != false){
			endtime = clock();
			for(i = 0 ; i < men.size() ; i++){
				nameToId(men[i],men,women,tr,k);
				if( i == 0) cout<<"[";
				cout<<men[i]<<"-"<<women[POSSIBLE_WIFE[i].value()];
				if( i == men.size()-1)cout<<"]"<<endl;
				else cout<<",";
			}
			cout<<"Time: "<<(endtime-starttime)/CLOCKS_PER_SEC<<" sec"<<endl<<endl;
			solution_flag=true;
		}
		endtime = clock();
		if(solution_flag == false)	cout<<"No ("<<(endtime-starttime)/CLOCKS_PER_SEC<<" sec)"<<endl;
		else				cout<<"Yes ("<<(endtime-starttime)/CLOCKS_PER_SEC<<" sec)"<<endl;
	}  catch (exception& exc)  {
		cerr << exc.what() << "\n";
	}  catch (...)  {
		cerr << "Unknown exception" << "\n";
	}
	exit(EXIT_SUCCESS);
}