#include <climits>

struct myhash_f
{
  static const size_t mychar0 = 255;
  static const size_t mychar1 = 255 << 8;
  static const size_t mychar2 = 255 << 16;
  static const size_t mychar3 = 255 << 24;
  
  size_t
  operator()(const std::set<int>& __s) const
  { 
    size_t hash = 5381;
    
    for(std::set<int>::const_iterator it = __s.begin();
	it != __s.end(); ++it )
      {
	hash = ((hash << 5) + hash) + (mychar0 & *it);
	hash = ((hash << 5) + hash) + (mychar1 & *it);
	hash = ((hash << 5) + hash) + (mychar2 & *it);
	hash = ((hash << 5) + hash) + (mychar3 & *it);
      }
    return hash;
  }
};


namespace t0c {
         const bool traza_t0c = true;
const bool traza_t0c_pi = false;
  const set<int> emptytag;

  set<int> precs_and_goals;
  // Only propagation needed: KL/tag -> -K-L/tag
  const bool use_internal_propagation = false;

  typedef map<int,set<set<int> > > lit2tags_t;

  // atom -> set of simultaneous tags (set)
  lit2tags_t tags;

  set<int> all_tags;
  set<int> really_all_tags;

  int tagged_t0c( int l, const set<int>& xis );

  vector<clause> disjunctions;
  vector<bool> is_oneof;
  void setup_I_disjunctions();
  void calc_new_width();
  bool if_tagged_t0c( int l, const set<int>& xis );

  void
  collect_atoms_in_tags( set<int>& atoms_in_tags )
  {
    FOR( lit2tags_t::const_iterator, it, tags )
      FOR( set<set<int> >::const_iterator, tag, it->second )
        atoms_in_tags.insert(tag->begin(), tag->end());
  }
    
void
ptag( int l, set<int> tag )
{
  cout << (l>0?"":"-") << atoms[abs(l)] << " / (";
  FOR( set<int>::const_iterator, s, tag )
    cout << (*s>0?"":"-") << atoms[abs(*s)] << ", ";
  cout << " ); ";
}

void
ptags2( const lit2tags_t& m )
{
  cout << endl << "TAGS: " << endl;
  for(lit2tags_t::const_iterator it = m.begin();
      it != m.end(); it++ )
    {
      int z = it->first;
      FOR( set<set<int> >::const_iterator, ss, it->second )
	ptag( z, *ss );
      cout << endl;
    }
  cout << endl;
}

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

void
pmap( const lit2tags_t& m )
{
  for(lit2tags_t::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
pset( const set<int>& ss )
{
  FOR( set<int>::const_iterator, s, ss)
    cout << *s << ", ";
  cout << endl;
}

void
pset( const set<set<int> >& ss )
{
  FOR( set<set<int> >::const_iterator, ssi, ss )
    {
      cout << "( ";
      FOR_P( set<int>::const_iterator, s, ssi)
	cout << *s << ", ";
      cout << " ); ";
    }
  cout << endl;
}

  typedef __gnu_cxx::hash_map<set<int>, bool, myhash_f> myhash;
  //typedef map<set<int>, bool> myhash;
  myhash isconsistent;
 
  void
  hash_q(const myhash& mh)
  {
    size_t n = 0, sum = 0;
    for(; n < mh.bucket_count(); n++)
      sum += mh.elems_in_bucket(n);
    cout << "hash quality is "<< double(sum)/double(n) << " average per bucket" << endl;
  }

  bool
  consistent(set<int> s) 
  {
    myhash::const_iterator it = isconsistent.find(s);
    if(it!=isconsistent.end())
      return it->second;
    bool ans = true;
    for( set<int>::iterator lit = s.begin();
	 ans && lit != s.end(); lit++ )
      if( true_literals.count( -*lit ) > 0 ||
	  s.count( -*lit ) > 0 )
	ans = false;
    
    if(0) // Maybe convinient because of efficiency
    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 ) return false;
      }

    // Can use just oneof, interpreting exclusion, and then Or, etc
    for( vector<set<int> >::iterator d = disj.begin();
	 ans && d != disj.end(); d++ )
      {
	bool invalid = true;
	for( set<int>::iterator lit = d->begin();
	     invalid && lit != d->end(); lit++ )
	  invalid = invalid && (s.count( -*lit ) > 0);
	if(invalid) ans = false;
      }
    isconsistent[s] = ans;
    return ans;
  }

  const bool trace_calc_models = false;
void
calc_models( set<set<int> >& dnf, set<int>& lits )
{
  map<int,int> var2cnf;
  map<int,int> cnf2var;
  set<int> vars;
  size_t idx = 0;

  string name (".init.cnf");
  string nameout (name+".sols");
  ofstream out( name.c_str() );

  // Adding Init
  FOR( vector<set<int> >::iterator, d, disj )
    FOR_P( set<int>::iterator, lit, d )
      if(var2cnf.find(abs(*lit)) == var2cnf.end() )
        {
	  int var = abs(*lit);
	  vars.insert(var);
	  var2cnf[var] = ++idx;
	  cnf2var[idx] = var;
	  if(trace_calc_models)
	    cout << "var " << var << " = cnf var " << idx << endl; 
	}

  // Unknown not in Init clauses
  FOR( set<int>::iterator, var, simple_unknown )
    if(var2cnf.find(*var) == var2cnf.end() )
      {
	vars.insert(*var);
	var2cnf[*var] = ++idx;
	cnf2var[idx] = *var;
	if(trace_calc_models)
	  cout << "var " << *var << " = cnf var " << idx << endl; 
      }
    

  out << "p cnf " << idx << " " << (disj.size()+simple_unknown.size()) << endl;
  FOR( vector<set<int> >::iterator, d, disj )
    {
      FOR_P( set<int>::iterator, lit, d )
	out << (*lit>0?1:-1) * var2cnf[abs(*lit)] << " ";
      out << "0" << endl;
    }
  FOR( set<int>::iterator, var, simple_unknown )
    {
      out << var2cnf[*var] << " "
	  << -var2cnf[*var] << " "
	  << "0" << endl;
    }
  
  string cmd("$TRANSLATOR_HOME/relsat -#a "+name+"|grep ^Solution|cut -d : -f 2 |sed 's/^\\ //' >"+nameout);
  system( cmd.c_str() );

  
  ifstream in( nameout.c_str() );
  
  string buff;
  std::getline(in, buff);
  while( in )
    {
      set<int> model;
      char *ptr = strdup(buff.c_str());
      char *str = strtok( ptr, " " );
      
      if(str)
	{
	  int cnf = atoi(str);
	  if(cnf != 0)
	    {
	      int cnflit = (cnf>0?1:-1)*cnf2var[abs(cnf)];
	      model.insert(cnflit);
	      lits.insert(cnflit);
	    }
	  
	  while(str)
	    {
	      cnf = atoi(str);
	      if(cnf != 0)
		{
		  int cnflit = (cnf>0?1:-1)*cnf2var[abs(cnf)];
		  model.insert(cnflit);
		  lits.insert(cnflit);
		}
	      
	      str = strtok( NULL, " " );
	    }
	}
      free(ptr);
      if(1) // Neg vars not necessary? Are necessary, because inclusion verification
      FOR( set<int>::iterator, v, vars )
	if(model.count(*v)==0)
	  model.insert(-*v);
      dnf.insert(model);
      if(trace_calc_models)
	cout << "Model: " << set2str(model) << endl;
      std::getline(in, buff);
    }
  
  in.close();

  string cmd2("/bin/rm "+name+" "+nameout);
  system( cmd.c_str() );
}

  void calc_ramifications( int e, const set<int>& tag_e, set<set<int> >& ramifications );

  void prop_support(int e, const set<int>& tag, set<int>& eff, bool do_cancel = true );

  // L --> O(L)
vector<set<int> > relevant_obs;
vector<set<int> > relevant_n_obs;

  // L --> L'
vector<set<int> > relevant;
vector<set<int> > relevant_n;

  // L <-- L''
vector<set<int> > rev_relevant;
vector<set<int> > rev_relevant_n;


  // l --> lit
bool 
is_relevant( int l, int lit )
{
  if( l > 0 )
    return relevant[l].count( lit ) > 0; 
  else
    return relevant_n[-l].count( lit ) > 0;
}

bool is_relevant_star( int l, int l2 );
bool is_relevant_star_obs( int t , int l );
bool relevant_to_obs_star( int t );
bool relevant_to_obs( int t );

// checks if t is in O(l)
bool is_relevant_to_obs( int t, int l )
{
        if ( t > 0 )
        { 
                if ( relevant_obs[t].empty() ) return false;
                return relevant_obs[t].count( l ) > 0;
        }
        else
        {
                if ( relevant_n_obs[t].empty() ) return false;
                return relevant_n_obs[t].count( l ) > 0;
        }
}

  // lits in O(l)
set<int>&
relevants_obs( int l )
{
  if( l > 0 )
    return relevant_obs[l];
  else
    return relevant_n_obs[-l];
}

  // l --> lits
set<int>&
relevants( int l )
{
  if( l > 0 )
    return relevant[l];
  else
    return relevant_n[-l];
}

  // lits -> l
set<int>&
rev_relevants( int l )
{
  if( l > 0 )
    return rev_relevant[l];
  else
    return rev_relevant_n[-l];
}

  // lit in O(l)
bool
set_relevant_obs( int l, int lit )
{
  bool changed = false;

  if( l > 0 )
    changed = relevant_obs[l].insert( lit ).second || changed;
  else
    changed = relevant_n_obs[-l].insert( lit ).second || changed;

  return changed;
}

bool
set_relevant( int l, int lit )
{
  bool changed = false;
  // L --> L'  
  if( l > 0 )
    changed = relevant[l].insert( lit ).second || changed;
  else
    changed = relevant_n[-l].insert( lit ).second || changed;

  // L <-- L''
  if( lit > 0 )
    changed = rev_relevant[lit].insert( l ).second || changed;
  else
    changed = rev_relevant_n[-lit].insert( l ).second || changed;
  return changed;
}

bool
close_transitivity( vector<set<int> >& rev_relevant, vector<set<int> >& relevant )
{
  bool changed = false;
  FOR_1( i, relevant )
    FOR( set<int>::iterator, from, rev_relevant[i] )
      FOR( set<int>::iterator, to, relevant[i] )
	changed = set_relevant(*from,*to) || changed;
  return changed;
}
 
bool
close_negative( vector<set<int> >& relevant, int phase )
{
  bool changed = false;
  FOR_1( i, relevant )
    FOR( set<int>::iterator, j, relevant[i] )
      changed = set_relevant(-i*phase,-*j) || changed;
  return changed;
}

void
print_relevant( vector<set<int> >& rel, string prefix, string s )
{
  cout << "====== Relevant result: " << s << endl;
  FOR_1( i, relevant )
    {
      cout << prefix << atoms[i] << ": ";
      FOR( set<int>::iterator, j, rel[i] )
	cout << (*j > 0?"":"-") << atoms[abs(*j)] << " ";
      cout << endl;
    }
  cout << "====== End of relevant result" << endl;
}


void
disjunctions_relevance()
{
  return;
  if(!use_contingent) 
    return; // ojo: QUITAR!!!! NO ERROR PERO LIMPIAR!!!!
  if( only_check_new_width )
    {
      FOR( vector<set<int> >::iterator, d, disj )
	if( d->size() == 2 )
	  FOR_P( set<int>::iterator, c1, d )
	    FOR_P( set<int>::iterator, c2, d )
	    if( *c1 != *c2 )
	      set_relevant( -*c1, *c2 );
    }
  else
    {
  // Adding Init
  FOR( vector<set<int> >::iterator, d, disj_orig )
    if( d->size() == 2 )
      FOR_P( set<int>::iterator, c1, d )
	FOR_P( set<int>::iterator, c2, d )
          if( *c1 != *c2 )
	    set_relevant( -*c1, *c2 );

  FOR( vector<set<int> >::iterator, d, oneof )
    {
      if( d->size() == 2 )
	FOR_P( set<int>::iterator, c1, d )
	  FOR_P( set<int>::iterator, c2, d )
            if( *c1 != *c2 )
	      set_relevant( -*c1, *c2 );

      FOR_P( set<int>::iterator, c1, d )
	FOR_P( set<int>::iterator, c2, d )
	  {
            if( *c1 == *c2 ) continue;
	    set_relevant( *c1, -*c2 );
	  }
//       FOR_P( set<int>::iterator, c1, d )
// 	{
// 	  set<int>::iterator c2 = c1;
// 	  ++c2;
// 	  for( ; c2 != d->end(); ++c2 )
// 	    set_relevant( *c1, -*c2 );
// 	}
    }

  // Literals in Observations are relevant
  FOR( set<int>::iterator, lit, atoms_observable )
    {
      set_relevant( *lit, -*lit );
      set_relevant( -*lit, *lit );
    }


  FOR( set<int>::iterator, lit, simple_unknown )
    {
      set_relevant( *lit, -*lit );
      set_relevant( -*lit, *lit );
    }
    }
}


