/*******************************************************************************
 **
 **   CF2CS: A compiler from conformant planning problems into classical planning problems
 **          Sound, but incomplete...
 **
 ******************************************************************************/

#include <iostream>
#include <algorithm>
#include <fstream>
#include <sstream>
#include <stdio.h>
#include <string.h>
#include <stdlib.h>
#include <math.h>
#include <sys/time.h>
#include <sys/resource.h>
#include <unistd.h>
#include <fcntl.h>
#include <values.h>
#include <assert.h>

#include <queue>
#include <deque>
#include <map>
#include <set>
#include <string>
#include <vector>
#include <sstream>
#include <algorithm>
#include <ext/hash_map>

#include "nnf.h"
#include "cnf.h"

#include "parser.h"
#include "planner.h"
#include "clauses.hpp"
#include "prime-impl.hpp"
#include "cartesian.hpp"

#include "cf2cs.h"
#include "parser-global.hpp"
#include "main.hpp"

using namespace prime_impl;

/*******************************************************************************
 **
 **   Macros
 **
 ******************************************************************************/

#define   NUMCONTROLS    9
#define   HASHSIZE       27449
#define   GOAL           1
#define   MARK           2
#define   SOLVED         4
#define   MILLION        (float)1000000

// goal type
#define   FORMULA        0
#define   CERTAINTY      1
#define   KNOWLEDGE      2

// Default costs
#ifndef _COSTS
#define _COSTS
#define ACTION_COST 1.0f
#define OBSERVATION_COST 1.0f
#define CLOSURE_COST 1.0f
#endif


/*******************************************************************************
 **
 **   Global Data
 **
 ******************************************************************************/



int             horizon = 1;

const char**    atom_names = 0;
std::set<int>   op_atoms;





std::set<int> static_oneof_atoms;

set<int> all_mentioned;


std::map<std::pair<size_t,formula_t*>,size_t> cmap;

const string active_pred("ACTIVE");
int active_pred_n = 0;
const string all_end_pred("ALL_END");
int all_end_pred_n = 0;
const string cont_dummy_pred("CONT_DUMMY");
int cont_dummy_pred_n = 0;
int t0_fail_pred_n = -1;

const bool use_t0 = false;
bool use_kp = false;

bool use_merge_act = false;
bool use_merge_only_goals_and_precs = true;

bool use_t0c = false;
bool use_s0s = false;
bool use_simple_cancellation = false;
bool use_only_I_disjunctions = true;
bool use_relevance = true; //OJO: poner true por defecto
bool use_relevance_calc_width = true;
bool only_check_new_width = false;
const bool use_propagation = true;
bool use_clause_b_tags = true;
const bool use_filter = true;
bool use_clean_actions = true;
const bool use_new_clean_actions = true; // Probably unsound if set to false
bool use_delete_free = false;

// Became true in parser.y when an observation is parsed
bool use_contingent = false;
const bool use_contingent_heuristic = true;
bool use_contingent_fail_check = false;
bool use_contingent_active_pred = true;
bool use_contingent_active_pred_disj = true;
const bool use_contingent_act_comp = false;
bool use_contingent_full_merge = false;
bool use_contingent_sl_merges = false;
// New
bool use_contingent_obs_nondeter = false;
bool use_contingent_obs_determ = false; // use_contingent_obs_determ \imply use_contingent_m
bool use_contingent_m = false;
bool use_contingent_k0 = false;
bool use_contingent_m0 = false;
bool use_contingent_knl_imply = false;
bool use_contingent_kt_imply = false;
bool use_contingent_mnl_imply = false;
bool use_contingent_mt_imply = false;
bool use_contingent_m_rules = false;
bool use_contingent_k0_prop = false;
bool use_delete_closure_sl = false;
bool use_k_preconds = true;
bool use_merge_act_m = false; // for reasoning with disjunctions over Ms, but not over oneof
bool use_merge_act_m_old = false; // exactly as -mac for Km
bool use_merge_act_k0 = false;
bool use_merge_act_m0 = false;
bool use_full_propagation = false;
bool use_obs_variables = true;
bool use_new_tag_gen = false;
bool use_costs = false;
bool use_no_cost_closures = false;
bool use_assumptions_on_tags = false;

/*******************************************************************************
 **
 **   Forward References
 **
 ******************************************************************************/

void                   _fatal( int, char*, char*, int );
std::ostream&          printOperator( std::ostream&, operator_t* );
std::ostream&          operator<<( std::ostream&, operator_t& );
void                   registerEntry( char* );
int                    registerExit( void );
char*                  operatorName( int*, int );
char*                  readAtomName( int );
iatom_t*               readAtomByNumber( int );


namespace merge_act
{
  void create_one_merge( string, string, Act&, size_t, int extra_prec = 0 );
}

namespace t0c
{
  void prop_k(int e, set<int>& eff1, bool do_cancel = true );
  void prop_k_cancel(int e, set<int>& eff1 );
  void pset( const set<int>& ss );
}

namespace t0c_cont {
  void prepare_action( Act& a );
  size_t action_comp_mutex();
  bool clean_act( When& w, string name );
}

bool
set_consistent( const set<int>& s )
{
  FOR( set<int>::const_iterator, si, s )
    if( s.count(-*si) > 0)
      return false;
  return true;
}   

// do indent
void
di( ostream& o, size_t z )
{
  if( z < 0 ) z=0;
  for( size_t i = 0; i < z; i++ )
    o << " ";
}

bool
includes( const set<int>& s1, const set<int>& s2 ){
  return includes( s2.begin(), s2.end(),
		   s1.begin(), s1.end() );
}


// s1 smaller is more efficient
bool
includes_abs( const set<int>& s1, const set<int>& s2, vector<int>& r2a ){
  for( set<int>::const_iterator ai = s1.begin(); 
       ai != s1.end(); ai++ )
    if( s2.count( r2a[abs(*ai)] ) == 0 )
      return false;
    else
      cout << *ai << " esta " << endl;
  return true;
}


/*******************************************************************************
 **
 **   new Atoms and Actions
 **
 ******************************************************************************/

vector<When*> whens;

// for problem P'
vector<Act> actions_p;
vector<Act> observations_p;

size_t
new_nwhen( bool include_nonused = false )
{
  size_t n = 0;
  FOR(vector<Act>::iterator, a, actions_p )
    FOR( std::vector<When>::const_iterator, wi, a->conds )
      if(include_nonused || wi->used)
        ++n;
  return n;
}

// actionReqPosAtom[atom] = actions that have +atom in prec
vector<set<unsigned> > actionReqPosAtom;
// actionReqNegAtom[atom] = actions that have -atom in prec
vector<set<unsigned> > actionReqNegAtom;
const set<unsigned>& actionReqLit( int lit )
{
  return lit>0?actionReqPosAtom[lit]:actionReqNegAtom[-lit];
}
void setActionReqLit( size_t a, int lit )
{
  if( lit > 0 )
    actionReqPosAtom[lit].insert(a);
  else
    actionReqNegAtom[-lit].insert(a);
}

// actionAddAtom[atom] = actions that add atom (uncond)
vector<set<unsigned> > actionAddAtom;
// actionDelAtom[atom] = actions that del atom (uncond)
vector<set<unsigned> > actionDelAtom;
const set<unsigned>& actionEffLit( int lit )
{
  return lit>0?actionAddAtom[lit]:actionDelAtom[-lit];
}
void setActionEffLit( size_t a, int lit )
{
  if( lit > 0 )
    actionAddAtom[lit].insert(a);
  else
    actionDelAtom[-lit].insert(a);
}

// whenAddAtom[atom] = when requiring +atom
vector<set<unsigned> > whenAddAtom;
// whenDelAtom[atom] = when requiring -atom
vector<set<unsigned> > whenDelAtom;
const set<unsigned>& whenEffLit( int lit )
{
  if( lit>0 )
    {
      if(lit >= whenAddAtom.size() )
	whenAddAtom.resize(lit+1);
      return whenAddAtom[lit];
    }
  else
    {
      if(-lit >= whenDelAtom.size() )
	whenDelAtom.resize(-lit+1);
      return whenDelAtom[-lit];
    }
}
void setWhenEffLit( size_t w, int lit )
{
  if( lit > 0 )
    {
      if(lit >= whenAddAtom.size() )
	whenAddAtom.resize(lit+1);
      whenAddAtom[lit].insert(w);
    }
  else
    {
      if(-lit >= whenDelAtom.size() )
	whenDelAtom.resize(-lit+1);
      whenDelAtom[-lit].insert(w);
    }
}

// whenReqPosAtom[atom] = when requiring +atom
vector<set<unsigned> > whenReqPosAtom;
// whenReqNegAtom[atom] = when requiring -atom
vector<set<unsigned> > whenReqNegAtom;
const set<unsigned>& whenReqLit( int lit )
{
  if(lit>0)
    {
      if(lit >= whenReqPosAtom.size() )
	whenReqPosAtom.resize(lit+1);
      return whenReqPosAtom[lit];
    }
  else
    {
      if(-lit >= whenReqNegAtom.size() )
	whenReqNegAtom.resize(-lit+1);
      return whenReqNegAtom[-lit];
    }
}
void setWhenReqLit( size_t w, int lit )
{
  if( lit > 0 )
    {
      if(lit >= whenReqPosAtom.size() )
	whenReqPosAtom.resize(lit+1);
      whenReqPosAtom[lit].insert(w);
    }
  else
    {
      if(-lit >= whenReqNegAtom.size() )
	whenReqNegAtom.resize(-lit+1);
      whenReqNegAtom[-lit].insert(w);
    }
}

// litModPosAtom[atom] = lits modified by +atom
vector<set<int> > litModPosAtom;
// litModNegAtom[atom] = lits modified by -atom
vector<set<int> > litModNegAtom;
const set<int>& litModEff( int lit )
{
  if(lit>0)
    {
      if(lit >= litModPosAtom.size() )
	litModPosAtom.resize(lit+1);
      return litModPosAtom[lit];
    }
  else
    {
      if(-lit >= litModNegAtom.size() )
	litModNegAtom.resize(-lit+1);
      return litModNegAtom[-lit];
    }
}
void setLitModEff( int lit, int eff )
{
  if( lit > 0 )
    {
      if(lit >= litModPosAtom.size() )
	litModPosAtom.resize(lit+1);
      litModPosAtom[lit].insert(eff);
    }
  else
    {
      if(-lit >= litModNegAtom.size() )
	litModNegAtom.resize(-lit+1);
      litModNegAtom[-lit].insert(eff);
    }
}

void initAtomsDB( size_t num_atoms )
{
  actionReqPosAtom.resize( num_atoms );
  actionReqNegAtom.resize( num_atoms );
  actionAddAtom.resize( num_atoms );
  actionDelAtom.resize( num_atoms );
  whenAddAtom.resize( num_atoms );
  whenDelAtom.resize( num_atoms );
  whenReqPosAtom.resize( num_atoms );
  whenReqNegAtom.resize( num_atoms );
  litModPosAtom.resize( num_atoms );
  litModNegAtom.resize( num_atoms );
}

void
print_actions()
{
  if( verbose > LEVEL4 )
    {
      cout << "Actions:" << actions.size() << endl;
      cout << "==================================" << endl;
      for( vector<Act>::const_iterator it = ++actions.begin(); 
	   it != actions.end(); it++ )
	cout << *it;
      cout << "==================================" << endl;
    }

  
  if( verbose > LEVEL4 )
    {
      cout << "===========" << endl;
      cout << "Reverse for atoms" << endl;
      for( int i = 1; i < atoms.size(); i++ )
	{
	  cout << " " << atoms[i] 
	       << "(" << i << "): " << endl;
	  
	  {
	    const set<unsigned>& a = actionReqLit( i );
	    cout << "requiered by: ";
	    for( set<unsigned>::const_iterator ai = a.begin(); ai != a.end(); ++ai )
	      cout << *ai << " ";
	    cout << endl;
	  }
	  {
	    const set<unsigned>& a = actionEffLit( i );
	    cout << "modified  by: ";
	    for( set<unsigned>::const_iterator ai = a.begin(); ai != a.end(); ++ai )
	      cout << *ai << " ";
	    cout << endl;
	  }
	  {
	    const set<unsigned>& a = whenEffLit( i );
	    cout << "modi by when: ";
	    for( set<unsigned>::const_iterator ai = a.begin(); ai != a.end(); ++ai )
	      cout << *ai << "(" << whens[*ai]->father << ") ";
	    cout << endl;
	  }
	  {
	    const set<unsigned>& a = whenReqLit( i );
	    cout << "req  by when: ";
	    for( set<unsigned>::const_iterator ai = a.begin(); ai != a.end(); ++ai )
	      cout << *ai << "(" << whens[*ai]->father << ") ";
	    cout << endl;
	  }	
	  cout << endl;
	  cout << "-" << atoms[i] 
	       << "(" << -i << "): " << endl;
	  {
	    const set<unsigned>& a = actionReqLit( -i );
	    cout << "requiered by: ";
	    for( set<unsigned>::const_iterator ai = a.begin(); ai != a.end(); ++ai )
	      cout << *ai << " ";
	    cout << endl;
	  }
	  {
	    const set<unsigned>& a = actionEffLit( -i );
	    cout << "modified  by: ";
	    for( set<unsigned>::const_iterator ai = a.begin(); ai != a.end(); ++ai )
	      cout << *ai << " ";
	    cout << endl;
	  }
	  {
	    const set<unsigned>& a = whenEffLit( -i );
	    cout << "modi by when: ";
	    for( set<unsigned>::const_iterator ai = a.begin(); ai != a.end(); ++ai )
	      cout << *ai << "(" << whens[*ai]->father << ") ";
	    cout << endl;
	  }
	  {
	    const set<unsigned>& a = whenReqLit( -i );
	    cout << "req  by when: ";
	    for( set<unsigned>::const_iterator ai = a.begin(); ai != a.end(); ++ai )
	      cout << *ai << "(" << whens[*ai]->father << ") ";
	    cout << endl;
	  }
	  cout << "-----------" << endl;
	}
      cout << "===========" << endl;
    }
}


set<int> unknown_relevant; // unknown: if simple, required + and -

