///////////////////////////////////////////////////////////////
// File: parity32_13.cpp
// Desc: Parity SAT problem. Follow the link below for a description
//       http://www.intellektik.informatik.tu-darmstadt.de/SATLIB/
//       Benchmarks/SAT/DIMACS/PARITY/descr.html
//       Secret parity function is: 00100010100111111101101100100110
// Auth: RMJ, VeCoS, ITU
// Date: Tue Jun  1 19:53:25 2004
//////////////////////////////////////////////////////////////

#include <ilsolver/ilosolverany.h>
#include <stdlib.h>
#include <fstream.h>
#include <time.h>
clock_t worst;

ILOSTLBEGIN


struct assignment_pair{
	int varid;
	int value;
};




int main(int argc, char** argv) {
  if (argc < 2)
    {
      cerr << "Usage: parity? <in trace .ti file>\n ";
      exit(1);
    }

  IloEnv env;
  try {
    IloModel mdl(env);

    IloIntVarArray a(env,32,0,1);

  ////////////////////////////////////////////////////////////
  // Make aux. data structures for interactive configuration
  ///////////////////////////////////////////////////////////

  vector<int> varDom;
  vector<IloIntVar*> varPtr;
  vector<string> varName;
    varPtr.push_back(&a[0]);
    varName.push_back("a[0]");
    varDom.push_back(2);
    varPtr.push_back(&a[1]);
    varName.push_back("a[1]");
    varDom.push_back(2);
    varPtr.push_back(&a[2]);
    varName.push_back("a[2]");
    varDom.push_back(2);
    varPtr.push_back(&a[3]);
    varName.push_back("a[3]");
    varDom.push_back(2);
    varPtr.push_back(&a[4]);
    varName.push_back("a[4]");
    varDom.push_back(2);
    varPtr.push_back(&a[5]);
    varName.push_back("a[5]");
    varDom.push_back(2);
    varPtr.push_back(&a[6]);
    varName.push_back("a[6]");
    varDom.push_back(2);
    varPtr.push_back(&a[7]);
    varName.push_back("a[7]");
    varDom.push_back(2);
    varPtr.push_back(&a[8]);
    varName.push_back("a[8]");
    varDom.push_back(2);
    varPtr.push_back(&a[9]);
    varName.push_back("a[9]");
    varDom.push_back(2);
    varPtr.push_back(&a[10]);
    varName.push_back("a[10]");
    varDom.push_back(2);
    varPtr.push_back(&a[11]);
    varName.push_back("a[11]");
    varDom.push_back(2);
    varPtr.push_back(&a[12]);
    varName.push_back("a[12]");
    varDom.push_back(2);
    varPtr.push_back(&a[13]);
    varName.push_back("a[13]");
    varDom.push_back(2);
    varPtr.push_back(&a[14]);
    varName.push_back("a[14]");
    varDom.push_back(2);
    varPtr.push_back(&a[15]);
    varName.push_back("a[15]");
    varDom.push_back(2);
    varPtr.push_back(&a[16]);
    varName.push_back("a[16]");
    varDom.push_back(2);
    varPtr.push_back(&a[17]);
    varName.push_back("a[17]");
    varDom.push_back(2);
    varPtr.push_back(&a[18]);
    varName.push_back("a[18]");
    varDom.push_back(2);
    varPtr.push_back(&a[19]);
    varName.push_back("a[19]");
    varDom.push_back(2);
    varPtr.push_back(&a[20]);
    varName.push_back("a[20]");
    varDom.push_back(2);
    varPtr.push_back(&a[21]);
    varName.push_back("a[21]");
    varDom.push_back(2);
    varPtr.push_back(&a[22]);
    varName.push_back("a[22]");
    varDom.push_back(2);
    varPtr.push_back(&a[23]);
    varName.push_back("a[23]");
    varDom.push_back(2);
    varPtr.push_back(&a[24]);
    varName.push_back("a[24]");
    varDom.push_back(2);
    varPtr.push_back(&a[25]);
    varName.push_back("a[25]");
    varDom.push_back(2);
    varPtr.push_back(&a[26]);
    varName.push_back("a[26]");
    varDom.push_back(2);
    varPtr.push_back(&a[27]);
    varName.push_back("a[27]");
    varDom.push_back(2);
    varPtr.push_back(&a[28]);
    varName.push_back("a[28]");
    varDom.push_back(2);
    varPtr.push_back(&a[29]);
    varName.push_back("a[29]");
    varDom.push_back(2);
    varPtr.push_back(&a[30]);
    varName.push_back("a[30]");
    varDom.push_back(2);
    varPtr.push_back(&a[31]);
    varName.push_back("a[31]");
    varDom.push_back(2);


  //  keep 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;



    mdl.add(   (0.0 != a[0] != a[3] != a[4] != a[6] != a[8] != a[11] != a[13] != a[15] != a[17] != a[18] != a[19] != a[23] != a[24] != a[27] != a[29] != a[31] != 1.0 )
             + (0.0 != a[0] != a[3] != a[5] != a[6] != a[8] != a[10] != a[11] != a[12] != a[13] != a[15] != a[17] != a[18] != a[21] != a[23] != a[24] != a[26] != a[27] != a[28] != a[29] != 0.0 )
             + (0.0 != a[0] != a[2] != a[3] != a[4] != a[5] != a[6] != a[8] != a[12] != a[17] != a[22] != a[26] != a[27] != a[28] != 1.0 )
             + (0.0 != a[1] != a[5] != a[7] != a[11] != a[12] != a[14] != a[15] != a[16] != a[18] != a[19] != a[22] != a[23] != a[24] != a[25] != a[28] != a[30] != a[31] != 1.0 )
             + (0.0 != a[1] != a[2] != a[11] != a[13] != a[15] != a[16] != a[17] != a[22] != a[23] != a[24] != a[25] != a[26] != a[30] != 0.0 )
             + (0.0 != a[0] != a[1] != a[4] != a[7] != a[10] != a[13] != a[14] != a[15] != a[16] != a[18] != a[19] != a[23] != a[25] != a[26] != a[31] != 1.0 )
             + (0.0 != a[0] != a[2] != a[4] != a[7] != a[9] != a[13] != a[15] != a[16] != a[17] != a[19] != a[25] != a[30] != a[31] != 1.0 )
             + (0.0 != a[1] != a[3] != a[4] != a[6] != a[7] != a[8] != a[9] != a[11] != a[14] != a[16] != a[17] != a[18] != a[19] != a[22] != a[24] != a[25] != a[27] != a[28] != a[29] != a[30] != 0.0 )
             + (0.0 != a[1] != a[2] != a[3] != a[4] != a[6] != a[8] != a[9] != a[10] != a[12] != a[17] != a[20] != a[21] != a[23] != a[24] != a[28] != a[29] != 0.0 )
             + (0.0 != a[2] != a[3] != a[6] != a[8] != a[9] != a[12] != a[14] != a[15] != a[16] != a[17] != a[18] != a[19] != a[21] != a[23] != a[24] != a[27] != a[30] != 1.0 )
             + (0.0 != a[3] != a[4] != a[5] != a[6] != a[9] != a[10] != a[12] != a[14] != a[16] != a[17] != a[18] != a[19] != a[21] != a[22] != a[25] != a[26] != a[28] != 1.0 )
             + (0.0 != a[2] != a[3] != a[8] != a[9] != a[12] != a[16] != a[18] != a[19] != a[20] != a[22] != a[23] != a[24] != a[26] != a[27] != a[30] != a[31] != 0.0 )
             + (0.0 != a[6] != a[7] != a[8] != a[9] != a[10] != a[12] != a[13] != a[16] != a[19] != a[21] != a[26] != a[30] != 0.0 ) <= 3.0 );

  ////////////////////////////////
  // Do interactive configuration
  // from trace file
  ///////////////////////////////

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

  IloSolver solver(mdl);

  do{

	  			   clock_t t1=clock();

      	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++){
      			mdl.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] = mdl.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 = mdl.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;
				   }
 				}
				else
					var_isvalid[i][j]=0;

				solver.endSearch();



      			mdl.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 (is_assigned[i])
           //           cout << " is assigned";
           //         else
           //           for (int j = 0; j < varDom[i]; j++)
           //   	   if (var_isvalid[i][j])
           //   	   cout << " " << j;
           //     cout << endl;
           //   }
           // cout << "\n\n";
           // cout.flush();


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


		clock_t t2=clock();

		if(itr_count==0)  worst = (t2-t1);

		if(worst < (t2-t1)) worst = (t2-t1);


      } while (inp != -2);

  solver.out() << "End Simulation of " << itr_count << " Requests" << endl;
	solver.out()<<"Worst Time is "<<(worst/(double)CLOCKS_PER_SEC) << endl;


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