  const bool no_precs = true;
void
calc_relevant()
{
  registerEntry( "calc_relevant()" );
  relevant.resize( natoms + 1 );
  relevant_n.resize( relevant.size() );
  rev_relevant.resize( relevant.size() );
  rev_relevant_n.resize( relevant.size() );

  // atoms are relevant to themselve
  FOR( set<int>::iterator, it, all_atoms )
    {
      set_relevant( *it, *it );
      set_relevant( -*it, -*it );
    }
  
  // Precs and Cond relevant to literals
  for( size_t i = 1; i < actions.size(); i++ )
    {
      Act& a = actions[i];

      if( !no_precs )
	FOR( set<int>::iterator, pi, a.prec )
	  {
	    FOR( set<int>::iterator, ei, a.eff )
	      set_relevant( *pi, *ei );
	    
	    FOR( vector<When>::iterator, wp, a.conds )
	      FOR( set<int>::iterator, cei, wp->eff )
	      set_relevant( *pi, *cei );
	  }
      FOR( vector<When>::iterator, wp, a.conds )
	FOR( set<int>::iterator, ci, wp->prec )
                 FOR( set<int>::iterator, cei, wp->eff )
                    set_relevant( *ci, *cei );
    }
  disjunctions_relevance();
  
  // Until fixpoint
  bool changed = true;
  size_t niter = 1;
  cout << "starting iterations..." << endl;
  while( changed )
    {
      changed = false;
      changed = close_transitivity( rev_relevant, relevant ) || changed;
      changed = close_transitivity( rev_relevant_n, relevant_n ) || changed;
      changed = close_negative( relevant, 1 ) || changed;
      changed = close_negative( relevant_n, -1 ) || changed;
      if( niter % 20 == 0 )
	cout << "iteration: " << niter << endl;
      niter++;
    }
  if( verbose > LEVEL2 )
    {
      print_relevant( relevant, "", "relevant" );
      print_relevant( relevant_n, "-", "relevant" );
//      print_relevant_star( relevant, "", "relevant*" );
//      print_relevant_star( relevant_n, "-", "relevant*" );
//
//       print_relevant( rev_relevant, "", "rev_relevant" );
//       print_relevant( rev_relevant_n, "-", "rev_relevant" );
    }
  registerExit( );
}

void calc_single_clause( set<int>& d );

// the sets O(L)
void calc_relevant_obs()
{
        registerEntry( "calc_relevant_obs()" );
        relevant_obs.resize( natoms + 1 );
        relevant_n_obs.resize( relevant.size() );

        // makes the O(c), i.e. all obs L' rel to L in c
        FOR( vector<set<int> >::iterator, d, disj) 
                calc_single_clause(*d);
        FOR( set<int>::iterator, l, simple_unknown) 
        {
                set<int> tmp_d;
                tmp_d.insert( *l );
                tmp_d.insert( -*l );
                calc_single_clause(tmp_d);        
        }
        
        bool changed = true;
        int n = 0;
        while (changed) 
        {
                n++;
                if( verbose > LEVEL2 ) 
                {
                        for(int i = 0; i < n; i++)
                                cout << " .";
                        cout << endl;
                }
                changed = false;
                FOR( set<int>::iterator, l, all_atoms )
                {
                        if (relevants_obs( *l ).size() == atoms_observable.size())
                                continue;
                        if (relevants_obs( *l ).size() == 0 )
                                continue;
                         
                        FOR( vector<set<int> >::iterator, d, disj) 
                        {
                                if ( d->find( *l ) != d->end() )
                                        continue;
                                bool o_c_made = false;
                                FOR_P( set<int>::iterator, l2, d )
                                {
                                        FOR(set<int>::iterator, t, relevants( *l2 ) )
                                                if ( is_relevant_to_obs(*t, *l) )
                                                {
                                                        vector<int> relevant_to_clause;
                                                        set<int> already_added;
                                                        FOR_P( set<int>::iterator, ci, d )
                                                        {
                                                                if (*ci == *l2) continue;
                                                                
                                                                set<int> rel;
                                                                if( *ci > 0 )
                                                                        rel = relevant[*ci]; 
                                                                else
                                                                        rel = relevant_n[-*ci];
                                                                
                                                                FOR( set<int>::iterator, j, rel )
                                                                {
                                                                        if (is_obs(*j) && 
                                                                            (already_added.find(*j) == already_added.end()) )
                                                                        {
                                                                                already_added.insert(*j);
                                                                                relevant_to_clause.push_back(*j);
                                                                        }
                                                                }
                                                        }
                                                        FOR( vector<int>::iterator, j, relevant_to_clause )
                                                                changed = set_relevant_obs(*l , *j) || changed;
                                                        
                                                        o_c_made = true;
                                                        break;
                                                }
                                }
                                if (o_c_made) break;
                        }
                } // end FOR l
        } // end while
        

        if( verbose > LEVEL2 )
        {
                print_relevant( relevant_obs, "", "relevant obs" );
                print_relevant( relevant_n_obs, "-", "relevant obs" );
        }
        registerExit( );
}

// Makes O(c) and adds it to O(L), for all L in c
void calc_single_clause(set<int>& d )
{
        vector<int> relevant_to_clause;
        set<int> already_added;


        FOR( set<int>::iterator, ci, d )
        {
                set<int> rel;
                if( *ci > 0 )
                        rel = relevant[*ci]; 
                else
                        rel = relevant_n[-*ci];
                
                FOR( set<int>::iterator, j, rel )
                {
//                                cout << "Printing: " << (*j>0?"":"-") << atoms[abs(*j)] << endl;
                        if (is_obs(*j) && 
                            (already_added.find(*j) == already_added.end()) )
                        {
                                already_added.insert(*j);
                                relevant_to_clause.push_back(*j);
                        }
                }
        }
        
        FOR( set<int>::iterator, ci, d ) 
                FOR( vector<int>::iterator, t, relevant_to_clause )
                    set_relevant_obs(*ci , *t);
}


bool
lit_accept_disjunction( int lit, set<int>& clause ) 
{
  bool accept = true;
  for( set<int>::iterator l = clause.begin();
       accept && l != clause.end(); ++l )
    {
      accept = accept && 
              ( is_relevant( *l, lit ) || is_relevant_to_obs( *l, lit ) ); // OJO SEP 2011.(ALEX)
    }
  return accept;
}

bool
lit_accept_disjunction_star( int lit, set<int>& clause ) 
{
  bool accept = true;
  // OJO-IJCAI09: cambiar false por true para usar 
  // definicion alternativa propuesta por HLP el 14/dic/08
  if( true || disjunction_is_static( clause ) )
    {
      bool accept_atleast_one = false;
      for( set<int>::iterator l = clause.begin();
	   accept && l != clause.end(); ++l )
	{
	  bool i = is_relevant_star( *l, lit );
	  accept = accept && 
                  ( i || is_relevant_to_obs( *l, lit ) );
	  accept_atleast_one = accept_atleast_one || i;
	}
      accept = accept && accept_atleast_one;
    }
  else
    {
      for( set<int>::iterator l = clause.begin();
	   accept && l != clause.end(); ++l )
	accept = accept && is_relevant_star_obs( *l, lit );
    }
  return accept;
}

  // Accept a clause if every literal is relevant to some goal literal
bool
accept_disjunction( set<int>& clause ) 
{
  FOR( set<int>::iterator, gl, goal_literals )
    if( lit_accept_disjunction( *gl, clause ) )
      {
	cout << "Accepted disjunction ";
	pset(clause);
	return true;
      }
  if( no_precs )
    FOR( set<int>::iterator, pl, precs_literals )
      if( lit_accept_disjunction( *pl, clause ) )
	{
	  cout << "Accepted disjunction ";
	  pset(clause);
	  return true;
	}
  cout << "Rejected disjunction ";
  pset(clause);
  return false;
}

// s <- { l2 | Init + l + s |=  l2 }
void
implies_with_init_gen( int l, set<int>& s, map<int, set<int> >& cache )
{
  static bool called_once = false;
  static clauses init;

  if( !called_once )
    {
      FOR( vector<clause>::iterator, c, disj )
	init.insert(*c);
      called_once = true;
    }

  map<int, set<int> >::iterator it = cache.find(l);
  if( it == cache.end() )
    {
      clauses res;
      unit_res( init, res, s );
      cache[l] = s;
      if(traza_t0c)
	{
	  cout << "IMPLIES_WITH_INIT: From lit " 
	       << atoms[abs(l)] << "(" << l << ") obtaing the following lits:";
	  FOR( set<int>::iterator, it, s )
	    cout << atoms[abs(*it)] << "(" << *it << ") ";
	  cout << endl;
	}
    }
  else
    s = it->second;
}

// s = { l2 | Init + l |=  l2 }
// s always includes lits known to be true in Init
// CLG OJO: just about tags!!
void
implies_with_init( int l, set<int>& s )
{
  static map<int, set<int> > cache;
  //s = true_literals;
  s.insert(l);
  implies_with_init_gen( l, s, cache );
}

// s = { l2 | Init + l + known |=  l2 }
// s always includes lits known to be true in Init
void
implies_with_init_and_known( int l, set<int>& s )
{
  static map<int, set<int> > cache;
  s = true_literals;
  s.insert(l);
  implies_with_init_gen( l, s, cache );
}

// si tag' relevant to tag2
// for any I + tag   |=   tag'
// not including true literals at I
bool 
is_relevant_star( int l, int l2 )
{
  if( is_relevant( l, l2 ) )
    return true;
  set<int> s;
  implies_with_init( l, s );
  FOR( set<int>::iterator, it, s )
    if( is_relevant( *it, l2 ) )
      return true;
  return false;
}

// Checks if l -> l2
bool
is_relevant_star_obs( int l, int l2 )
{
        return ( is_relevant_star( l, l2 ) || is_relevant_to_obs( l, l2 ) );
}

// checks if t is relevant star to *any* observable
bool // ALEX TODO should be eliminated thanks to new defs
relevant_to_obs_star( int t )
{
  static map<int,bool> rel_to_obs;
  map<int,bool>::iterator it = rel_to_obs.find(t);
  if( it == rel_to_obs.end() )
    {
      FOR( set<int>::iterator, l, atoms_observable )
	if( is_relevant_star( t, *l ) || is_relevant_star( t, -*l ) )
	  {
	    rel_to_obs[t] = true;
	    return true;
	  }
      rel_to_obs[t] = false;
    }
  else
    return it->second;
}

// checks if t is relevant to *any* observable
bool // ALEX TODO should be eliminated thanks to new defs
relevant_to_obs( int t )
{
  static map<int,bool> rel_to_obs;
  map<int,bool>::iterator it = rel_to_obs.find(t);
  if( it == rel_to_obs.end() )
    {
      FOR( set<int>::iterator, l, atoms_observable )
	if( is_relevant( t, *l ) || is_relevant( t, -*l ) )
	  {
	    rel_to_obs[t] = true;
	    return true;
	  }
      rel_to_obs[t] = false;
      return false;
    }
  else
    return it->second;
}

map<int,set<clause> > c_i;
bool c_i_calculated = false;

void
tags_in_merge( int g, set<int>& res ) // OJO CLG: cambiar a *res si funciona...
{
  assert( c_i_calculated );
  static map<int,set<int> > tags_g;
  map<int,set<int> >::iterator tags = tags_g.find(g);
  if( tags == tags_g.end() )
    {
      tags_g[g].clear();
      map<int,set<clause> >::iterator it = c_i.find(g);
      if( it != c_i.end() )
	{
	  set<clause>& c_i_g = it->second;
	  set<int>& tags = tags_g[g];
	  FOR( set<clause>::iterator, c, c_i_g )
	    {
	      FOR_P( clause::iterator, ci, c )
		tags.insert(*ci);
	    }
	}
    }
  if(traza_t0c)
    {
      set<int>& tags = tags_g[g];
      cout << "For lit " << atoms[abs(g)] << "(" << g << ")" << " relevants tags are: ";
      FOR( set<int>::iterator, it, tags )
	cout << atoms[abs(*it)] << "(" << *it << ") ";
      cout << endl;
    }
  res = tags_g[g];
}

void
print_width()
{
  size_t max_width = 0;
  c_i_calculated = true;
  FOR( set<int>::iterator, gl, goal_literals )
    {
      size_t width = 0;
      FOR( vector<clause>::iterator, c, disjunctions )
	if( lit_accept_disjunction( *gl, *c ) )
	  {
	    c_i[*gl].insert(*c);
	    width++;
	  }
      max_width = max( width, max_width );
      if( width != 0 && verbose > LEVEL1 )
	cout << "Width " << width << " for goal literal " << (*gl>0?"":"-") << atoms[abs(*gl)] << endl;
    }
  FOR( set<int>::iterator, pl, precs_literals )
    {
      size_t width = 0;
      FOR( vector<clause>::iterator, c, disjunctions )
	if( lit_accept_disjunction( *pl, *c ) )
	  {
	    c_i[*pl].insert(*c);
	    width++;
	  }
      max_width = max( width, max_width );
      if( width != 0 && verbose > LEVEL1 )
	cout << "Width " << width << " for precondition literal " << (*pl>0?"":"-") << atoms[abs(*pl)] << endl;
    }
  cout << "STAT Max-width: " << max_width << endl;
}


