///////////////////////////////////////////////////////////////
// File: psr1.cpp number of planes n=1
// Desc: PSR problem. Follow the link below for a description
//       http://discus.anu.edu.au/~thiebaux
//       The planes are connected by a connector on line 39.
//       When n=1, line 39 is dangling as usual.
//       Obs. the file reads a tracefile with the name psr1.ti
// Auth: RMJ, VeCoS, ITU
// Date: Tue May 18 16:50:51 2004
//////////////////////////////////////////////////////////////

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

ILOSTLBEGIN



// Aux functions for printing assignment information

string strOfvalueLine(int val) {
  if (val == 0)
    return string("noFlow");
  else if (val == 1)
    return string("posFlow");
  else if (val == 2)
    return string("negFlow");
  else
    {
      cerr << "Value " << val << " of a Line is not possible\n";
	exit(1);
    }
}


string strOfvalueSwitch(int val) {
  if (val == 0)
    return string("on");
  else if (val == 1)
    return string("off");
  else
    {
      cerr << "Value " << val << " of a Switch is not possible\n";
	exit(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);
    }

  //////////////////
  // Make PSR model
  //////////////////

  IloEnv env;
  try {
    IloModel mdl(env);

      // 0: noFlow, 1: posFlow, 2: negFlow
    IloIntVar p1L1(env,0,2);
    IloIntVar p1L2(env,0,2);
    IloIntVar p1L3(env,0,2);
    IloIntVar p1L4(env,0,2);
    IloIntVar p1L5(env,0,2);
    IloIntVar p1L6(env,0,2);
    IloIntVar p1L7(env,0,2);
    IloIntVar p1L8(env,0,2);
    IloIntVar p1L9(env,0,2);
    IloIntVar p1L10(env,0,2);
    IloIntVar p1L11(env,0,2);
    IloIntVar p1L12(env,0,2);
    IloIntVar p1L13(env,0,2);
    IloIntVar p1L14(env,0,2);
    IloIntVar p1L15(env,0,2);
    IloIntVar p1L16(env,0,2);
    IloIntVar p1L17(env,0,2);
    IloIntVar p1L18(env,0,2);
    IloIntVar p1L19(env,0,2);
    IloIntVar p1L20(env,0,2);
    IloIntVar p1L21(env,0,2);
    IloIntVar p1L22(env,0,2);
    IloIntVar p1L23(env,0,2);
    IloIntVar p1L24(env,0,2);
    IloIntVar p1L25(env,0,2);
    IloIntVar p1L26(env,0,2);
    IloIntVar p1L27(env,0,2);
    IloIntVar p1L28(env,0,2);
    IloIntVar p1L29(env,0,2);
    IloIntVar p1L30(env,0,2);
    IloIntVar p1L31(env,0,2);
    IloIntVar p1L32(env,0,2);
    IloIntVar p1L33(env,0,2);
    IloIntVar p1L34(env,0,2);
    IloIntVar p1L35(env,0,2);
    IloIntVar p1L36(env,0,2);
    IloIntVar p1L37(env,0,2);
    IloIntVar p1L38(env,0,2);
    IloIntVar p1L39(env,0,2);
    IloIntVar p1L40(env,0,2);
    IloIntVar p1L41(env,0,2);
    IloIntVar p1L42(env,0,2);
    IloIntVar p1L43(env,0,2);
    IloIntVar p1L44(env,0,2);
    IloIntVar p1L45(env,0,2);
      // 0: on, 1: off
    IloIntVar p1CB1(env,0,1);
    IloIntVar p1CB2(env,0,1);
    IloIntVar p1CB3(env,0,1);
    IloIntVar p1CB4(env,0,1);
    IloIntVar p1CB5(env,0,1);
    IloIntVar p1CB6(env,0,1);
    IloIntVar p1CB7(env,0,1);
      // 0: on, 1: off
    IloIntVar p1SD50(env,0,1);
    IloIntVar p1SD40(env,0,1);
    IloIntVar p1SD42(env,0,1);
    IloIntVar p1SD43(env,0,1);
    IloIntVar p1SD44(env,0,1);
    IloIntVar p1SD41(env,0,1);
    IloIntVar p1SD52(env,0,1);
    IloIntVar p1SD51(env,0,1);
    IloIntVar p1SD30(env,0,1);
    IloIntVar p1SD31(env,0,1);
    IloIntVar p1SD71(env,0,1);
    IloIntVar p1SD70(env,0,1);
    IloIntVar p1SD53(env,0,1);
    IloIntVar p1SD20(env,0,1);
    IloIntVar p1SD21(env,0,1);
    IloIntVar p1SD32(env,0,1);
    IloIntVar p1SD34(env,0,1);
    IloIntVar p1SD72(env,0,1);
    IloIntVar p1SD33(env,0,1);
    IloIntVar p1SD61(env,0,1);
    IloIntVar p1SD60(env,0,1);
    IloIntVar p1SD62(env,0,1);
    IloIntVar p1SD10(env,0,1);
    IloIntVar p1SD11(env,0,1);
    IloIntVar p1SD12(env,0,1);
    IloIntVar p1SD13(env,0,1);


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

  vector<int> varDom;
  vector<IloIntVar*> varPtr;
  vector<string> varName;
  varPtr.push_back(&p1CB4);
  varName.push_back("p1CB4");
  varDom.push_back(2);
  varPtr.push_back(&p1L3);
  varName.push_back("p1L3");
  varDom.push_back(3);
  varPtr.push_back(&p1SD40);
  varName.push_back("p1SD40");
  varDom.push_back(2);
  varPtr.push_back(&p1L4);
  varName.push_back("p1L4");
  varDom.push_back(3);
  varPtr.push_back(&p1L8);
  varName.push_back("p1L8");
  varDom.push_back(3);
  varPtr.push_back(&p1SD41);
  varName.push_back("p1SD41");
  varDom.push_back(2);
  varPtr.push_back(&p1L9);
  varName.push_back("p1L9");
  varDom.push_back(3);
  varPtr.push_back(&p1SD52);
  varName.push_back("p1SD52");
  varDom.push_back(2);
  varPtr.push_back(&p1L10);
  varName.push_back("p1L10");
  varDom.push_back(3);
  varPtr.push_back(&p1SD51);
  varName.push_back("p1SD51");
  varDom.push_back(2);
  varPtr.push_back(&p1L45);
  varName.push_back("p1L45");
  varDom.push_back(3);
  varPtr.push_back(&p1L2);
  varName.push_back("p1L2");
  varDom.push_back(3);
  varPtr.push_back(&p1SD50);
  varName.push_back("p1SD50");
  varDom.push_back(2);
  varPtr.push_back(&p1L1);
  varName.push_back("p1L1");
  varDom.push_back(3);
  varPtr.push_back(&p1CB5);
  varName.push_back("p1CB5");
  varDom.push_back(2);
  varPtr.push_back(&p1L44);
  varName.push_back("p1L44");
  varDom.push_back(3);
  varPtr.push_back(&p1SD53);
  varName.push_back("p1SD53");
  varDom.push_back(2);
  varPtr.push_back(&p1L43);
  varName.push_back("p1L43");
  varDom.push_back(3);
  varPtr.push_back(&p1SD13);
  varName.push_back("p1SD13");
  varDom.push_back(2);
  varPtr.push_back(&p1L20);
  varName.push_back("p1L20");
  varDom.push_back(3);
  varPtr.push_back(&p1SD12);
  varName.push_back("p1SD12");
  varDom.push_back(2);
  varPtr.push_back(&p1L11);
  varName.push_back("p1L11");
  varDom.push_back(3);
  varPtr.push_back(&p1L41);
  varName.push_back("p1L41");
  varDom.push_back(3);
  varPtr.push_back(&p1SD11);
  varName.push_back("p1SD11");
  varDom.push_back(2);
  varPtr.push_back(&p1L40);
  varName.push_back("p1L40");
  varDom.push_back(3);
  varPtr.push_back(&p1L38);
  varName.push_back("p1L38");
  varDom.push_back(3);
  varPtr.push_back(&p1SD10);
  varName.push_back("p1SD10");
  varDom.push_back(2);
  varPtr.push_back(&p1L39);
  varName.push_back("p1L39");
  varDom.push_back(3);
  varPtr.push_back(&p1L37);
  varName.push_back("p1L37");
  varDom.push_back(3);
  varPtr.push_back(&p1CB1);
  varName.push_back("p1CB1");
  varDom.push_back(2);
  varPtr.push_back(&p1L42);
  varName.push_back("p1L42");
  varDom.push_back(3);
  varPtr.push_back(&p1SD62);
  varName.push_back("p1SD62");
  varDom.push_back(2);
  varPtr.push_back(&p1L36);
  varName.push_back("p1L36");
  varDom.push_back(3);
  varPtr.push_back(&p1L34);
  varName.push_back("p1L34");
  varDom.push_back(3);
  varPtr.push_back(&p1SD60);
  varName.push_back("p1SD60");
  varDom.push_back(2);
  varPtr.push_back(&p1L35);
  varName.push_back("p1L35");
  varDom.push_back(3);
  varPtr.push_back(&p1CB6);
  varName.push_back("p1CB6");
  varDom.push_back(2);
  varPtr.push_back(&p1L33);
  varName.push_back("p1L33");
  varDom.push_back(3);
  varPtr.push_back(&p1SD61);
  varName.push_back("p1SD61");
  varDom.push_back(2);
  varPtr.push_back(&p1L32);
  varName.push_back("p1L32");
  varDom.push_back(3);
  varPtr.push_back(&p1SD33);
  varName.push_back("p1SD33");
  varDom.push_back(2);
  varPtr.push_back(&p1L31);
  varName.push_back("p1L31");
  varDom.push_back(3);
  varPtr.push_back(&p1L23);
  varName.push_back("p1L23");
  varDom.push_back(3);
  varPtr.push_back(&p1SD21);
  varName.push_back("p1SD21");
  varDom.push_back(2);
  varPtr.push_back(&p1L22);
  varName.push_back("p1L22");
  varDom.push_back(3);
  varPtr.push_back(&p1SD20);
  varName.push_back("p1SD20");
  varDom.push_back(2);
  varPtr.push_back(&p1L21);
  varName.push_back("p1L21");
  varDom.push_back(3);
  varPtr.push_back(&p1CB2);
  varName.push_back("p1CB2");
  varDom.push_back(2);
  varPtr.push_back(&p1L24);
  varName.push_back("p1L24");
  varDom.push_back(3);
  varPtr.push_back(&p1SD32);
  varName.push_back("p1SD32");
  varDom.push_back(2);
  varPtr.push_back(&p1L25);
  varName.push_back("p1L25");
  varDom.push_back(3);
  varPtr.push_back(&p1L15);
  varName.push_back("p1L15");
  varDom.push_back(3);
  varPtr.push_back(&p1SD31);
  varName.push_back("p1SD31");
  varDom.push_back(2);
  varPtr.push_back(&p1L14);
  varName.push_back("p1L14");
  varDom.push_back(3);
  varPtr.push_back(&p1SD30);
  varName.push_back("p1SD30");
  varDom.push_back(2);
  varPtr.push_back(&p1L13);
  varName.push_back("p1L13");
  varDom.push_back(3);
  varPtr.push_back(&p1CB3);
  varName.push_back("p1CB3");
  varDom.push_back(2);
  varPtr.push_back(&p1L26);
  varName.push_back("p1L26");
  varDom.push_back(3);
  varPtr.push_back(&p1SD34);
  varName.push_back("p1SD34");
  varDom.push_back(2);
  varPtr.push_back(&p1L27);
  varName.push_back("p1L27");
  varDom.push_back(3);
  varPtr.push_back(&p1L28);
  varName.push_back("p1L28");
  varDom.push_back(3);
  varPtr.push_back(&p1SD72);
  varName.push_back("p1SD72");
  varDom.push_back(2);
  varPtr.push_back(&p1L29);
  varName.push_back("p1L29");
  varDom.push_back(3);
  varPtr.push_back(&p1L16);
  varName.push_back("p1L16");
  varDom.push_back(3);
  varPtr.push_back(&p1SD71);
  varName.push_back("p1SD71");
  varDom.push_back(2);
  varPtr.push_back(&p1L17);
  varName.push_back("p1L17");
  varDom.push_back(3);
  varPtr.push_back(&p1L18);
  varName.push_back("p1L18");
  varDom.push_back(3);
  varPtr.push_back(&p1SD70);
  varName.push_back("p1SD70");
  varDom.push_back(2);
  varPtr.push_back(&p1L30);
  varName.push_back("p1L30");
  varDom.push_back(3);
  varPtr.push_back(&p1L19);
  varName.push_back("p1L19");
  varDom.push_back(3);
  varPtr.push_back(&p1CB7);
  varName.push_back("p1CB7");
  varDom.push_back(2);
  varPtr.push_back(&p1L12);
  varName.push_back("p1L12");
  varDom.push_back(3);
  varPtr.push_back(&p1SD44);
  varName.push_back("p1SD44");
  varDom.push_back(2);
  varPtr.push_back(&p1L7);
  varName.push_back("p1L7");
  varDom.push_back(3);
  varPtr.push_back(&p1SD43);
  varName.push_back("p1SD43");
  varDom.push_back(2);
  varPtr.push_back(&p1L6);
  varName.push_back("p1L6");
  varDom.push_back(3);
  varPtr.push_back(&p1SD42);
  varName.push_back("p1SD42");
  varDom.push_back(2);
  varPtr.push_back(&p1L5);
  varName.push_back("p1L5");
  varDom.push_back(3);


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


  ////////////////////////////////////////////////////////////
  // Add rules
  ///////////////////////////////////////////////////////////

    mdl.add(p1CB1 != 0 || p1L37 == 1);
    mdl.add(p1CB1 != 1 || p1L37 != 1);

    mdl.add(p1CB2 != 0 || p1L21 == 1);
    mdl.add(p1CB2 != 1 || p1L21 != 1);

    mdl.add(p1CB3 != 0 || p1L13 == 1);
    mdl.add(p1CB3 != 1 || p1L13 != 1);

    mdl.add(p1CB4 != 0 || p1L3 == 1);
    mdl.add(p1CB4 != 1 || p1L3 != 1);

    mdl.add(p1CB5 != 0 || p1L1 == 1);
    mdl.add(p1CB5 != 1 || p1L1 != 1);

    mdl.add(p1CB6 != 0 || p1L35 == 2);
    mdl.add(p1CB6 != 1 || p1L35 != 2);

    mdl.add(p1CB7 != 0 || p1L19 == 2);
    mdl.add(p1CB7 != 1 || p1L19 != 2);

    mdl.add(p1SD50 != 0 || p1L1 == 0 && p1L2 == 0
        || p1L1 == 1 && p1L2 == 1
        || p1L1 == 2 && p1L2 == 2);
    mdl.add(p1SD50 != 1 || p1L1 != 2 && p1L2 != 1);

    mdl.add(p1SD40 != 0 || p1L3 == 0 && p1L4 == 0
        || p1L3 == 1 && p1L4 == 1
        || p1L3 == 2 && p1L4 == 2);
    mdl.add(p1SD40 != 1 || p1L3 != 2 && p1L4 != 1);

    mdl.add(p1SD42 != 0 || p1L5 == 0 && p1L6 == 0
        || p1L5 == 1 && p1L6 == 1
        || p1L5 == 2 && p1L6 == 2);
    mdl.add(p1SD42 != 1 || p1L5 != 2 && p1L6 != 1);

    mdl.add(p1SD43 != 0 || p1L6 == 0 && p1L7 == 0
        || p1L6 == 1 && p1L7 == 1
        || p1L6 == 2 && p1L7 == 2);
    mdl.add(p1SD43 != 1 || p1L6 != 2 && p1L7 != 1);

    mdl.add(p1SD44 != 0 || p1L7 == 0 && p1L12 == 0
        || p1L7 == 1 && p1L12 == 1
        || p1L7 == 2 && p1L12 == 2);
    mdl.add(p1SD44 != 1 || p1L7 != 2 && p1L12 != 1);

    mdl.add(p1SD41 != 0 || p1L8 == 0 && p1L9 == 0
        || p1L8 == 1 && p1L9 == 1
        || p1L8 == 2 && p1L9 == 2);
    mdl.add(p1SD41 != 1 || p1L8 != 2 && p1L9 != 1);

    mdl.add(p1SD52 != 0 || p1L9 == 0 && p1L10 == 0
        || p1L9 == 1 && p1L10 == 1
        || p1L9 == 2 && p1L10 == 2);
    mdl.add(p1SD52 != 1 || p1L9 != 2 && p1L10 != 1);

    mdl.add(p1SD51 != 0 || p1L10 == 0 && p1L45 == 0
        || p1L10 == 1 && p1L45 == 1
        || p1L10 == 2 && p1L45 == 2);
    mdl.add(p1SD51 != 1 || p1L10 != 2 && p1L45 != 1);

    mdl.add(p1SD30 != 0 || p1L13 == 0 && p1L14 == 0
        || p1L13 == 1 && p1L14 == 1
        || p1L13 == 2 && p1L14 == 2);
    mdl.add(p1SD30 != 1 || p1L13 != 2 && p1L14 != 1);

    mdl.add(p1SD31 != 0 || p1L14 == 0 && p1L15 == 0
        || p1L14 == 1 && p1L15 == 1
        || p1L14 == 2 && p1L15 == 2);
    mdl.add(p1SD31 != 1 || p1L14 != 2 && p1L15 != 1);

    mdl.add(p1SD71 != 0 || p1L16 == 0 && p1L17 == 0
        || p1L16 == 1 && p1L17 == 1
        || p1L16 == 2 && p1L17 == 2);
    mdl.add(p1SD71 != 1 || p1L16 != 2 && p1L17 != 1);

    mdl.add(p1SD70 != 0 || p1L18 == 0 && p1L30 == 0
        || p1L18 == 1 && p1L30 == 1
        || p1L18 == 2 && p1L30 == 2);
    mdl.add(p1SD70 != 1 || p1L18 != 2 && p1L30 != 1);

    mdl.add(p1SD53 != 0 || p1L44 == 0 && p1L43 == 0
        || p1L44 == 1 && p1L43 == 2
        || p1L44 == 2 && p1L43 == 1);
    mdl.add(p1SD53 != 1 || p1L44 != 2 && p1L43 != 2);

    mdl.add(p1SD20 != 0 || p1L21 == 0 && p1L22 == 0
        || p1L21 == 1 && p1L22 == 1
        || p1L21 == 2 && p1L22 == 2);
    mdl.add(p1SD20 != 1 || p1L21 != 2 && p1L22 != 1);

    mdl.add(p1SD21 != 0 || p1L22 == 0 && p1L23 == 0
        || p1L22 == 1 && p1L23 == 1
        || p1L22 == 2 && p1L23 == 2);
    mdl.add(p1SD21 != 1 || p1L22 != 2 && p1L23 != 1);

    mdl.add(p1SD32 != 0 || p1L24 == 0 && p1L25 == 0
        || p1L24 == 1 && p1L25 == 1
        || p1L24 == 2 && p1L25 == 2);
    mdl.add(p1SD32 != 1 || p1L24 != 2 && p1L25 != 1);

    mdl.add(p1SD34 != 0 || p1L26 == 0 && p1L27 == 0
        || p1L26 == 2 && p1L27 == 2
        || p1L26 == 1 && p1L27 == 1);
    mdl.add(p1SD34 != 1 || p1L26 != 1 && p1L27 != 2);

    mdl.add(p1SD72 != 0 || p1L28 == 0 && p1L29 == 0
        || p1L28 == 1 && p1L29 == 1
        || p1L28 == 2 && p1L29 == 2);
    mdl.add(p1SD72 != 1 || p1L28 != 2 && p1L29 != 1);

    mdl.add(p1SD33 != 0 || p1L31 == 0 && p1L32 == 0
        || p1L31 == 1 && p1L32 == 1
        || p1L31 == 2 && p1L32 == 2);
    mdl.add(p1SD33 != 1 || p1L31 != 2 && p1L32 != 1);

    mdl.add(p1SD61 != 0 || p1L32 == 0 && p1L33 == 0
        || p1L32 == 1 && p1L33 == 1
        || p1L32 == 2 && p1L33 == 2);
    mdl.add(p1SD61 != 1 || p1L32 != 2 && p1L33 != 1);

    mdl.add(p1SD60 != 0 || p1L34 == 0 && p1L35 == 0
        || p1L34 == 1 && p1L35 == 1
        || p1L34 == 2 && p1L35 == 2);
    mdl.add(p1SD60 != 1 || p1L34 != 2 && p1L35 != 1);

    mdl.add(p1SD62 != 0 || p1L36 == 0 && p1L42 == 0
        || p1L36 == 1 && p1L42 == 2
        || p1L36 == 2 && p1L42 == 1);
    mdl.add(p1SD62 != 1 || p1L36 != 2 && p1L42 != 2);

    mdl.add(p1SD10 != 0 || p1L38 == 0 && p1L39 == 0
        || p1L38 == 2 && p1L39 == 2
        || p1L38 == 1 && p1L39 == 1);
    mdl.add(p1SD10 != 1 || p1L38 != 1 && p1L39 != 2);

    mdl.add(p1SD11 != 0 || p1L40 == 0 && p1L41 == 0
        || p1L40 == 1 && p1L41 == 1
        || p1L40 == 2 && p1L41 == 2);
    mdl.add(p1SD11 != 1 || p1L40 != 2 && p1L41 != 1);

    mdl.add(p1SD12 != 0 || p1L11 == 0 && p1L20 == 0
        || p1L11 == 1 && p1L20 == 1
        || p1L11 == 2 && p1L20 == 2);
    mdl.add(p1SD12 != 1 || p1L11 != 2 && p1L20 != 1);

    mdl.add(p1SD13 != 0 || p1L20 == 0 && p1L43 == 0
        || p1L20 == 1 && p1L43 == 1
        || p1L20 == 2 && p1L43 == 2);
    mdl.add(p1SD13 != 1 || p1L20 != 2 && p1L43 != 1);

    mdl.add(p1L4 == 0 && p1L5 == 0 && p1L8 == 0
         || p1L4 == 1 && p1L5 == 1 && p1L8 == 1
         || p1L4 == 2 && p1L5 == 2 && p1L8 == 1
         || p1L4 == 2 && p1L5 == 1 && p1L8 == 2);

    mdl.add(p1L44 == 0 && p1L45 == 0 && p1L2 == 0
         || p1L44 == 2 && p1L45 == 2 && p1L2 == 2
         || p1L44 == 1 && p1L45 == 1 && p1L2 == 2
         || p1L44 == 1 && p1L45 == 2 && p1L2 == 1);

    mdl.add(p1L12 == 0 && p1L29 == 0 && p1L16 == 0
         || p1L12 == 1 && p1L29 == 2 && p1L16 == 1
         || p1L12 == 2 && p1L29 == 1 && p1L16 == 1
         || p1L12 == 2 && p1L29 == 2 && p1L16 == 2);

    mdl.add(p1L17 == 0 && p1L18 == 0 && p1L19 == 0
         || p1L17 == 1 && p1L18 == 1 && p1L19 == 1
         || p1L17 == 2 && p1L18 == 2 && p1L19 == 1
         || p1L17 == 2 && p1L18 == 1 && p1L19 == 2);

    mdl.add(p1L23 == 0 && p1L24 == 0 && p1L31 == 0
         || p1L23 == 1 && p1L24 == 1 && p1L31 == 1
         || p1L23 == 2 && p1L24 == 2 && p1L31 == 1
         || p1L23 == 2 && p1L24 == 1 && p1L31 == 2);

    mdl.add(p1L25 == 0 && p1L15 == 0 && p1L26 == 0 && p1L28 == 0
         || p1L25 == 1 && p1L15 == 2 && p1L26 == 2 && p1L28 == 1
         || p1L25 == 2 && p1L15 == 1 && p1L26 == 2 && p1L28 == 1
         || p1L25 == 2 && p1L15 == 2 && p1L26 == 1 && p1L28 == 1
         || p1L25 == 2 && p1L15 == 2 && p1L26 == 2 && p1L28 == 2);

    mdl.add(p1L33 == 0 && p1L34 == 0 && p1L36 == 0
         || p1L33 == 1 && p1L34 == 1 && p1L36 == 1
         || p1L33 == 2 && p1L34 == 2 && p1L36 == 1
         || p1L33 == 2 && p1L34 == 1 && p1L36 == 2);

    mdl.add(p1L41 == 0 && p1L11 == 0 && p1L42 == 0
         || p1L41 == 1 && p1L11 == 1 && p1L42 == 1
         || p1L41 == 2 && p1L11 == 2 && p1L42 == 1
         || p1L41 == 2 && p1L11 == 1 && p1L42 == 2);

    mdl.add(p1L37 == 0 && p1L38 == 0 && p1L40 == 0
         || p1L37 == 1 && p1L38 == 2 && p1L40 == 1
         || p1L37 == 2 && p1L38 == 1 && p1L40 == 1
         || p1L37 == 2 && p1L38 == 2 && p1L40 == 2);

    mdl.add(p1L27 != 1);
    mdl.add(p1L30 != 2);

    mdl.add(p1L8 == 0 && p1L9 == 0 && p1L10 == 0 && p1L45 == 0 && p1L44 == 0 && p1L43 == 0 && p1L20 == 0 && p1L11 == 0 && p1L42 == 0 && p1L36 == 0 && p1L33 == 0 && p1L32 == 0 && p1L31 == 0 && p1L24 == 0 && p1L25 == 0 && p1L28 == 0 && p1L29 == 0 && p1L12 == 0 && p1L7 == 0 && p1L6 == 0 && p1L5 == 0       ||
      p1L4 == 1 || p1L2 == 1 || p1L41 == 1 || p1L34 == 2 || p1L23 == 1 || p1L15 == 1 || p1L26 == 1 || p1L16 == 2);

   mdl.add(p1L39 != 1);





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

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

  IloSolver solver(mdl);

  do{

	  // cerr<<"aa"<<endl;
      	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;
		//cerr<<"bb"<<endl;
      	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;
      	}
		//cerr<<"cc"<<endl;
      	for(int i = 0; i < varPtr.size(); i++)
      		for(int j = 0; j < varDom[i];j++)
      			var_shownValidThisStep[i][j] = 0;

       //cerr<<"ccc "<<endl;
      	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);




			   clock_t t1=clock();


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

				clock_t t2=clock();

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

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


      			mdl.remove(current);
      		}

      	}
      	//cerr<<"dd"<<endl;
/*
           // 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++;
      	cout <<itr_count<<" ";  cout.flush();
      	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;
}