void *dir_oneof = 0;
//void *dir_disj = 0;

// Simplified version
// works perfect if cond_effects are normalized (conditions not consistent each other)
// and not unconditional effect affects the clause
bool
disjunction_is_static( const set<int>& clause, bool do_xor = false ) 
{
  assert( do_xor == false );
  if( clause.size() == 2 )
    {
      set<int>::iterator it = clause.begin();
      int a = *it++;
      int b = *it++;
      if( a == -b )
	return true;
    }
      
  FOR( set<int>::iterator, Xi, clause )
    {
      if( !actionEffLit(-*Xi).empty() )
	continue;
      set<unsigned> mod = whenEffLit( -*Xi );
      if( false )
	{
	  const set<unsigned>& add = whenEffLit( *Xi );
	  set<unsigned> tmp;
	  set_union( add.begin(), add.end(),
		     mod.begin(), mod.end(),
		     inserter(tmp, tmp.begin()));
	  swap(tmp,mod);
	}
      
      FOR( set<unsigned>::const_iterator, wi, mod )
	{
	  When& w = *whens[*wi];
	  if(!w.used) continue;

	  if(false){
	    cout << "HLP seeing when for static: ";
	    w.dumpPDDL( cout, name_l_old, "", false );
	    w.dump( cout );
	    cout << " for clause: ";
	    t0c::pset(clause); 
	  }
	  bool it_preserve = false;
	  FOR( set<int>::const_iterator, Yi, w.eff )
	    if( *Yi != -*Xi )
	    {
	      bool preserve = false;
	      // -a -> b
	      if( clause.count(*Yi) > 0 )
		{
		  it_preserve = true;
		  break;
		}
	    }	  
	  if(!it_preserve) return false;
	}
    }
  return true;
}

bool
oneof_is_static( const set<int>& oneof )
{
  if( oneof.size() == 2 )
    {
      set<int>::iterator it = oneof.begin();
      int a = *it++;
      int b = *it++;
      if( a == -b )
	return true;
    }

  /* 
     For all Xi,
       for each W deleting Xi
          ok if also: require Xi, add only other Xj, 
  */
  FOR( set<int>::iterator, Xi, oneof )
    {
      if( !actionEffLit(-*Xi).empty() )
	continue;
      set<unsigned> mod = whenEffLit( -*Xi );
      
      FOR( set<unsigned>::const_iterator, wi, mod )
	{
	  When& w = *whens[*wi];
	  if(!w.used) continue;
	  if( w.prec.count(*Xi) == 0 )
	    return false;

	  if(false){
	    cout << "For " << -*Xi << " HLP seeing when for static ONEOF: ";
	    w.dumpPDDL( cout, name_l_old, "", false );
	    w.dump( cout );
	    cout << " for clause: ";
	    t0c::pset(oneof); 
	  }
	  size_t how_many_yi_add = 0;
	  FOR( set<int>::const_iterator, Yi, w.eff )
	    if( *Yi != -*Xi &&
		oneof.count(*Yi) > 0 )
	      how_many_yi_add++;
	    if(how_many_yi_add != 1) return false;
	}
    }


  /* 
     For all Xi,
       for each W ADDING Xi
          ok if also: add only other Xj, and require such Xj
  */
  FOR( set<int>::iterator, Xi, oneof )
    {
      if( !actionEffLit(*Xi).empty() )
	continue;
      set<unsigned> mod = whenEffLit( *Xi );
      
      FOR( set<unsigned>::const_iterator, wi, mod )
	{
	  When& w = *whens[*wi];
	  if(!w.used) continue;

	  if(false){
	    cout << "For " << *Xi << " HLP seeing (case 2) when for static ONEOF: ";
	    w.dumpPDDL( cout, name_l_old, "", false );
	    w.dump( cout );
	    cout << " for clause: ";
	    t0c::pset(oneof); 
	  }
	  size_t how_many_yi_add = 0;
	  FOR( set<int>::const_iterator, Yi, w.eff )
	    if( *Yi != *Xi &&
		oneof.count(-*Yi) > 0 )
	      {
		if( w.prec.count(-*Yi) == 0 )
		  return false;
		how_many_yi_add++;
	      }
	  if(how_many_yi_add != 1) return false;
	}
    }




  return true;
}

void calc_reqs()
{
  whens.resize( 2*whens.size() );
  whens.clear();
  whens.push_back(0);
  for( size_t i = 1; i < actions.size(); i++ )
    {
      Act& a = actions[i];
      
      for( set<int>::iterator ai = a.prec.begin(); ai != a.prec.end(); ++ai )
	{
	  setActionReqLit( a.index, *ai );
	  precs_literals.insert( *ai );
	}
      for( set<int>::iterator ai = a.eff.begin(); ai != a.eff.end(); ++ai )
	setActionEffLit( a.index, *ai );

      for( size_t j = 0; j < actions[i].conds.size(); j++ )
	{
	  When* wp = &actions[i].conds[j];
	  if(!wp->used) continue;

	  // Should be reset because were shifted if some cond-effect
	  // was added to some action
	  wp->index = whens.size(); 
	  whens.push_back( wp );
	  
	  assert( 0 < wp->index && wp->index < whens.size() );
	  for( set<int>::iterator ai = wp->prec.begin(); ai != wp->prec.end(); ++ai )
	    setWhenReqLit( wp->index, *ai );
	  for( set<int>::iterator ai = wp->eff.begin(); ai != wp->eff.end(); ++ai )
	    setWhenEffLit( wp->index, *ai );

	  FOR( set<int>::iterator, pi, wp->prec )
	    FOR( set<int>::iterator, ei, wp->eff )
	      setLitModEff( *pi, *ei );
	}

    }
}

void
prepare_action( Act& a )
{
  t0c_cont::prepare_action(a);
}

void
finishInstanceDB(void)
{
  registerEntry("finishInstanceDB(void)");
  atoms[++natoms] = active_pred;
  active_pred_n = natoms;
  atoms[++natoms] = all_end_pred;
  all_end_pred_n = natoms;
  atoms[++natoms] = cont_dummy_pred;
  cont_dummy_pred_n = natoms;

  initAtomsDB( natoms+1 );

  // Dependencias
  // ----------------------------------------

  size_t nwhens = 0;
  whens.clear();
  // 0 doesn't contain a pointer to when
  whens.push_back(0);

  for( size_t i = 1; i < actions.size(); i++ )
    {
      Act& a = actions[i];
      assert( actions[i].index == i );

      for( set<int>::const_iterator ai = a.prec.begin(); ai != a.prec.end(); ++ai )
	setActionReqLit( a.index, *ai );
      for( set<int>::const_iterator ai = a.eff.begin(); ai != a.eff.end(); ++ai )
	setActionEffLit( a.index, *ai );

      //nwhens += actions[i].conds.size();
      for( size_t j = 0; j < actions[i].conds.size(); j++ )
	{
	  When* wp = &actions[i].conds[j];
	  if(!wp->used) continue;
	  wp->father = i;
	  wp->index = whens.size();
	  whens.push_back( wp );
	  ++nwhens;

	  if( verbose > LEVEL5 )
	    cout << "para action " << a.name << " Registrado " << (void*)whens.back() 
		 << " cond=" << wp
		 << " with index = " << wp->index <<endl;
	  
	  assert( 0 < wp->index && wp->index < whens.size() );
	  for( set<int>::const_iterator ai = wp->prec.begin(); ai != wp->prec.end(); ++ai )
	    setWhenReqLit( wp->index, *ai );
	  for( set<int>::const_iterator ai = wp->eff.begin(); ai != wp->eff.end(); ++ai )
	    setWhenEffLit( wp->index, *ai );

	  FOR( set<int>::iterator, pi, wp->prec )
	    FOR( set<int>::iterator, ei, wp->eff )
	      setLitModEff( *pi, *ei );
	}

      if( verbose > LEVEL4 )
	{
	  cout << "Action (" << i << ")" << endl;
	  actions[i].dump( cout );
	}
    }

  // Unknown relevant (check definition)
  // are unknowns
  // explicit said in disjunctions of Init
  // or requiered positive or negative
  if( true ) // necesary for old version with prime implicates
    {
      for( set<int>::const_iterator e = unknown.begin();
	   e != unknown.end(); e++ )
	{
	  assert( *e > 0 );
	  if( simple_unknown.count(*e) == 0 ||
	      (!whenReqLit(*e).empty() &&
	       !whenReqLit(-*e).empty() ) )
	    unknown_relevant.insert(*e);
	}
      cout << "Unknown relevant = " << unknown_relevant.size() << endl;
    }
  cout << "Unknown = " << unknown.size() << endl;

  set<int> new_static_atoms;
  FOR( set<int>::iterator, s, static_atoms )
    new_static_atoms.insert( r2a[*s] );
  static_atoms = new_static_atoms;
  FOR( vector<set<int> >::const_iterator, it, oneof )
    if( disjunction_is_static(*it, false) )
      {
	if(true)
	  {
	    cout << "HLP static oneof during collectin ";
	    t0c::pset(*it);
	  }
	FOR_P( set<int>::const_iterator, x, it )
	  static_oneof_atoms.insert( *x );
      }
  cout << "Static oneof atoms: ";
  FOR( set<int>::const_iterator, it, static_oneof_atoms )
    cout << *it << " ";
  cout << endl;

  assert( nwhens + 1 == whens.size() );

  if( use_contingent &&
      use_contingent_act_comp ) // Activar para t0c sin contingent: falla uts-k03
    {
      nwhens += t0c_cont::action_comp_mutex();
      calc_reqs();
    }

  assert( nwhens + 1 == whens.size() );
  for( size_t i = 1; i < whens.size(); i++ )
    {
      if( whens[i]->index != i )
	{
	  cout << "Error on index of when[i] != " << whens[i]->index << " with i " << i << endl;
	  whens[i]->dump(cout);
	}
      assert( whens[i]->index == i );
    }
  //print_actions();
  registerExit();
}

void report_static_disj()
{
  FOR( vector<clause>::iterator, c, disj )
    {
      if( disjunction_is_static( *c ) )
	cout << " static ";
      else
	cout << " non-static ";
      t0c::pset( *c );
    }
}

// for problem P'
// name of the atoms 
vector<string> atoms_p;
set<int> goal_atoms_p;
set<int> atoms_p_todel;
set<int> atoms_p_not_todel;

size_t natoms_p = 0;
int k_base = -10000;
int m_base = -10000;
int k0_base = -10000;
int m0_base = -10000;
int k0_max = -1000;
int generate_katoms = false;

// Translation of atoms
int k_abs( int lit )
{
  assert( lit != 0 );
  if( lit > 0 )
    return lit*2;
  else
    return (-lit*2)-1;
}

// Translation of atoms
int k( int lit )
{
  assert( k_base >= 0 );
  return k_base + k_abs(lit);
}

// Translation of atoms
int m( int lit )
{
  assert( m_base >= 0 );
  return m_base + k_abs(lit);
}

int k0( int lit )
{
  assert( k0_base >= 0 );
  if( generate_katoms && static_atoms.count(abs(lit)) > 0 )
    return k(lit);
  else
    return k0_base + k_abs(lit);
}

int m0( int lit )
{
  assert( m0_base >= 0 );
  if( generate_katoms && static_atoms.count(abs(lit)) > 0 )
    return m(lit);
  else
    return m0_base + k_abs(lit);
}

set<int> atoms_observable;
map<int,int> observable_to_O;
bool is_obs( int lit )
{
  return atoms_observable.count(abs(lit)) > 0;
}
int obs( int lit )
{
  assert( is_obs(lit) );
  return observable_to_O[abs(lit)];
}

vector<int (*)( int lit )> assert_lit_func;
void
add_assert_lit( int (*f)( int lit ) )
{
  assert_lit_func.push_back(f);
}

void
assert_lit( int lit, set<int>& eff, bool do_cancel = true, bool do_prop = true, bool do_delete = true )
{
  FOR( vector<int (*)( int lit )>::iterator, fi, assert_lit_func )
    {
      eff.insert( (*(*fi)) (lit ) );
      if( do_delete || *fi != &k)
	eff.insert( - (*(*fi)) (-lit) );
      if( do_prop && *fi == &k )
	t0c::prop_k( lit, eff, do_cancel );
    }
}

void prepare_observables_init(){
  for( size_t i = 1; i < observations.size(); i++ )
    {
      Act& a = observations[i];
      for( std::set<int>::const_iterator ai = a.eff.begin(); ai != a.eff.end(); ++ai )
	atoms_observable.insert(abs(*ai));
    }
}
void prepare_observables_final(){
  // Reserva space in atoms_p for the observables.
  size_t new_index = atoms_p.size();
  string mod_obs = "o_";
  for( std::set<int>::const_iterator ai = atoms_observable.begin(); 
       ai != atoms_observable.end(); ++ai )
    {
      atoms_p.push_back( mod_obs + atoms[*ai] );
      observable_to_O[*ai] = new_index;      
      atoms_p_not_todel.insert(new_index);
      new_index = atoms_p.size();
    }
  natoms_p += atoms_observable.size();
}
// aqui


set<int> atoms_to_keep_name;
vector<string> prefix_to_save;
bool use_short_names = true;
bool use_table_short = false;
// string base_name_l_1 = "abcdefghijklmnopqsrtuvwxyz";
// Not using first letters as a, o, etc, because can be a prefix
// of a keyword like and, or, etc...
string base_name_l_1 = "bcghjklmqrtuvxyz";
string base_name_l_2 = "abcdefghijklmnopqsrtuvwxyz1234567890";
size_t append_one( string& res, string src, size_t val )
{
  size_t i = val % src.size();
  res.append(src.c_str()+i,1);
  return val / src.size();
}
string name_l( int lit )
{
  assert( lit != 0 );
  if( atoms_p[abs(lit)] == "" )
    return "";
  if( use_short_names &&
      atoms_to_keep_name.count(abs(lit)) == 0)
    {
      size_t val = abs(lit);
      string res;
      FOR( vector<string>::iterator, p, prefix_to_save)
	if( !strncmp( p->c_str(), atoms_p[val].c_str(), p->length() ) )
	  {
	    res += *p;
	    break;
	  }

      val = append_one( res, base_name_l_1, val );
      while( val != 0 )
	val = append_one( res, base_name_l_2, val );
      if(lit>0)
	return "(" + res + ")";
      else
	return "(not (" + res + "))";
    }
  else
    {
      if(lit>0)
	return "(" + atoms_p[lit] + ")";
      else
	return "(not (" + atoms_p[-lit] + "))";
    }
}