  int max_size_tag = INT_MAX;

lit2tags_t init_tags;
lit2tags_t ntags;
  set<int> init_atoms;

void add_init_tag( int a, int b, set<int>& init_atoms )
{
  set<int> t;
  t.insert(-a);
  if( if_tagged_t0c( b, t ) )
    {
      int natom = tagged_t0c( b, t );
      init_atoms.insert( natom );
      prop_support(b, t, init_atoms );
    }
}
  // OJO: esto necesita urgente refactoring
  // se hace lo mismo varias veces.
  // Lo mejor es construir todo desde el principio
  // aplicando la definicion del paper
void
create_init_atoms_old()
{
  // updating init_tags
  lit2tags_t init_tags_tmp = init_tags;
  for( lit2tags_t:: iterator it = init_tags_tmp.begin();
       it != init_tags_tmp.end(); it++ )
    {
      int i = it->first;
      set<set<int> >& mtags = it->second;
      FOR( set<set<int> >::iterator, it2, mtags )
	{
	  const set<int>& tag = *it2;
	  set<set<int> > ramifications;
	  calc_ramifications( i, tag, ramifications );
	  FOR( set<set<int> >::iterator, tagi, ramifications )
	    init_tags[i].insert(*tagi );
	}
    }

  // Ojo: Porque es necesario? 
  // Ramification over initial state
  FOR( set<int>::iterator, a, true_literals )
    { 
      prop_k( *a, init_atoms, false );
//       set<set<int> > ramifications;
//       calc_ramifications( *a, emptytag, ramifications );
//       FOR( set<set<int> >::iterator, tagi, ramifications )
// 	init_tags[*a].insert(*tagi );
    }
  
  for(map<int,set<set<int> > >::const_iterator it = t0c::init_tags.begin();
      it != t0c::init_tags.end(); it++ )
    FOR( set<set<int> >::iterator, tag, (it->second) )
      {
	int natom = tagged_t0c(it->first, *tag );
	init_atoms.insert( natom );
	prop_support(natom, *tag, init_atoms );
      }

  // Para todas las disjunciones binarias...
  FOR( vector<set<int> >::iterator, op, disj )
    if( op->size() == 2 )
      {
	int a = *(op->begin());
	int b = *(++(op->begin()));
	add_init_tag( a, b, init_atoms ); 
	add_init_tag( b, a, init_atoms ); 
      }
  // Clean negatives...
  for( set<int>::iterator it = init_atoms.begin();
       it != init_atoms.end(); )
    if( *it < 0 )
      init_atoms.erase(it++);
    else
      ++it;
}

void
create_init_atoms()
{ 
  FOR( set<int>::iterator, t, all_tags )
    {  
      set<int> tag;
      tag.insert(*t);

      set<int> s;
      implies_with_init_and_known( *t, s );

      FOR( set<int>::iterator, it, s )
	if( if_tagged_t0c( *it, tag ) )
	  init_atoms.insert( tagged_t0c( *it, tag ) );
      }

  // Ramification over initial state
  // Redundant because KL/t for L literal will arise from previous part
  FOR( set<int>::iterator, a, true_literals )
    {
      init_atoms.insert(k(*a));
      prop_k( *a, init_atoms, false );
    }
  

  // Clean negatives...
  for( set<int>::iterator it = init_atoms.begin();
       it != init_atoms.end(); )
    if( *it < 0 )
      init_atoms.erase(it++);
    else
      ++it;
}

struct l_tag_t
{
  int l;
  set<int> tag;
  l_tag_t( int ltmp, const set<int>& tagtmp): l(ltmp), tag(tagtmp) {}
};
typedef struct l_tag_t l_tag;

struct less_l_tag
{
  bool operator()(const l_tag& m1, const l_tag& m2) const 
  { return( (m1.l < m2.l) ||
	    (m1.l == m2.l && m1.tag < m2.tag ) ); }
};

typedef set<l_tag,less_l_tag> set_tag_t;
typedef queue<l_tag> queue_tag_t;

void
update_q( int l, const set<int>& tag, 
	  queue_tag_t& tags_iter_idx, set_tag_t& tags_iter_set )
{ 
  l_tag lt( l, tag );
  if( tags_iter_set.count(lt) == 0 )
    {
      tags_iter_idx.push(lt);
      tags_iter_set.insert(lt);
    }
}

  long double comb = 0;
  long double rcomb = 0;
  unsigned long ncomb = 0;
  const bool stat_combis = true;
bool do_clause_a( queue_tag_t& tags_iter_idx, set_tag_t& tags_iter_set, const l_tag& tl )
{
  const int l = tl.l;
  const set<int>& tag = tl.tag;
  const set<unsigned>& wreq = whenReqLit( l );
  FOR( set<unsigned>::iterator, wi, wreq )
    {
      const When& w = *whens[*wi];
      if(!w.used) continue;

      // OJO: quizas para p == lt.l, solo agregar tags >= lt.tag
      set<set<set<int> > > tags_set;
      FOR( set<int>::iterator, p, w.prec )
	{
	  lit2tags_t::iterator it = ntags.find(*p);
	    
	  set<set<int> > s;
	  // Comment out because inefficient
	  // 	    if( *p == l )  
	  // 	      FOR( set<set<int> >::iterator, tagp, it->second )
	  // 		if( includes( tagp->begin(), tagp->end(), 
	  // 			      tag.begin(), tag.end() ) )
	  // 		  s.insert( *tagp );
	  // 	    else
	  {
	    if( it != ntags.end() )
	      s = it->second;
	    s.insert( set<int>() ); // Consider also that *p may not be tagged
	  }

	  tags_set.insert( s );
	}
      if(tags_set.empty()) return false;

      // Make cartesian products of set of tags
      set<set<set<int> > > combis = cartesian(tags_set);
      set<set<int> > real_combis;

      // merging tags
      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;
	  // or with size > max
	  if(s.size() > max_size_tag) continue;
	  // or with contradictories tags
	  if(!consistent(s)) continue; 
	      
	  real_combis.insert(s);
	}
	
      if(stat_combis)
	{
	  comb += combis.size();
	  rcomb += real_combis.size();
	  ++ncomb;
	}

      // For each combination, 
      FOR( set<int>::iterator, ep, w.eff )
	{
	  const int e = *ep;
	  lit2tags_t::iterator it_e = ntags.find(e);
	  FOR( set<set<int> >::iterator, com, real_combis )
	    {
	      // if new, add to nlab
	      if( it_e == ntags.end() ||
		  it_e->second.count( *com ) == 0 )
		{
		  if( false && verbose > LEVEL4 )
		    {
		      cout << "new tag for atom " <<  name_l_old( e )  << ": ";
		      FOR_P( set<int>::iterator, c, com )
			cout << name_l_old( *c ) << ", ";
		      cout << endl;
		    }
		  ntags[e].insert( *com );
		  // update queue
		  update_q( e, *com, tags_iter_idx, tags_iter_set );
		}
	    }
	}
    }
  return true;
}

void do_clause_b( queue_tag_t& tags_iter_idx, set_tag_t& tags_iter_set, const l_tag& tl )
{
  const int li = tl.l;
  const set<int>& tag_li = tl.tag;
  const set<int>& modif_by_nli = litModEff( -li );
  FOR( set<int>::const_iterator, lp, modif_by_nli )
    {
      const int nl = -(*lp);
      lit2tags_t::iterator it_l = ntags.find(nl);
      set<set<int> > tags_nl;
      if( it_l != ntags.end() )
	tags_nl = it_l->second;
      tags_nl.insert(emptytag);

      FOR( set<set<int> >::iterator, ptag_nl, tags_nl )
	{
	  set<int> uniontag;
	  set_union( tag_li.begin(), tag_li.end(),
		     ptag_nl->begin(), ptag_nl->end(),
		     inserter(uniontag, uniontag.begin()));

	  // Reject s empty or 
	  if(uniontag.empty()) continue;
	  // or with size > max
	  if(uniontag.size() > max_size_tag) continue;
	  //  ... with contradictories tags
	  if(!consistent(uniontag)) continue; 
		      
	  if( tags_nl.count(uniontag) != 0 ) continue;

	  //if new tag
	  ntags[nl].insert(uniontag);
	  update_q( nl, uniontag, tags_iter_idx, tags_iter_set );
	}
    }
}

// fixpoint with queue
// Input: ntags
void
calc_tags_propagate( )
{
  tags.clear();
  size_t niter = 0;
  queue_tag_t tags_iter_idx;
  set_tag_t tags_iter_set;

  // propagate initial ntags to tags_iter
  for(lit2tags_t::const_iterator it = ntags.begin();
      it != ntags.end(); it++ )
    FOR( set<set<int> >::const_iterator, tag, it->second )
      update_q( it->first, *tag, tags_iter_idx, tags_iter_set );
    
  // iterate over tags_iter
  while( !tags_iter_idx.empty() )
    {
      if( verbose > LEVEL1 )
	{
	  niter++;
	  if( niter % 100 == 0 )
	    cout << "Calc tags, iter #" << niter << endl;
	}
      if( verbose > LEVEL4 )
	{
	  cout << "=========================" << endl;
	  cout << "tags: ";
	  pmap( tags );
	  cout << "ntags: ";
	  pmap( ntags );
	}
      if( verbose > LEVEL4 )
	{
	  cout << "after: tags: ";
	  pmap( tags );
	  cout << "ntags: ";
	  pmap( ntags );
	  cout << endl;
	}

      // Pick a l/tag
      l_tag tl = tags_iter_idx.front();
      tags_iter_idx.pop();
      tags_iter_set.erase(tl);

      // Propagate from it
      if( !do_clause_a( tags_iter_idx, tags_iter_set, tl ) )
	continue;

      if( use_clause_b_tags ) 
	do_clause_b( tags_iter_idx, tags_iter_set, tl );
    }

  // Copy to tags
  for(lit2tags_t::const_iterator it = ntags.begin();
      it != ntags.end(); it++ )
    FOR( set<set<int> >::const_iterator, ss, it->second )
      tags[it->first].insert(*ss);

  // Post cond: \forall literal l, tags[l] = { all the possibles tags(set<int>) that it can have }

  if(stat_combis)
    {
      cout << "Rate of compact after combination of tags combis: " 
	   << (double(comb)/ncomb) << " vs real combis: "
	   << (double(rcomb)/ncomb) << endl;
    }

  if(0)
    {
      set<int> vars;
      for( lit2tags_t::iterator pair = tags.begin();
	   pair != tags.end(); pair++ )
	vars.insert(pair->first);
      FOR(set<int>::iterator, var, vars)
	assert( tags[*var] == tags[-*var] );
      // If do not violated, all can be redone to base on tag[positive_var]
    }
}

  void
  add_simple_tag( int lit, int tag, lit2tags_t& tags )
  {
    set<int> s;
    s.insert(tag);
    if( tags[lit].count(s) == 0 )
      {
	tags[lit].insert(s);
	if( verbose > LEVEL1 )
	  cout << "Simple tag: " << name_l_old( lit ) 
	       << "(" << lit << ") /"
	       << name_l_old( tag ) << "(" << tag << ")   " << endl;
      }
  }

  set<set<int> > dnf;
  set<int> lits_dnf;
  bool dnf_calculated = false;
  bool const test_newtags = false;
  bool debug_newtags = false;
