/*PM generated from Renault Car benchmark*/
/* Reference :
Amilhastre, J., Fargier, H., Marquis, P.: Consistency restoration
and explanations in dynamic CSPs-application to configuration.
Artificial Intelligence (1-2) (2002) 199--234
ftp://fpt.irit.fr/pub/IRIT/RPDMP/Configuration/
*/

/////////////////////////////////////////////////
// renault.cpp  // code for ILOG Solver 6.0
// Sathi
// IT-University of Copenhagen  07-April-2004
/////////////////////////////////////////////////

#include <ilsolver/ilosolverany.h>
#include <stdlib.h>
#include <fstream.h>


# include <iostream.h>
#include  <vector.h>
#include  <set.h>

ILOSTLBEGIN


int getID(set<string> &s, string value){
   set<string>::iterator i;
     int loc=0;			//
     for (i= s.begin(); i != s.end(); ++i){
       if (value.compare(*i)==0){
           return loc;
	   }
	   loc++;
     }



     //cerr<<"Error : unable to locate "<<endl;
     //cerr<<value<<endl;
     //exit(1);

     return -1;
}



struct assignment_pair{
	int varid;
	int value;
};


int main(int argc, char** argv) {

  if (argc < 2)
    {
      cerr << "Usage: psr? <in trace .ti file>\n ";
      exit(1);
    }


  IloEnv env;
  try {
    IloModel model(env);


    vector<int> varDom;
    vector<IloIntVar*> varPtr;

	IloIntVar var0(env,0,8);
	varPtr.push_back(&var0);
	varDom.push_back(9);
	IloIntVar var1(env,0,4);
	varPtr.push_back(&var1);
	varDom.push_back(5);
	IloIntVar var2(env,0,24);
	varPtr.push_back(&var2);
	varDom.push_back(25);
	IloIntVar var3(env,0,1);
	varPtr.push_back(&var3);
	varDom.push_back(2);
	IloIntVar var4(env,0,41);
	varPtr.push_back(&var4);
	varDom.push_back(42);
	IloIntVar var5(env,0,1);
	varPtr.push_back(&var5);
	varDom.push_back(2);
	IloIntVar var6(env,0,1);
	varPtr.push_back(&var6);
	varDom.push_back(2);
	IloIntVar var7(env,0,1);
	varPtr.push_back(&var7);
	varDom.push_back(2);
	IloIntVar var8(env,0,1);
	varPtr.push_back(&var8);
	varDom.push_back(2);
	IloIntVar var9(env,0,0);
	varPtr.push_back(&var9);
	varDom.push_back(1);
	IloIntVar var10(env,0,1);
	varPtr.push_back(&var10);
	varDom.push_back(2);
	IloIntVar var11(env,0,1);
	varPtr.push_back(&var11);
	varDom.push_back(2);
	IloIntVar var12(env,0,1);
	varPtr.push_back(&var12);
	varDom.push_back(2);
	IloIntVar var13(env,0,5);
	varPtr.push_back(&var13);
	varDom.push_back(6);
	IloIntVar var14(env,0,1);
	varPtr.push_back(&var14);
	varDom.push_back(2);
	IloIntVar var15(env,0,1);
	varPtr.push_back(&var15);
	varDom.push_back(2);
	IloIntVar var16(env,0,0);
	varPtr.push_back(&var16);
	varDom.push_back(1);
	IloIntVar var17(env,0,1);
	varPtr.push_back(&var17);
	varDom.push_back(2);
	IloIntVar var18(env,0,1);
	varPtr.push_back(&var18);
	varDom.push_back(2);
	IloIntVar var19(env,0,1);
	varPtr.push_back(&var19);
	varDom.push_back(2);
	IloIntVar var20(env,0,1);
	varPtr.push_back(&var20);
	varDom.push_back(2);
	IloIntVar var21(env,0,1);
	varPtr.push_back(&var21);
	varDom.push_back(2);
	IloIntVar var22(env,0,1);
	varPtr.push_back(&var22);
	varDom.push_back(2);
	IloIntVar var23(env,0,0);
	varPtr.push_back(&var23);
	varDom.push_back(1);
	IloIntVar var24(env,0,2);
	varPtr.push_back(&var24);
	varDom.push_back(3);
	IloIntVar var25(env,0,2);
	varPtr.push_back(&var25);
	varDom.push_back(3);
	IloIntVar var26(env,0,1);
	varPtr.push_back(&var26);
	varDom.push_back(2);
	IloIntVar var27(env,0,1);
	varPtr.push_back(&var27);
	varDom.push_back(2);
	IloIntVar var28(env,0,1);
	varPtr.push_back(&var28);
	varDom.push_back(2);
	IloIntVar var29(env,0,2);
	varPtr.push_back(&var29);
	varDom.push_back(3);
	IloIntVar var30(env,0,5);
	varPtr.push_back(&var30);
	varDom.push_back(6);
	IloIntVar var31(env,0,1);
	varPtr.push_back(&var31);
	varDom.push_back(2);
	IloIntVar var32(env,0,1);
	varPtr.push_back(&var32);
	varDom.push_back(2);
	IloIntVar var33(env,0,2);
	varPtr.push_back(&var33);
	varDom.push_back(3);
	IloIntVar var34(env,0,1);
	varPtr.push_back(&var34);
	varDom.push_back(2);
	IloIntVar var35(env,0,0);
	varPtr.push_back(&var35);
	varDom.push_back(1);
	IloIntVar var36(env,0,1);
	varPtr.push_back(&var36);
	varDom.push_back(2);
	IloIntVar var37(env,0,2);
	varPtr.push_back(&var37);
	varDom.push_back(3);
	IloIntVar var38(env,0,1);
	varPtr.push_back(&var38);
	varDom.push_back(2);
	IloIntVar var39(env,0,2);
	varPtr.push_back(&var39);
	varDom.push_back(3);
	IloIntVar var40(env,0,2);
	varPtr.push_back(&var40);
	varDom.push_back(3);
	IloIntVar var41(env,0,2);
	varPtr.push_back(&var41);
	varDom.push_back(3);
	IloIntVar var42(env,0,1);
	varPtr.push_back(&var42);
	varDom.push_back(2);
	IloIntVar var43(env,0,1);
	varPtr.push_back(&var43);
	varDom.push_back(2);
	IloIntVar var44(env,0,1);
	varPtr.push_back(&var44);
	varDom.push_back(2);
	IloIntVar var45(env,0,2);
	varPtr.push_back(&var45);
	varDom.push_back(3);
	IloIntVar var46(env,0,1);
	varPtr.push_back(&var46);
	varDom.push_back(2);
	IloIntVar var47(env,0,0);
	varPtr.push_back(&var47);
	varDom.push_back(1);
	IloIntVar var48(env,0,1);
	varPtr.push_back(&var48);
	varDom.push_back(2);
	IloIntVar var49(env,0,3);
	varPtr.push_back(&var49);
	varDom.push_back(4);
	IloIntVar var50(env,0,1);
	varPtr.push_back(&var50);
	varDom.push_back(2);
	IloIntVar var51(env,0,1);
	varPtr.push_back(&var51);
	varDom.push_back(2);
	IloIntVar var52(env,0,2);
	varPtr.push_back(&var52);
	varDom.push_back(3);
	IloIntVar var53(env,0,1);
	varPtr.push_back(&var53);
	varDom.push_back(2);
	IloIntVar var54(env,0,1);
	varPtr.push_back(&var54);
	varDom.push_back(2);
	IloIntVar var55(env,0,12);
	varPtr.push_back(&var55);
	varDom.push_back(13);
	IloIntVar var56(env,0,1);
	varPtr.push_back(&var56);
	varDom.push_back(2);
	IloIntVar var57(env,0,1);
	varPtr.push_back(&var57);
	varDom.push_back(2);
	IloIntVar var58(env,0,1);
	varPtr.push_back(&var58);
	varDom.push_back(2);
	IloIntVar var59(env,0,1);
	varPtr.push_back(&var59);
	varDom.push_back(2);
	IloIntVar var60(env,0,1);
	varPtr.push_back(&var60);
	varDom.push_back(2);
	IloIntVar var61(env,0,4);
	varPtr.push_back(&var61);
	varDom.push_back(5);
	IloIntVar var62(env,0,1);
	varPtr.push_back(&var62);
	varDom.push_back(2);
	IloIntVar var63(env,0,1);
	varPtr.push_back(&var63);
	varDom.push_back(2);
	IloIntVar var64(env,0,4);
	varPtr.push_back(&var64);
	varDom.push_back(5);
	IloIntVar var65(env,0,2);
	varPtr.push_back(&var65);
	varDom.push_back(3);
	IloIntVar var66(env,0,1);
	varPtr.push_back(&var66);
	varDom.push_back(2);
	IloIntVar var67(env,0,2);
	varPtr.push_back(&var67);
	varDom.push_back(3);
	IloIntVar var68(env,0,0);
	varPtr.push_back(&var68);
	varDom.push_back(1);
	IloIntVar var69(env,0,10);
	varPtr.push_back(&var69);
	varDom.push_back(11);
	IloIntVar var70(env,0,4);
	varPtr.push_back(&var70);
	varDom.push_back(5);
	IloIntVar var71(env,0,4);
	varPtr.push_back(&var71);
	varDom.push_back(5);
	IloIntVar var72(env,0,11);
	varPtr.push_back(&var72);
	varDom.push_back(12);
	IloIntVar var73(env,0,1);
	varPtr.push_back(&var73);
	varDom.push_back(2);
	IloIntVar var74(env,0,1);
	varPtr.push_back(&var74);
	varDom.push_back(2);
	IloIntVar var75(env,0,1);
	varPtr.push_back(&var75);
	varDom.push_back(2);
	IloIntVar var76(env,0,1);
	varPtr.push_back(&var76);
	varDom.push_back(2);
	IloIntVar var77(env,0,6);
	varPtr.push_back(&var77);
	varDom.push_back(7);
	IloIntVar var78(env,0,1);
	varPtr.push_back(&var78);
	varDom.push_back(2);
	IloIntVar var79(env,0,4);
	varPtr.push_back(&var79);
	varDom.push_back(5);
	IloIntVar var80(env,0,3);
	varPtr.push_back(&var80);
	varDom.push_back(4);
	IloIntVar var81(env,0,1);
	varPtr.push_back(&var81);
	varDom.push_back(2);
	IloIntVar var82(env,0,1);
	varPtr.push_back(&var82);
	varDom.push_back(2);
	IloIntVar var83(env,0,1);
	varPtr.push_back(&var83);
	varDom.push_back(2);
	IloIntVar var84(env,0,1);
	varPtr.push_back(&var84);
	varDom.push_back(2);
	IloIntVar var85(env,0,1);
	varPtr.push_back(&var85);
	varDom.push_back(2);
	IloIntVar var86(env,0,2);
	varPtr.push_back(&var86);
	varDom.push_back(3);
	IloIntVar var87(env,0,2);
	varPtr.push_back(&var87);
	varDom.push_back(3);
	IloIntVar var88(env,0,1);
	varPtr.push_back(&var88);
	varDom.push_back(2);
	IloIntVar var89(env,0,4);
	varPtr.push_back(&var89);
	varDom.push_back(5);
	IloIntVar var90(env,0,1);
	varPtr.push_back(&var90);
	varDom.push_back(2);
	IloIntVar var91(env,0,3);
	varPtr.push_back(&var91);
	varDom.push_back(4);
	IloIntVar var92(env,0,4);
	varPtr.push_back(&var92);
	varDom.push_back(5);
	IloIntVar var93(env,0,9);
	varPtr.push_back(&var93);
	varDom.push_back(10);
	IloIntVar var94(env,0,1);
	varPtr.push_back(&var94);
	varDom.push_back(2);
	IloIntVar var95(env,0,2);
	varPtr.push_back(&var95);
	varDom.push_back(3);
	IloIntVar var96(env,0,4);
	varPtr.push_back(&var96);
	varDom.push_back(5);
	IloIntVar var97(env,0,28);
	varPtr.push_back(&var97);
	varDom.push_back(29);
	IloIntVar var98(env,0,9);
	varPtr.push_back(&var98);
	varDom.push_back(10);


   // Add Rules


   set<string> var[102];
   vector<int> map;
   map.resize(102);
   int number;
   int         support_size;
   int         table_number;
   string eof("EOF");
   string contrainte("CONTRAINTE");
   string fincont("FINCONT");
   string lsqbr("[");
   string rsqbr("]");

   string inp_str;


   ifstream inf("renault.csp");
   inf>>inp_str;
   table_number=0;
   while(inp_str.compare(eof)!=0){
      if(inp_str.compare(contrainte)==0){
        table_number++;
        inf>>inp_str;
        if(inp_str.compare(lsqbr)==0){
   		 support_size=0;
   		 inf>>inp_str;
   		 while(inp_str.compare(rsqbr)!=0){
   			 map[support_size]=(int)atoi(inp_str.c_str())-1;
			  if(map[support_size]>36) map[support_size]-=2;
			 support_size++;
   			 inf>>inp_str;
   	     }
   	    // cerr<<"Size of Table "<<table_number<<" is "<<support_size<<endl;
   	     inf>>inp_str;

   		//for each tuple read it and map values into the corresponding set;
   		while(inp_str.compare(fincont)!=0){
   			for(int i=0;i<support_size;i++){
   				var[map[i]].insert(inp_str);
   				inf>>inp_str;
   			}
   		}
        }
        else{
         cerr<<"Error in parsing "<<endl; exit(1);
        }
    }
    inf>>inp_str;
   };

   IloConstraint rule;
   IloConstraint tuple;
   IloConstraint rule2,rule_combo;
   IloConstraint rulen[20];
   int  curr=-1;

   ifstream inf2("renault.csp");
   inf2>>inp_str;
   table_number=0;
   cout<<endl<<"rule"<<endl;
   int first_of_rule;
   int first_of_tuple;
   int tuple_count=0;
   int count=0;
   while(inp_str.compare(eof)!=0){
      if(inp_str.compare(contrainte)==0){
        table_number++;
        inf2>>inp_str;
        if(inp_str.compare(lsqbr)==0){
   		 support_size=0;
   		 inf2>>inp_str;
   		 while(inp_str.compare(rsqbr)!=0){
   			 map[support_size]=(int)atoi(inp_str.c_str())-1;
			  if(map[support_size]>36) map[support_size]-=2;
			 support_size++;
   			 inf2>>inp_str;
   	     }
   	    // cerr<<"Size of Table "<<table_number<<" is "<<support_size<<endl;
   	     inf2>>inp_str;
   		//for each tuple read it and map values into the corresponding set;
   		 int first_tuple=1;

   		while(inp_str.compare(fincont)!=0){

   			for(int i=0;i<support_size;i++){

   				int attr =  map[i];

				if(attr<0 || attr >98) {cerr<<"Attr value is unbounded .."<<attr<<endl;exit(1);}

   				int value = getID(var[map[i]], inp_str);

				if(value==-1) {
				  cerr<<"getID returned -1 "<<endl;
				  cerr<<"inp_str is "<<inp_str<<endl;
				  cerr<<"map[i] is "<<map[i]<<endl;
				  cerr<<"Tuple Count is "<<tuple_count<<endl;
				  cerr<<"i is "<<i<<endl;
				  cerr<<"curr is "<<curr<<endl;

				  exit(1);
				}


   				inf2>>inp_str;


   				if(i==0){
   					tuple = (*varPtr[attr] == value);
   				}
   				else{

   					tuple = tuple && (*varPtr[attr] == value);

   				}
   			}






		    if((tuple_count%5000)==0){
		    	curr++;
			rulen[curr] = tuple;
			tuple_count++;
  	 	    }
		   else{

		   	rulen[curr] = ( rulen[curr] || tuple );
			tuple_count++;
		   }

  		}

		rule = rulen[0];

		for(int i=1; i<=curr ; i++)
		{
			rule = rule || rulen[curr];
		}
		curr=-1;


		count++;
		if(tuple_count<50000 ){
		  model.add(rule);
		  cerr<<"Added Rule :"<<count<<" , which has "<<tuple_count<<" tuples"<<endl;
         	}
		else{

		  cerr<<"Not Added Rule :"<<count<<" , which has "<<tuple_count<<" tuples"<<endl;
		  exit(1);
	        }


		tuple_count=0;

		//if(count==65) break;
        }
        else{
         cerr<<"Error in parsing "<<endl; exit(1);
        }
    }
    inf2>>inp_str;
   };

   inf2.close();

  // Adding rules complete

   cerr<<"Adding Rules Complete "<<endl;


 // Sathi's approach for keeping track of interaction
  int**  var_isvalid = new int*[varPtr.size()];
  int*  is_assigned = new int[varPtr.size()];
  for(int i=0;i< varPtr.size();i++)
    {
      var_isvalid[i] = new int[varDom[i]];
      is_assigned[i] = 0;
      for(int j=0; j < varDom[i]; j++)
        var_isvalid[i][j] = 1;
    }

  int**  var_shownValidThisStep = new int*[varPtr.size()];
  for(int i=0;i< varPtr.size();i++)
    {
      var_shownValidThisStep[i] = new int[varDom[i]];
      for(int j=0; j < varDom[i]; j++)
        var_shownValidThisStep[i][j] = 0;
    }

  assignment_pair* assignments = new assignment_pair[varPtr.size()];
  assignment_pair* old_assignments = new assignment_pair[varPtr.size()];
  int old_num_assigns = 0;
  int start_from_scratch = 1;

  ifstream ti(argv[1]);
  if (!ti) { cerr << argv[1] << " cannot be opened\n"; exit(1); }
  int num_assigns = 0;
  int varid;
  int value;
  int inp;
  int inp2;
  int itr_count=0;
  ti >> inp; ti >> inp2;
  int start_assign = 0;



   IloExtractableArray iloextractablearray(env,varPtr.size());





    IloSolver solver(model);

    cerr<<"Obtained Model"<<endl;




  do{
      	for(int k = 0; k < old_num_assigns; k++)
      		old_assignments[k] = assignments[k];
      	ti >> inp; ti >> inp2;
      	while(inp != -1 && inp != -2){
      		varid = inp;
      		value = inp2;
      		assignments[num_assigns].varid = varid;
      		assignments[num_assigns].value = value;
      		//cerr<<"varid "<<varid<<"    "<<"value "<<value<<endl;
      		num_assigns++;
      		ti >> inp; ti >> inp2;
      	}

      	// make the assignments
      	// check for each valid value in previous request.
      	if(num_assigns == old_num_assigns + 1){
      		int i;
      		for(i = 0; i < old_num_assigns; i++){
      			if(assignments[i].varid != old_assignments[i].varid ||
                             assignments[i].value != old_assignments[i].value)
      				break;
      		}
      		if(i == old_num_assigns)
      			start_from_scratch = 0;
      		else
      			start_from_scratch = 1;

      	}
      	else
      		start_from_scratch=1;

      	if(start_from_scratch){
      		//remove old_num_assigns of iloextractable array constraints from the model
      		//valid all values are valid values
      		for(int i = 0; i < old_num_assigns; i++){
      			model.remove(iloextractablearray[i]);
      		}
      		for(int i = 0; i < varPtr.size(); i++)
      			for(int j = 0; j < varDom[i];j++)
      				var_isvalid[i][j] = 1;
      		for(int i = 0; i < varPtr.size(); i++)
      			is_assigned[i]=0;

      		start_assign = 0;
      	}
      	else
      	  start_assign = old_num_assigns;

      	for(int i = start_assign; i < num_assigns; i++){
      		iloextractablearray[i] = model.add(*varPtr[assignments[i].varid] == assignments[i].value);
                  // debug: I want to know what is assigned
                  //cout << "Assigned: " << varName[assignments[i].varid] << " = " << assignments[i].value << endl;
		// cout.flush();
      		is_assigned[assignments[i].varid] = 1;
      	}

      	for(int i = 0; i < varPtr.size(); i++)
      		for(int j = 0; j < varDom[i];j++)
      			var_shownValidThisStep[i][j] = 0;
      	for(int i = 0; i < varPtr.size(); i++){

      		if (is_assigned[i]) continue;

      		for(int j = 0; j < varDom[i]; j++) {

      			if (!var_isvalid[i][j]) continue;
      			if (var_shownValidThisStep[i][j]) continue;

                         cout << "i=" << i << " j=" << j << endl;
                         cout.flush();

      			IloExtractable current = model.add(*varPtr[i] == j);

      			solver.startNewSearch();

      			if( solver.next() )
      			   for (int g = 0; g < varPtr.size(); g++) {
      			      var_shownValidThisStep[g][int(solver.getValue(*varPtr[g]))] = 1;
      			      // cout << " fi=" << g << " fj=" << int(solver.getValue(*varPtr[g]));
      			      }
                          else
                             var_isvalid[i][j] = 0;

                          // cout << endl;
      			solver.endSearch();

      			model.remove(current);
      		}

      	}



	/*
           // debug: print possible remaining values for each variable
            cout << "\nRemaing values of variable domains\n";
            for (int i = 0; i < varPtr.size(); i++)
              {
                cout << varName[i] << "(" << i << ") ";
                if (varDom[i] == 3) // line
                  {
                    if (is_assigned[i])
                      cout << " is assigned";
                    else
                      for (int j = 0; j < varDom[i]; j++)
              	   if (var_isvalid[i][j])
              	   cout << " " << strOfvalueLine(j);
                  }
                else // switch
                  {
                    if (is_assigned[i])
                      cout << " is assigned";
                    else
                      for (int j = 0; j < varDom[i]; j++)
              	   if (var_isvalid[i][j])
              	   cout << " " << strOfvalueSwitch(j);
                  }
                cout << endl;
              }
            cout << "\n\n";
            cout.flush();
*/

      	itr_count++;
      	old_num_assigns = num_assigns;
      	num_assigns = 0;


      } while (inp != -2);

  solver.out() << "End Simulation of " << itr_count << " Requests" << endl;

	  }
  catch (IloException& ex) {
    cerr << "Error: " << ex << endl;
  }
  env.end();
  return 0;
}