// Ojo: no responde exactamente "Is k0 lit?"
// pero si se hace exacto, falla
// Parece corresponder a los literales K0, M0, M, K
// pero sin tag.
bool
is_k0_lit( int lit )
{
  //return abs(lit) <= k0_max;//natoms_p;
  return abs(lit) <= natoms_p;
}

size_t old_num_lit_eff;

void
create_actions_p()
{
  // Rehacer con map de Mod a bool (done)
  static bool done;
  if( done )
    return;
  done = true; 

  actions_p.resize( actions.size() );
  for( size_t i = 1; i < actions.size(); i++ )
    {
      Act& a = actions[i];
      Act& a_p = actions_p[i];
      a_p.index = a.index;
      a_p.name = a.name;
    }
}

// Create first than others atoms....
// otherwise natoms_p will be wrongly set
// then first, create k atoms
// ...... not sure... check later.
void
create_copy_atoms( string mod, int &base )
{
  const bool traza_k_0 = false;

  int old_k_base = k_base;
  k_base = atoms_p.size();

  atoms_p.resize(atoms_p.size() + atoms.size()*2-1);
  for( size_t i = 1; i <= natoms; i++ )
    {
      atoms_p[k(-i)] = mod + "n_" + atoms[i];
      atoms_p[k(i)] = mod + "_" + atoms[i];
      if(traza_k_0)
	{
	  cout << k(-i) << " = " <<  atoms_p[k(-i)] << endl;
	  cout << k(i) << " = " <<  atoms_p[k(i)] << endl;
	}
    }
  natoms_p = k(natoms);
  base = k_base;
  k_base = old_k_base;
  if(traza_k_0)
    {
      //cout << "natoms_p = " << natoms_p << endl;
      cout << "new base = " << base << " k_base = " << k_base << endl;
    }
}

// Rehacer con map de Mod a bool (done)
static map<string,bool> k_0_done;

void
make_k_0_prec( string mod, int base )
{
  //assert( k_0_done[mod] );
  int old_kbase = k_base;
  k_base = base;
  for( size_t i = 1; i < actions.size(); i++ )
    {
      Act& a = actions[i];
      Act& a_p = actions_p[i];
      
      for( std::set<int>::const_iterator  ai = a.prec.begin(); ai != a.prec.end(); ++ai )
	{
	  assert( k(*ai) < atoms_p.size() );
	  a_p.prec.insert(k(*ai));
	}
    }      
  k_base = old_kbase;
}

void
make_k_0( string mod, int &base, bool use_cancel = true, 
	  bool trans_prec = true )
{
  if( k_0_done[mod] )
    return;
  k_0_done[mod] = true;

  /*
    same number and name of actions
    duplicate atoms -> Mod p, Mod -p (provide function for mapping)
  */

  string e = "make_k_0(" + mod + ")";
  char *ec = (char*)malloc(e.size()+1);
  strcpy( ec, e.c_str() );
  registerEntry( ec );

  create_copy_atoms( mod, base );
  int old_k_base = k_base;
  k_base = base;
  //cout << "kbase (in make_k_0) = " << k_base <<endl;

  create_actions_p();
  if( trans_prec )
    make_k_0_prec( mod, base );
  old_num_lit_eff = 0;
  for( size_t i = 1; i < actions.size(); i++ )
    {
      Act& a = actions[i];
      Act& a_p = actions_p[i];

      std::set<int>::const_iterator ai;
      std::vector<When>::const_iterator wi;

      for( set<int>::const_iterator ai = a.eff.begin(); ai != a.eff.end(); ++ai )
	assert_lit( *ai, a_p.eff, true, true );
      old_num_lit_eff+= a.eff.size();;

      for( wi = a.conds.begin(); wi != a.conds.end(); ++wi )
	{
	  old_num_lit_eff += wi->eff.size();
	  const When& w = *wi;

	  // Mod C -> Mod L & -Mod -L
	  When w_p1;
	  string keep = mod + "C -> " + mod + "L & -" + mod + "-L     (" + mod + "_0)"; 
	  w_p1.comment = keep;

	  for( set<int>::const_iterator ai = w.prec.begin(); ai != w.prec.end(); ++ai )
	    {
	      assert( k(*ai) < atoms_p.size() );
	      w_p1.prec.insert(k(*ai));   // Mod C_i
	    }
	  for( set<int>::const_iterator ai = w.eff.begin(); ai != w.eff.end(); ++ai )
	    {
	      assert( k(*ai) < atoms_p.size() );
	      assert( k(-*ai) < atoms_p.size() );
	      assert_lit( *ai, w_p1.eff, true, false ); // Mod L_i & -Mod -L_i
	    }
	  a_p.addWhen(w_p1);
	}

      if( use_cancel ) 
	for( wi = a.conds.begin(); wi != a.conds.end(); ++wi )
	  {
	    const When& w = *wi;
	    
	    // -Mod -C -> -Mod -L
	    When w_p2;
	    string cancel = "-" + mod + "-C -> -" + mod + "-L        ("+ mod + "_0)";
	    w_p2.comment = cancel;
	    
	    for( set<int>::const_iterator ai = w.prec.begin(); ai != w.prec.end(); ++ai )
	      w_p2.prec.insert(-k(-*ai)); // -Mod -C_i
	    
	    for( set<int>::const_iterator ai = w.eff.begin(); ai != w.eff.end(); ++ai )
	      {
		w_p2.eff.insert(-k(-*ai)); // -Mod -L_i
		
		t0c::prop_k_cancel( *ai, w_p2.eff );
	      }
	    a_p.addWhen(w_p2);
	  }
    }
  k_base = old_k_base;
  registerExit();
}

void 
check_contradiction( string prefix, int (*f)( int lit ) )
{
  // add fail atom to atoms_p
  t0_fail_pred_n = atoms_p.size();
  atoms_p.push_back( "T0_FAIL" + prefix );
  // goal: not t0_fail_pred_n
  //goal_atoms_p.insert( -t0_fail_pred_n );
  atoms_p_not_todel.insert(t0_fail_pred_n);
  atoms_to_keep_name.insert(t0_fail_pred_n);
  // create closure action
  Act a;
  merge_act::create_one_merge( "check_contradiction", prefix, a, 0 );
  // If fx & f-x -> not_fail
  for( size_t i = 1; i <= natoms; i++ )
    {
      When w;
      w.prec.insert( f(i) );
      w.prec.insert( f(-i) );
      w.eff.insert( t0_fail_pred_n );
      a.addWhen(w);
    }  
  actions_p.push_back(a);
}

vector<set<int> > oneof_ext;
vector<bool> is_dynamic;
set<int> no_oneof;
set<int> in_oneof_both;
map<int, set<int> > x2oneof;
bool oneof_set = false;
set<int> all_unknown;


void
setup_from_oneof()
{
  if( oneof_set )
    return;
  oneof_set = true;

  is_dynamic.resize(oneof.size());
  size_t i = 0;
  FOR( vector<set<int> >::const_iterator, o, oneof)
    {
      bool is = false;
      FOR_P( set<int>::const_iterator, lit, o )
	{
	  if( actionEffLit( *lit ).size() != 0 ||
	      actionEffLit( -*lit ).size() != 0 ||
	      whenEffLit( *lit ).size() != 0 ||
	      whenEffLit( -*lit ).size() != 0 )
	    {
	      is = true;
	      is_dynamic[i] = true;
	      break;
	    }
	}
      if( !is )
	is_dynamic[i] = false;
      i++;
    }
  
  all_unknown = unknown;
  no_oneof = unknown;
  FOR( vector<set<int> >::const_iterator, it, oneof )
    {
      set<int> tmp;
      set_difference( no_oneof.begin(), no_oneof.end(),
		      it->begin(), it->end(), 
		      inserter(tmp, tmp.begin()));
      swap( tmp, no_oneof );
      tmp.clear();
      set_union( all_unknown.begin(), all_unknown.end(),
		      it->begin(), it->end(), 
		      inserter(tmp, tmp.begin()));
      swap( tmp, all_unknown );
    }
  cout << "Unknown atoms: ";
  FOR( set<int>::const_iterator, it, all_unknown )
    cout << *it << " ";
  cout << endl;

  cout << "Unknown not in oneof: ";
  FOR( set<int>::const_iterator, it, no_oneof )
    cout << *it << " ";
  cout << endl;

  for( set<int>::const_iterator it = no_oneof.begin();
       it != no_oneof.end(); it++ )
    {
      oneof.push_back(set<int>());
      oneof.back().insert( *it );
      oneof.back().insert( -*it );
    }
  dir_oneof = oneof.empty()?0:(void*) &oneof[0];

  size_t index_oneof = 0;
  FOR( vector<set<int> >::const_iterator, it, oneof )
    {
      FOR_P( set<int>::const_iterator, e, it )
	// OJO: quizas deba ser esto if( true || *e > 0 )
	if( *e > 0 )
	  // because used by KP, all positive explicit unknown
	  {
	    in_oneof_both.insert( *e );
	    x2oneof[*e].insert(index_oneof);
	  }
      index_oneof++;
    }
  if(false)
    {
      cout << "In oneof both: ";
      FOR( set<int>::const_iterator, it, in_oneof_both )
	cout << *it << " ";
      cout << endl;
    }
}


// Unknown atoms not appearing in oneof
// or static binary disjunction
void
make_k_0_plus()
{
  return; // OJO AQUI ¿Deshabilitado?
  // OJO AQUI ¿Deshabilitado?
  registerEntry( "make_k_0_plus()" );
  make_k_0("k", k_base);
  setup_from_oneof();

  vector<pair<int, int> > binary_disj;
//   for( set<int>::const_iterator it = no_oneof.begin();
//        it != no_oneof.end(); it++ )
  for( set<int>::const_iterator it = all_unknown.begin();
       it != all_unknown.end(); it++ )
    {
      binary_disj.push_back(pair<int,int>(*it, -*it));
      binary_disj.push_back(pair<int,int>(-*it, *it));
    }

  if( verbose > LEVEL1 )
    cout << "binary disjunctions " << binary_disj.size() << endl;
  // For each binary disjunction (some are just positive, negative)
  for( vector<pair<int, int> >::const_iterator bin = binary_disj.begin();
       bin != binary_disj.end(); bin++)
    {
      int pos = bin->first;
      int neg = bin->second;

      if( verbose > LEVEL1 )
	cout << "Considering pair: " << pos << ", " << neg << endl;

      const set<unsigned>& wmod = whenEffLit( neg );
      const set<unsigned>& wreq = whenReqLit( pos );
      set<unsigned> conds;
      set_intersection( wmod.begin(), wmod.end(),
			wreq.begin(), wreq.end(), 
			inserter(conds, conds.begin()));

      // conds = whens: C & X -> -X & Y....

      for( set<unsigned>::const_iterator cond = conds.begin();
	   cond != conds.end(); cond++ )
	{
	  When& w = *whens[*cond];
	  if(!w.used) continue;
	  // Action with w as when
	  Act& a = actions[w.father];

	  if( verbose > LEVEL1 )
	    cout << "Transforming when: " << w;

	  bool do_continue = false;
	  vector<int> conds_adding;
	  for( vector<When>::const_iterator wi = a.conds.begin();
	       wi != a.conds.end(); wi++ )
	    if( wi->eff.count( pos ) > 0 )
	      {
		// Not the same cond 
		// OJO: Not clear... is it a rule like this?
		// C & X -> -X & X & ....
		// and we then refuse to process when w?
		if( wi->index == *cond )
		  {
		    do_continue = true;
		    break;
		  }
		//assert( wi->index != *cond );
		// should deleting only modify X??
		conds_adding.push_back( wi->index );
		if( verbose > LEVEL2 )
		  cout << "This when adds the atom to eliminate " << pos << ": " 
		       << *whens[*cond] << endl;
	      }
	  if(do_continue) continue;

	  set<set<int> > combinaciones;
	  // Generando combinaciones de las precondiciones
	  if( conds_adding.size() > 0 )
	    {
	      set<set<int> > tmp;
	      vector<int>::const_iterator add = conds_adding.begin(); 
	      When& w_add1 = *whens[*add];
	      if(!w_add1.used) continue;

	      for( set<int>::const_iterator pi = w_add1.prec.begin();
		   pi != w_add1.prec.end(); pi++ )
		{
		  set<int> c;
		  c.insert( *pi );
		  combinaciones.insert(c);
		}
	      add++;
	      for( ;add != conds_adding.end(); ++add)
		{
		  tmp.clear();
		  When& w_add = *whens[*add];
		  if(!w_add.used) continue;
		  FOR( set<int>::const_iterator, pi, w_add.prec )
		    FOR( set<set<int> >::const_iterator, combi, combinaciones )
		    {
		      set<int> s(*combi);
		      s.insert( *pi );
		      tmp.insert(s);
		    }
		  swap( tmp, combinaciones );
		}
	    }
	  

	  Act& a_p = actions_p[a.index];
	  if( combinaciones.size() == 0 )
	    {
	      When w_p;
	      w_p.comment = "KC -> K-x      (K^+_0:  deleting X from C)";
	      
	      for( set<int>::const_iterator pi = w.prec.begin();
		   pi != w.prec.end(); pi++ )
		if( *pi != pos )
		  w_p.prec.insert(k(*pi)); // KC
	      assert_lit( neg, w_p.eff, true );
	      a_p.addWhen(w_p);
	    }
	  else
	    {
	      size_t c=0;
	      FOR( set<set<int> >::const_iterator, comb, combinaciones)
		{
		  When w_p;
		  ostringstream str_l;
		  str_l << c;
		  w_p.comment = "KC -> K-x      (K^+_0:  deleting X from C: comb #" + str_l.str() +")"; 
		  for( set<int>::const_iterator pi = w.prec.begin();
		       pi != w.prec.end(); pi++ )
		    if( *pi != pos )
		      w_p.prec.insert(k(*pi)); // KC
		  
		  for( set<int>::const_iterator ci = comb->begin();
		       ci != comb->end(); ci++ )
		    w_p.prec.insert(k(-*ci)); // KC
		  
		  assert_lit( neg, w_p.eff, true );
		  a_p.addWhen(w_p);

		  c++;
		}
	      if( false && c > 1 )
		{
		  cerr << "Warning agregando mas de una combinacion en action compilation."
		       << " Verificar el codigo. " << endl;
		  cout << "Warning agregando mas de una combinacion en action compilation."
		       << " Verificar el codigo. " << endl;
		}
	    }
	}
    }
  registerExit();
}