void
add_simple_tags_contingent( set<int>& c, bool define, bool exclusive = false )
{
  return; // OJO HLP AQUI: reemplazado por regla de relevancia...
  if(debug_newtags)
    {
      cout << "HLP adding simple tag for ";
      pset(c);
    }
  // OJO! solo es cierto para oneof
  if( (test_newtags || use_contingent) &&
      c.size() == 2 )
    {
      int first = *(c.begin());
      int second = *(++(c.begin()));
      add_simple_tag( -first, second, ntags);
      add_simple_tag( -second, first, ntags);
      if( define || exclusive )
	{
	  add_simple_tag( first, -second, ntags);
	  add_simple_tag( second, -first, ntags);
	}
      if( define )
	{
	  add_simple_tag( -first, -second, ntags);
	  add_simple_tag( -second, -first, ntags);
	  add_simple_tag( first, second, ntags);
	  add_simple_tag( second, first, ntags);
	}
    }
}

void
add_tags_contingent( set<int>& c, bool define )
{
  // Deshabilitadas porque seran subsummed por nuevas reglas, mas eficiente, etc
  //return; 

  if( !use_contingent && 
      !test_newtags ) return;
  if(debug_newtags)
    cout << "HLP ok!!!!!!!" << endl;
  if( c.size() == 2 )
    add_simple_tags_contingent( c, define, true );
  else
    FOR( set<int>::iterator, c1, c )
      {
	set<int>::iterator c2 = c1;
	++c2;
	for( ; c2 != c.end(); ++c2 )
	  {
	    set<int> mini_c;
	    mini_c.insert(*c1);
	    mini_c.insert(*c2);
	    if(debug_newtags)
	      {
		cout << "Ned tag: ";
		pset(mini_c);
	      }
	    add_simple_tags_contingent( mini_c, define );
	  }
      }
}
 
void
calc_tags( )
{
  static bool tags_calculated = false;
  bool use_new_gen_tags = true;
  if(tags_calculated) return;
  tags_calculated = true;

  registerEntry( "calc_tags()" );

  if( use_s0s )
    {
      dnf_calculated = true;
      calc_models( dnf, lits_dnf );

      if( verbose > LEVEL4 )
	cout << "Models of Init calculated. Tagging with them" << endl;

      FOR(set<set<int> >::iterator, conj, dnf)
	FOR_P(set<int>::iterator, lit, conj )
	//if(*lit > 0 ) // For s0s, k-l/tag \equiv -k l/tag
	  ntags[*lit].insert(*conj);

      init_tags = ntags;

      FOR(set<set<int> >::iterator, conj, dnf)
	FOR(set<int>::iterator, atom, all_atoms)
	if( conj->count(-*atom) == 0 )
	  ntags[*atom].insert(*conj);
    }
  else if( use_only_I_disjunctions && use_relevance && !use_new_gen_tags )
    {
      calc_relevant();
      calc_relevant_obs();
      if( only_check_new_width )
	{
	  calc_new_width();
	  exit(0);
	}
      setup_I_disjunctions();
      
      // For each relevant literal, create tags
      //FOR( vector<clause>::iterator, c, disjunctions )
      set<int> all_tags;
      FOR_0( i, disjunctions )
	{
	  set<int>& c = disjunctions[i];
	  FOR( clause::iterator, tag, c )
	    {
	      const set<int> rel = relevants( *tag );
	      FOR( set<int>::const_iterator, affected, rel )
		add_simple_tag( *affected, *tag, ntags);
	    }
	  //}
	  if( is_oneof[i] )
	    add_tags_contingent( c, true );
	  else if( c.size() == 2 )
	    add_simple_tags_contingent( c, true );
	}

      tags = ntags;
      ntags.clear();
      //FOR( vector<clause>::iterator, c, disjunctions )
      FOR_0( i, disjunctions )
	{
	  set<int>& c = disjunctions[i];
	  FOR( clause::iterator, tag, c )
	    add_simple_tag( *tag, *tag, ntags);
	  if( is_oneof[i] )
	    add_tags_contingent( c, false );
	  else if( c.size() == 2 )
	    add_simple_tags_contingent( c, true );
	}
      init_tags = ntags;
    }
  else if( use_only_I_disjunctions && use_relevance && use_new_gen_tags )
    {
      calc_relevant();
      calc_relevant_obs();
      if( only_check_new_width )
	{
	  calc_new_width();
	  exit(0);
	}
      setup_I_disjunctions();

      // Collect tags
      FOR_0( i, disjunctions )
	{
	  set<int>& c = disjunctions[i];
	  FOR( clause::iterator, tag, c )
	    all_tags.insert( *tag );
	}
      
      FOR( vector<set<int> >::iterator, d, disj )
	{
	  set<int>& c = *d;
	  FOR( clause::iterator, tag, c )
	    really_all_tags.insert( *tag );
	}

      cout << "All tags: ";
      FOR( set<int>::const_iterator, tag, all_tags )
	cout << atoms[abs(*tag)] << "(" << *tag << ") ";
      cout << endl;

      precs_and_goals.clear();
      FOR( set<int>::iterator, gl, goal_literals )
	precs_and_goals.insert(*gl);
      FOR( set<int>::iterator, pl, precs_literals )
	precs_and_goals.insert(*pl);
      
      FOR( set<int>::iterator, g, precs_and_goals )
	  {
	    const set<int> rel = rev_relevants( *g );
	    set<int> tags;
	    tags_in_merge( *g, tags);
	    FOR( set<int>::const_iterator, tag, tags )
		{
		  FOR( set<int>::const_iterator, affects, rel )
		    //for( int phase = 1; phase > -2; phase -= 2 ) 
		    for( int phase = 1; phase > 0; phase -= 2 ) 
		      {
			int l = *affects * phase; // OJO: CLG probar sin phase
			if( is_relevant_star( *tag, l ) )
			  add_simple_tag( l, *tag, ntags);
		      }
		}
	  }
      
      FOR( set<int>::iterator, l, atoms_observable )
	FOR( set<int>::const_iterator, tag, all_tags )
  	  if( is_relevant_star( *tag, *l ) ||
	      is_relevant_star( *tag, -*l ) )
	    {
	      add_simple_tag( *l, *tag, ntags);
	      add_simple_tag( -*l, *tag, ntags);
	    }
      
      tags = ntags;
      ntags.clear();
      init_tags = ntags;
    }
  else if( use_only_I_disjunctions )
    {
      if( use_contingent )
	{
	  cout << "Don't use -nr option" << endl;
	  exit(1);
	}
      // init_tags = lits in Initial + cond negativas
      // quizas = lits in Initial + unknown simples (but not in Initial)
      if( verbose > LEVEL1 )
	cout << "Starting simple calc_tag with..." << endl;

      set<int> init_labs;

      // Lits in original Oneof, Or
      FOR( set<int>::iterator, lit, disj_orig_lits )
	add_simple_tag( *lit, *lit, ntags);
      FOR( set<int>::iterator, lit, oneof_lits )
	add_simple_tag( *lit, *lit, ntags);

      FOR( set<int>::iterator, lit, simple_unknown )
	{
	  if( !whenReqLit(*lit).empty() )
	    add_simple_tag( *lit, *lit, ntags);
	  if( !whenReqLit(-*lit).empty() )
	    add_simple_tag( -*lit, -*lit, ntags);
	}

      if( test_newtags )
	FOR_0( i, disjunctions )
	  {
	    set<int>& c = disjunctions[i];
	    add_tags_contingent( c, false );
	  }

      if( verbose > LEVEL1 )
	cout << "----- end of init tags ----" << endl;

      init_tags = ntags;
    }
  else // All relevant tags. OJO: check concept of relevant.
    {
      assert( 0 != 0 );
      if( verbose > LEVEL4 )
	cout << "Starting calc_tag FULL with..." << endl;
     
      int limit;
      const bool use_tags_negative = true;
      if( use_tags_negative )
	limit = -2;
      else
	limit = 0;
      for( int phase = 1; phase > limit; phase -= 2 ) // limit -2 for both phase
	FOR( set<int>::const_iterator, e, unknown_relevant )
	  {
	    // Every unknown l: l/l, -l/-l
	    set<int> s;
	    int en = *e * phase;
	    s.insert(en);
	    ntags[en].insert(s);
	    if( verbose > LEVEL4 )
	      cout << name_l_old( en ) << "/" 
		   << name_l_old( en ) << "   " << endl;
	  }
      if( verbose > LEVEL4 )
	cout << endl;
      
      init_tags = ntags;
    }

  if( ! (use_only_I_disjunctions && use_relevance ) )
    calc_tags_propagate( ); 
  
  if( verbose > LEVEL1 )
    {
      cout << "=========================" << endl;
      cout << "tags calculated: " << endl;
      ptags( tags );
      cout << "=========================" << endl;
    }

  if(0)
    {
      cout << "inconsistent: ";
      hash_q(isconsistent);
    }
  registerExit( );
}

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

map<tag_t,int> tags_t0c;
map<int,tag_t> inv_tags_t0c;
  
  int tagval = 1;
  map<set<int>, int> tag2val;


string
get_name_lxi( int l, const set<int>& xis ) 
{
  string name_lxi("k");
  if( l < 0 )
    name_lxi.append("n");
  name_lxi.append("_");
  name_lxi.append(atoms[abs(l)]);
  name_lxi += "__";
  if(xis.size() < 4 ) //Ojo: numero magico
    FOR( set<int>::const_iterator, xi, xis )
      {
	name_lxi += "_";
	if( *xi < 0 )
	  name_lxi += "-";
	name_lxi += atoms[abs(*xi)];
      }
  else // Dont put all variables, but a unique identifier
    {
      int nval;
      map<set<int>, int>::iterator it = tag2val.find(xis);
      if(it == tag2val.end())
	{
	  nval = tagval++;
	  tag2val[xis] = nval;
	}
      else
	nval = it->second;
      name_lxi += "tag_"+int2str(nval);
    }
  return name_lxi;
}

int
tagged_t0c( int l, const set<int>& xis ) 
{
  if( xis.empty() )
    return k(l); // If violated, can be sent to k(l)
  if( tags[l].count(xis) != 1 ) 
    {
      // if( use_s0s ) // add tag OJO! VERDADERA VERSION
      if( true || use_s0s ) // add tag
	tags[l].insert(xis);
      else
	{
	  cout << "Failed with l = " << l
	       << " tag = " << set2str(xis) << endl;
	  // assert( tags[l].count(xis) == 1 ); // this option was considered
	}
    }
  int sign = 1;
  if( use_s0s ) // For s0 k-l/tag \equiv -k l/tag
    {
      sign = l > 0 ? 1 : -1 ;
      l = abs( l );
    }
  tag_t lab(l, xis);
  if( tags_t0c.find( lab ) == tags_t0c.end() ) 
    {
      string name_lxi = get_name_lxi(l, xis);
      atoms_p.push_back(name_lxi);
      int ntag = atoms_p.size()-1;
      tags_t0c[lab] = ntag;
      if( true || use_contingent )
	inv_tags_t0c[ntag] = lab; 
      assert( tagged_t0c( l, xis ) == ntag );
      if( traza_t0c )
        cout << ntag << " = " << name_lxi << endl;
    }
  assert( tags_t0c.find( make_pair(l,xis) ) != tags_t0c.end() );
  return sign * tags_t0c[lab];
}

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


