///////////////////////////////////////////////////////////////
// File: cnf2ilog.cpp
// Auth: Sathi
// Date:  Jun  21  2004
//////////////////////////////////////////////////////////////

#include <ilsolver/ilosolverany.h>


ILOSTLBEGIN

#include <vector>
#include <set>
#include <cmath>
#include <iostream>
#include <fstream>
#include <cstdio>
#include <cstdlib>
#include <cstring>
#include <ctime>

#include <time.h>
clock_t worst;

using namespace std;



struct assignment_pair{
	int varid;
	int value;
};


vector<int> readClause(char* line,int lineNo,int varNum) {
  // line defines a term
  int lit;

  vector<int> litList;

  if (sscanf(line,"%i",&lit) != 1) {
    cout << "Error line " << lineNo << ": enable to match lit pattern\n";
    exit(1);
  }
   //cerr<<lit<<endl;

  while (lit != 0) // list of literals is terminated by 0
    {

      if (abs(lit) > varNum) {
	cout << "Error line " << lineNo << ": var number of literal " << lit << " exeeds number of vars\n";
	cout <<abs(lit)<<endl;
	cout<<"curr line is "<<line<<endl;
	cout<<varNum<<endl;
	exit(1);
      }

      // lit is legal add it to list
      litList.push_back(lit);

      // scan next lit
      while (*line == ' ' || *line == '\t')
      {
      	line++;
      }

      while (*line != ' ' && *line != '\t' ) line++;

      while (*line == ' ' || *line == '\t') line++;

      if (sscanf(line,"%i",&lit) != 1) {
	cout << "Error line " << lineNo << ": enable to match lit pattern\n";
	exit(1);
      }
    }

  if (litList.size() == 0) {
    cout << "Error line " << lineNo << ": literal list is empty\n";
    exit(1);
  }

  return litList;
}




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



  IloEnv env;
  try {
    IloModel mdl(env);

	char inName[512] = "";
	strcpy(inName,argv[1]);
 // open files
  FILE *in;
  if ( (in = fopen(inName,"r")) == NULL ) {
    cout << "Error: could not open " << inName << endl;
    exit(1);
  }


  //+++++++++++++++++++++++++++++
  // Read input
  //+++++++++++++++++++++++++++++

  char line[2048];
  int varNum;
  int clauseNum;
  vector< vector<int> > clause;

  int lineNo = 0;
  while (fgets(line,2048,in) != NULL)
    {

      lineNo++;
      //cerr<<"Line :"<<lineNo<<" is "<<line<<endl;

      // ignore empty lines
      if (line[0] != '\n')
	// ignore comments
	if (line[0] != 'c')
	  // line defines cnf format
	  if (line[0] == 'p')
	    {
	      if (sscanf(line,"p cnf %i %i",&varNum,&clauseNum) != 2) {
		cout << "Error line " << lineNo << ": enable to match pattern for cnf definition line \"p cnf . .\"\n";
		exit(1);
	      }
	    }
	  else // line defines a clause read it
	    clause.push_back(readClause(line,lineNo,varNum));
    }



  IloIntVarArray v(env,varNum,0,1);
  vector<int> varDom;
  vector<IloIntVar*> varPtr;

   for(int i=0; i<varNum;i++){
		varPtr.push_back(&(v[i]));
		varDom.push_back(2);

   }


  vector<IloConstraint>   constraint;
  constraint.resize(((clause.size()+varNum)/5000));

  if((clause.size()+varNum)%5000 != 0)
    constraint.resize(constraint.size()+1);


  for (int i=0; i < clause.size()+varNum; i++)
    {

       IloConstraint  cls;
     if(i<clause.size())
     {

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


		if (j==0){
		        if(abs(clause[i][j])<0 || abs(clause[i][j])>varNum)
			  cerr<<"Literal out of range "<<abs(clause[i][j])<<endl;
			if(clause[i][j]<0)
			   cls=(*varPtr[abs(clause[i][j])-1] ==0 );
			else
			   cls=(*varPtr[abs(clause[i][j])-1]==1);
		}
		else{
		        if(abs(clause[i][j])<0 || abs(clause[i][j])>varNum)
			      cerr<<"Literal out of range2"<<abs(clause[i][j])<<endl;

			if(clause[i][j]<0)
			   cls=(cls||(*varPtr[abs(clause[i][j])-1]==0));
			else
			   cls=(cls||(*varPtr[abs(clause[i][j])-1]==1));

		}
	 }

	 if(i%5000==0)
	 {
		constraint[i/5000]=cls;
	 }else
	 {
	 	constraint[i/5000]= constraint[i/5000]&&cls;
	 }
        }
        else{
	  int k= i-clause.size();
	  cls=((*varPtr[k]==0) || (*varPtr[k]==1));

         if(i%5000==0)
	 {
		constraint[i/5000]=cls;
	 }else
	 {
	 	constraint[i/5000]= constraint[i/5000]&&cls;
	 }

        }


      }

	for(int i=0 ;i<constraint.size(); i++){
		mdl.add(constraint[i]);
	}



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




  //  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[2]);
  if (!ti) { cerr << argv[2] << " 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;


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

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

      			mdl.remove(current);
      		}

      	}




      	itr_count++;

    	cout<<"\rRequest No : "<<itr_count<<flush;

				clock_t t2=clock();

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

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


      	old_num_assigns = num_assigns;
      	num_assigns = 0;


      } 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;
}