/*******************************************************************************
 **
 **   transformation using L//xi, L true if xi was true at t=0
 **
 ******************************************************************************/
namespace lxi_t0 {
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;
  if( labs[l].count(xis) != 1 ) // this option was considered
    {
      cout << "Error: " << l << "/" << set2str(xis) 
	   << " wasnt considered" << 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 );
    }
}

map<int,int> flags;

int
make_flag( int l )
{
  map<int,int>::iterator it = flags.find(l);
  if( it == flags.end() )
    {
      string n_flag = "flag_";
      if( l < 0 )
	n_flag.append("n_");
      n_flag += atoms[abs(l)];
      atoms_p.push_back(n_flag);
      int flag = atoms_p.size()-1;
      flags[l] = flag;
      return flag;
    }
  else
    return it->second;
}



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

  set<int> merge_protected;
  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;
		    }
		}
	      
	      if( add )
		{
		  w_p.prec.insert( make_flag( l ) );
		  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 );
		    }

		  //si existe action with eff: -L
		  if( merge_protected.count(l) == 0 )
		    {
		      merge_protected.insert(l);
		      const set<unsigned>& del_nl = actionEffLit( -l );
		      FOR( set<unsigned>::const_iterator, ai, del_nl )
			{
			  Act& a = actions_p[*ai];
			  // agregar effect -Flag(L)
			  a.eff.insert( -make_flag(l) ); // -flag(l)
			}
		    }
		}
	      a_p.addWhen(w_p);
	    }
	}
    }

  registerExit();
}

}
/*******************************************************************************
 **
 **   Make pure merges for each initial oneof
 **
 ******************************************************************************/

namespace merge_act {

vector<int> flags;
bool allow_flag = false;
int
make_flag( size_t index )
{
  string n_flag = "flagp_";
  ostringstream str_l;
  str_l << index;
  n_flag += str_l.str();
  atoms_p.push_back(n_flag);
  int flag = atoms_p.size()-1;
  flags.push_back(flag);
  return flag;
}

void
create_one_merge( string prefix, string sufix, Act& a_p, size_t oi, int extra_prec )
{
  a_p.clear();
  a_p.index = actions_p.size();
  
  string name = prefix;
  if(use_contingent)
    name = "closure_" + name;
  ostringstream str_l;
  str_l << oi;
  name += "_" + str_l.str();
  name = name + sufix;
  a_p.name = string(name);
  if (use_no_cost_closures)
    a_p.cost = 0.0;
  else
    a_p.cost = CLOSURE_COST;
  if( extra_prec )
    a_p.prec.insert( extra_prec );

  if( verbose > LEVEL1 )
    {
      cout << "Haciendo " << name << endl;
    }
}

void
make_merge_act( string sufix, int (*f)( int lit ), bool allow_flag = false, bool asume_static = false,
		bool ramif = true, bool use_activate = false, bool use_oneof = true )
{
  const string prefix = "mergep_";
  const bool debugit = false;
  //make_k_0("k", k_base);
  setup_from_oneof();

  registerEntry( "make_merge_act()" );

  int active = 0;
  if( use_contingent_active_pred_disj && use_activate)
    active = k(active_pred_n);

  size_t oi = 0;

  vector<set<int> >* d = 0; 
  if( true || use_contingent )
    {
      d = &disj;
      if( verbose > LEVEL0 )
	cout << "Using oneof as XOR for conclude by unit propagation" << endl;
    }
  else
    {
      d = &oneof;
      if( verbose > LEVEL0 )
	cout << "Using oneof as OR for conclude by unit propagation" << endl;
    }

  Act a_p;
  // In principle, because many actions with same conditions 
  // can be generated by using disj instead of oneof,
  // compact the actions can be relevant...
  // It can have a undesired effect in t0 theories,
  // having hundred of cond-effects. Not sure about it...
  const bool only_one_action = true;
//   const bool only_one_action = use_contingent;
  if( only_one_action )
    create_one_merge( prefix, sufix, a_p, oi, active );
  FOR( vector<set<int> >::iterator, op, (*d) )
    {
      set<int>& o = *op;
      if( debugit )
	{
	  cout << "Merge_act_comp considering ";
	  t0c::pset(o);
	}
      const bool is_static = disjunction_is_static( o, false ) || asume_static;
      //       const bool is_static = disjunction_is_static( o, true ) || asume_static;
      if( !allow_flag && !is_static ) continue;
      if( !only_one_action )
	create_one_merge( prefix, sufix, a_p, oi, active );
      vector<When> a_p_whens;

      if( is_static )
	{
	  if( debugit )
	    cout << "\tis static..." << endl;
	  FOR( set<int>::iterator, Xi, o )
	    {
	      {
		When w_p;
		w_p.comment = "K-x1 & .. & K-xn -> K xi & -K-xi  (merge static disjunction)";
		FOR( set<int>::const_iterator, Xj, o )
		  if( *Xi != *Xj ) // if l is a xi, it is not necessary
		    w_p.prec.insert( f(-*Xj) );

		if( ramif )
		  assert_lit( *Xi, w_p.eff, false, true, false );
		else
		  w_p.eff.insert( f(*Xi) );
	    
		// useless rule
		if( w_p.prec.size() == 1 && w_p.eff.count( *w_p.prec.begin() ) > 0 )
		  continue;

		a_p_whens.push_back(w_p);

		if( verbose > LEVEL2 )
		  {
		    cout << "Agregando When: " << endl;
		    string s = "   ";
		    w_p.dumpPDDL( cout, &name_l, s );
		  }
	      }
	      if( false && ( *Xi > 0 && o.count(-*Xi) > 0 ) &&
		  ( *Xi < 0 && o.count(*Xi) > 0 ) )
		{
		  When w_p;
		  w_p.comment = "K x1 -> K-x2 & .. & K-xn  (merge static disjunction)";
		  w_p.prec.insert( f(*Xi) );
		  FOR( set<int>::const_iterator, Xj, o )
		    if( *Xi != *Xj ) // if l is a xi, it is not necessary
		      {
			if( ramif )
			  assert_lit( -*Xj, w_p.eff, false, true, false );
			else
			  w_p.eff.insert( f(-*Xj) );
		      }
	    
		  // useless rule
		  if( w_p.prec.size() == 1 && w_p.eff.count( *w_p.prec.begin() ) > 0 )
		    continue;

		  a_p_whens.push_back(w_p);

		  if( verbose > LEVEL2 )
		    {
		      cout << "Agregando When: " << endl;
		      string s = "   ";
		      w_p.dumpPDDL( cout, &name_l, s );
		    }
		}
	    }
	}
      else
	{
	  if( debugit )
	    cout << "\tisn't static..." << endl;
	  int flagp = make_flag(oi);
	  vector<When> a_p_whens;
	  FOR( set<int>::iterator, Xi, o )
	    {
	      When w_p;
	      w_p.comment = "K-x1&K-y1 & .. & K-xn&K-yn & {flagp(x)}? -> K xi & -K-xi  (merge disjunction)";
	      FOR( set<int>::const_iterator, Xj, o )
		if( *Xi != *Xj ) // if l is a xi, it is not necessary
		  w_p.prec.insert( f(-*Xj) );
	      w_p.prec.insert( flagp ); 

	      if( ramif )
		assert_lit( *Xi, w_p.eff, false, true, false );
	      else
		w_p.eff.insert( f(*Xi) );
	    
	      // useless rule
	      if( w_p.prec.size() == 1 && w_p.eff.count( *w_p.prec.begin() ) > 0 )
		continue;

	      a_p_whens.push_back(w_p);

	      if( verbose > LEVEL2 )
		{
		  cout << "Agregando When: " << endl;
		  string s = "   ";
		  w_p.dumpPDDL( cout, &name_l, s );
		}

	      // protecting flagp
	      const set<unsigned>& del = whenEffLit( -*Xi );
	      FOR( set<unsigned>::const_iterator, wi, del )
		{
		  When& w = *whens[*wi];
		  bool add = true;
		  FOR( set<int>::const_iterator, Xj, w.eff )
		    {
		      if( o.count( *Xj ) > 0 )
			{
			  assert( *Xj != *Xi );
			  add = false;
			  break;
			}		  
		    }
		  if(!add) continue;
		  Act& a_p = actions_p[w.father];
		  When w_p;
		  w_p.comment = "-K-C -> -Flagp    ( protect flag of merge pure act compilation )";
		  FOR( set<int>::const_iterator, c, w.prec )
		    w_p.prec.insert(-f(-*c)); // -K-C
		  w_p.eff.insert( -flagp ); // -flagp
		  a_p.addWhen(w_p);
		}
	    }
	}
      // Add them to the action
      FOR( vector<When>::iterator, it, a_p_whens )
	a_p.addWhen(*it);
      
      // Action should be added, if contains some effect
      if( !only_one_action &&
	  a_p.conds.size() > 0 )	  
	actions_p.push_back(a_p);
      
      oi++;
    }
  
  // Now for oneof
  if(use_oneof)
  FOR( vector<set<int> >::iterator, op, oneof )
    {
      set<int>& o = *op;
      if( debugit )
	{
	  cout << "Merge_act_comp considering ONEOF ";
	  t0c::pset(o);
	}
      const bool is_static = oneof_is_static( o );
      if( !is_static ) continue;
      if( !only_one_action )
	create_one_merge( prefix, sufix, a_p, oi, active );
      vector<When> a_p_whens2;

      if( debugit )
	cout << "\tis static..." << endl;
      FOR( set<int>::iterator, Xi, o )
	{
	  {
	    When w_p;
	    w_p.comment = "K-x1 & .. & K-xn -> K xi & -K-xi  (merge static oneof)";
	    FOR( set<int>::const_iterator, Xj, o )
	      if( *Xi != *Xj ) // if l is a xi, it is not necessary
		w_p.prec.insert( f(-*Xj) );

	    if( ramif )
	      assert_lit( *Xi, w_p.eff, false, true, false );
	    else
	      w_p.eff.insert( f(*Xi) );
	    
	    // useless rule
	    if( w_p.prec.size() == 1 && w_p.eff.count( *w_p.prec.begin() ) > 0 )
	      continue;

	    if( verbose > LEVEL2 )
	      {
		cout << "Agregando When: " << endl;
		string s = "   ";
		w_p.dumpPDDL( cout, &name_l, s );
	      }
	    a_p_whens2.push_back(w_p);

	  }
	  {
	    When w_p2;
	    w_p2.comment = "K x1 -> K-x2 & .. & K-xn  (merge static oneof)";
	    w_p2.prec.insert( f(*Xi) );
	    FOR( set<int>::const_iterator, Xj, o )
	      if( *Xi != *Xj ) // if l is a xi, it is not necessary
		{
		  if( ramif )
		    assert_lit( -*Xj, w_p2.eff, false, true, false );
		  else
		    w_p2.eff.insert( f(-*Xj) );
		}
	    
	    // useless rule
	    if( w_p2.prec.size() == 1 && w_p2.eff.count( *w_p2.prec.begin() ) > 0 )
	      continue;
	    
	    a_p_whens2.push_back(w_p2);
	    
	    if( verbose > LEVEL2 )
	      {
		cout << "Agregando When: " << endl;
		string s = "   ";
		w_p2.dumpPDDL( cout, &name_l, s );
	      }
	  }
	}
      // Add them to the action
      FOR( vector<When>::iterator, it, a_p_whens2 )
	{
	  // ojo: borrar
	  if(false)
	    {
	      cout << "Agregando finalmente When: " << endl;
	      string s = "   ";
	      it->dumpPDDL( cout, &name_l, s );
	    }
	  a_p.addWhen(*it);
	}
      
      // Action should be added, if contains some effect
      if( !only_one_action &&
	  a_p.conds.size() > 0 )	  
	actions_p.push_back(a_p);
      
      oi++;
    }

  if( only_one_action &&
      a_p.conds.size() > 0)
    actions_p.push_back(a_p);
  registerExit();
}

}

/*******************************************************************************
 **
 **   transformation using L/xi, L true if xi is true.
 **
 ******************************************************************************/