map<tag_t,int> tags_t0c_sl;
  // Is not necesary to update the initial state
  // it will be done by axioms

int
tagged_t0c_sl( int l, const set<int>& xis ) 
{
  assert( !use_s0s );
  assert( !xis.empty() );
  tag_t lab(l, xis);
  if( tags_t0c_sl.find( lab ) == tags_t0c_sl.end() ) 
    {
      // assert( tags_t0c.find( lab ) != tags_t0c.end() );      
      string name_lxi = "S_" + get_name_lxi( l, xis );
      atoms_p.push_back(name_lxi);
      int tag_sl = atoms_p.size()-1;
      tags_t0c_sl[lab] = tag_sl;
    }
  return tags_t0c_sl[lab];
}

  // Set of tags st includes tag_e
void
calc_ramifications( int e, const set<int>& tag_e, set<set<int> >& ramifications )
{
  //assert( !tags.empty() );
  ramifications.clear();
  set<set<int> >& tags_e = tags[e];
  FOR( set<set<int> >::iterator, tag, tags_e )
    if( //*tag != tag_e &&  // Sometimes add again, but makes function more useful
	includes( tag->begin(), tag->end(), 
		  tag_e.begin(), tag_e.end() ) )
      ramifications.insert( *tag );
}

  // Set of tags T st T includes tag_e or tag_e includes T 
void
calc_ramifications_both( int e, const set<int>& tag_e, set<set<int> >& ramifications )
{
  assert(0!=0);
  assert( !tags.empty() );
  ramifications.clear();
  set<set<int> >& tags_e = tags[e];
  FOR( set<set<int> >::iterator, tag, tags_e )
    if( //*tag != tag_e &&  // Sometimes add again, but function more useful
       ( includes( tag->begin(), tag->end(), 
		   tag_e.begin(), tag_e.end() ) || 
	 includes( tag_e.begin(), tag_e.end(), 
		   tag->begin(), tag->end() ) ) )
      ramifications.insert( *tag );
  ramifications.insert( emptytag );
}


void
add_one_eff( set<int>& eff, int e, const set<int>& tagi, int phase = 1 )
{
  if( if_tagged_t0c( e, tagi ) )
    eff.insert( phase * tagged_t0c( e, tagi ) );
}

void
add_eff( set<int>& eff, int e, const set<int>& tagi, int phase = 1 )
{
  assert( phase == 1 || phase == -1 );
  add_one_eff( eff, e, tagi, phase );
  add_one_eff( eff, -e, tagi, phase*-1 );
//   if( if_tagged_t0c( e, tagi ) )
//     eff.insert( phase * tagged_t0c( e, tagi ) );
//   if( if_tagged_t0c( -e, tagi ) )
//     eff.insert( phase * -tagged_t0c( -e, tagi ) );
  assert( eff.size() > 0 );
}

void prop_support(int e, const set<int>& tag, set<int>& eff, bool do_cancel )
{
  if(!use_propagation)
    return; 

  set<set<int> > ramifications;
  calc_ramifications( e, tag, ramifications );
  FOR( set<set<int> >::iterator, tagi, ramifications )
    add_one_eff( eff, e, *tagi, 1 );

  // Nothing else should be neede
  //return;
  // Pseudo mutex
  if( do_cancel )
    {
      calc_ramifications( -e, tag, ramifications );
      FOR( set<set<int> >::iterator, tagi, ramifications )
	add_one_eff( eff, -e, *tagi, -1 );
    }

  // Ojo: no deberia hacerse aqui
  // OJO: INSISTO, no deberia hacerse aqui.
  if( use_contingent && use_contingent_heuristic &&
      tag.size() == 0 ) 
    {
      if( use_contingent_m ) // && use_contingent_m_rules )
	eff.insert(m(e));
      if( use_contingent_k0 && 
	  use_contingent_k0_prop &&
	  static_atoms.count( abs(e) ) )
	eff.insert(k0(e));
      if( use_contingent_m &&
	  use_contingent_k0 && 
	  use_contingent_k0_prop &&
	  static_atoms.count( abs(e) ) )
	eff.insert(m0(e));
    }
}

void
prop_cancellation(int e, const set<int>& tag, set<int>& eff )
{
  //return; // Propagation of cancallation is not needed or sound?

  if(!use_propagation)
    return; 

  // The following is done because under simple cancellation 
  // there are no rules that negate all the -K-L/tag for every tag in tags(-L)
  if( use_simple_cancellation && !use_s0s )
    { 
      set<set<int> > ramifications_c;
      calc_ramifications( -e, emptytag, ramifications_c );
      FOR( set<set<int> >::iterator, tagi, ramifications_c )
	eff.insert( -tagged_t0c( -e, *tagi ) );      
    }
  eff.insert( -tagged_t0c( -e, tag ) );

  // Ojo: no deberia hacerse aqui
  // OJO: INSISTO, no deberia hacerse aqui.
  if( use_contingent && use_contingent_heuristic &&
      tag.size() == 0 ) 
    {
      if( use_contingent_m )
//       if( use_contingent_m && use_contingent_m_rules )
	eff.insert(-m(-e));
      if( use_contingent_k0 && 
	  use_contingent_k0_prop &&
	  static_atoms.count( abs(e) ) )
	eff.insert(-k0(-e));
      if( use_contingent_m &&
	  use_contingent_k0 && 
	  use_contingent_k0_prop &&
	  static_atoms.count( abs(e) ) )
	eff.insert(-m0(-e));
    }
}

  // When e becomes true, eff2 for cancellation rule
void
prop_k_gen(int e, const set<int>& tag, set<int>& eff1, set<int>* eff2p )
{
  assert( 0 != 0 );
  prop_support(e, tag, eff1);
  
  if(eff2p)
    {
      set<int>& eff2 = *eff2p;
      prop_cancellation(e, tag, eff2);
    }  
}

  // Those two following functions are called directly by basic transformation K_0
  // So, they should be robust enough

void
prop_k_cancel(int e, set<int>& eff1 )
{
  if( !use_t0c ) return;
  prop_cancellation(e, emptytag, eff1 );
}

  // When e becomes true
void
prop_k(int e, set<int>& eff1, bool do_cancel )
{
  if( !use_t0c ) return;
  prop_support(e, emptytag, eff1, do_cancel );
}

  // When e becomes true, eff2 for cancellation rule
void
prop_k2(int e, set<int>& eff1, set<int>& eff2 )
{
  assert( 0 != 0 );
  if( !use_t0c ) return;
  if( use_simple_cancellation )  
    prop_k_gen(e, emptytag, eff1, &eff2 );
  else
    prop_k_gen(e, emptytag, eff1, NULL );
}

// Maximal 
void
proc_when_t0c_maximal( When& w, Act& a_p )
{
  set<set<int> > all_tags;
  set<set<int> > all_tags_t;

  FOR( set<int>::iterator, e, w.eff ) 
    {
      set<set<int> >& tags_s = tags[*e];
      set_union( tags_s.begin(), tags_s.end(),
		 all_tags.begin(), all_tags.end(),
		 inserter(all_tags_t, all_tags_t.begin()));
      all_tags = all_tags_t;
    }
  FOR( set<int>::iterator, c, w.prec ) 
    {
      set<set<int> >& tags_s = tags[*c];
      set_union( tags_s.begin(), tags_s.end(),
		 all_tags.begin(), all_tags.end(),
		 inserter(all_tags_t, all_tags_t.begin()));
      all_tags = all_tags_t;
    }

  if(1) // OJO: tags > 1 not supported
    {
      FOR( set<set<int> >::iterator, t, all_tags )
	assert( t->size() == 1);
    }
  
  // all_tags contains all tags of conds and effects
  FOR( set<set<int> >::iterator, tp, all_tags )
    {
      int t = *(tp->begin()); // set of size 1.
  { // Support 
    When w_p;
    w_p.comment = "K Ci//tagi -> KL//tag, tagi maximal";
    
    FOR( set<int>::iterator, c, w.prec ) 
      {
	if ( is_relevant_star_obs(t, *c) )
	  w_p.prec.insert( tagged_t0c(*c, *tp) );
	else
	  w_p.prec.insert( k(*c) );
      }
    
    FOR( set<int>::iterator, e, w.eff ) 
      {
	if ( is_relevant_star_obs(t, *e) )
	  w_p.eff.insert( tagged_t0c(*e, *tp) );
	else
	  w_p.eff.insert( k(*e) );
      }
    
    if( !t0c_cont::clean_act( w_p, a_p.name ) )
      continue;
    a_p.addWhen(w_p);
  }
  { // Cancel 
    When w_p;
    w_p.comment = "-K -Ci//tagi -> -K-L//tag, all tagi maximal";
    
    FOR( set<int>::iterator, c, w.prec ) 
      {
	if ( is_relevant_star_obs(t, -*c) )
	  w_p.prec.insert( -tagged_t0c(-*c, *tp) );
	else
	  w_p.prec.insert( -k(-*c) );
      }
    
    FOR( set<int>::iterator, e, w.eff ) 
      {
	if ( is_relevant_star_obs(t, -*e) )
	  w_p.eff.insert( -tagged_t0c(-*e, *tp) );
	else
	  w_p.eff.insert( -k(-*e) );
      }
    
    if( !t0c_cont::clean_act( w_p, a_p.name ) )
      continue;
    a_p.addWhen(w_p);
  }
}
}

