/*******************************************************************************
 **
 **   transformation using L//xi, L true if xi was true at t=0
 **
 ******************************************************************************/
namespace lxi_dnf {
const bool traza_new_l_xi = false;

// atom -> set of simultaneous labels (set)

map<int,set<set<int> > > labs;

void
pmap( const map<int,set<set<int> > >& m )
{
  for(map<int,set<set<int> > >::const_iterator it = m.begin();
      it != m.end(); it++ )
    {
      cout << it->first << " -> [";
      FOR( set<set<int> >::const_iterator, ss, it->second )
	{
	  cout << "( ";
	  FOR_P( set<int>::const_iterator, s, ss)
	    cout << *s << ", ";
	  cout << " ); ";
	}
      cout << " ]   ";
    }
  cout << endl;
}

void
calc_labels( )
{
  map<int,set<set<int> > > nlabs;

  if( verbose > LEVEL4 )
    cout << "Starting calc_label with..." << endl;
  FOR( vector<set<int> >::const_iterator, it, oneof )
    {
      FOR_P( set<int>::const_iterator, e, it )
	{
	  // Every xi in X, labelable[xi]+= { X }
	  set<int> s;
	  s.insert(*e);
	  nlabs[*e].insert(s);
	  if( verbose > LEVEL4 )
	    cout << name_l_old( *e) << "/" << name_l_old( *e) << "   ";
	}
      if( verbose > LEVEL4 )
	cout << endl;
    } 
      
  labs.clear();
  while( !nlabs.empty() )
    {
      if( verbose > LEVEL4 )
	{
	  cout << "=========================" << endl;
	  cout << "labs: ";
	  pmap( labs );
	  cout << "nlabs: ";
	  pmap( nlabs );
	}
      for(map<int,set<set<int> > >::const_iterator it = nlabs.begin();
	  it != nlabs.end(); it++ )
	FOR( set<set<int> >::const_iterator, ss, it->second )
	  labs[it->first].insert(*ss);
      nlabs.clear();
      if( verbose > LEVEL4 )
	{
	  cout << "after: labs: ";
	  pmap( labs );
	  cout << "nlabs: ";
	  pmap( nlabs );
	  cout << endl;
	}
      FOR_1( wi, whens )
	{
	  When& w = *whens[wi];

	  set<set<set<int> > > labels_set;
	  FOR( set<int>::iterator, p, w.prec )
	    {
	      map<int,set<set<int> > >::iterator it = labs.find(*p);

	      set<set<int> > s;
	      if( it != labs.end() )
		s = it->second;
	      s.insert( set<int>() ); // Consider also that *p may be not labeled
	      labels_set.insert( s );
	    }
	  if(labels_set.empty()) continue;
	  
	  // Make cartesian products of set of labels
	  set<set<set<int> > > combis = cartesian(labels_set);
	  set<set<int> > real_combis;

	  // merging labels
	  FOR( set<set<set<int> > >::iterator, c, combis )
	    {
	      set<int> s;
	      FOR_P( set<set<int> >::iterator, c1, c )
		{
		  set<int> tmp;
		  set_union( s.begin(), s.end(),
			     c1->begin(), c1->end(),
			     inserter(tmp, tmp.begin()));
		  swap(s,tmp);
		}
	      // Reject s empty or 
	      if(s.empty()) continue;
	      // ... with contradictories labels
	      bool reject = false;
	      FOR( vector<set<int> >::const_iterator, it, oneof )
		{
		  set<int> tmp;
		  set_intersection( it->begin(), it->end(),
				    s.begin(), s.end(),
				    inserter(tmp, tmp.begin()));
		  if( tmp.size() > 1 ) reject = true;
		}
	      if(reject) continue;
	      real_combis.insert(s);
	    }
		  
	  // For each combination, 
	  FOR( set<int>::iterator, ep, w.eff )
	    {
	      int e = abs(*ep);
	      // For each combination, 
	      FOR( set<set<int> >::iterator, com, real_combis )
		{
		  map<int,set<set<int> > >::iterator it_e = labs.find(e);
	      
		  // if new, add to nlab
		  if( it_e == labs.end() ||
		      it_e->second.count( *com ) == 0 )
		    {
		      if( false && verbose > LEVEL4 )
			{
			  cout << "new label for atom " <<  name_l_old( e )  << ": ";
			  FOR_P( set<int>::iterator, c, com )
			    cout << name_l_old( *c ) << ", ";
			  cout << endl;
			}
		      nlabs[e].insert( *com );
		    }
		}
	    }
	}
    }

  // Post cond: \forall atom a, labs[a] = { all the possibles labels(set<int>) that it can have }
}

typedef pair<int,set<int> > label_t;

map<label_t,int> labels_t0;

int
labeled_t0( int l, const set<int>& xis ) 
{
  //cout << "labeling " << atoms[l] << " with " << xis.size() << " labs" << endl;
//   FOR( set<int>::const_iterator, xi, xis )
//     cout << "l = " << *xi << ", ";
  //cout << endl;
  assert( labs[l].count(xis) == 1 ); // this option was considered
  assert( !xis.empty() );
  label_t lab(l, xis);
  if( labels_t0.find( lab ) == labels_t0.end() ) 
    {
      string name_lxi;
      if( l < 0 )
	name_lxi.append("n_");
      name_lxi.append(atoms[abs(l)]);
      name_lxi += "_-_";
      FOR( set<int>::const_iterator, xi, xis )
	{
	  name_lxi += "_";
	  if( *xi < 0 )
	    name_lxi += "n";
	  name_lxi += atoms[abs(*xi)];
	}
      if( traza_new_l_xi )
        cout << " = " << name_lxi << endl;
      atoms_p.push_back(name_lxi);
      int nlabel = atoms_p.size()-1;
      labels_t0[lab] = nlabel;
      assert( labeled_t0( l, xis ) == nlabel );
    }
  assert( labels_t0.find( make_pair(l,xis) ) != labels_t0.end() );
  return labels_t0[lab];
}

bool
if_labeled_t0( int l, const set<int>& xis ) 
{
  return ( labs[l].count(xis) == 1 );
}

class reject{
public:
  bool operator()( const set<pair<size_t,int> >& s, const pair<size_t,int>& p )
  {
    for( set<pair<size_t,int> >::iterator pi = s.begin(); 
	 pi != s.end(); pi++ )
      if( pi->second == p.second ) return true;
    return false;
  }
};

void
proc_when( set<int>& prec_left, set<int>& new_precs, set<int>& current_labels, When& w, Act& a_p )
{
  // prec_left = precondition not labeled
  // new_precs = preconditions labeled (or Kprec)
  // Current labels = labels used
  
  if( prec_left.empty() )
    // new_preconditions ready. Just set effects to labels.
    {
      // Dont want to imitate K_0
      if( current_labels.empty() ) return;
      
      When w_p;
      w_p.comment = "C//xi -> L//xi, M//xi";
      FOR( set<int>::iterator, c, new_precs )
	w_p.prec.insert( *c ); // KCs or Ls/xi
      
      FOR( set<int>::iterator, e, w.eff ) // Same effect, but labeled
	{
	  //assert( labs.find(*e) != labs.end() );
	  w_p.eff.insert( (*e>0?1:-1)*labeled_t0( abs(*e), current_labels ) );      
	}
      a_p.addWhen(w_p);
    }
  else 
    // Take one prec, process each posible label
    {
      int p = *prec_left.begin();
      prec_left.erase(p);
      
      // Always put p without label
      new_precs.insert( k(p) );
      proc_when( prec_left, new_precs, current_labels, w, a_p );
      new_precs.erase( k(p) );
      
      // if p has labels
      if( labs.find(p) != labs.end() )
	{
	  set<set<int> >& prec_posible_labels = labs[p];
	  // for each set of possible simultaneos labels
	  FOR( set<set<int> >::iterator, labelp, prec_posible_labels )
	    {
	      set<int> tmp_current_labels( current_labels);
	      tmp_current_labels.insert(labelp->begin(), labelp->end());

	      // Reject inconsistent labels...
	      bool reject = false;
	      FOR( vector<set<int> >::const_iterator, it, oneof )
		{
		  set<int> tmp;
		  set_intersection( it->begin(), it->end(),
				    tmp_current_labels.begin(), tmp_current_labels.end(),
				    inserter(tmp, tmp.begin()));
		  if( tmp.size() > 1 ) reject = true;
		}
	      if(reject) continue;

	      int plab = (p>0?1:-1)*labeled_t0( abs(p), *labelp );      
	      new_precs.insert( plab );
	      proc_when( prec_left, new_precs, tmp_current_labels, w, a_p );
	      new_precs.erase( plab );
	    }
	}
      prec_left.insert(p);
    }
}

// Split atoms
void
make_split_t0( )
{
  //etiquetables.clear();
  // Para cada when W:
  FOR_1( wi, whens )
    {
      When& w = *whens[wi];

      // Local labels has the 
      Act& a_p = actions_p[w.father];

      // process when
      set<int> new_precs;
      set<int> current_labels;
      proc_when( w.prec, new_precs, current_labels, w, a_p );
    }
}

// Using atoms L//Xi, meaning that L is true if Xi was true at t = 0
void
make_k_1_t0()
{
  make_k_0("k", k_base);
  setup_from_oneof();

  registerEntry( "make_k_1_t0()" );

  calc_labels(  );
  make_split_t0(  );
  
  if( traza_new_l_xi )
    cout << "\n\nHaciendo merge..." << endl;


  const bool debugit = false;
  set<pair<int, set<int> > > merge_generated;
  // For each posible candidate to be merge
  for( map<int,set<set<int> > >:: iterator it = labs.begin();
       it != labs.end(); it ++ )
    {
      int l = it->first;
      set<set<int> >& labels = it->second;
      if(debugit)
	cout << "Doing merge for (" << l << ") " << name_l_old(l) << endl;
      // For each label it can have
      FOR(set<set<int> >::iterator, lab, labels)
	{
	  if(debugit)
	    {
	      cout << "\tSeeing label: "; 
	      FOR_P(set<int>::iterator, l_it, lab)
		cout << name_l_old(*l_it) << "(" << *l_it << ") ";
	      cout << endl;
	    }
	  // Build merge candidate
	  set<set<int> > Xss;
	  FOR_P(set<int>::iterator, l_it, lab)
	    Xss.insert(x2oneof[*l_it]);
	  
	  if(debugit)
	    {
	      cout << "\t   considering " << Xss.size() << " oneof's: ";
	      FOR_P(set<int>::iterator, l_it, lab)
		{
		  set<int>& s = x2oneof[*l_it];
		  cout << "(";
		  FOR(set<int>::iterator, xi, s)
		    cout << *xi << ", ";
		  cout << ") ";
		}
	      cout << endl; 
	    }

	  set<set<int> > comb_Xss = cartesian(Xss);
	  if( comb_Xss.size() > 1 )
	    cerr << "Warning: leading with overlapping oneof. It should work, but hasn't been tested" << endl;

	  if(debugit)
	    {
	      cout << "\t  " << comb_Xss.size() << " combs obtained: ";
	      FOR(set<set<int> >::iterator, comb, comb_Xss)
		{
		  const set<int>& s = *comb;
		  cout << "(";
		  FOR(set<int>::iterator, xi, s)
		    cout << *xi << ", ";
		  cout << ") ";
		}
	      cout << endl; 
	    }

	  FOR(set<set<int> >::iterator, merge_comb, comb_Xss)
	    {
	      const set<int>& Xs = *merge_comb;
	      pair<int, set<int> > lXs(l, Xs);
	      if( merge_generated.count(lXs) > 0 )
		continue;
	      merge_generated.insert(lXs);
	  
	      if(debugit)
		{
		  cout << "\t-> Trying to merge: "; 
		  FOR( set<int>::iterator, x, Xs )
		    cout << *x << " ";
		  cout << endl;
		}
		      // Try to generate, check if each label exist
	      Act a_p;
	      a_p.ground = 0;
	      a_p.index = actions_p.size();
	  
	      string name = "merge_";
	      if(l < 0 )
		name.append("n_");
	      name += atoms[abs(l)];
	      name += "_-_";
	      FOR( set<int>::iterator, x, Xs )
		{
		  ostringstream str_l;
		  str_l << *x;
		  name += "_" + str_l.str();
		}
	      a_p.name = string(name);
	  
	      When w_p;
	      w_p.comment = "merge l//xi";
	      
	      w_p.eff.insert( k(l) );
	      w_p.eff.insert( -k(-l) );
	  
	      set<set<int> > xss;
	      FOR( set<int>::iterator, x, Xs )
		xss.insert( oneof[*x] );
	      set<set<int> > comb_xis = cartesian(xss);
	  
	      bool add = true;
	      FOR( set<set<int> >::iterator, xis, comb_xis )
		{
		  if(debugit)
		    {
		      cout << "\t  -> Verifying if label (" << l << ", ";
		      FOR_P( set<int>::iterator, x, xis )
			cout << *x << " ";
		      cout << ") exists : " << if_labeled_t0( l, *xis ) <<endl;
		    }
		  if( if_labeled_t0( l, *xis ) )
		    w_p.prec.insert( labeled_t0( l, *xis ) );
		  else
		    {
		      add = false;
		      break;
		    }
		}
	      
	      a_p.addWhen(w_p);

	      if( add )
		{
		  actions_p.push_back(a_p);
		  if( verbose > LEVEL1 )
		    {
		      cout << "Haciendo merge de etiquetas de atomo " << name_l_old(l)  
			   << ". Action: " << name << endl;
		    }
		  if( verbose > LEVEL2 )
		    {
		      cout << "Agregando When: " << endl;
		      string s = "   ";
		      w_p.dumpPDDL( cout, &name_l, s );
		    }
		}
	    }
	}
    }
  registerExit();
}

}