namespace lxi {

bool check = false;

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

map<label_t,int> labels;
map<flag_t,int> flags;

bool 
there_is_labeled( int l, const set<int>& xis ) 
{
  return( labels.find( make_pair(l,xis) ) != labels.end() );
}

int
labeled( int l, const set<int>& xis ) 
{
  label_t lab( l, xis );
  assert( labels.find( make_pair(l,xis) ) != labels.end() );
  return labels[lab];
}

// Every atom l/xs exists
bool 
is_labelable_static( int l, const set<int>& xs ) 
{
  set<set<int> > xss;
  FOR( set<int>::iterator, x, xs )
    xss.insert( oneof[*x] );
  set<set<int> > comb_xis = cartesian(xss);

  FOR( set<set<int> >::const_iterator, xis, comb_xis )
    if(!there_is_labeled(l, *xis) )
      return false;
  return true;
}

void 
make_flag( int l, const set<int>& xs )
{
  flag_t f(l, xs);
  if( flags.find(f) != flags.end() ) return;
  string n_flag = "flag_";
  if( l < 0 )
    n_flag.append("n_");
  n_flag += atoms[abs(l)];
  FOR( set<int>::iterator, xsi, xs )
    {
      ostringstream str_l;
      str_l << *xsi;
      n_flag += "__" + str_l.str();
    }
  atoms_p.push_back(n_flag);
  flags[f] = atoms_p.size()-1;
}

int
flag( int l, const set<int>& xs )
{
  flag_t f(l, xs);
  assert( flags.find(f) != flags.end() );
  return flags[f];
}

void make_label( Act& a, int l, const set<int>& xis )
{
  label_t lab(l, xis);
  if( labels.find( lab ) == labels.end() ) 
    {
      string name_lxi;
      if( l < 0 )
	name_lxi.append("n_");
      name_lxi.append(atoms[abs(l)]);
      name_lxi += "__";
      FOR( set<int>::iterator, xi, xis )
	{
	  name_lxi += "_";
	  if( *xi < 0 )
	    name_lxi += "-";
	  name_lxi += atoms[abs(*xi)];
	}
      atoms_p.push_back(name_lxi);
      int nlabel = atoms_p.size()-1;
      labels[lab] = nlabel;
      assert( there_is_labeled( l, xis ) );
      assert( labeled( l, xis ) == nlabel );

      // We must merge for every oneof having an xi
      set<set<int> > xss;
      FOR( set<int>::iterator, xi, xis )
	{
	  //assert( *xi > 0 );
	  xss.insert( x2oneof[*xi] );
	}
      set<set<int> > combs = cartesian(xss);
      FOR( set<set<int> >::const_iterator, combi, combs )
	make_flag( l, *combi );
    }
}



// Split atoms
void
make_split_dynamic( set<int>& in_oneof1, string rule )
{
  //etiquetables.clear();
  // Para cada when W:
  FOR_1( wi, whens )
    {
      When& w = *whens[wi];

      //Si exite un solo unknown-oneof Xi \in cond(w)
      set<int> xis;
      FOR( set<int>::const_iterator, c, w.prec )
	if( in_oneof1.count( *c ) > 0 ) // in_oneof son todos positivos
	  xis.insert(*c);
      if( xis.size() == 0 ) continue;
      if( xis.size() > 1 )
	{
	  cerr << "Warning: labeling the following When" << endl
	       << "that have more than one unknown option" << endl;
	  cerr << w << endl;
	}
     
      Act& a_p = actions_p[w.father];
      // Para cada L \in eff(w)
      Act & a = actions[w.father];
      FOR( set<int>::const_iterator, l, w.eff )
	{

	  if( check )
	    cerr << "-----------------" << endl;
	  make_label( a, *l, xis );
	
	  set<set<int> > tmp;
	  FOR( vector<When>::const_iterator, wi, a.conds )
	    FOR( set<int>::const_iterator, xi, xis )
	    if( wi->eff.count(*xi) ) 
	      {
		tmp.insert( wi->prec );
		break;
	      }
	  // tmp = preconds of rules adding X_i
	  set<set<int> > comb_nlits = cartesian(tmp);

	  size_t count = 0;
	  if( comb_nlits.empty() )
	    {
	      When w_p;
	      w_p.comment = "KC -> L/xi          split-> " + rule;
	      FOR( set<int>::const_iterator, c, w.prec )
		if( xis.count(*c) == 0 )
		  w_p.prec.insert(k(*c)); // KC
	      // Agregar KC -> L/xi 
	      w_p.eff.insert( labeled( *l, xis ));
	      a_p.addWhen(w_p);
	      count++;
	    }
	  else		
	    FOR( set<set<int> >::const_iterator, combit, comb_nlits )
	    {
	      const set<int>& nlits = *combit;
	      When w_p;
	      ostringstream str_l;
	      str_l << count;
	      w_p.comment = "KC & K-Lj... -> L/xi          split: comb#" + str_l.str() + " " + rule;
	      FOR( set<int>::const_iterator, c, w.prec )
		if( xis.count(*c) == 0 )
		  w_p.prec.insert(k(*c)); // KC
	      FOR( set<int>::const_iterator, li, nlits )
		w_p.prec.insert(k(-*li)); // K-Li
	      // Agregar KC -> L/xi 
	      w_p.eff.insert( labeled( *l, xis ));
	      
	      a_p.addWhen(w_p);
	      count++;
	    }
	  if( count > 1 )
	    {
	      cerr << "Warning agregando mas de una combinacion en splitting."
		   << " Verificar el codigo. " << endl;
	      cout << "Warning agregando mas de una combinacion en splitting."
		   << " Verificar el codigo. " << endl;
	    }
	  if( check )
	    cerr << "END -----------------" << endl;

	}
    }
}

void
make_k_1_dynamic()
{
  /*
    Provide way to add atoms: L/Xi, Flags. Function with cache??
  */
  make_k_0("k", k_base);
  setup_from_oneof();

  registerEntry( "make_k_1_dynamic()" );

  make_split_dynamic( in_oneof_both, "(K_1 dynamic)" );
  
  // Comienza diferencia del K_1 dynamic

  //para cada etiquetable(L,X) generar merge
  for( map<flag_t,int>::iterator it = flags.begin();
       it != flags.end(); it++ )
    {
      const set<int>& xs = it->first.second;
      const int l = it->first.first;
      
      actions_p.push_back(Act());
      Act& a_p = actions_p.back();
      a_p.ground = 0;
      a_p.index = actions_p.size()-1;

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

      if( verbose > LEVEL1 )
	{
	  cout << "Haciendo merge de etiquetas de atomo " << name_l_old(l)  
	       << ". Action: " << name << endl;
	}
      

      set<set<int> > xss;
      FOR( set<int>::iterator, x, xs )
	xss.insert( oneof[*x] );
      set<set<int> > comb_xis = cartesian(xss);

      // Ideal: "(l/x1y1 | (K-x1 & K-y1 )) & .. & (l/xnyn | (K-xn & K-yn)) & flag(l,xy) -> K l    (K_1 static)";
      // but generating some cases

      // l/x1y1 & .. & l/xnyn & flag(l,xy) -> K l
      if( is_labelable_static( l, xs ) )
	{
	  When w_p;
	  w_p.comment = "l/x1y1 & .. & l/xnyn & flag(l,xy) -> K l & -K-l   (K_1 dynamic)";

	  FOR( set<set<int> >::iterator, xis, comb_xis )
	    if( !(xis->size() == 1 && xis->count(l) == 1) ) // if l is a xi, it is not necessary
	      w_p.prec.insert( labeled( l, *xis ) );
	  w_p.prec.insert( flag(l,xs) ); // If all the X's are static, flag not necessary
	  w_p.eff.insert( k(l) );
	  w_p.eff.insert( -k(-l) );
	  a_p.addWhen(w_p);
	  if( verbose > LEVEL2 )
	    {
	      cout << "Agregando When: " << endl;
	      string s = "   ";
	      w_p.dumpPDDL( cout, &name_l, s );
	    }
	}
      // K-x1&K-y1 & .. & K-xn&K-yn & flag(l,xy) -> K l  
      {
	When w_p;
	w_p.comment = "K-x1&K-y1 & .. & K-xn&K-yn & flag(l,xy) -> K l & -K-l  (K_1 dynamic)";
	FOR( set<int>::iterator, x, xs )
	  FOR( set<int>::const_iterator, xi, oneof[*x] )
	  if( l != *xi ) // if l is a xi, it is not necessary
	    w_p.prec.insert( k(-*xi) );
	w_p.prec.insert( flag(l,xs) ); 
	w_p.eff.insert( k(l) );
	w_p.eff.insert( -k(-l) );
	a_p.addWhen(w_p);

	if( verbose > LEVEL2 )
	  {
	    cout << "Agregando When: " << endl;
	    string s = "   ";
	    w_p.dumpPDDL( cout, &name_l, s );
	  }
      }

      // K-x1 & .. l/xiyj .. & K-xn & flag(l,xy) -> K l
      FOR( set<set<int> >::iterator, xis, comb_xis )
      {
	if( xis->size() == 1 && xis->count(l) == 1 ) continue;
	if( !there_is_labeled( l, *xis ) ) continue;
	When w_p;
	w_p.prec.insert( labeled( l, *xis ) );
	w_p.comment = "K-x1&K-y1 & .. l/xiyj .. & K-xn&K-yn & flag(l,xy) -> K l & -K-l  (K_1 dynamic)";
	FOR( set<int>::iterator, x, xs )
	  FOR( set<int>::const_iterator, xi, oneof[*x] )
	  if( l != *xi && xis->count(*xi) != 1) // if l is a xi, it is not necessary
	    w_p.prec.insert( k(-*xi) );
	w_p.prec.insert( flag(l,xs) );
	w_p.eff.insert( k(l) );
	w_p.eff.insert( -k(-l) );
	a_p.addWhen(w_p);
	if( verbose > LEVEL2 )
	  {
	    cout << "Agregando When: " << endl;
	    string s = "   ";
	    w_p.dumpPDDL( cout, &name_l, s );
	  }
      }

      // This case doesn't seem to be useful
      // Maybe relaxing it by allowing to put it 
      // l/x1y1 & .. K-xi&K-xj .. & l/xnyn & flag(l,xy) -> K l
      FOR( set<set<int> >::iterator, xis, comb_xis )
      {
	if( xis->size() == 1 && xis->count(l) == 1 ) continue;
	bool all = true;
	When w_p;
	w_p.comment = "l/x1y1 & .. K-xi K-yj .. & l/xnyn & flag(l,xy) -> K l & -K-l  (K_1 dynamic)";
	FOR( set<set<int> >::iterator, xjs, comb_xis )
	  if( xjs->count(l) != 1 && *xis != *xjs ) // if l is a xi, it is not necessary
	    {
	      if( there_is_labeled( l, *xjs ) )
		w_p.prec.insert( labeled(l,*xjs ) );
	      else
		{
		  all = false;
		  break;
		}
	    }

	if( all )
	  {
	    FOR_P( set<int>::const_iterator, xi, xis )
	      w_p.prec.insert( k(-*xi) );
	    w_p.prec.insert( flag(l,xs) );
	    w_p.eff.insert( k(l) );
	    w_p.eff.insert( -k(-l) );
	    a_p.addWhen(w_p);
	    if( verbose > LEVEL2 )
	      {
		cout << "Agregando When: " << endl;
		string s = "   ";
		w_p.dumpPDDL( cout, &name_l, s );
	      }
	  }
      }
      

      //si existe when w: C -> -L
      const set<unsigned>& mod_nl = whenEffLit( -l );
      FOR( set<unsigned>::const_iterator, wi, mod_nl )
	{
	  When& w = *whens[*wi];

	  // agregar: -K-C -> -Flag(L)
	  Act& a_p = actions_p[w.father];
	  When w_p;
	  w_p.comment = "-K-C -> -Flag(L,xy)    (K_1 dynamic / protect rule (a))";
	  FOR( set<int>::const_iterator, c, w.prec )
	    w_p.prec.insert(-k(-*c)); // -K-C
	  w_p.eff.insert( -flag(l,xs) ); // -flag(l,xy)
	  a_p.addWhen(w_p);
	}
      // Si hubiera varios efectos etiquetados en a_p
      // podrian etiquetarse todos de una vez      

      //si existe action with eff: -L
      const set<unsigned>& del_nl = actionEffLit( -l );
      FOR( set<unsigned>::const_iterator, ai, del_nl )
	{
	  Act& a = actions_p[*ai];
	  // agregar effect -Flag(L)
	  a.eff.insert( -flag(l,xs) ); // -flag(l,xy)
	}


      FOR( set<int>::iterator, x, xs )
	FOR( set<int>::const_iterator, xi, oneof[*x] )
	{
	  const set<unsigned>& del = whenEffLit( -*xi );
	  FOR( set<unsigned>::const_iterator, wi, del )
	    {
	      When& w = *whens[*wi];
	      if( w.eff.count( l ) > 0 )
		continue;
	      bool add = true;
	      FOR( set<int>::const_iterator, Xk, w.eff )
		{
		  if( oneof[*x].count( *Xk ) > 0 )
		    {
		      //assert( *Xk != *xi );
		      add = false;
		      break;
		    }		  
		}
	      if(!add) continue;
	      Act& a_p = actions_p[w.father];
	      When w_p;
	      w_p.comment = "-K-C -> -Flag(L,xy)    (K_1 dynamic / protect rule (b))";
	      FOR( set<int>::const_iterator, c, w.prec )
		w_p.prec.insert(-k(-*c)); // -K-C
	      w_p.eff.insert( -flag(l,xs) ); // -flag(x,l)
	      a_p.addWhen(w_p);
	      
	    }
	}

      FOR( set<set<int> >::iterator, xks, comb_xis )
	{
	  if( !there_is_labeled( l, *xks ) ) continue;
	  FOR_P( set<int>::const_iterator, xk, xks )
	    {
	      const set<unsigned>& add = whenEffLit( *xk );
	      FOR( set<unsigned>::const_iterator, wi, add )
		{
		  When& w = *whens[*wi];
		  Act& a_p = actions_p[w.father];
		  When w_p;
		  w_p.comment = "-K-C & -Kxi & L/xkxi -> -Flag(L,xy)    (K_1 dynamic / protect rule (c))";
		  FOR( set<int>::const_iterator, c, w.prec )
		    w_p.prec.insert(-k(-*c)); // -K-C
		  FOR_P( set<int>::const_iterator, xi, xks )
		    if( *xi != *xk )
		      w_p.prec.insert(-k(-*xi)); // -K-xi
		  w_p.prec.insert( labeled( l, *xks ) ); // l / xi xk
		  w_p.eff.insert( -flag(l,xs) ); // -flag(x,l)
		  a_p.addWhen(w_p);
		}
	    }
	}
    }
  registerExit();
}
}

/*******************************************************************************
 **
 **   Other modules
 **
 ******************************************************************************/

#include "t0c.cc"
#include "t0c_cont.cc"
#include "lxi_dnf.cc"

/*******************************************************************************
 **
 **   post processing and printing new PDDL
 **
 ******************************************************************************/