// Maximal 
void
proc_when_t0c_maximal_old( When& w, Act& a_p )
{
  /*
    AQUI!
    Observar si dado los tags, correctamente calculados,
    se dejan de generar algunos porque los tags
    de la condicion no coinciden con los de los efectos,
    o viceversa.
   */
  FOR( set<int>::iterator, e, w.eff ) 
    {
      { // Support 
	set<set<int> >& tags_e = tags[*e];
// 	set<set<int> >& tags_ne = tags[-*e];
	//assert( tags_ne.size() == tags_e.size() ); // falla para sort-4
// 	set<set<int> > all_tags;
// 	set_union( tags_e.begin(), tags_e.end(),
// 		   tags_ne.begin(), tags_ne.end(),
// 		   inserter(all_tags, all_tags.begin()));

	// for each possible tag for e or -l
	// if want only tags for e, replace all_tags by tags_e
	//FOR( set<set<int> >::iterator, tag_e, all_tags )
	FOR( set<set<int> >::iterator, tag_e, tags_e )
	  {
	    if( traza_t0c )
	      {
		cout << "Processing effect " << *e << " with tag ";
		pset(*tag_e);
	      }
	  
	    // For each condition, look for maximal
	    set<set<int> > maximal_pos;
	    set<int> emptytagged_pos;
	    FOR( set<int>::iterator, c, w.prec ) 
	      {
		set<set<int> >& tags_c = tags[*c];
		
		if( traza_t0c )
		  {
		    cout << "\tfor condition " << *c << ", tags: ";
		    pset(tags_c);
		  }
		// search largest tags pos
		bool isset_pos = false;
		set<int> largest_pos;
		size_t largest_pos_size = 0;
		FOR( set<set<int> >::iterator, tag_c, tags_c )
		  if( includes( tag_e->begin(), tag_e->end(), 
				tag_c->begin(), tag_c->end() ) &&
		      ( !isset_pos ||
			tag_c->size() >= largest_pos_size) ) 
		    {
		      if( !isset_pos || tag_c->size() > largest_pos_size )
			{
			  largest_pos.clear();
			  isset_pos = true;
			}
		      largest_pos_size = tag_c->size();
		      largest_pos.insert(tagged_t0c(*c, *tag_c) );
		    }
		if( !isset_pos )
		  {
		    assert( largest_pos.empty() );
		    largest_pos.insert( tagged_t0c(*c, emptytag ) );
		  }
		maximal_pos.insert(largest_pos);
		emptytagged_pos.insert( tagged_t0c(*c, emptytag ) );
	      }
	    
	    set<set<int> > conds = cartesian(maximal_pos);
	    // Don't want to imitate K_0
	    // NO... it cause ramificacion when there are no tags...
            //  conds.erase( emptytagged_pos );
	    if(!conds.empty())
	      {
		// For each combination of maximal_pos
		FOR(set<set<int> >::iterator, cond, conds)
		  {
		    When w_p;
		    w_p.comment = "K Ci//tagi -> KL//tag, tagi maximal";
		    
		    FOR_P( set<int>::iterator, c, cond)
		      {
			// if tag not relevant, simplify CLG
			tag_t &l_tag = t0c::inv_tags_t0c[abs(*c)];
			set<int>& tag = l_tag.second;
			if( tag.size() != 1 )
			  w_p.prec.insert(*c);
			else
			  {
			    int t = *(tag.begin());
			    int l = l_tag.first;
			    if( is_relevant( t, l) )
			      w_p.prec.insert(*c);
			    else
			      {
				int sign = (*c > 0? 1 : -1 );
				w_p.prec.insert(sign*k(l));
			      }
			  }
		      }
		    
		    add_eff( w_p.eff, *e, *tag_e );
		    
		    // Add ramifications
		    if( use_internal_propagation )
		      prop_support( *e, *tag_e, w_p.eff );

		    if( !t0c_cont::clean_act( w_p, a_p.name ) )
		      continue;
		    
		    a_p.addWhen(w_p);
		  }
	      }
	  }
      }

      // When using simple cancellation, this part is done in K_0
      // Ojo: poner en true esto un momento a ver si genera reglas de cancellation cuando
      // los tags estan bien calculados
      if( !use_simple_cancellation )  // ojo!!!
      { 
        // ****  Cancellation Rules ***
        set<set<int> >& tags_ne = tags[-*e];
        // tags_cancel are the ones used in cancellation that
        // are relevant to the effect but not to the conditions.
        //set<set<int> > tags_cancel = tags[-*e];
	
        // for each possible tag
	FOR( set<set<int> >::iterator, tag_ne, tags_ne )
	  {
	    if( traza_t0c )
	      {
		cout << "Processing effect " << -*e << " with tag ";
		pset(*tag_ne);
	      }
	  
	    // For each condition, look for maximal
	    set<int> maximal_neg;
	    set<int> emptytagged_neg;
	    FOR( set<int>::iterator, c, w.prec ) 
	      {
		// search largest tags neg
		set<set<int> >& tags_nc = tags[-*c];

                cout << "Printing tags for effect"  << endl;
                pset(tags_ne);
		
		if( traza_t0c )
		  {
		    cout << "\tfor condition " << -*c << ", tags: ";
		    pset(tags_nc);
		  }
                if ( is_relevant(*c, *e) )
                        cout << "contition " << -*c << " is relevant to effect " << -*e << endl;
                
		bool isset_neg = false;
		set<int> largest_neg;
		size_t largest_neg_size = 0;
		FOR( set<set<int> >::iterator, tag_nc, tags_nc )
		  if( includes( tag_ne->begin(), tag_ne->end(), 
				tag_nc->begin(), tag_nc->end() ) &&
		      ( !isset_neg ||
			tag_nc->size() >= largest_neg_size) ) 
		    {
		      if( !isset_neg || tag_nc->size() > largest_neg_size )
			{
			  largest_neg.clear();
			  isset_neg = true;
			}
		      largest_neg_size = tag_nc->size();
		      largest_neg.insert(tagged_t0c(-*c, *tag_nc) );
		    }
	      
		if( !isset_neg )
		  {
		    assert( largest_neg.empty() );
		    largest_neg.insert( tagged_t0c(-*c, emptytag ) );
		  }


		FOR( set<int>::iterator, l, largest_neg )
		  maximal_neg.insert(*l);
		emptytagged_neg.insert( tagged_t0c(-*c, emptytag ) );
	      }

	    // Don't want to imitate K_0
            //    if( maximal_neg != emptytagged_neg )
	      {
		When w_p;
		w_p.comment = "-K -Ci//tagi -> -K-L//tag, all tagi maximal";
	      
		FOR( set<int>::iterator, c, maximal_neg)
                {
                        w_p.prec.insert(-*c);
                        if ( is_relevant(-*c, -*e) )
                                cout << "contition " << -*c << " is relevant to effect " << -*e << endl;
                        //  cout << "cond: " << -*c << " " << (*c>0?"":"-") << atoms[abs(*c)] << ", ";
                }


		w_p.eff.insert( -tagged_t0c( -*e, *tag_ne ) );






 		if( use_internal_propagation )
 		  prop_cancellation( *e, *tag_ne, w_p.eff );

                // for all tags relevant to e, add a cancellation effect

		if( !t0c_cont::clean_act( w_p, a_p.name ) )
		  continue;
		
		a_p.addWhen(w_p);
	      }
	    
	  }
      }
    }
}



// Split atoms
void
make_split_t0c( )
{
  registerEntry( "make_split_t0c()" );

  // Para cada when W:
  FOR_1( wi, whens )
    {
      When& w = *whens[wi];
      if(!w.used) continue;

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

      proc_when_t0c_maximal( w, a_p );
      
    }

  //Ojo: tambien para efectos de acciones y precondiciones.
  // Tomar cada accion, ver los efectos que puso K_0 y agregar
  // el resultado de la ramificacion.
  /*if(0) // Was done in make_k_0, but violates encapsuling :-S
    for( size_t i = 1; i < actions_p.size(); i++ )
      {
	Act& a = actions[i];
	Act& a_p = actions_p[i];
	
	//for( set<int>::iterator e = a.eff.begin(); e != a.eff.end(); ++e )
	//prop_______( *e, a_p.eff );
	}*/
  registerExit();
}


  map<set<int>, int> tag2index;
  map<int, set<int> > index2tag;


  // Esto deberia estar afuera, pero dependemos de disjunctions
  // que esta erroneamente en este namespace
  // Cuando en algun mundo futuro repare/rehaga el codigo
  // las disjunciones estaran en su sitio...
  map<int,set<int> > xi2disj;
void 
oneof_with( int xi, set<int>& res, bool includes = true  )
{
  // no es cierto en general, mejor quitar... pero permite comenzar a verificar
  // OJO: activar .... assert( xi > 0 );
  res.clear();
  map<int,set<int> >::iterator it = xi2disj.find(xi);
  if( it != xi2disj.end() )
    res = it->second;
  else
    {
      FOR_0( i, oneof )
	if( oneof[i].count( xi ) > 0 )
	  FOR( set<int>::iterator, xj, oneof[i] )
	    if( //includes || 
		*xj != xi )
	      res.insert( *xj );
      xi2disj[xi] = res;
    }
}

bool trivial( const clause& c )
{
  return( c.size() == 2 &&
	  *(c.begin()) == -*(++(c.begin())));
}

void
calc_new_width()
{
  bool debug_it = verbose > LEVEL3;
  registerEntry( "calc_new_width()" );

  set<clause> disj_tmp;
  FOR( vector<set<int> >::iterator, it, disj )
    disj_tmp.insert( *it );
  for( set<int>::const_iterator e = unknown.begin();
       e != unknown.end(); e++ )
    {
      clause nc;
      nc.insert( *e );
      nc.insert( -*e );
      disj_tmp.insert( nc );
    }
  disj.clear();
  FOR( set<clause>::iterator, it, disj_tmp )
    disj.push_back( *it );

  // Check if in PI Form
  for( size_t i = 0; i < disj.size(); i++ )
    {
      const set<int>& d1 = disj[i];
      if( debug_it )
	{
	  cout << "Clause: ";
	  pset(d1);
	}
      if( trivial(d1) )
	continue;
      for( size_t j = i+1; j < disj.size(); j++ )
	{
	  const set<int>& d2 = disj[j];
	  if( trivial(d2) )
	    continue;
	  FOR( set<int>::iterator, l1, d1 )
	    FOR( set<int>::iterator, l2, d2 )
	    // Can resolve d1 and d2
	       if( *l1 == -*l2 )
		 {
		   set<int> nc;
		   FOR( set<int>::iterator, l1, d1 )
		     nc.insert(*l1);
		   FOR( set<int>::iterator, l2, d2 )
		     nc.insert(*l2);
		   nc.erase(*l1);
		   nc.erase(*l2);
		   bool subssumed = false;
		   for( size_t i = 0; !subssumed && i < disj.size(); i++ )
		     if( includes( disj[i], nc ) )
		       subssumed = true;
		   if( !subssumed )
		     {
		       cout << "ERROR: Initial situation not in Prime Implicate form. Offending:" << endl;
		       pset(d1);
		       pset(d2);
		       exit(1);
		     }
		 }
	}
    }
  // check width = 0 o fast width = 1
  precs_and_goals.clear();
  FOR( set<int>::iterator, gl, goal_literals )
    precs_and_goals.insert(*gl);
  FOR( set<int>::iterator, pl, precs_literals )
    precs_and_goals.insert(*pl);
  
  int max_width = 0;
  FOR( set<int>::iterator, l, precs_and_goals )
    {
      int width = 0;
      if( verbose > LEVEL3 )
	cout << "==> Considering literal " << *l << endl;
      clauses ci_l;
      for( size_t i = 0; i < disj.size(); i++ )
	if( lit_accept_disjunction_star( *l, disj[i] ) )
	  {
	    ci_l.insert( disj[i] );
	    if( verbose > LEVEL3 )
	      {
		cout << *l << " accepted by ";
		pset(disj[i]);
	      }
	  }
      
      // At least is one
      if( ci_l.size() > 0 )
	width = max(1,width);

      // check invariant
      set<int> lits_ci_l;
      FOR( clauses::iterator, c, ci_l )
	FOR_P( clause::iterator, lit, c )
	   lits_ci_l.insert(abs(*lit));
      FOR( clauses::iterator, c, ci_l )
	if( trivial(*c) )
	  lits_ci_l.erase( abs(*(c->begin())) );
//       if(lits_ci_l.size() != 0 )
// 	{
// 	  cout << "Invariant violated: if lit in C_I(L), then lit || -lit in C_I(L)" << endl;
// 	  pset(lits_ci_l);
// 	  exit(1);
// 	}

      // Try to probe that width = 1
      bool one_hits = false; 
      for( clauses::reverse_iterator c = ci_l.rbegin();
	   c != ci_l.rend(); ++c )
	//      FOR( clauses::iterator, c, ci_l )
	{
	  if( debug_it )
	    {
	      cout << "Trying with clause: ";
	      pset(*c);
	    }
	  // Try with c
	  bool c_hits = true;
	  FOR_P( clause::iterator, lit, c )
	    {
	      if( debug_it )
		cout << "\tTrying with literal " << *lit << endl;
	      // Each lit should hit* all
	      clauses res;
	      set<int> lits;

	      // OJO-IJCAI09: Antes las consecuencias de un literal eran solo
	      // sobre las clausulas locales (ci_l), pero deberian ser sobre toda la teoria
	      // de acuerdo al t0-journal paper.
// 	      lits.insert(*lit);
// 	      unit_res( ci_l, res, lits );

	      implies_with_init( *lit, lits );

	      if( debug_it )
		{
		  cout << "\tLits after unit-prop: ";
		  pset(lits);
		}
	      bool hits_all = true;
	      FOR( clauses::iterator, ci, ci_l )
		{
		  set<int> inter;
		  set_intersection( lits.begin(), lits.end(),
				    ci->begin(), ci->end(), 
				    inserter(inter, inter.begin()));
		  if( inter.empty() )
		    {
		      hits_all = false;
		      if( debug_it )
			{
			  cout << "\t\tDoesn't hit: ";
			  pset(*ci);
			}
		      break;
		    }
		}
	      if(!hits_all)
		{
		  c_hits = false;
		  break;
		}
	    }
	  if( c_hits )
	    {
	      if( debug_it )
		{
		  cout << "this clause accept all: ";
		  pset(*c);
		}
	      one_hits = true;
	      break;
	    }
	}
      if( width != 0 && !one_hits )
	{
	  width = 1000;
	  cout << "Rejected lit " << *l << " with width " << width << endl;
	}
      max_width = max(max_width,width);
    }
  cout << "Max-width " << max_width << endl;
  registerExit();
}

void
setup_I_disjunctions()
{
  const bool use_all_disjunctions = false; // OJO: CLG. usar false si funciona y true seria muy grande
  static bool done = false;
  if(done) return;

  assert( disjunctions.size() == 0 );
  if(use_all_disjunctions)
    {
      set<clause> disj_tmp;
      // Adding Init
      FOR( vector<set<int> >::iterator, d, disj )
	if( !use_relevance ||
	    accept_disjunction( *d ) )
	  {
	    disj_tmp.insert( *d );
	    is_oneof.push_back(false);
	  }
      FOR( set<clause>::iterator, it, disj_tmp )
	disjunctions.push_back( *it );
    }
  else
    {
      // Adding Init
      FOR( vector<set<int> >::iterator, d, disj_orig )
	if( !use_relevance ||
	    accept_disjunction( *d ) )
	  {
	    disjunctions.push_back( *d );
	    is_oneof.push_back(false);
	  }
      
      FOR( vector<set<int> >::iterator, d, oneof )
	if( !use_relevance ||
	    accept_disjunction( *d ) )
	  {
	    disjunctions.push_back( *d );
	    is_oneof.push_back(true);
	  }
    }
  if( use_relevance )
    {
      FOR( set<int>::iterator, lit, simple_unknown )
	{
	  set<int> d;
	  d.insert(*lit);
	  d.insert(-*lit);
	  if( accept_disjunction( d ) )
	    {
	      disjunctions.push_back( d );
	      is_oneof.push_back(true);
	    }
	}
      print_width();
    }
  
  if(true)
    {
      cout << "Final disjunctions: " << use_relevance << endl;
      FOR_0( i, disjunctions )
	{
	  set<int>& c = disjunctions[i];
	  pset(c);
	}
      cout << "==== End of Final disjunctions: " << endl;
    }
  done = true;
}

void
obtain_I_disjunctions() {
  // Create theory to calculate prime implicates
  // verificar que no se crean units. Que hacer en ese caso?

  setup_I_disjunctions();

  FOR( vector<clause>::iterator, c, disjunctions )
    FOR_P( clause::iterator, lit, c )
    {
      set<int> t;
      t.insert(*lit);
      tag2index[t] = *lit;
      index2tag[*lit] = t;
    }
}

void
obtain_prime_implicates() {
  vector<clause>& pi = disjunctions;
  // Create theory to calculate prime implicates
  // verificar que no se crean units. Que hacer en ese caso?

  registerEntry( "obtain_prime_implicates()" );

  clauses theory;
  // Adding Init
  FOR( vector<set<int> >::iterator, d, disj )
    theory.insert( *d );

  set<int> var_used;
  // Var for each tag
  int init_index = atoms.size()+10;
  int index = init_index;
  for( lit2tags_t:: iterator it = tags.begin();
       it != tags.end(); it++ )
    {
      set<set<int> >& ts = it->second;
      FOR( set<set<int> >:: iterator, t, ts )
	{
	  if( t->size() == 1 )
	    {
	      int lit = *(t->begin());
	      var_used.insert(abs(lit));
	      tag2index[*t] = lit;
	      index2tag[lit] = *t;
	      continue;
	    }
	  map<set<int>, int>::iterator tagit = tag2index.find(*t);
	  if( tagit == tag2index.end() )
	    {
	      int var = index++;
	      tag2index[*t] = var;
	      index2tag[var] = *t;
	      
	      if( traza_t0c_pi )
		cout << "Var " << int2str(var) 
		     << " equiv to " << set2str(*t) << endl;
	      
	      // Equivalence between tag and var
	      // tag -> var \equiv -tag || var
	      clause c1;
	      c1.insert(var);
	      FOR_P( set<int>:: iterator, lit, t )
		c1.insert( -*lit );
	      theory.insert(c1);
	      
	      // var -> tag \equiv 
	      FOR_P( set<int>:: iterator, lit, t )
		{
		  clause c2;
		  c2.insert(-var);
		  c2.insert(*lit);
		  theory.insert(c2);
		}
	    }
	}
    }
  
  // Ordering. We want tag vars at the end
  prime_impl::order_t order; // pair of var, number
  int ord = 1;
  for( int i = 1; i <= atoms.size()-1; i++ )
    if( var_used.count(i) == 0 )
      order.push_back( make_pair(i, ord++) );
  int i = init_index;
  for( ; i < index; i++ )
    order.push_back( make_pair(i, ord++) );
  FOR( set<int>::iterator, v, var_used )
    order.push_back( make_pair(*v, ord++) );    
  clauses pitmp;

  if( traza_t0c_pi )
    {
      cout << "========================================" << endl;
      cout << "original theory" << endl;
      pr_clauses( theory );
    }
  int saved;
  // Get prime implicates
  if( use_filter )
    saved = prime_impl::get( theory, order, pitmp, init_index );  
  else
    saved = prime_impl::get( theory, order, pitmp );
  // Only clausules over tag variables
  FOR( clauses::iterator, disjp, pitmp )
    {
      bool add = true;
      FOR_P( clause::iterator, lit, disjp )
	if( abs(*lit) < init_index &&
	    var_used.count(abs(*lit)) == 0 )
	  {
	    add = false;
	    break;
	  }
      if( add &&
	  disjp->size() == 2 )
	{
	  set<int>& first_s = index2tag[*disjp->begin()];
	  set<int>& second_s = index2tag[*(++(disjp->begin()))];
	  if( first_s.size() == 1 &&
	      second_s.size() == 1 )
	    {
	      int first = *first_s.begin();
	      int second = *second_s.begin();
	      if( first == -second &&
		  unknown_relevant.count( abs(first) ) == 0 )
		{
		  add = false;
		  if( verbose > LEVEL3 )
		    {
		      cout << "Deleting prime implicate: " << first 
			   << " or " << second << endl; 
		    }
		}
	    }
	}
      if(add)
	pi.push_back( *disjp );
    }

  if( traza_t0c_pi )
    {
      cout << "========================================" << endl;
      cout << "prime implicates" << endl;
      FOR( vector<clause>::iterator, c, pi )
	pr_clause(*c);
    }
  if( verbose > LEVEL1 )
    {
      std::cout << "Init theory + tags with " << theory.size() << " clauses" << std::endl
		<< "\tincluding " << index-init_index+1 << " tag variables " << std::endl
		<< "Prime implicates with " << pitmp.size() << " clauses"  << std::endl;
      if(use_filter)
	std::cout<< "Saved " << saved << " because skip filtering" << std::endl ;
      std::cout	      << "Relevant prime implicates with " << pi.size() << " clauses"  << std::endl;
    }
  registerExit();

}

class add_conds_all_tagged
{
public:
  void operator()( set<int>& prec, int l, const set<set<int> >& tags ) const {
    FOR( set<set<int> >::iterator, tagi, tags )
      prec.insert( tagged_t0c( l, *tagi ) );
  }
};

class add_conds_sl_tagged
{
public:
  void operator()( set<int>& prec, int l, const set<set<int> >& tags ) const {
    FOR( set<set<int> >::iterator, tagi, tags )
      prec.insert( tagged_t0c_sl( l, *tagi ) );
  }
};

template <class Add_cond>
void
do_one_merge( int l, size_t& merge_num, const set<set<int> >& tags, 	      
	      const set<int>& precs, Add_cond add_cond )
{
  Act a_p;
  a_p.ground = 0;
  a_p.index = actions_p.size();

  if (use_no_cost_closures)
    a_p.cost = 0.0;
  else
    a_p.cost = CLOSURE_COST;
	    
  string name = "merge_";
  if(use_contingent)
    name = "closure_" + name;
  if(l < 0 )
    name.append("-");
  name += atoms[abs(l)];
  name += "__";
  ostringstream str_l;
  str_l << ++merge_num;
  name += "_" + str_l.str();
  a_p.name = string(name);
		    
  When w_p;
  w_p.comment = "merge l//xi";
		    
  // Merge l and ramifications
  assert_lit( l, w_p.eff, true, use_full_propagation, false );
		    
  // Preconditions
  add_cond( w_p.prec, l, tags );
  FOR( set<int>::const_iterator, p, precs )
    w_p.prec.insert( *p );
  a_p.addWhen(w_p);

  actions_p.push_back(a_p);
}


// Add cond of the form
// K-t1 & ... l/t ... & K-tn
class add_conds_one_tagged
{
public:
  int t;
  add_conds_one_tagged(int mt): t(mt) {}

  void operator()( set<int>& cond, int l, const set<set<int> >& tags ) const {
    FOR( set<set<int> >::iterator, tagi, tags )
      {
	assert( tagi->size() == 1 );
	int ti = *tagi->begin();
	if( ti == t )
	  cond.insert( tagged_t0c( l, *tagi ) );
	else
	  cond.insert( k0(-ti ) );
      }
  }
};

class add_no_conds
{
public:
  void operator()( set<int>& prec, int l, const set<set<int> >& tags ) const {
  }
};

void
do_all_merges( int l, size_t& merge_num, const set<set<int> >& tags )
{
  // combinations K-t || Kl/t
  set<set<int> > cases;
  set<int> todel1, todel2;
  FOR( set<set<int> >::const_iterator, tag, tags )
    {
      set<int> s;
      if( tag->size() > 1 )
	return;
      int t = *(tag->begin());
      s.insert( k0(-t) );
      s.insert( tagged_t0c(l,*tag) );
      todel1.insert( k0(-t ) );
      todel2.insert( tagged_t0c(l,*tag) );
      cases.insert(s);
    }
  
  set<set<int> > rules;
  rules = cartesian(cases);
  rules.erase(todel1);
  rules.erase(todel2);

  FOR( set<set<int> >::const_iterator, rule, rules )
    do_one_merge( l, merge_num, set<set<int> >(), *rule, add_no_conds() );
}

void
do_sl_merges( int l, size_t& merge_num, const set<set<int> >& tags )
{
  // combinations K-t || Kl/t
  set<set<int> > cases;
  set<int> todel1, todel2;
  FOR( set<set<int> >::const_iterator, tag, tags )
    {
      set<int> s;
      if( tag->size() > 1 )
	return;
      int t = *(tag->begin());
      s.insert( k0(-t) );
      s.insert( tagged_t0c(l,*tag) );
      todel1.insert( k0(-t ) );
      todel2.insert( tagged_t0c(l,*tag) );
      cases.insert(s);
    }
  
  set<set<int> > rules;
  rules = cartesian(cases);
  rules.erase(todel1);
  rules.erase(todel2);

  FOR( set<set<int> >::const_iterator, rule, rules )
    do_one_merge( l, merge_num, set<set<int> >(), *rule, add_no_conds() );
}

void
create_sl_rules( int l, size_t& merge_num, const set<set<int> >& tags )
{
  string prefix = "__";
  if(l < 0 )
    prefix.append("-");
  prefix += atoms[abs(l)];
  prefix += "__";
  ostringstream str_l;
  str_l << ++merge_num;
  prefix += "_" + str_l.str();
  
  Act a_add, a_del;
  a_add.ground = 0;
  a_add.index = actions_p.size();
  a_add.name = "closure_add_sl" + prefix;
  a_del.ground = 0;
  a_del.index = actions_p.size()+1;
  a_del.name = "delete_closure_sl" + prefix;

  if (use_no_cost_closures) {
    a_add.cost = 0.0; 
    a_del.cost = 0.0;
  }
  else {
    a_add.cost = CLOSURE_COST;
    a_del.cost = CLOSURE_COST;
  }

  // For each SL/tag, create rules
  FOR( set<set<int> >::iterator, it, tags )
    {
      const set<int>& lab = *it;
      assert( lab.size() == 1 );
      int t = *(lab.begin());
      int sl = tagged_t0c_sl( l, lab );
      if( if_tagged_t0c( l, lab ) )
	{
	  int kl = tagged_t0c( l, lab );
	  
	  // K L\t --> S L\t
	  When w_kl_sl;
	  w_kl_sl.prec.insert( kl ); 
	  w_kl_sl.eff.insert( sl );
	  a_add.addWhen( w_kl_sl );
	}

      // K@0 -t --> S L\t 
      When w_k0_sl;
      w_k0_sl.prec.insert( k0( -t ) ); 
      w_k0_sl.eff.insert( sl );
      a_add.addWhen( w_k0_sl );

      // SL/t  ->  -SL/t
      When w_del_sl;
      w_del_sl.prec.insert( sl ); 
      w_del_sl.eff.insert( -sl );
      w_del_sl.eff.insert( k( cont_dummy_pred_n ) );
      a_del.addWhen( w_del_sl );
    }
  actions_p.push_back(a_add);
  if( use_delete_closure_sl )
    actions_p.push_back(a_del);
}

  // OJO: esto deberia estar en contingent...