void
collect_aux(vector<Act>& acts)
{
  for( size_t i = 1; i < acts.size(); i++ )
    {
      const Act& a = acts[i];
      FOR( set<int>::const_iterator, p, a.prec )
	all_mentioned.insert(abs(*p));
      FOR( set<int>::const_iterator, e, a.eff )
	all_mentioned.insert(abs(*e));
      FOR( vector<When>::const_iterator, wi, a.conds )
	{
	  FOR( set<int>::const_iterator, c, wi->prec )
	    all_mentioned.insert(abs(*c));
	  FOR( set<int>::const_iterator, e, wi->eff )
	    all_mentioned.insert(abs(*e));
	}
    }
}
void
collect_mentioned()
{
  return; 
  collect_aux(observations_p);
  collect_aux(actions_p);

  FOR( set<int>::iterator, l, goal_literals )
    all_mentioned.insert(abs(*l));
  FOR( set<int>::iterator, l, t0c::init_atoms )
    all_mentioned.insert(abs(*l));

  all_mentioned.insert(k(dummy_pred_n));
  all_mentioned.insert(k(-dummy_pred_n));
  all_mentioned.insert(k(active_pred_n));
  all_mentioned.insert(k(-active_pred_n));
  all_mentioned.insert(k(all_end_pred_n));
  all_mentioned.insert(k(-all_end_pred_n));
  all_mentioned.insert(k(cont_dummy_pred_n));
  all_mentioned.insert(k(-cont_dummy_pred_n));

  if(false)
    {
      cout << "ALL MENTIONED: "; 
      FOR( set<int>::iterator, a, all_mentioned )
	cout << atoms_p[*a] << " ";
      cout << endl;
    }
}


void
del_neg_effects()
{
  registerEntry( "del_neg_effects()" );
  for( size_t i = 1; i < actions_p.size(); i++ )
    {
      Act& a = actions_p[i];
      set<int> del;
      FOR( set<int>::const_iterator, ei, a.eff )
	if( *ei < 0 )
	  del.insert(*ei);
      FOR( set<int>::iterator, di, del )
	a.eff.erase(*di);

      FOR( vector<When>::iterator, wi, a.conds )
	{
	  set<int> del;
	  FOR( set<int>::const_iterator, ei, wi->eff )
	    if( *ei < 0 )
	      del.insert(*ei);
	  FOR( set<int>::iterator, di, del )
	    wi->eff.erase(*di);
	  if(wi->eff.size() == 0)
	    wi->used = false;
	}
    }
}

// Todos los when con precondiciones vacias
// son subidos effectos de sus acciones
void
post_process_whens()
{
  FOR_1( i, actions_p )
    {
      Act& a = actions_p[i];
      FOR( vector<When>::iterator, wi, a.conds )
	// If the cond effect becomes useless, desactivate
	if( wi->eff.empty() )
	  wi->used = false;
	else if( wi->prec.size() == 0 )
	  {
	    FOR( set<int>::const_iterator, e, wi->eff )
	      a.eff.insert(*e);
	    wi->used = false;
	  }
    }
}

// From old atom to K(new atom)
string trans(int atom)
{
  int natom = (atom>0)?r2a[abs(atom)]:-r2a[abs(atom)];
  assert( natom != 0 );
  return name_l( k(natom) );
}

string pddl_name("new");

void
printNewPDDL()
{
  /*
    print all atoms_p as predicates
    print all actions_p

    print old init and goal, transforming online
    ojo: asumir lista de literales en Init y en Goal, excepto unknown, oneof
  */

  registerEntry( "printNewPDDL()" );

  collect_mentioned();

  if( use_short_names && use_table_short )
    {
      cout << "Table of short names" << endl;
      for( size_t i = 1; i < atoms_p.size(); i++ )
	{
	  use_short_names = false;
	  cout << name_l(i) << "=";
	  use_short_names = true;
	  cout << name_l(i) << endl;
	}
      cout << "End of table of short names" << endl;
    }

  
  cout << "Generating PDDL" << endl;
  string domain = pddl_name + "-d.pddl";
  string problem = pddl_name + "-p.pddl";
  std::ofstream outd( domain.c_str() );
  std::ofstream outp( problem.c_str() );

  size_t ind = 0;
  outd << "(define (domain " << _low_domainName << ")" << endl;
  ind += 2; 
  di(outd, ind); 

  // Printing meaning of tags
  if( !t0c::tag2val.empty() )
    {
      outd << ";;;; Meaning of tag_*" << endl;
      for( map<set<int>, int>::iterator it = t0c::tag2val.begin(); 
	   it != t0c::tag2val.end(); it++ )
	{
	  di(outd, ind);
	  outd << "; tag_" << it->second << " = ";
	  const set<int>& xis = it->first;
	  FOR( set<int>::const_iterator, xi, xis )
	    {
	      outd<< "  ";
	      if( *xi < 0 )
		outd << "-";
	      outd << atoms[abs(*xi)];
	    }
	  outd << endl;
	}
      outd << endl;
    }
    
  di(outd, ind);
  outd << "(:predicates" << endl;
  ind += 2; 
  di(outd, ind);
  outd << "(" << dummy_pred << ")" << endl;
  for( size_t i = 1; i < atoms_p.size(); i++ )
    if( atoms_p_todel.count(i) == 0 &&
 	(all_mentioned.empty () || all_mentioned.count(i) > 0 ) )
      {
	di(outd, ind);
	outd << name_l(i) << endl;
      }
  if(0) // No es necesario imprimir cada cosa por separado
        // Todo esta en atoms_p
    { 
      for( size_t i = 1; i < atoms_p.size(); i++ )
    //for( size_t i = 1; i <= natoms_p; i++ )
    {
      di(outd, ind);
      outd << name_l(i) << endl;
    }

  if( lxi::labels.begin() != lxi::labels.end() )
    {
      di(outd, ind);
      outd << ";Label" << endl;
    }
  for( map<lxi::label_t,int>::const_iterator plabel = lxi::labels.begin();
       plabel != lxi::labels.end(); plabel++ )
    {
      assert( plabel->second > 0 );
      di(outd, ind);
      outd << name_l(plabel->second) << endl;
    }
    
  if( t0c::tags.begin() != t0c::tags.end() )
    {
      di(outd, ind);
      outd << ";Tagged for t0c" << endl;
    }
  for(map<int,set<set<int> > >::const_iterator it = t0c::tags.begin();
      it != t0c::tags.end(); it++ )
    FOR( set<set<int> >::const_iterator, ss, it->second )
    {
      di(outd, ind);
      if( !use_s0s || it->first > 0 ) // Dont print negative tags
	outd << name_l( t0c::tagged_t0c(it->first, *ss) ) << endl;
    }

  if( lxi_t0::labs.begin() != lxi_t0::labs.end() )
    {
      di(outd, ind);
      outd << ";Label t0" << endl;
    }
  for(map<int,set<set<int> > >::const_iterator it = lxi_t0::labs.begin();
      it != lxi_t0::labs.end(); it++ )
    FOR( set<set<int> >::const_iterator, ss, it->second )
    {
      di(outd, ind);
      outd << name_l( lxi_t0::labeled_t0(it->first, *ss) ) << endl;
    }
    
  if( lxi::flags.begin() != lxi::flags.end() )
    {
      di(outd, ind);
      outd << ";Flags X,L" << endl;
    }
  for( map<lxi::flag_t,int>::const_iterator pflag_l = lxi::flags.begin();
       pflag_l != lxi::flags.end(); pflag_l++ )
    {
      di(outd, ind);
      assert( pflag_l->second > 0 );
      outd << name_l(pflag_l->second) << endl;
    }
    
  if( merge_act::flags.begin() != merge_act::flags.end() )
    {
      di(outd, ind);
      outd << ";Flags X" << endl;
    }
  FOR( vector<int>::iterator, pflag, merge_act::flags )
    {
      di(outd, ind);
      outd << name_l(*pflag) << endl;
    }
    
  if( lxi_t0::flags.begin() != lxi_t0::flags.end() )
    {
      di(outd, ind);
      outd << ";Flags L" << endl;
    }
  for( map<int,int>::const_iterator pflag_l = lxi_t0::flags.begin();
       pflag_l != lxi_t0::flags.end(); pflag_l++ )
    {
      di(outd, ind);
      assert( pflag_l->second > 0 );
      outd << name_l(pflag_l->second) << endl;
    }
    }
  ind -= 2; 
  di(outd, ind);
  outd << ")" << endl;

  // OJO: mover a lugar para colectar estadisticas
  size_t num_lit_eff = 0;
  for( size_t i = 1; i < actions_p.size(); i++ )
    {
      Act& a = actions_p[i];
      num_lit_eff += a.eff.size();

      std::vector<When>::const_iterator wi;
      for( wi = a.conds.begin(); wi != a.conds.end(); ++wi )
	if(wi->used) num_lit_eff += wi->eff.size();
    }

  cout << "printing " << actions_p.size()-1 << " actions" << endl;
  for( size_t i = 1; i < actions_p.size(); i++ )
    {
      Act& a = actions_p[i];
      assert( a.index == i );
      a.dumpPDDL( outd, &name_l, ind );
    }

  if( use_contingent &&
      ( use_contingent_obs_nondeter ||
        use_contingent_obs_determ ) )
    {
      cout << "printing " << observations_p.size()-1 << " observations" << endl;
      for( size_t i = 1; i < observations_p.size(); i++ )
	{
	  Act& a = observations_p[i];
	  a.dumpPDDL( outd, &name_l, ind, use_contingent_obs_nondeter, use_contingent_obs_determ );
	}
    }

  ind -= 2;
  di(outd,ind);
  outd << ") ; ==================== END domain PDDL" << endl;

  di(outp,ind);
  outp << "(define (problem " << _low_problemName << ")" << endl;
  ind += 2; 
  di(outp,ind);
  outp << "(:domain " << _low_domainName << ")" << endl;

  di(outp,ind);
  outp << "(:init " << endl;
  ind += 2; 
  di(outp,ind);
  outp << "(" << dummy_pred << ")" << endl;

  if(1) { // ??????' obsolete because unit resolution of init theory
  set<int> init;
  collectPlainFormulaCertainAtoms( initialSituation, init );
  set<int> init_n;
  for( set<int>::const_iterator it = init.begin(); 
       it != init.end(); it++ )
    init_n.insert( (*it>0)?r2a[abs(*it)]:-r2a[abs(*it)]);

  if( use_contingent && 
      use_contingent_fail_check )
    {
      di(outp, ind);
      outp << "(" << atoms_p[t0_fail_pred_n] << ") " 
	   << endl;
    }
  init_n.insert(dummy_pred_n);
  init_n.insert(active_pred_n);
  // Don't print negative atoms
  for( size_t i = 1; i < atoms.size(); i++ )
    if( all_mentioned.empty () || all_mentioned.count(i) > 0 )
    if( init_n.count(i) > 0 )
      {
	di(outp, ind);
	outp << name_l(k(i)) << " " 
	     << endl;
      }
    else if( init_n.count(-i) > 0 || 
	     unknown.count(i) == 0 )
      {
	di(outp, ind);
	outp << name_l(k(-i)) << " " 
	     << endl;
      }
  }
  if(0)
  FOR( set<int>::iterator, a, true_literals )
    {
      di(outp, ind);
      outp << name_l(k(*a)) << " " 
	   << endl;
    }

    
  if( lxi::flags.begin() != lxi::flags.end() )
    {
      di(outp, ind);
      outp << ";Flags X,L" << endl;
    }

  for( map<lxi::flag_t,int>::const_iterator pflag_l = lxi::flags.begin();
       pflag_l != lxi::flags.end(); pflag_l++ )
    {
      di(outp, ind);
      assert( pflag_l->second > 0 );
      outp << name_l(pflag_l->second) << endl;
    }

  if( merge_act::flags.begin() != merge_act::flags.end())
    {
      di(outp, ind);
      outp << ";Flags X" << endl;
    }
  FOR( vector<int>::iterator, pflag, merge_act::flags )
    {
      di(outp, ind);
      outp << name_l(*pflag) << endl;
    }

  if( lxi_t0::flags.begin() != lxi_t0::flags.end() )
    {
      di(outp, ind);
      outp << ";Flags L" << endl;
    }
  for( map<int,int>::const_iterator pflag_l = lxi_t0::flags.begin();
       pflag_l != lxi_t0::flags.end(); pflag_l++ )
    {
      di(outp, ind);
      assert( pflag_l->second > 0 );
      outp << name_l(pflag_l->second) << endl;
    }

  if( use_t0 )
    {
      di(outp, ind);
      outp << ";Init Xi//Xi" << endl;
    }
  FOR( vector<set<int> >::const_iterator, it, oneof )
    {
      FOR_P( set<int>::const_iterator, e, it )
	{
	  set<int> s;
	  s.insert(*e);
	  if( lxi_t0::if_labeled_t0(*e, s) )
	    {
	      di(outp, ind);
	      outp << name_l( lxi_t0::labeled_t0(*e, s) ) << endl;
	    }
	}
    }

  if( use_t0c )
    {
      di(outp, ind);
      outp << ";Init Xi//Xi for t0c" << endl;
    }
  for(set<int>::iterator it = t0c::init_atoms.begin();
      it != t0c::init_atoms.end(); it++ )
    {
      di(outp, ind);
      outp << name_l( *it ) << endl;
    }
  di(outp,ind);
  outp << ")" << endl;

  ind -= 2; 

  di(outp,ind);
  outp << "(:goal " << endl;
  ind += 2; 
  di(outp,ind);
  //printFormulaPDDLTrans( outp, goalSituation, &trans );
  outp << "(and " << endl;
  FOR( set<int>::iterator, l, goal_literals )
    outp << name_l( k(*l) ) << endl;
  FOR( set<int>::iterator, l, goal_atoms_p )
    outp << name_l( *l ) << endl;
  outp << ")" << endl;
  outp << endl;
  di(outp,ind);
  outp << ")" << endl;

  ind -= 2; 
  di(outp,ind);
  outp << ")" << endl;

  cout << "STAT old-Actions: " << actions.size()-1 << endl
       << "STAT old-Atoms: " << atoms.size()-1 << endl
       << "STAT old-cond-effects: " 
       << whens.size() << endl
       << "STAT old-condicionales: " 
       << old_num_lit_eff << endl;
  cout << "STAT KP-NActions: " << actions_p.size()-1 << endl
       << "STAT KP-NAtoms: " << (atoms_p.size()-1-atoms_p_todel.size()) << endl
       << "STAT KP-deleted-NAtoms: " << atoms_p_todel.size() << endl
       << "STAT KP-Nconds-effects-and-notused: " << new_nwhen(true) << endl
       << "STAT KP-Ncond-effects: " << new_nwhen() << endl
       << "STAT KP-Numero_lit_en_efectos_condicionales: " 
       << num_lit_eff << endl;
  

  registerExit();

}



void
printDebugPDDL()
{
  /*
    print all atoms_p as predicates
    print all actions_p

    print old init and goal, transforming online
    ojo: asumir lista de literales en Init y en Goal, excepto unknown, oneof
  */

  registerEntry( "printDebugPDDL()" );

  collect_mentioned();

  if( use_short_names && use_table_short )
    {
      cout << "Table of short names" << endl;
      for( size_t i = 1; i < atoms_p.size(); i++ )
	{
	  use_short_names = false;
	  cout << name_l(i) << "=";
	  use_short_names = true;
	  cout << name_l(i) << endl;
	}
      cout << "End of table of short names" << endl;
    }

  
  cout << "Generating PDDL" << endl;
  string domain = pddl_name + "-debug-d.pddl";
  string problem = pddl_name + "-debug-p.pddl";
  std::ofstream outd( domain.c_str() );
  std::ofstream outp( problem.c_str() );

  size_t ind = 0;
  outd << "(define (domain " << _low_domainName << ")" << endl;
  ind += 2; 
  di(outd, ind); 

  // Printing meaning of tags
  if( !t0c::tag2val.empty() )
    {
      outd << ";;;; Meaning of tag_*" << endl;
      for( map<set<int>, int>::iterator it = t0c::tag2val.begin(); 
	   it != t0c::tag2val.end(); it++ )
	{
	  di(outd, ind);
	  outd << "; tag_" << it->second << " = ";
	  const set<int>& xis = it->first;
	  FOR( set<int>::const_iterator, xi, xis )
	    {
	      outd<< "  ";
	      if( *xi < 0 )
		outd << "-";
	      outd << atoms[abs(*xi)];
	    }
	  outd << endl;
	}
      outd << endl;
    }
    
  di(outd, ind);
  outd << "(:predicates" << endl;
  ind += 2; 
  di(outd, ind);
  outd << "(" << dummy_pred << ")" << endl;
  for( size_t i = 1; i < atoms_p.size(); i++ )
    if( atoms_p_todel.count(i) == 0 &&
 	(all_mentioned.empty () || all_mentioned.count(i) > 0 ) )
      {
	di(outd, ind);
	outd << name_l(i) << endl;
      }
  if(0) // No es necesario imprimir cada cosa por separado
        // Todo esta en atoms_p
    { 
      for( size_t i = 1; i < atoms_p.size(); i++ )
    //for( size_t i = 1; i <= natoms_p; i++ )
    {
      di(outd, ind);
      outd << name_l(i) << endl;
    }

  if( lxi::labels.begin() != lxi::labels.end() )
    {
      di(outd, ind);
      outd << ";Label" << endl;
    }
  for( map<lxi::label_t,int>::const_iterator plabel = lxi::labels.begin();
       plabel != lxi::labels.end(); plabel++ )
    {
      assert( plabel->second > 0 );
      di(outd, ind);
      outd << name_l(plabel->second) << endl;
    }
    
  if( t0c::tags.begin() != t0c::tags.end() )
    {
      di(outd, ind);
      outd << ";Tagged for t0c" << endl;
    }
  for(map<int,set<set<int> > >::const_iterator it = t0c::tags.begin();
      it != t0c::tags.end(); it++ )
    FOR( set<set<int> >::const_iterator, ss, it->second )
    {
      di(outd, ind);
      if( !use_s0s || it->first > 0 ) // Dont print negative tags
	outd << name_l( t0c::tagged_t0c(it->first, *ss) ) << endl;
    }

  if( lxi_t0::labs.begin() != lxi_t0::labs.end() )
    {
      di(outd, ind);
      outd << ";Label t0" << endl;
    }
  for(map<int,set<set<int> > >::const_iterator it = lxi_t0::labs.begin();
      it != lxi_t0::labs.end(); it++ )
    FOR( set<set<int> >::const_iterator, ss, it->second )
    {
      di(outd, ind);
      outd << name_l( lxi_t0::labeled_t0(it->first, *ss) ) << endl;
    }
    
  if( lxi::flags.begin() != lxi::flags.end() )
    {
      di(outd, ind);
      outd << ";Flags X,L" << endl;
    }
  for( map<lxi::flag_t,int>::const_iterator pflag_l = lxi::flags.begin();
       pflag_l != lxi::flags.end(); pflag_l++ )
    {
      di(outd, ind);
      assert( pflag_l->second > 0 );
      outd << name_l(pflag_l->second) << endl;
    }
    
  if( merge_act::flags.begin() != merge_act::flags.end() )
    {
      di(outd, ind);
      outd << ";Flags X" << endl;
    }
  FOR( vector<int>::iterator, pflag, merge_act::flags )
    {
      di(outd, ind);
      outd << name_l(*pflag) << endl;
    }
    
  if( lxi_t0::flags.begin() != lxi_t0::flags.end() )
    {
      di(outd, ind);
      outd << ";Flags L" << endl;
    }
  for( map<int,int>::const_iterator pflag_l = lxi_t0::flags.begin();
       pflag_l != lxi_t0::flags.end(); pflag_l++ )
    {
      di(outd, ind);
      assert( pflag_l->second > 0 );
      outd << name_l(pflag_l->second) << endl;
    }
    }
  ind -= 2; 
  di(outd, ind);
  outd << ")" << endl;

  // OJO: mover a lugar para colectar estadisticas
  size_t num_lit_eff = 0;
  for( size_t i = 1; i < actions_p.size(); i++ )
    {
      Act& a = actions_p[i];
      num_lit_eff += a.eff.size();

      std::vector<When>::const_iterator wi;
      for( wi = a.conds.begin(); wi != a.conds.end(); ++wi )
	if(wi->used) num_lit_eff += wi->eff.size();
    }

  cout << "printing " << actions_p.size()-1 << " actions" << endl;
  for( size_t i = 1; i < actions_p.size(); i++ )
    {
      Act& a = actions_p[i];
      assert( a.index == i );
      a.dumpPDDL( outd, &name_l, ind );
    }

  if( use_contingent &&
      ( use_contingent_obs_nondeter ||
        use_contingent_obs_determ ) )
    {
      cout << "printing " << observations_p.size()-1 << " observations" << endl;
      for( size_t i = 1; i < observations_p.size(); i++ )
	{
	  Act& a = observations_p[i];
	  a.dumpPDDL( outd, &name_l, ind, use_contingent_obs_nondeter, use_contingent_obs_determ );
	}
    }

  ind -= 2;
  di(outd,ind);
  outd << ") ; ==================== END domain PDDL" << endl;

  di(outp,ind);
  outp << "(define (problem " << _low_problemName << ")" << endl;
  ind += 2; 
  di(outp,ind);
  outp << "(:domain " << _low_domainName << ")" << endl;

  di(outp,ind);
  outp << "(:init " << endl;
  ind += 2; 
  di(outp,ind);
  outp << "(" << dummy_pred << ")" << endl;

  if(1) { // ??????' obsolete because unit resolution of init theory
  set<int> init;
  collectPlainFormulaCertainAtoms( initialSituation, init );
  set<int> init_n;
  for( set<int>::const_iterator it = init.begin(); 
       it != init.end(); it++ )
    init_n.insert( (*it>0)?r2a[abs(*it)]:-r2a[abs(*it)]);

  if( use_contingent && 
      use_contingent_fail_check )
    {
      di(outp, ind);
      outp << "(" << atoms_p[t0_fail_pred_n] << ") " 
	   << endl;
    }
  init_n.insert(dummy_pred_n);
  init_n.insert(active_pred_n);
  // Don't print negative atoms
  for( size_t i = 1; i < atoms.size(); i++ )
    if( all_mentioned.empty () || all_mentioned.count(i) > 0 )
    if( init_n.count(i) > 0 )
      {
	di(outp, ind);
	outp << name_l(k(i)) << " " 
	     << endl;
      }
    else if( init_n.count(-i) > 0 || 
	     unknown.count(i) == 0 )
      {
	di(outp, ind);
	outp << name_l(k(-i)) << " " 
	     << endl;
      }
  }
  if(0)
  FOR( set<int>::iterator, a, true_literals )
    {
      di(outp, ind);
      outp << name_l(k(*a)) << " " 
	   << endl;
    }

    
  if( lxi::flags.begin() != lxi::flags.end() )
    {
      di(outp, ind);
      outp << ";Flags X,L" << endl;
    }

  for( map<lxi::flag_t,int>::const_iterator pflag_l = lxi::flags.begin();
       pflag_l != lxi::flags.end(); pflag_l++ )
    {
      di(outp, ind);
      assert( pflag_l->second > 0 );
      outp << name_l(pflag_l->second) << endl;
    }

  if( merge_act::flags.begin() != merge_act::flags.end())
    {
      di(outp, ind);
      outp << ";Flags X" << endl;
    }
  FOR( vector<int>::iterator, pflag, merge_act::flags )
    {
      di(outp, ind);
      outp << name_l(*pflag) << endl;
    }

  if( lxi_t0::flags.begin() != lxi_t0::flags.end() )
    {
      di(outp, ind);
      outp << ";Flags L" << endl;
    }
  for( map<int,int>::const_iterator pflag_l = lxi_t0::flags.begin();
       pflag_l != lxi_t0::flags.end(); pflag_l++ )
    {
      di(outp, ind);
      assert( pflag_l->second > 0 );
      outp << name_l(pflag_l->second) << endl;
    }

  if( use_t0 )
    {
      di(outp, ind);
      outp << ";Init Xi//Xi" << endl;
    }
  FOR( vector<set<int> >::const_iterator, it, oneof )
    {
      FOR_P( set<int>::const_iterator, e, it )
	{
	  set<int> s;
	  s.insert(*e);
	  if( lxi_t0::if_labeled_t0(*e, s) )
	    {
	      di(outp, ind);
	      outp << name_l( lxi_t0::labeled_t0(*e, s) ) << endl;
	    }
	}
    }

  if( use_t0c )
    {
      di(outp, ind);
      outp << ";Init Xi//Xi for t0c" << endl;
    }
  for(set<int>::iterator it = t0c::init_atoms.begin();
      it != t0c::init_atoms.end(); it++ )
    {
      di(outp, ind);
      outp << name_l( *it ) << endl;
    }
  di(outp,ind);
  outp << ")" << endl;

  ind -= 2; 

  di(outp,ind);
  outp << "(:goal " << endl;
  ind += 2; 
  di(outp,ind);
  //printFormulaPDDLTrans( outp, goalSituation, &trans );
  outp << "(and " << endl;
  FOR( set<int>::iterator, l, goal_literals )
    outp << name_l( k(*l) ) << endl;
  FOR( set<int>::iterator, l, goal_atoms_p )
    outp << name_l( *l ) << endl;
  outp << ")" << endl;
  outp << endl;
  di(outp,ind);
  outp << ")" << endl;

  ind -= 2; 
  di(outp,ind);
  outp << ")" << endl;

  cout << "STAT old-Actions: " << actions.size()-1 << endl
       << "STAT old-Atoms: " << atoms.size()-1 << endl
       << "STAT old-cond-effects: " 
       << whens.size() << endl
       << "STAT old-condicionales: " 
       << old_num_lit_eff << endl;
  cout << "STAT KP-NActions: " << actions_p.size()-1 << endl
       << "STAT KP-NAtoms: " << (atoms_p.size()-1-atoms_p_todel.size()) << endl
       << "STAT KP-deleted-NAtoms: " << atoms_p_todel.size() << endl
       << "STAT KP-Nconds-effects-and-notused: " << new_nwhen(true) << endl
       << "STAT KP-Ncond-effects: " << new_nwhen() << endl
       << "STAT KP-Numero_lit_en_efectos_condicionales: " 
       << num_lit_eff << endl;
  

  registerExit();

}

void
usage( std::ostream &os )
{
  os << std::endl
     << "usage: cf2cs {-s <prefix>} {FLAGS} <domain> <problem>"
     << std::endl << std::endl
     << "\tCompiles the conformant PDDL problem specified in the domain and problem file" << std::endl
     << "\tinto a classical problem on files <prefix>-d.pddl and <prefix>-p.pddl.\n" << std::endl
     << "\tdefault prefix = 'new'"  << std::endl
     << "\tThis transformation is not complete, but sound. "  << std::endl
     << "\tRequires an ADL classical planner"  << std::endl
     << std::endl
     << "Flags:" << std::endl << std::endl
     << "  -t0              Use atoms L/xi, that guarantee L if xi is true at t=0." << std::endl
     << "  -mac             merge:  AND_L' K-L' -> KL" << std::endl
     << "  -cdisjm          merge:  AND_L' M-L' -> ML." << std::endl
     << std::endl 
     << "  -cond            ND observation actions." << std::endl 
     << "  -cod             D observations, introduces M-Literals, changes the precons." << std::endl 
     << std::endl 
     << "  -ckinl           merge imply: KL/t & K-L -> K-t" << std::endl 
     << "  -cminl           merge imply: KL/t & M-L -> M-t" << std::endl  
     << "  -ckit            merge KL/t & Kt -> KL" << std::endl 
     << "  -cmit            merge KL/t & Mt -> ML" << std::endl
     << "  -cdisjk0         merge:  AND_t' K-t'@0 -> Kt@0." << std::endl
     << "  -cdisjm0         merge:  AND_t' M-t'@0 -> Mt@0." << std::endl
     << "  -cpropk0         propagate k -> k@0 and m -> m@0 when lit is static" << std::endl 
     << "  -csl             full merge, introduces SL/xi atoms" << std::endl 
     << "  -cfm             full merge. A lot of actions!" << std::endl 
     << "  -obs             Don't use Obs(x) for observations. Use Mx" << std::endl
     << std::endl
     << "  -mog             merge of everything (not only goal and preconds)." << std::endl 
     << "  -fp              use Full Propagation: ramification KL -> KL/t in many cases" << std::endl 
     << "  -cfc             Problem fails when Kx & K-x" << std::endl    
     << "  -cmr             MC -> ML" << std::endl    
     << "  -fct             force contingent: move preconds." << std::endl 
     << "  -npc             no use of preconditions (force conformant)." << std::endl
     << "  -dsl             Add also DELETE_CLOSURE for using SL/xi" << std::endl
     << "  -cnap            dishabilitate HABILITATE flags..." << std::endl    
     << "  -cnamac          stop using HABILITATE flags for -mac and -cdisjk0" << std::endl    
     << "  -sn              DON'T use SHORT unreadable names. (i.e short by default)" << std::endl    
     << "  -tsn             print table of equivalence between short names and K_L/t" << std::endl  
     << "  -ncc             no cost to closures" << std::endl  
     << "  -ass             uses 'assumptions' to get out of deadends" << std::endl
     << "  -cost            habilitate action costs" << std::endl    
     << "  -v <n>           Set verbosity level to <n>. Useful values are 5, 10, 15, and 20." << std::endl
     << std::endl
     << std::endl;
  exit(1);
}