void
do_contingent_merges( int l, size_t& merge_num, const set<set<int> >& tags )
{
  if( !use_contingent ) return;
  size_t max_size = 0;
  FOR( set<set<int> >::iterator, tag, tags )
    max_size = MAX(max_size, tag->size() );
  if( max_size == 1 )
    {
      if( use_contingent_full_merge )
	do_all_merges( l, merge_num, tags );
      else if( use_contingent_sl_merges )
	{
	  do_one_merge( l, merge_num, tags, set<int>(), add_conds_sl_tagged() );
	  create_sl_rules( l, merge_num, tags );
	}
      else
	FOR( set<set<int> >::iterator, tag, tags )
	  {
	    int t = *tag->begin();
	    do_one_merge( l, merge_num, tags, set<int>(), add_conds_one_tagged(t) );
	  }
    }
}

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

  calc_tags(  );

  make_split_t0c(  );
//  printDebugPDDL();
  if( traza_t0c )
    cout << "\n\nHaciendo merge..." << endl;

  if( use_s0s )
    {
      assert(dnf_calculated);

      int init_index = atoms.size()+10;
      int index = init_index;
      disjunctions.push_back(clause());
      clause& d = disjunctions.back();
      FOR( set<set<int> >::iterator, c, dnf )
	{

	  int var = index++;
	  d.insert(var);
	  tag2index[*c] = var;
	  index2tag[var] = *c;
	}
    }
  else if(use_only_I_disjunctions)
    obtain_I_disjunctions();
  else
    obtain_prime_implicates();

  registerEntry( "make_k_t0c()" );

  // Create merge
  // For each l/tag
  for( lit2tags_t::iterator it = tags.begin();
       it != tags.end(); ++it )
    {
      int l = it->first;
      if( use_merge_only_goals_and_precs && 
	  goal_literals.count(l) == 0 &&
	  precs_literals.count(l) == 0 )
	continue;
      set<set<int> >& ts = it->second;
      size_t merge_num = 0;
      
      // Disjunctions used with l
      set<size_t> merge_tried;

      // From l/tag into set of iterator processed
      FOR( set<set<int> >::iterator, tagp, ts )
	{
	  const set<int>& tag = *tagp;
	  // Given a l/tag

	  // Var of tag, if possible
	  int var;
	  map<set<int>, int>::iterator it = tag2index.find(tag);
	  if( it == tag2index.end() ) continue;
	  var = it->second;

	  if( traza_t0c )
	    cout << "Trying to merge: " << atoms[abs(l)] << "(" << l << ")/"
		 << set_atoms2str(tag) << " with var = " << var << endl;

	  FOR_0( disji, disjunctions ) // Seems to be costly
	    {
	      const clause& disj = disjunctions[disji];
	      if( disj.count(var) > 0 &&
		  merge_tried.count(disji) == 0 )
		{
		  merge_tried.insert(disji);
		  
		  if( traza_t0c )
		    cout << "Trying to make merge with (" << disji 
			 << ") = " << set_atoms2str(disj) << endl;
		  // OJO CLG: create merge if t relevant to any observation
		  bool doit = true;
		  bool all_tags = true;
		  // Look for others l/tagi
		  set<set<int> > newtags;
		  FOR( clause::iterator, vtagi, disj )
		    {
		      map<int, set<int> >::iterator it = index2tag.find(*vtagi);
		      if( it == index2tag.end() ||
			  ts.count(it->second) == 0 )
			{
			  all_tags = false;
			  if( is_relevant_star_obs( *vtagi, l ) )
			    {
			      set<int> s;
			      s.insert( *vtagi );
			      newtags.insert(s); // OJO: not a real tag
			      if( traza_t0c )
				cout << "accepting " << *vtagi << " "
				     << (is_relevant_star( *vtagi, l )?"t*":"obs") << endl;
			    }
			  else
			    {
			      doit = false;
			      if( traza_t0c )
				cout << "rejecting " << *vtagi << endl;
			    }
			}
		      else
			{
			  newtags.insert(it->second);
			  if( traza_t0c )
			    cout << "accepting " << *vtagi << " tagged " << endl;
			}
		    }

		  //If the disjuntion is covered by tags, make merge
		  if(doit)
		    {
		      if( traza_t0c )
			cout << "Merging with (" << disji 
			     << ") = " << set2str(disj) << endl;
		      if( all_tags )
			do_one_merge( l, merge_num, newtags, set<int>(), add_conds_all_tagged() );
		      if( use_contingent &&
			  ( use_contingent_full_merge || use_contingent_sl_merges ) ) 
			do_contingent_merges( l, merge_num, newtags );
		      //else
		    }
		}
	    }
	}
    }  
  
  registerExit();
}

void
clean_tags( map<int,set<set<int> > >& tags, const set<int>& todel )
{
  for(map<int,set<set<int> > >::iterator it = tags.begin();
      it != tags.end(); it++ )
    {
      set<set<int> > del;
      FOR( set<set<int> >::iterator, ss, it->second )
	{
	  int e = tagged_t0c(it->first, *ss);
	  if( todel.count(e) > 0 )
	    del.insert(*ss);
	}
      FOR(set<set<int> >::iterator, d, del )
	it->second.erase(*d);
//       if(it->second.empty())
// 	tags.erase(*it);
    }  
}

  /*
    Go over all new actions collecting:
    - atoms metioned
    - atoms in conditions
    
    Todel = mentioned - conditions - basic atoms Kx K-x
    Go again over all actions, deleting 
       every atom in Todel from: effects
    Del also from init_tags and tags


    OJO: no tomar en cuenta cancellation rules.
    idea: todo el acarreo sucede a traves de support rules.
    las cancellation rules solo pueden quitar atomos.
    quizas es lo mismo no considerar "in_conds" atomos negativos.
   */

void
clean_eff(set<int> &eff)
{
  set<int> del_e;
  FOR( set<int>::iterator, ei, eff )
    {
      int e = abs(*ei);
      if( atoms_p_todel.count(e) > 0 )
	del_e.insert(*ei);
    }
  FOR( set<int>::iterator, d, del_e )
    eff.erase(*d);	
};
  
void 
clean_cond( When& w )
{
  set<int> del;
  FOR( set<int>::iterator, ei, w.eff )
    {
      int e = abs(*ei);
      if( atoms_p_todel.count(e) > 0 )
	del.insert(*ei);
    }
  FOR( set<int>::iterator, d, del )
    w.eff.erase(*d);

  FOR( set<int>::iterator, pi, w.prec )
    {
      int p = abs(*pi);
      if( atoms_p_todel.count(p) > 0 )
	w.used = false;
    }
}

void
clean_acts( vector<Act>& acts_p )
{
  for( size_t i = 1; i < acts_p.size(); i++ )
    {
      Act& a = acts_p[i];
      clean_eff( a.eff );
      
      FOR( vector<When>::iterator, wi, a.conds )
	clean_cond( *wi );
      
      FOR( vector<Act::branch_t>::iterator, it, a.branch_eff )
	{
	  set<int>& eff = it->first;
	  Conds& condeff = it->second;
	  
	  clean_eff( it->first );
	  FOR( vector<When>::iterator, wi2, it->second )
	    clean_cond( *wi2 );
	  
      	}
    }
}

void
clean_actions()
{
  registerEntry( "clean_actions()" );
  set<int> used;
  set<int> mentioned;
  for( size_t i = 1; i < actions_p.size(); i++ )
    {
      const Act& a = actions_p[i];
      FOR( vector<When>::const_iterator, wi, a.conds )
	{
	  FOR( set<int>::const_iterator, ci, wi->prec )
	    {
	      int c = abs(*ci);
	      if( !is_k0_lit(c) )
		{
		  if(*ci > 0) used.insert(c);
		  mentioned.insert(c);
		}
	    }
	  FOR( set<int>::const_iterator, ei, wi->eff )
	    {
	      int e = abs(*ei);
	      if( !is_k0_lit(e) )
		mentioned.insert(e);
	    }
	  assert( !wi->eff.empty() );

	}
    }
  if(use_new_clean_actions)
    {
      const bool use_prec_clean = false;
      set<int> mod_lits;
      FOR( set<int>::iterator, l, goal_literals )
	mod_lits.insert(k(*l));
      FOR( set<int>::iterator, l, precs_literals )
	mod_lits.insert(k(*l));
      bool fixpoint = false;
      while(!fixpoint)
	{
	  fixpoint = true;
	  // From every action goes backwards
	  for( size_t i = 1; i < actions_p.size(); i++ )
	    {
	      const Act& a = actions_p[i];
	      bool use_prec = false;
	      if( use_prec_clean )
		FOR( set<int>::iterator, e, a.eff )
		  if( mod_lits.count( *e) > 0 ||
		      mod_lits.count( -*e) > 0 )
		    {
		      FOR( set<int>::iterator, p, a.prec )
			if( mod_lits.count( *p ) == 0 )
			  {
			    mod_lits.insert(*p);
			    fixpoint = false;
			  }
		      break;
		    }
	      FOR( vector<When>::const_iterator, wi, a.conds )
		{
		  FOR( set<int>::const_iterator, ei, wi->eff )
		    if( mod_lits.count( *ei) > 0 ||
			mod_lits.count( -*ei) > 0 )
		      {
			FOR( set<int>::iterator, c, wi->prec )
			  if( mod_lits.count( *c ) == 0 )
			    {
			      mod_lits.insert(*c);
			      fixpoint = false;
			    }
			if( use_prec_clean )
			  FOR( set<int>::iterator, p, a.prec )
			    if( mod_lits.count( *p ) == 0 )
			      {
				mod_lits.insert(*p);
				fixpoint = false;
			      }
			break;
		      }
		}
	    }
	  cout << "fixpoint " << fixpoint << endl;
	}
      if(true)
	{ // Sound
	  used.clear();
	  FOR( set<int>::iterator, it, mod_lits )
	    used.insert( abs(*it ));
	  if( false )
	    {
	      cout << "Atoms used:" << endl;
	      FOR( set<int>::iterator, usedit, used )
		cout << *usedit << ": " << name_l(*usedit) << endl;
	    }
	}
      else // not sound
	used = mod_lits;
    }
  set<int> new_todel;
  set_difference( mentioned.begin(), mentioned.end(),
		  used.begin(), used.end(),
		  inserter(new_todel, new_todel.begin()));
  set_difference( new_todel.begin(), new_todel.end(),
		  atoms_p_not_todel.begin(), atoms_p_not_todel.end(),
		  inserter(atoms_p_todel, atoms_p_todel.begin()));
  bool debugit = true;
  if( debugit )
    {
      cout << "Number of Atoms to del: " << atoms_p_todel.size() << endl;
      if(false)
	{
	  cout << "Atoms to del:" << endl;
	  FOR( set<int>::iterator, delit, atoms_p_todel )
	    cout << *delit << ": " << name_l(*delit) << endl;
	}
    }

  clean_tags( init_tags, atoms_p_todel );
  clean_tags( tags, atoms_p_todel );

  clean_acts( actions_p );
  clean_acts( observations_p );
  registerExit();
}

}