void
parseArg(  int argc, char **argv )
{
  // read arguments (if any)
  vector<string> args;
  for( ++argv ; *argv != 0; ++argv )
    {
      cout << *argv << endl << flush;
      args.push_back(string(*argv));
    }

  size_t argn = 0;

  for( argn = 0; argn < args.size(); ++argn )
    {
      string& arg = args[argn];
      if( arg == "-v" )
	verbose = atoi( args[++argn].c_str() );

      else if( arg == "-obs" )
	use_obs_variables = !use_obs_variables;
      else if( arg == "-cfc" )
	use_contingent_fail_check = !use_contingent_fail_check;
      else if( arg == "-cfm" )
	use_contingent_full_merge = !use_contingent_full_merge;
      else if( arg == "-csl" )
	use_contingent_sl_merges = !use_contingent_sl_merges;
      else if( arg == "-cnap" )
	use_contingent_active_pred = !use_contingent_active_pred;
      else if( arg == "-cnamac" )
	use_contingent_active_pred_disj = !use_contingent_active_pred_disj;
      else if( arg == "-cond" )
	use_contingent_obs_nondeter = !use_contingent_obs_nondeter;
      else if( arg == "-cod" )
	use_contingent_obs_determ = !use_contingent_obs_determ; 
      //       else if( arg == "-cm" )
      // 	use_contingent_m = !use_contingent_m;
      else if( arg == "-cminl" )
	use_contingent_mnl_imply = !use_contingent_mnl_imply;
      else if( arg == "-cmit" )
	use_contingent_mt_imply = !use_contingent_mt_imply;
      else if( arg == "-ckinl" )
	use_contingent_knl_imply = !use_contingent_knl_imply;
      else if( arg == "-ckit" )
	use_contingent_kt_imply = !use_contingent_kt_imply;
      else if( arg == "-cmr" )
	use_contingent_m_rules = !use_contingent_m_rules;
      else if( arg == "-cdisjm" )
	use_merge_act_m = !use_merge_act_m; 
      else if( arg == "-old_cdisjm" )
	use_merge_act_m_old = !use_merge_act_m_old;
      else if( arg == "-cdisjk0" )
	use_merge_act_k0 = !use_merge_act_k0; 
      else if( arg == "-cdisjm0" )
	use_merge_act_m0 = !use_merge_act_m0; 
      else if( arg == "-cpropk0" )
	use_contingent_k0_prop = !use_contingent_k0_prop; 
      else if( arg == "-dsl")
	use_delete_closure_sl = !use_delete_closure_sl;

      else if( arg == "-fct" )
	use_contingent = true;
      else if( arg == "-f" )
	{
	  use_simple_cancellation = false;
	  use_only_I_disjunctions = false;
	  use_s0s = false;
	}
      else if( arg == "-df" )
	use_delete_free = !use_delete_free;
      else if( arg == "-d" )
	{
	  use_only_I_disjunctions = true;
	  use_s0s = false;
	}
      else if( arg == "-ncb" )
	use_clause_b_tags = false;
      else if( arg == "-npc" )
	use_k_preconds = false;
      else if( arg == "-nr" )
	use_relevance = !use_relevance;
      else if( arg == "-ntag" )
	use_new_tag_gen = !use_new_tag_gen;
      else if( arg == "-cw" )
	only_check_new_width = true;
      else if( arg == "-nca" )
	use_clean_actions = false;
      //       else if( arg == "-ca2" )
      // 	use_new_clean_actions = true;
      else if( arg == "-s0" )
	{
	  use_s0s = true;
	  use_only_I_disjunctions = false;
	  use_merge_only_goals_and_precs = true;
	  use_simple_cancellation = true;
	}
      else if( arg == "-sc" )
	use_simple_cancellation = !use_simple_cancellation;
      else if( arg == "-s" )
	pddl_name = string( args[++argn] );
      else if( arg == "-or" )
	use_oneof_or = true;
      else if( arg == "-t0" )
	use_t0c = true;
      else if( arg == "-mac" )
	use_merge_act = !use_merge_act;
      else if( arg == "-maxt" )
	{
	  t0c::max_size_tag = atoi( args[++argn].c_str() );
	  if( t0c::max_size_tag < 0 )
	    {
	      cout << "-maxt <n> with <n> a number > 0" << endl;
	      exit(1);
	    }
	}
      else if( arg == "-mog" )
	use_merge_only_goals_and_precs = !use_merge_only_goals_and_precs;
      else if( arg == "-fp" )
	use_full_propagation = !use_full_propagation;
      else if( arg == "-af" )
	merge_act::allow_flag = true;
      else if( arg == "-kp" )
	use_kp = true;
      else if( arg == "-sn" )
	use_short_names = !use_short_names;
      else if( arg == "-tsn" )
	use_table_short = !use_table_short;
      else if( arg == "-cost")
	use_costs = !use_costs; 
      else if( arg == "-ncc")
	use_no_cost_closures = !use_no_cost_closures;
      else if( arg == "-ass")
	use_assumptions_on_tags = !use_assumptions_on_tags;
      else if( arg.c_str()[0] == '-' )	
	usage( std::cout );
      else 
	break;
    }
  
  // Contingent implication and verifications
  if( use_contingent_knl_imply || 
      use_contingent_kt_imply || 
      use_contingent_full_merge ||
      use_contingent_sl_merges )
    use_contingent_k0 = true;

  if( use_contingent_obs_determ )//  || 
//       use_contingent_m_rules )
    use_k_preconds = false;

  if( use_merge_act_k0 && !use_contingent_k0 )
    {
      cout << "-cdisjk0 requires that atoms k0 are being used" << endl;
      exit(1);
    }

  if( use_contingent_mnl_imply || 
      use_contingent_mt_imply )
    use_contingent_m0 = true;
  if( use_merge_act_m0 && !use_contingent_m0 )
    {
      cout << "-cdisjm0 requires that atoms m0 are being used" << endl;
      exit(1);
    }

  if( use_contingent_obs_determ ||
      use_contingent_m_rules || 
      use_contingent_mnl_imply ||
      use_contingent_mt_imply )
    use_contingent_m = true;
  if( use_merge_act_m && !use_contingent_m )
    {
      cout << "-cdisjm requires that atoms M are being used" << endl;
      exit(1);
    }

  if( use_contingent_fail_check && !use_contingent_knl_imply )
    {
      cout << "-fc requires imply rules for k (-ckinl), for concluding k0 atoms" << endl;
      exit(1);
    }

  // T0 verification
  if(use_t0c)
    {
      if( use_only_I_disjunctions &  use_s0s ) 
	{
	  cout << "ERROR: can't use -s0 and -d at the same time " << endl;
	  usage( std::cout );
	}

      //       if(use_s0s)
      // 	use_simple_cancellation = false;
      //       if(use_only_I_disjunctions )
      // 	use_simple_cancellation = true;
      
      if( use_only_I_disjunctions) 
	cout << "Using only initial disjunctions for merge" << endl;
      else
	cout << "Calculating combinations for merge" << endl;
      
      if( use_s0s ) 
	cout << "Using initial states s0 as unique possible tags" << endl;
      else
	cout << "Clousuring for obtaining possible tags" << endl;

      if(use_simple_cancellation )
	cout << "Simple cancellation: Translating delete of atoms incomplete. More efficient" << endl;
      else
	cout << "Full cancellation: Translating deletes properly. Maybe complete if '-s0' or '-f' option was used" << endl;

      if( use_propagation )
	cout << "Propagating ramifications in effects" << endl;
      else
	cout << "No propagating ramifications in effects" << endl;

      if( use_merge_act )
	cout << "Using action compilation + merge" << endl;
      else
	cout << "Not using action compilation + merge" << endl;

      if(use_merge_only_goals_and_precs)
	cout << "Merging only goals and preconditions" << endl;
      else
	cout << "Merging all possible atoms" << endl;
    }

}


void
do_cf2cs()
{
  if( observation_detected )
    use_contingent = true;
  if( use_contingent_heuristic )
    {
      if( use_contingent )
	cout << "Generating PDDL for contingent heuristic" << endl;
      else
	cout << "Ignoring generation of PDDL for contingent heuristic: "
	  "No observation detected in problem" << endl;
    }
  
  const bool reject_complex = false;
  if( reject_complex )
    {
      if( isComplexFormula( goalSituation ) )
	{
	  cerr << "FATAL ERROR: Rejecting to generate transformation for complex goal." << endl
	       << "REASON: Some classical planners do not lead well with them " << endl;
	  exit(1);
	}
      if( isComplexFormula2( initialSituation ) )
	{
	  cerr << "FATAL ERROR: Rejecting to generate transformation for complex init." << endl
	       << "REASON: It doesn't deal with some wff yet " << endl;
	  exit(1);
	}
    }

  cout << "Objects: ";
  for( map<const char*,idList_t*,ltstr>::iterator it2 = objects.begin(); 
       it2 != objects.end(); ++it2 )
    cout<< it2->second->name << " ";
  cout << endl;

  // Load atoms and actions and init Databases for transforming
  finishInstanceDB();

  // Update static atoms. For example, observations were excluded
  for( size_t i = 1; i <= natoms; i++ )
    if( actionEffLit(i).empty() &&
	actionEffLit(-i).empty() &&
	whenEffLit(i).empty() &&
	whenEffLit(-i).empty() )
      static_atoms.insert(i);

  cout << "Static atoms (" << static_atoms.size() << "): ";
  FOR( std::set<int>::iterator, it, static_atoms )
    cout << atoms[*it] << " ";
  cout << endl;

  if( verbose > LEVEL1 )
    report_static_disj();
  if( use_t0c )
    {
      if( use_contingent && use_obs_variables ) 
	prepare_observables_init();
      t0c::calc_tags();

      if( only_check_new_width )
	exit(0);

      if( use_contingent )
	{
	  if( use_contingent_sl_merges )
	    prefix_to_save.push_back("S_");
	  if( use_contingent_k0 )
	    {
	      create_copy_atoms( "k0", k0_base );
	      k0_max = atoms_p.size()-1;
	    }
	  if( use_contingent_heuristic && use_contingent_m )
	    { // maybe-atoms
	      add_assert_lit( &m );
	      if( use_contingent_m0 )
		create_copy_atoms( "m0", m0_base );
	      if( use_contingent_m_rules )
		make_k_0( "m", m_base, false, false );
	      else
		create_copy_atoms( "m", m_base );
	    }
	}
      add_assert_lit( &k );
      generate_katoms = true;
      int new_k_base;
      if( use_contingent && use_contingent_heuristic )
	make_k_0("k", new_k_base, true, use_k_preconds);
      else
	make_k_0("k", new_k_base );
      k_base = new_k_base;
      //cout << "kbase = " << k_base <<endl;
	
      if( use_obs_variables ) 
      {
              prepare_observables_final();
              std::cout << "GENERAL: number of observations = " << atoms_observable.size() << std::endl;
      }
      if( use_merge_act )
	make_k_0_plus();

      t0c::make_k_t0c();

      if (use_assumptions_on_tags)
	{
	  t0c_cont::create_assumptions( );
	}

      if( use_contingent )
	{
	  t0c_cont::merge_imply_l_tags( );
	  if( use_contingent_heuristic )
	    // For static copies of atoms at Init
	    t0c_cont::create_observations_heur( );
	  else
	    t0c_cont::create_observations_prog( );
	  if( use_contingent_k0 && use_contingent_fail_check )
	    check_contradiction( "_k0", &k0 );

	  if( use_contingent_m && use_contingent_obs_determ )
	    // Create M preconds...
	    make_k_0_prec( "m", m_base );
	}
    }
  else
    {
      add_assert_lit( &k );
      make_k_0("k", k_base);
	  
      if( use_merge_act )
	make_k_0_plus();

      if( use_t0 )
	lxi_t0::make_k_1_t0();

      if( use_kp )
	lxi::make_k_1_dynamic();
    }

  if( use_merge_act )
    merge_act::make_merge_act( "_k", &k, merge_act::allow_flag, false, true, true );
  if( use_contingent )
    {
      if( use_contingent_k0 && use_merge_act_k0 )
	merge_act::make_merge_act( "_k0", &k0, false, true, false, true );
      if( use_contingent_m && use_merge_act_m )
	merge_act::make_merge_act( "_m", &m, false, false, false, false, use_merge_act_m_old );
      if( use_contingent_m0 && use_merge_act_m0 )
	merge_act::make_merge_act( "_m0", &m0, false, true, false );
    }
 
  if( use_t0c )
    {
      if( use_clean_actions )
	t0c::clean_actions();
      t0c::create_init_atoms();
    }

  if( use_contingent &&
      use_contingent_active_pred )
    t0c_cont::create_flag_actions();

  if( use_delete_free )
    {
      del_neg_effects();
      use_delete_free = false;
    }


  post_process_whens();

  print_actions();

  // Reorganize whens...
  printNewPDDL();

  assert( !dir_oneof || dir_oneof == (void*)(oneof.empty()?0:&oneof[0]) );

#ifdef __STATS_HASH
  cout << "max_rec" << max_rec << endl;
  cout << "ave_rec" << (sum_rec/n_rec) << endl;
#endif
  //registerExit();
}
