#define YY_parse_h_included
/*#define YY_USE_CLASS 
*/
/*  A Bison++ parser, made from parser.y  */

 /* with Bison++ version bison++ Version 1.21.9-1, adapted from GNU bison by coetmeur@icdc.fr
Maintained by Magnus Ekdahl <magnus@debian.org>
  */


#line 1 "/usr/share/bison++/bison.cc"
/* -*-C-*-  Note some compilers choke on comments on `#line' lines.  */
/* Skeleton output parser for bison,
   Copyright (C) 1984, 1989, 1990 Bob Corbett and Richard Stallman

   This program is free software; you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation; either version 1, or (at your option)
   any later version.

   This program is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with this program; if not, write to the Free Software
   Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.  

   As a special exception, when this file is copied by Bison++ into a
   Bison++ output file, you may use that output file without restriction.
   This special exception was added by the Free Software Foundation
   in version 1.24 of Bison, and has been in Bison++ since 1.21.9.  

*/

/* HEADER SECTION */
#if defined( _MSDOS ) || defined(MSDOS) || defined(__MSDOS__) 
 #define __MSDOS_AND_ALIKE
#endif

#if defined(_WINDOWS) && defined(_MSC_VER)
 #define __HAVE_NO_ALLOCA
 #define __MSDOS_AND_ALIKE
#endif

#ifndef alloca
 #if defined( __GNUC__)
  #define alloca __builtin_alloca

 #elif (!defined (__STDC__) && defined (sparc)) || defined (__sparc__) || defined (__sparc)  || defined (__sgi)
  #include <alloca.h>

 #elif defined (__MSDOS_AND_ALIKE)
  #include <malloc.h>
  #ifndef __TURBOC__
   /* MS C runtime lib */
   #define alloca _alloca
  #endif

 #elif defined(_AIX)
  /* pragma must be put before any C/C++ instruction !! */
  #pragma alloca
  #include <malloc.h>

 #elif defined(__hpux)
  #ifdef __cplusplus
   extern "C" {
     void *alloca (unsigned int);
   };
  #else /* not __cplusplus */
   void *alloca ();
  #endif /* not __cplusplus */

 #endif /* not _AIX  not MSDOS, or __TURBOC__ or _AIX, not sparc.  */
#endif /* alloca not defined.  */

#ifdef c_plusplus
 #ifndef __cplusplus
  #define __cplusplus
 #endif
#endif

#ifdef __cplusplus
 #ifndef YY_USE_CLASS
/*#warning "For C++ its recomended to use bison++, otherwise classes won't be generated"*/
 #endif
#else
 #ifndef __STDC__
  #define const
 #endif
 #ifdef YY_USE_CLASS
  #error "This is a C++ header generated by bison++, please use a C++ compiler!"
 #endif
#endif

#include <stdio.h>
#define YYBISON 1  

 #line 88 "/usr/share/bison++/bison.cc"
#line 1 "parser.y"

/*
 *  Copyright (C) 2006 Universitat Pompeu Fabra
 *
 *  Permission is hereby granted to distribute this software for
 *  non-commercial research purposes, provided that this copyright
 *  notice is included with any such distribution.
 *
 *  THIS SOFTWARE IS PROVIDED "AS IS" WITHOUT WARRANTY OF ANY KIND,
 *  EITHER EXPRESSED OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE
 *  IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
 *  PURPOSE.  THE ENTIRE RISK AS TO THE QUALITY AND PERFORMANCE OF THE
 *  SOFTWARE IS WITH YOU.  SHOULD THE PROGRAM PROVE DEFECTIVE, YOU
 *  ASSUME THE COST OF ALL NECESSARY SERVICING, REPAIR OR CORRECTION.
 *
 *  Blai Bonet, bonet@ldc.usb.ve
 *  Hector Palacios, hector.palacios@upf.edu, hectorpal@gmail.com
 *
 */

#include <stdio.h>
#include <assert.h>
#include <iostream>

#include <map>
#include <nnf.h>

#include "parser.h"
#include "planner.h"

#ifdef USE_CLAUSE
#include "clauses.hpp"
#endif

  // Sometimes it use a lot the stack...
#define YYINITDEPTH 5000

extern int yylex(void);
using namespace std;


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

int                _low_numberSchema = 0;
char*              _low_yyfile = NULL;
char*              _low_problemName = NULL;
char*              _low_domainName = NULL;
char**             _low_schemaName = NULL;
char**             _low_objectName = NULL;
char**             _low_predicateName = NULL;
int                _low_numberPredicates = 0;
int                _low_requirements = 0;
schema_t*          _low_schemaTable[MAXSCHEMA];
int**              _low_initialAtoms;

// operators
operator_t         _low_operator;
int                _low_groundingOperators;

// variables and domain instantiation
int**              _low_vars = NULL;
int**              _low_values = NULL;

// initial/goal formulas
formula_t*         structural = NULL;
formula_t*         initialSituation = NULL;
formula_t*         goalSituation = NULL;

// tables
typedef map<const char*,formula_t*,ltstr> str2wff_t;
str2wff_t predicates;
str2wff_t defined;
map<const char*,idList_t*,ltstr>   objects;
map<const char*,idList_t*,ltstr>   types;


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

static int         domainParsed = 0;
static int         maxParameters = 0;
static int         numberObjects = 0;
static schema_t*   schemas = NULL;


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

static void       checkRequirement( int );
static formula_t* unfoldQuantifiers( formula_t* );
static formula_t* linearizeEffect( formula_t*, formula_t*& );
       void       printFormula( FILE*, formula_t* );
       void       printFormulaPDDL( ostream& o, formula_t *formula );
       void       printInitialPDDL( ostream& out, formula_t *formula );
static nnf::node  generateEffect( nnf::Manager*, nnf::node, formula_t*, int*, lit_effect_t& );
//static void       collectEffectAtoms( formula_t*, int*, std::vector<int>& );
static void       collectEffectAtoms( formula_t*, int*, std::vector<int>&, std::vector<int> *atoms_conds = 0 );
static nnf::node  generateAtomicFormula( nnf::Manager*, formula_t *, int*, bool );
       nnf::node  generateFormula( nnf::Manager*, formula_t*, int*, bool );
static void       collectPlainFormulaAtoms( formula_t* formula, int* parameters, 
					    std::vector<int> &atoms );
static void       collectFormulaAtomsPos( formula_t*, int*, std::vector<int>& );
static void       collectFormulaAtoms( formula_t*, int*, std::vector<int>& );
static int        atomId( formula_t *literal, int* parameters );

 static void idMatchArgsVars( formula_t *formula, idList_t *vars );
 static void generateNames( void );
 static instantiation_t * buildInstantiation( idList_t *vars, idList_t *args );
 static formula_t * copyReplaceFormula( formula_t *formula, instantiation_t *inst );
 void yyerror( char const *s );


extern int        lineno;
extern int        numberAtoms;
extern iatom_t*   readAtomHash( int* );
extern std::map<int,int> inv_reachable;
extern std::map<int,int> reachable;
extern unsigned   time_shift;
extern bool observation_detected;

#line 88 "/usr/share/bison++/bison.cc"
/* %{ and %header{ and %union, during decl */
#define YY_parse_BISON 1

#ifndef YY_parse_COMPATIBILITY
 #ifndef YY_USE_CLASS
  #define  YY_parse_COMPATIBILITY 1
 #else
  #define  YY_parse_COMPATIBILITY 0
 #endif
#endif

#if YY_parse_COMPATIBILITY != 0
 /* backward compatibility */
 #ifdef YYLTYPE
  #ifndef YY_parse_LTYPE
   #define YY_parse_LTYPE YYLTYPE
  #endif
 #endif
/* Testing alternative bison solution
   /#ifdef YYSTYPE*/
#ifndef YY_parse_STYPE 
   #define YY_parse_STYPE YYSTYPE
#endif
/*#endif*/
 #ifdef YYDEBUG
  #ifndef YY_parse_DEBUG
   #define  YY_parse_DEBUG YYDEBUG
  #endif
 #endif
 
 /* use goto to be compatible */
 #ifndef YY_parse_USE_GOTO
  #define YY_parse_USE_GOTO 1
 #endif
#endif

/* use no goto to be clean in C++ */
#ifndef YY_parse_USE_GOTO
 #define YY_parse_USE_GOTO 0
#endif

#ifndef YY_parse_PURE

 #line 130 "/usr/share/bison++/bison.cc"

#line 130 "/usr/share/bison++/bison.cc"
/*  YY_parse_PURE */
#endif

/* section apres lecture def, avant lecture grammaire S2 */

 #line 134 "/usr/share/bison++/bison.cc"
#ifndef YY_USE_CLASS
# ifndef YYSTYPE
#  define YYSTYPE int
#  define YYSTYPE_IS_TRIVIAL 1
# endif
#endif

#line 134 "/usr/share/bison++/bison.cc"
/* prefix */
#ifndef YY_parse_DEBUG

 #line 136 "/usr/share/bison++/bison.cc"
#define YY_parse_DEBUG 1

#line 136 "/usr/share/bison++/bison.cc"
/* YY_parse_DEBUG */
#endif


#ifndef YY_parse_LSP_NEEDED

 #line 141 "/usr/share/bison++/bison.cc"

#line 141 "/usr/share/bison++/bison.cc"
 /* YY_parse_LSP_NEEDED*/
#endif



/* DEFAULT LTYPE*/
#ifdef YY_parse_LSP_NEEDED
#ifndef YY_parse_LTYPE
#ifndef BISON_YYLTYPE_ISDECLARED
#define BISON_YYLTYPE_ISDECLARED
typedef
  struct yyltype
    {
      int timestamp;
      int first_line;
      int first_column;
      int last_line;
      int last_column;
      char *text;
   }
  yyltype;

#endif
#define YY_parse_LTYPE yyltype
#endif
#endif
/* DEFAULT STYPE*/
      /* We used to use `unsigned long' as YY_parse_STYPE on MSDOS,
	 but it seems better to be consistent.
	 Most programs should declare their own type anyway.  */

#ifndef YY_parse_STYPE
#define YY_parse_STYPE int
#endif
/* DEFAULT MISCELANEOUS */
#ifndef YY_parse_PARSE
#define YY_parse_PARSE yyparse
#endif
#ifndef YY_parse_LEX
#define YY_parse_LEX yylex
#endif
#ifndef YY_parse_LVAL
#define YY_parse_LVAL yylval
#endif
#ifndef YY_parse_LLOC
#define YY_parse_LLOC yylloc
#endif
#ifndef YY_parse_CHAR
#define YY_parse_CHAR yychar
#endif
#ifndef YY_parse_NERRS
#define YY_parse_NERRS yynerrs
#endif
#ifndef YY_parse_DEBUG_FLAG
#define YY_parse_DEBUG_FLAG yydebug
#endif
#ifndef YY_parse_ERROR
#define YY_parse_ERROR yyerror
#endif

#ifndef YY_parse_PARSE_PARAM
 #ifndef YY_USE_CLASS
  #ifdef YYPARSE_PARAM
   #define YY_parse_PARSE_PARAM void* YYPARSE_PARAM 
  #else
   #ifndef __STDC__
    #ifndef __cplusplus
     #define YY_parse_PARSE_PARAM
    #endif
   #endif
  #endif
 #endif
 #ifndef YY_parse_PARSE_PARAM
  #define YY_parse_PARSE_PARAM void
 #endif
#endif

#if YY_parse_COMPATIBILITY != 0
/* backward compatibility */
#ifdef YY_parse_LTYPE
#ifndef YYLTYPE
#define YYLTYPE YY_parse_LTYPE
#else
/* WARNING obsolete !!! user defined YYLTYPE not reported into generated header */
#endif
#endif

/* Removed due to bison compabilityproblems
/#ifndef YYSTYPE
/#define YYSTYPE YY_parse_STYPE
/#else*/
/* WARNING obsolete !!! user defined YYSTYPE not reported into generated header */
/*#endif*/

#ifdef YY_parse_PURE
#  ifndef YYPURE
#    define YYPURE YY_parse_PURE
#  endif
#endif

#ifdef YY_parse_DEBUG
#  ifndef YYDEBUG
#    define YYDEBUG YY_parse_DEBUG 
#  endif
#endif

#ifndef YY_parse_ERROR_VERBOSE
 #ifdef YYERROR_VERBOSE
  #define YY_parse_ERROR_VERBOSE YYERROR_VERBOSE
 #endif
#endif

#ifndef YY_parse_LSP_NEEDED
#  ifdef YYLSP_NEEDED
#    define YY_parse_LSP_NEEDED YYLSP_NEEDED
#  endif
#endif

#endif

#ifndef YY_USE_CLASS
/* TOKEN C */

 #line 263 "/usr/share/bison++/bison.cc"
#define	LEFTPAR	258
#define	RIGHTPAR	259
#define	NAME	260
#define	DEF_NAME	261
#define	TWODOTS	262
#define	HYPHEN	263
#define	DEFINE	264
#define	DOMAIN	265
#define	REQUIREMENTS	266
#define	CONSTANTS	267
#define	PREDICATES	268
#define	QUESTION	269
#define	EITHER	270
#define	NOT	271
#define	AND	272
#define	OR	273
#define	FORALL	274
#define	WHEN	275
#define	EQUAL	276
#define	ACTION	277
#define	OBSERVE	278
#define	EQUALITY	279
#define	CONDITIONAL_EFFECTS	280
#define	NEGATIVE_PRECONDITIONS	281
#define	PARAMETERS	282
#define	PRECONDITION	283
#define	EFFECT	284
#define	PROBLEM	285
#define	INIT	286
#define	GOAL	287
#define	STRUCTURAL	288
#define	SITUATION	289
#define	OBJECTS	290
#define	SERIAL	291
#define	PARALLEL	292
#define	INTEGER	293
#define	FLOAT	294
#define	SET	295
#define	TYPING	296
#define	STRIPS	297
#define	TYPES	298
#define	CERTAINTY	299
#define	KNOW	300
#define	UNKNOWN	301
#define	DEFINED	302
#define	FORMULA	303
#define	ONEOF	304


#line 263 "/usr/share/bison++/bison.cc"
 /* #defines tokens */
#else
/* CLASS */
#ifndef YY_parse_CLASS
#define YY_parse_CLASS parse
#endif
#ifndef YY_parse_INHERIT
#define YY_parse_INHERIT
#endif
#ifndef YY_parse_MEMBERS
#define YY_parse_MEMBERS 
#endif
#ifndef YY_parse_LEX_BODY
#define YY_parse_LEX_BODY  
#endif
#ifndef YY_parse_ERROR_BODY
#define YY_parse_ERROR_BODY  
#endif
#ifndef YY_parse_CONSTRUCTOR_PARAM
#define YY_parse_CONSTRUCTOR_PARAM
#endif
#ifndef YY_parse_CONSTRUCTOR_CODE
#define YY_parse_CONSTRUCTOR_CODE
#endif
#ifndef YY_parse_CONSTRUCTOR_INIT
#define YY_parse_CONSTRUCTOR_INIT
#endif
/* choose between enum and const */
#ifndef YY_parse_USE_CONST_TOKEN
#define YY_parse_USE_CONST_TOKEN 0
/* yes enum is more compatible with flex,  */
/* so by default we use it */ 
#endif
#if YY_parse_USE_CONST_TOKEN != 0
#ifndef YY_parse_ENUM_TOKEN
#define YY_parse_ENUM_TOKEN yy_parse_enum_token
#endif
#endif

class YY_parse_CLASS YY_parse_INHERIT
{
public: 
#if YY_parse_USE_CONST_TOKEN != 0
/* static const int token ... */

 #line 307 "/usr/share/bison++/bison.cc"
static const int LEFTPAR;
static const int RIGHTPAR;
static const int NAME;
static const int DEF_NAME;
static const int TWODOTS;
static const int HYPHEN;
static const int DEFINE;
static const int DOMAIN;
static const int REQUIREMENTS;
static const int CONSTANTS;
static const int PREDICATES;
static const int QUESTION;
static const int EITHER;
static const int NOT;
static const int AND;
static const int OR;
static const int FORALL;
static const int WHEN;
static const int EQUAL;
static const int ACTION;
static const int OBSERVE;
static const int EQUALITY;
static const int CONDITIONAL_EFFECTS;
static const int NEGATIVE_PRECONDITIONS;
static const int PARAMETERS;
static const int PRECONDITION;
static const int EFFECT;
static const int PROBLEM;
static const int INIT;
static const int GOAL;
static const int STRUCTURAL;
static const int SITUATION;
static const int OBJECTS;
static const int SERIAL;
static const int PARALLEL;
static const int INTEGER;
static const int FLOAT;
static const int SET;
static const int TYPING;
static const int STRIPS;
static const int TYPES;
static const int CERTAINTY;
static const int KNOW;
static const int UNKNOWN;
static const int DEFINED;
static const int FORMULA;
static const int ONEOF;


#line 307 "/usr/share/bison++/bison.cc"
 /* decl const */
#else
enum YY_parse_ENUM_TOKEN { YY_parse_NULL_TOKEN=0

 #line 310 "/usr/share/bison++/bison.cc"
	,LEFTPAR=258
	,RIGHTPAR=259
	,NAME=260
	,DEF_NAME=261
	,TWODOTS=262
	,HYPHEN=263
	,DEFINE=264
	,DOMAIN=265
	,REQUIREMENTS=266
	,CONSTANTS=267
	,PREDICATES=268
	,QUESTION=269
	,EITHER=270
	,NOT=271
	,AND=272
	,OR=273
	,FORALL=274
	,WHEN=275
	,EQUAL=276
	,ACTION=277
	,OBSERVE=278
	,EQUALITY=279
	,CONDITIONAL_EFFECTS=280
	,NEGATIVE_PRECONDITIONS=281
	,PARAMETERS=282
	,PRECONDITION=283
	,EFFECT=284
	,PROBLEM=285
	,INIT=286
	,GOAL=287
	,STRUCTURAL=288
	,SITUATION=289
	,OBJECTS=290
	,SERIAL=291
	,PARALLEL=292
	,INTEGER=293
	,FLOAT=294
	,SET=295
	,TYPING=296
	,STRIPS=297
	,TYPES=298
	,CERTAINTY=299
	,KNOW=300
	,UNKNOWN=301
	,DEFINED=302
	,FORMULA=303
	,ONEOF=304


#line 310 "/usr/share/bison++/bison.cc"
 /* enum token */
     }; /* end of enum declaration */
#endif
public:
 int YY_parse_PARSE (YY_parse_PARSE_PARAM);
 virtual void YY_parse_ERROR(char *msg) YY_parse_ERROR_BODY;
#ifdef YY_parse_PURE
#ifdef YY_parse_LSP_NEEDED
 virtual int  YY_parse_LEX (YY_parse_STYPE *YY_parse_LVAL,YY_parse_LTYPE *YY_parse_LLOC) YY_parse_LEX_BODY;
#else
 virtual int  YY_parse_LEX (YY_parse_STYPE *YY_parse_LVAL) YY_parse_LEX_BODY;
#endif
#else
 virtual int YY_parse_LEX() YY_parse_LEX_BODY;
 YY_parse_STYPE YY_parse_LVAL;
#ifdef YY_parse_LSP_NEEDED
 YY_parse_LTYPE YY_parse_LLOC;
#endif
 int   YY_parse_NERRS;
 int    YY_parse_CHAR;
#endif
#if YY_parse_DEBUG != 0
 int YY_parse_DEBUG_FLAG;   /*  nonzero means print parse trace     */
#endif
public:
 YY_parse_CLASS(YY_parse_CONSTRUCTOR_PARAM);
public:
 YY_parse_MEMBERS 
};
/* other declare folow */
#if YY_parse_USE_CONST_TOKEN != 0

 #line 341 "/usr/share/bison++/bison.cc"
const int YY_parse_CLASS::LEFTPAR=258;
const int YY_parse_CLASS::RIGHTPAR=259;
const int YY_parse_CLASS::NAME=260;
const int YY_parse_CLASS::DEF_NAME=261;
const int YY_parse_CLASS::TWODOTS=262;
const int YY_parse_CLASS::HYPHEN=263;
const int YY_parse_CLASS::DEFINE=264;
const int YY_parse_CLASS::DOMAIN=265;
const int YY_parse_CLASS::REQUIREMENTS=266;
const int YY_parse_CLASS::CONSTANTS=267;
const int YY_parse_CLASS::PREDICATES=268;
const int YY_parse_CLASS::QUESTION=269;
const int YY_parse_CLASS::EITHER=270;
const int YY_parse_CLASS::NOT=271;
const int YY_parse_CLASS::AND=272;
const int YY_parse_CLASS::OR=273;
const int YY_parse_CLASS::FORALL=274;
const int YY_parse_CLASS::WHEN=275;
const int YY_parse_CLASS::EQUAL=276;
const int YY_parse_CLASS::ACTION=277;
const int YY_parse_CLASS::OBSERVE=278;
const int YY_parse_CLASS::EQUALITY=279;
const int YY_parse_CLASS::CONDITIONAL_EFFECTS=280;
const int YY_parse_CLASS::NEGATIVE_PRECONDITIONS=281;
const int YY_parse_CLASS::PARAMETERS=282;
const int YY_parse_CLASS::PRECONDITION=283;
const int YY_parse_CLASS::EFFECT=284;
const int YY_parse_CLASS::PROBLEM=285;
const int YY_parse_CLASS::INIT=286;
const int YY_parse_CLASS::GOAL=287;
const int YY_parse_CLASS::STRUCTURAL=288;
const int YY_parse_CLASS::SITUATION=289;
const int YY_parse_CLASS::OBJECTS=290;
const int YY_parse_CLASS::SERIAL=291;
const int YY_parse_CLASS::PARALLEL=292;
const int YY_parse_CLASS::INTEGER=293;
const int YY_parse_CLASS::FLOAT=294;
const int YY_parse_CLASS::SET=295;
const int YY_parse_CLASS::TYPING=296;
const int YY_parse_CLASS::STRIPS=297;
const int YY_parse_CLASS::TYPES=298;
const int YY_parse_CLASS::CERTAINTY=299;
const int YY_parse_CLASS::KNOW=300;
const int YY_parse_CLASS::UNKNOWN=301;
const int YY_parse_CLASS::DEFINED=302;
const int YY_parse_CLASS::FORMULA=303;
const int YY_parse_CLASS::ONEOF=304;


#line 341 "/usr/share/bison++/bison.cc"
 /* const YY_parse_CLASS::token */
#endif
/*apres const  */
YY_parse_CLASS::YY_parse_CLASS(YY_parse_CONSTRUCTOR_PARAM) YY_parse_CONSTRUCTOR_INIT
{
#if YY_parse_DEBUG != 0
YY_parse_DEBUG_FLAG=0;
#endif
YY_parse_CONSTRUCTOR_CODE;
};
#endif

 #line 352 "/usr/share/bison++/bison.cc"


#define	YYFINAL		235
#define	YYFLAG		-32768
#define	YYNTBASE	50

#define YYTRANSLATE(x) ((unsigned)(x) <= 304 ? yytranslate[x] : 108)

static const char yytranslate[] = {     0,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     2,     2,     2,     2,     2,
     2,     2,     2,     2,     2,     1,     2,     3,     4,     5,
     6,     7,     8,     9,    10,    11,    12,    13,    14,    15,
    16,    17,    18,    19,    20,    21,    22,    23,    24,    25,
    26,    27,    28,    29,    30,    31,    32,    33,    34,    35,
    36,    37,    38,    39,    40,    41,    42,    43,    44,    45,
    46,    47,    48,    49
};

#if YY_parse_DEBUG != 0
static const short yyprhs[] = {     0,
     0,     2,     5,     8,     9,    10,    11,    12,    26,    30,
    33,    36,    39,    42,    45,    48,    51,    53,    55,    57,
    59,    61,    63,    66,    69,    71,    76,    78,    80,    82,
    84,    86,    88,    93,    97,   102,   106,   111,   115,   118,
   120,   123,   125,   128,   129,   131,   134,   137,   140,   142,
   147,   149,   151,   156,   159,   161,   163,   165,   169,   172,
   173,   178,   181,   184,   187,   189,   193,   196,   197,   202,
   205,   207,   212,   214,   219,   224,   229,   234,   239,   247,
   250,   252,   257,   262,   265,   266,   268,   270,   273,   275,
   277,   281,   284,   287,   289,   291,   297,   302,   310,   316,
   319,   321,   323,   328,   329,   330,   341,   344,   345,   349,
   353,   358,   363,   368,   374,   379,   382,   384,   389,   391
};

static const short yyrhs[] = {    51,
     0,    51,   101,     0,    51,    52,     0,     0,     0,     0,
     0,     3,     9,     3,    10,    73,     4,    53,     3,    56,
    54,    79,    55,     4,     0,    56,    57,     3,     0,    57,
     3,     0,    11,    58,     0,    43,    61,     0,    12,    62,
     0,    13,    75,     0,    59,     4,     0,    59,    60,     0,
    60,     0,    41,     0,    25,     0,    26,     0,    24,     0,
    42,     0,    64,     4,     0,    65,     4,     0,    73,     0,
     3,    15,    70,     4,     0,    67,     0,    70,     0,    68,
     0,    71,     0,    69,     0,    72,     0,    67,    70,     8,
    63,     0,    70,     8,    63,     0,    68,    71,     8,    63,
     0,    71,     8,    63,     0,    72,     8,    63,    69,     0,
    72,     8,    63,     0,    70,    73,     0,    73,     0,    71,
    73,     0,    73,     0,    74,    72,     0,     0,     5,     0,
    14,    73,     0,    76,     4,     0,    76,    77,     0,    77,
     0,     3,    78,    66,     4,     0,     5,     0,    21,     0,
    79,     3,    80,     4,     0,    80,     4,     0,    82,     0,
    86,     0,    22,     0,    81,    73,    83,     0,    83,    84,
     0,     0,    27,     3,    85,     4,     0,    28,    90,     0,
    29,    95,     0,    23,    95,     0,    66,     0,    47,    73,
    87,     0,    87,    88,     0,     0,    27,     3,    85,     4,
     0,    48,    90,     0,    92,     0,     3,    16,    92,     4,
     0,    92,     0,     3,    16,    90,     4,     0,     3,    46,
    90,     4,     0,     3,    17,    91,     4,     0,     3,    18,
    91,     4,     0,     3,    49,    91,     4,     0,     3,    19,
     3,    66,     4,    90,     4,     0,    91,    90,     0,    90,
     0,     3,    78,    93,     4,     0,     3,     6,    93,     4,
     0,    94,    93,     0,     0,    73,     0,    74,     0,    95,
    96,     0,    96,     0,    98,     0,     3,    98,     4,     0,
     3,     4,     0,    97,    98,     0,    98,     0,    89,     0,
     3,    40,    89,    90,     4,     0,     3,    17,    97,     4,
     0,     3,    19,     3,    66,     4,    98,     4,     0,     3,
    20,    90,   100,     4,     0,    99,    89,     0,    89,     0,
    89,     0,     3,    17,    99,     4,     0,     0,     0,     3,
     9,     3,    30,    73,     4,   102,   104,   103,     4,     0,
   104,   105,     0,     0,     3,    11,    58,     0,     3,    34,
   106,     0,     3,    33,    90,     4,     0,     3,    31,    91,
     4,     0,     3,    32,   107,     4,     0,     3,     7,    10,
    73,     4,     0,     3,    35,    65,     4,     0,    73,     4,
     0,    90,     0,     3,    45,    91,     4,     0,    44,     0,
     0
};

#endif

#if (YY_parse_DEBUG != 0) || defined(YY_parse_ERROR_VERBOSE) 
static const short yyrline[] = { 0,
   161,   165,   166,   167,   177,   181,   187,   199,   204,   205,
   208,   209,   210,   211,   214,   217,   221,   227,   231,   235,
   239,   252,   259,   262,   265,   273,   280,   281,   285,   286,
   294,   295,   298,   306,   316,   325,   336,   345,   353,   361,
   371,   380,   391,   399,   405,   408,   418,   422,   423,   427,
   448,   449,   456,   457,   460,   461,   464,   471,   548,   553,
   559,   565,   571,   577,   585,   595,   623,   628,   634,   640,
   648,   649,   656,   657,   671,   677,   683,   689,   695,   704,
   711,   720,   730,   740,   748,   754,   755,   759,   766,   773,
   783,   787,   795,   802,   812,   813,   820,   826,   833,   874,
   881,   891,   892,   907,   912,   918,   920,   921,   924,   925,
   926,   930,   934,   938,   939,   942,   945,   946,   952,   957
};

static const char * const yytname[] = {   "$","error","$illegal.","LEFTPAR",
"RIGHTPAR","NAME","DEF_NAME","TWODOTS","HYPHEN","DEFINE","DOMAIN","REQUIREMENTS",
"CONSTANTS","PREDICATES","QUESTION","EITHER","NOT","AND","OR","FORALL","WHEN",
"EQUAL","ACTION","OBSERVE","EQUALITY","CONDITIONAL_EFFECTS","NEGATIVE_PRECONDITIONS",
"PARAMETERS","PRECONDITION","EFFECT","PROBLEM","INIT","GOAL","STRUCTURAL","SITUATION",
"OBJECTS","SERIAL","PARALLEL","INTEGER","FLOAT","SET","TYPING","STRIPS","TYPES",
"CERTAINTY","KNOW","UNKNOWN","DEFINED","FORMULA","ONEOF","start","list_domain_problem",
"domain","@1","@2","@3","list_def","definition","require_def","list_require_key",
"require_key","types_def","constants_def","type","plain_or_typed_list_type",
"plain_or_typed_list_name","plain_or_typed_list_var","typed_list_type","typed_list_name",
"typed_list_var","list_type","list_name","list_var","name","variable","predicates_def",
"list_atomic_formula_skeleton","atomic_formula_skeleton","predicate","list_structure_def",
"structure_def","action_type","schema_def","list_schema_body","schema_body",
"list_parameters","defined_def","list_defined_body","defined_body","literal",
"formula","list_formula","atomic_formula","list_term","term","non_det_effect_list",
"non_det_effect","list_one_effect_formula","one_effect_formula","list_literal",
"list_atomic_effect","problem","@4","@5","list_def_prob","def_prob","situation_def",
"goal_formula",""
};
#endif

static const short yyr1[] = {     0,
    50,    51,    51,    51,    53,    54,    55,    52,    56,    56,
    57,    57,    57,    57,    58,    59,    59,    60,    60,    60,
    60,    60,    61,    62,    63,    63,    64,    64,    65,    65,
    66,    66,    67,    67,    68,    68,    69,    69,    70,    70,
    71,    71,    72,    72,    73,    74,    75,    76,    76,    77,
    78,    78,    79,    79,    80,    80,    81,    82,    83,    83,
    84,    84,    84,    84,    85,    86,    87,    87,    88,    88,
    89,    89,    90,    90,    90,    90,    90,    90,    90,    91,
    91,    92,    92,    93,    93,    94,    94,    95,    95,    95,
    96,    96,    97,    97,    98,    98,    98,    98,    98,    99,
    99,   100,   100,   102,   103,   101,   104,   104,   105,   105,
   105,   105,   105,   105,   105,   106,   107,   107,   107,   107
};

static const short yyr2[] = {     0,
     1,     2,     2,     0,     0,     0,     0,    13,     3,     2,
     2,     2,     2,     2,     2,     2,     1,     1,     1,     1,
     1,     1,     2,     2,     1,     4,     1,     1,     1,     1,
     1,     1,     4,     3,     4,     3,     4,     3,     2,     1,
     2,     1,     2,     0,     1,     2,     2,     2,     1,     4,
     1,     1,     4,     2,     1,     1,     1,     3,     2,     0,
     4,     2,     2,     2,     1,     3,     2,     0,     4,     2,
     1,     4,     1,     4,     4,     4,     4,     4,     7,     2,
     1,     4,     4,     2,     0,     1,     1,     2,     1,     1,
     3,     2,     2,     1,     1,     5,     4,     7,     5,     2,
     1,     1,     4,     0,     0,    10,     2,     0,     3,     3,
     4,     4,     4,     5,     4,     2,     1,     4,     1,     0
};

static const short yydefact[] = {     4,
     1,     0,     3,     2,     0,     0,     0,     0,    45,     0,
     0,     5,   104,     0,   108,     0,   105,     0,     0,     0,
     0,     6,     0,     0,     0,   107,    21,    19,    20,    18,
    22,    11,     0,    17,    13,     0,    29,    30,    42,     0,
    14,     0,    49,    12,     0,    27,    28,    40,     0,     0,
    10,     0,     0,     0,   120,     0,     0,     0,   106,    15,
    16,    24,     0,     0,    41,    51,    52,    44,    47,    48,
    23,     0,     0,    39,    57,     0,     7,     0,     0,    55,
    56,     9,     0,   109,     0,    81,     0,    73,     0,   119,
   117,     0,     0,     0,   110,     0,     0,     0,    36,    25,
     0,     0,    31,    32,    44,     0,    34,    68,     0,     0,
    54,    60,     0,    85,     0,     0,     0,     0,     0,     0,
    85,   112,    80,     0,   113,   111,   116,   115,    35,     0,
    46,    50,     0,    43,    33,    66,     0,     8,    58,   114,
    86,    87,     0,    85,     0,     0,     0,    44,     0,     0,
     0,     0,     0,    38,     0,     0,    67,    53,     0,     0,
     0,     0,    59,    83,    84,    74,    76,    77,     0,    75,
    78,    82,   118,    26,    37,     0,    44,    70,     0,    95,
    71,    64,    89,    90,    44,    62,    63,     0,    65,     0,
     0,    92,     0,     0,     0,     0,     0,     0,     0,    88,
     0,     0,    69,     0,     0,     0,    94,    44,     0,     0,
     0,    91,    61,    79,    72,    97,    93,     0,     0,   102,
     0,     0,     0,     0,    99,    96,     0,   101,     0,    98,
   103,   100,     0,     0,     0
};

static const short yydefgoto[] = {   233,
     1,     3,    14,    49,   110,    22,    23,    32,    33,    34,
    44,    35,    99,    45,    36,   189,    46,    37,   103,    47,
    38,   104,   100,   105,    41,    42,    43,   121,    77,    78,
    79,    80,   139,   163,   190,    81,   136,   157,   180,    86,
    87,    88,   143,   144,   182,   183,   206,   184,   229,   221,
     4,    15,    25,    17,    26,    95,    92
};

static const short yypact[] = {-32768,
    36,    40,-32768,-32768,    63,    32,    66,    66,-32768,    71,
    76,-32768,-32768,   108,-32768,    16,   111,   145,    66,   124,
    66,    16,   129,   146,   132,-32768,-32768,-32768,-32768,-32768,
-32768,-32768,   105,-32768,-32768,   140,    66,    60,-32768,    42,
-32768,     9,-32768,-32768,   155,    66,    74,-32768,   -14,   159,
-32768,   156,   145,   165,    13,   165,    66,    66,-32768,-32768,
-32768,-32768,    82,    95,-32768,-32768,-32768,   162,-32768,-32768,
-32768,   102,    95,-32768,-32768,    66,   170,   193,    66,-32768,
-32768,-32768,    66,-32768,    99,-32768,    90,-32768,     5,-32768,
-32768,   199,   213,   214,-32768,   215,    95,   206,-32768,-32768,
    66,   216,-32768,   217,   162,    95,-32768,-32768,   -14,   218,
-32768,-32768,   219,    29,   165,   165,   165,   221,   165,   165,
    29,-32768,-32768,   165,-32768,-32768,-32768,-32768,-32768,    66,
-32768,-32768,    95,-32768,-32768,   -18,   222,-32768,   173,-32768,
-32768,-32768,   223,    29,   224,   122,   151,   162,   225,   202,
   226,   204,   205,    38,   228,   165,-32768,-32768,   229,   230,
   165,   229,-32768,-32768,-32768,-32768,-32768,-32768,   231,-32768,
-32768,-32768,-32768,-32768,-32768,   217,   162,-32768,   118,-32768,
-32768,   233,-32768,-32768,   162,-32768,   233,   165,-32768,   234,
   144,-32768,   236,   237,   238,   165,   239,   240,   208,-32768,
   241,   242,-32768,   183,   243,   210,-32768,   162,   245,   169,
   165,-32768,-32768,-32768,-32768,-32768,-32768,   246,   177,-32768,
   247,   248,   237,   239,-32768,-32768,   249,-32768,   212,-32768,
-32768,-32768,   254,   255,-32768
};

static const short yypgoto[] = {-32768,
-32768,-32768,-32768,-32768,-32768,-32768,   227,   181,-32768,   232,
-32768,-32768,   -66,-32768,   179,   -65,-32768,-32768,    89,   -44,
   220,  -101,    -2,   -96,-32768,-32768,   235,   244,-32768,   147,
-32768,-32768,-32768,-32768,    73,-32768,-32768,-32768,   -57,   -55,
    75,  -121,  -107,-32768,    97,  -167,-32768,  -110,-32768,-32768,
-32768,-32768,-32768,-32768,-32768,-32768,-32768
};


#define	YYLAST		284


static const short yytable[] = {    91,
    93,    72,   102,   134,    10,    11,   107,    75,   155,    66,
   114,    40,    69,   151,   200,    89,    39,   142,    48,   200,
   115,   116,   117,   118,   142,    67,    18,    19,    20,   156,
   129,   123,    76,     9,    39,    65,   165,   181,     2,   135,
   181,     7,   101,    48,    74,   -44,    66,   142,     5,   124,
   119,   101,   176,   120,    94,    39,    90,   181,    21,   145,
    65,     8,    67,   149,     9,     6,   154,    64,   198,    74,
     9,   205,   181,   108,    12,   181,   112,   181,     9,    13,
   113,    73,   169,   207,   181,   153,     9,   181,   198,    97,
   123,   123,    85,   122,   123,   217,   123,    98,   131,     9,
   178,   181,   181,    66,   114,   186,     9,   181,    60,   106,
    16,   141,   227,    24,   115,   116,   117,   118,   141,    67,
   191,   192,    66,   114,    85,   167,    40,    48,    27,    28,
    29,    51,   202,   193,   194,    59,   195,   196,    67,   211,
   209,   141,   218,    62,   119,    30,    31,   120,    66,   114,
    74,   220,    52,    85,   168,   222,    53,   197,    71,   193,
   194,    82,   195,   196,    67,    83,   228,    85,    27,    28,
    29,   232,   109,    66,   114,   101,    54,    55,    56,    57,
    58,    66,   114,   197,   193,    30,    31,    66,   114,    67,
   146,   147,   193,   224,   150,   159,   111,    67,   152,   160,
   161,   162,   125,    67,    85,   171,    85,   173,   174,     9,
   191,   192,   191,   216,   210,   231,   126,   127,   128,   132,
   130,   138,   140,   148,   133,   158,   164,   166,   170,   172,
   177,   179,   185,    84,   188,   199,    96,   203,   204,   191,
   208,   210,   175,   212,   213,   214,   215,   219,    50,   223,
   225,   226,   230,   234,   235,   137,    63,   201,   187,     0,
     0,     0,     0,     0,    61,     0,     0,     0,     0,     0,
     0,     0,     0,     0,     0,     0,    70,     0,     0,     0,
     0,     0,     0,    68
};

static const short yycheck[] = {    55,
    56,    46,    68,   105,     7,     8,    73,    22,    27,     5,
     6,     3,     4,   121,   182,     3,    19,   114,    21,   187,
    16,    17,    18,    19,   121,    21,    11,    12,    13,    48,
    97,    87,    47,     5,    37,    38,   144,   159,     3,   106,
   162,    10,    14,    46,    47,     8,     5,   144,     9,    45,
    46,    14,   154,    49,    57,    58,    44,   179,    43,   115,
    63,    30,    21,   119,     5,     3,   133,     8,   179,    72,
     5,   193,   194,    76,     4,   197,    79,   199,     5,     4,
    83,     8,   148,   194,   206,   130,     5,   209,   199,     8,
   146,   147,     3,     4,   150,   206,   152,     3,   101,     5,
   156,   223,   224,     5,     6,   161,     5,   229,     4,     8,
     3,   114,   223,     3,    16,    17,    18,    19,   121,    21,
     3,     4,     5,     6,     3,     4,     3,   130,    24,    25,
    26,     3,   188,    16,    17,     4,    19,    20,    21,   197,
   196,   144,   208,     4,    46,    41,    42,    49,     5,     6,
   153,   209,     7,     3,     4,   211,    11,    40,     4,    16,
    17,     3,    19,    20,    21,    10,   224,     3,    24,    25,
    26,   229,     3,     5,     6,    14,    31,    32,    33,    34,
    35,     5,     6,    40,    16,    41,    42,     5,     6,    21,
   116,   117,    16,    17,   120,    23,     4,    21,   124,    27,
    28,    29,     4,    21,     3,     4,     3,     4,     4,     5,
     3,     4,     3,     4,     3,     4,     4,     4,     4,     4,
    15,     4,     4,     3,     8,     4,     4,     4,     4,     4,
     3,     3,     3,    53,     4,     3,    58,     4,     3,     3,
     3,     3,   154,     4,     4,     4,     4,     3,    22,     4,
     4,     4,     4,     0,     0,   109,    37,   185,   162,    -1,
    -1,    -1,    -1,    -1,    33,    -1,    -1,    -1,    -1,    -1,
    -1,    -1,    -1,    -1,    -1,    -1,    42,    -1,    -1,    -1,
    -1,    -1,    -1,    40
};

#line 352 "/usr/share/bison++/bison.cc"
 /* fattrs + tables */

/* parser code folow  */


/* This is the parser code that is written into each bison parser
  when the %semantic_parser declaration is not specified in the grammar.
  It was written by Richard Stallman by simplifying the hairy parser
  used when %semantic_parser is specified.  */

/* Note: dollar marks section change
   the next  is replaced by the list of actions, each action
   as one case of the switch.  */ 

#if YY_parse_USE_GOTO != 0
/* 
 SUPRESSION OF GOTO : on some C++ compiler (sun c++)
  the goto is strictly forbidden if any constructor/destructor
  is used in the whole function (very stupid isn't it ?)
 so goto are to be replaced with a 'while/switch/case construct'
 here are the macro to keep some apparent compatibility
*/
#define YYGOTO(lb) {yy_gotostate=lb;continue;}
#define YYBEGINGOTO  enum yy_labels yy_gotostate=yygotostart; \
                     for(;;) switch(yy_gotostate) { case yygotostart: {
#define YYLABEL(lb) } case lb: {
#define YYENDGOTO } } 
#define YYBEGINDECLARELABEL enum yy_labels {yygotostart
#define YYDECLARELABEL(lb) ,lb
#define YYENDDECLARELABEL  };
#else
/* macro to keep goto */
#define YYGOTO(lb) goto lb
#define YYBEGINGOTO 
#define YYLABEL(lb) lb:
#define YYENDGOTO
#define YYBEGINDECLARELABEL 
#define YYDECLARELABEL(lb)
#define YYENDDECLARELABEL 
#endif
/* LABEL DECLARATION */
YYBEGINDECLARELABEL
  YYDECLARELABEL(yynewstate)
  YYDECLARELABEL(yybackup)
/* YYDECLARELABEL(yyresume) */
  YYDECLARELABEL(yydefault)
  YYDECLARELABEL(yyreduce)
  YYDECLARELABEL(yyerrlab)   /* here on detecting error */
  YYDECLARELABEL(yyerrlab1)   /* here on error raised explicitly by an action */
  YYDECLARELABEL(yyerrdefault)  /* current state does not do anything special for the error token. */
  YYDECLARELABEL(yyerrpop)   /* pop the current state because it cannot handle the error token */
  YYDECLARELABEL(yyerrhandle)  
YYENDDECLARELABEL
/* ALLOCA SIMULATION */
/* __HAVE_NO_ALLOCA */
#ifdef __HAVE_NO_ALLOCA
int __alloca_free_ptr(char *ptr,char *ref)
{if(ptr!=ref) free(ptr);
 return 0;}

#define __ALLOCA_alloca(size) malloc(size)
#define __ALLOCA_free(ptr,ref) __alloca_free_ptr((char *)ptr,(char *)ref)

#ifdef YY_parse_LSP_NEEDED
#define __ALLOCA_return(num) \
            do { return( __ALLOCA_free(yyss,yyssa)+\
		    __ALLOCA_free(yyvs,yyvsa)+\
		    __ALLOCA_free(yyls,yylsa)+\
		   (num)); } while(0)
#else
#define __ALLOCA_return(num) \
            do { return( __ALLOCA_free(yyss,yyssa)+\
		    __ALLOCA_free(yyvs,yyvsa)+\
		   (num)); } while(0)
#endif
#else
#define __ALLOCA_return(num) do { return(num); } while(0)
#define __ALLOCA_alloca(size) alloca(size)
#define __ALLOCA_free(ptr,ref) 
#endif

/* ENDALLOCA SIMULATION */

#define yyerrok         (yyerrstatus = 0)
#define yyclearin       (YY_parse_CHAR = YYEMPTY)
#define YYEMPTY         -2
#define YYEOF           0
#define YYACCEPT        __ALLOCA_return(0)
#define YYABORT         __ALLOCA_return(1)
#define YYERROR         YYGOTO(yyerrlab1)
/* Like YYERROR except do call yyerror.
   This remains here temporarily to ease the
   transition to the new meaning of YYERROR, for GCC.
   Once GCC version 2 has supplanted version 1, this can go.  */
#define YYFAIL          YYGOTO(yyerrlab)
#define YYRECOVERING()  (!!yyerrstatus)
#define YYBACKUP(token, value) \
do                                                              \
  if (YY_parse_CHAR == YYEMPTY && yylen == 1)                               \
    { YY_parse_CHAR = (token), YY_parse_LVAL = (value);                 \
      yychar1 = YYTRANSLATE (YY_parse_CHAR);                                \
      YYPOPSTACK;                                               \
      YYGOTO(yybackup);                                            \
    }                                                           \
  else                                                          \
    { YY_parse_ERROR ("syntax error: cannot back up"); YYERROR; }   \
while (0)

#define YYTERROR        1
#define YYERRCODE       256

#ifndef YY_parse_PURE
/* UNPURE */
#define YYLEX           YY_parse_LEX()
#ifndef YY_USE_CLASS
/* If nonreentrant, and not class , generate the variables here */
int     YY_parse_CHAR;                      /*  the lookahead symbol        */
YY_parse_STYPE      YY_parse_LVAL;              /*  the semantic value of the */
				/*  lookahead symbol    */
int YY_parse_NERRS;                 /*  number of parse errors so far */
#ifdef YY_parse_LSP_NEEDED
YY_parse_LTYPE YY_parse_LLOC;   /*  location data for the lookahead     */
			/*  symbol                              */
#endif
#endif


#else
/* PURE */
#ifdef YY_parse_LSP_NEEDED
#define YYLEX           YY_parse_LEX(&YY_parse_LVAL, &YY_parse_LLOC)
#else
#define YYLEX           YY_parse_LEX(&YY_parse_LVAL)
#endif
#endif
#ifndef YY_USE_CLASS
#if YY_parse_DEBUG != 0
int YY_parse_DEBUG_FLAG;                    /*  nonzero means print parse trace     */
/* Since this is uninitialized, it does not stop multiple parsers
   from coexisting.  */
#endif
#endif



/*  YYINITDEPTH indicates the initial size of the parser's stacks       */

#ifndef YYINITDEPTH
#define YYINITDEPTH 200
#endif

/*  YYMAXDEPTH is the maximum size the stacks can grow to
    (effective only if the built-in stack extension method is used).  */

#if YYMAXDEPTH == 0
#undef YYMAXDEPTH
#endif

#ifndef YYMAXDEPTH
#define YYMAXDEPTH 10000
#endif


#if __GNUC__ > 1                /* GNU C and GNU C++ define this.  */
#define __yy_bcopy(FROM,TO,COUNT)       __builtin_memcpy(TO,FROM,COUNT)
#else                           /* not GNU C or C++ */

/* This is the most reliable way to avoid incompatibilities
   in available built-in functions on various systems.  */

#ifdef __cplusplus
static void __yy_bcopy (char *from, char *to, int count)
#else
#ifdef __STDC__
static void __yy_bcopy (char *from, char *to, int count)
#else
static void __yy_bcopy (from, to, count)
     char *from;
     char *to;
     int count;
#endif
#endif
{
  register char *f = from;
  register char *t = to;
  register int i = count;

  while (i-- > 0)
    *t++ = *f++;
}
#endif


int
#ifdef YY_USE_CLASS
 YY_parse_CLASS::
#endif
     YY_parse_PARSE(YY_parse_PARSE_PARAM)
#ifndef __STDC__
#ifndef __cplusplus
#ifndef YY_USE_CLASS
/* parameter definition without protypes */
YY_parse_PARSE_PARAM_DEF
#endif
#endif
#endif
{
  register int yystate;
  register int yyn;
  register short *yyssp;
  register YY_parse_STYPE *yyvsp;
  int yyerrstatus;      /*  number of tokens to shift before error messages enabled */
  int yychar1=0;          /*  lookahead token as an internal (translated) token number */

  short yyssa[YYINITDEPTH];     /*  the state stack                     */
  YY_parse_STYPE yyvsa[YYINITDEPTH];        /*  the semantic value stack            */

  short *yyss = yyssa;          /*  refer to the stacks thru separate pointers */
  YY_parse_STYPE *yyvs = yyvsa;     /*  to allow yyoverflow to reallocate them elsewhere */

#ifdef YY_parse_LSP_NEEDED
  YY_parse_LTYPE yylsa[YYINITDEPTH];        /*  the location stack                  */
  YY_parse_LTYPE *yyls = yylsa;
  YY_parse_LTYPE *yylsp;

#define YYPOPSTACK   (yyvsp--, yyssp--, yylsp--)
#else
#define YYPOPSTACK   (yyvsp--, yyssp--)
#endif

  int yystacksize = YYINITDEPTH;

#ifdef YY_parse_PURE
  int YY_parse_CHAR;
  YY_parse_STYPE YY_parse_LVAL;
  int YY_parse_NERRS;
#ifdef YY_parse_LSP_NEEDED
  YY_parse_LTYPE YY_parse_LLOC;
#endif
#endif

  YY_parse_STYPE yyval;             /*  the variable used to return         */
				/*  semantic values from the action     */
				/*  routines                            */

  int yylen;
/* start loop, in which YYGOTO may be used. */
YYBEGINGOTO

#if YY_parse_DEBUG != 0
  if (YY_parse_DEBUG_FLAG)
    fprintf(stderr, "Starting parse\n");
#endif
  yystate = 0;
  yyerrstatus = 0;
  YY_parse_NERRS = 0;
  YY_parse_CHAR = YYEMPTY;          /* Cause a token to be read.  */

  /* Initialize stack pointers.
     Waste one element of value and location stack
     so that they stay on the same level as the state stack.
     The wasted elements are never initialized.  */

  yyssp = yyss - 1;
  yyvsp = yyvs;
#ifdef YY_parse_LSP_NEEDED
  yylsp = yyls;
#endif

/* Push a new state, which is found in  yystate  .  */
/* In all cases, when you get here, the value and location stacks
   have just been pushed. so pushing a state here evens the stacks.  */
YYLABEL(yynewstate)

  *++yyssp = yystate;

  if (yyssp >= yyss + yystacksize - 1)
    {
      /* Give user a chance to reallocate the stack */
      /* Use copies of these so that the &'s don't force the real ones into memory. */
      YY_parse_STYPE *yyvs1 = yyvs;
      short *yyss1 = yyss;
#ifdef YY_parse_LSP_NEEDED
      YY_parse_LTYPE *yyls1 = yyls;
#endif

      /* Get the current used size of the three stacks, in elements.  */
      int size = yyssp - yyss + 1;

#ifdef yyoverflow
      /* Each stack pointer address is followed by the size of
	 the data in use in that stack, in bytes.  */
#ifdef YY_parse_LSP_NEEDED
      /* This used to be a conditional around just the two extra args,
	 but that might be undefined if yyoverflow is a macro.  */
      yyoverflow("parser stack overflow",
		 &yyss1, size * sizeof (*yyssp),
		 &yyvs1, size * sizeof (*yyvsp),
		 &yyls1, size * sizeof (*yylsp),
		 &yystacksize);
#else
      yyoverflow("parser stack overflow",
		 &yyss1, size * sizeof (*yyssp),
		 &yyvs1, size * sizeof (*yyvsp),
		 &yystacksize);
#endif

      yyss = yyss1; yyvs = yyvs1;
#ifdef YY_parse_LSP_NEEDED
      yyls = yyls1;
#endif
#else /* no yyoverflow */
      /* Extend the stack our own way.  */
      if (yystacksize >= YYMAXDEPTH)
	{
	  YY_parse_ERROR("parser stack overflow");
	  __ALLOCA_return(2);
	}
      yystacksize *= 2;
      if (yystacksize > YYMAXDEPTH)
	yystacksize = YYMAXDEPTH;
      yyss = (short *) __ALLOCA_alloca (yystacksize * sizeof (*yyssp));
      __yy_bcopy ((char *)yyss1, (char *)yyss, size * sizeof (*yyssp));
      __ALLOCA_free(yyss1,yyssa);
      yyvs = (YY_parse_STYPE *) __ALLOCA_alloca (yystacksize * sizeof (*yyvsp));
      __yy_bcopy ((char *)yyvs1, (char *)yyvs, size * sizeof (*yyvsp));
      __ALLOCA_free(yyvs1,yyvsa);
#ifdef YY_parse_LSP_NEEDED
      yyls = (YY_parse_LTYPE *) __ALLOCA_alloca (yystacksize * sizeof (*yylsp));
      __yy_bcopy ((char *)yyls1, (char *)yyls, size * sizeof (*yylsp));
      __ALLOCA_free(yyls1,yylsa);
#endif
#endif /* no yyoverflow */

      yyssp = yyss + size - 1;
      yyvsp = yyvs + size - 1;
#ifdef YY_parse_LSP_NEEDED
      yylsp = yyls + size - 1;
#endif

#if YY_parse_DEBUG != 0
      if (YY_parse_DEBUG_FLAG)
	fprintf(stderr, "Stack size increased to %d\n", yystacksize);
#endif

      if (yyssp >= yyss + yystacksize - 1)
	YYABORT;
    }

#if YY_parse_DEBUG != 0
  if (YY_parse_DEBUG_FLAG)
    fprintf(stderr, "Entering state %d\n", yystate);
#endif

  YYGOTO(yybackup);
YYLABEL(yybackup)

/* Do appropriate processing given the current state.  */
/* Read a lookahead token if we need one and don't already have one.  */
/* YYLABEL(yyresume) */

  /* First try to decide what to do without reference to lookahead token.  */

  yyn = yypact[yystate];
  if (yyn == YYFLAG)
    YYGOTO(yydefault);

  /* Not known => get a lookahead token if don't already have one.  */

  /* yychar is either YYEMPTY or YYEOF
     or a valid token in external form.  */

  if (YY_parse_CHAR == YYEMPTY)
    {
#if YY_parse_DEBUG != 0
      if (YY_parse_DEBUG_FLAG)
	fprintf(stderr, "Reading a token: ");
#endif
      YY_parse_CHAR = YYLEX;
    }

  /* Convert token to internal form (in yychar1) for indexing tables with */

  if (YY_parse_CHAR <= 0)           /* This means end of input. */
    {
      yychar1 = 0;
      YY_parse_CHAR = YYEOF;                /* Don't call YYLEX any more */

#if YY_parse_DEBUG != 0
      if (YY_parse_DEBUG_FLAG)
	fprintf(stderr, "Now at end of input.\n");
#endif
    }
  else
    {
      yychar1 = YYTRANSLATE(YY_parse_CHAR);

#if YY_parse_DEBUG != 0
      if (YY_parse_DEBUG_FLAG)
	{
	  fprintf (stderr, "Next token is %d (%s", YY_parse_CHAR, yytname[yychar1]);
	  /* Give the individual parser a way to print the precise meaning
	     of a token, for further debugging info.  */
#ifdef YYPRINT
	  YYPRINT (stderr, YY_parse_CHAR, YY_parse_LVAL);
#endif
	  fprintf (stderr, ")\n");
	}
#endif
    }

  yyn += yychar1;
  if (yyn < 0 || yyn > YYLAST || yycheck[yyn] != yychar1)
    YYGOTO(yydefault);

  yyn = yytable[yyn];

  /* yyn is what to do for this token type in this state.
     Negative => reduce, -yyn is rule number.
     Positive => shift, yyn is new state.
       New state is final state => don't bother to shift,
       just return success.
     0, or most negative number => error.  */

  if (yyn < 0)
    {
      if (yyn == YYFLAG)
	YYGOTO(yyerrlab);
      yyn = -yyn;
      YYGOTO(yyreduce);
    }
  else if (yyn == 0)
    YYGOTO(yyerrlab);

  if (yyn == YYFINAL)
    YYACCEPT;

  /* Shift the lookahead token.  */

#if YY_parse_DEBUG != 0
  if (YY_parse_DEBUG_FLAG)
    fprintf(stderr, "Shifting token %d (%s), ", YY_parse_CHAR, yytname[yychar1]);
#endif

  /* Discard the token being shifted unless it is eof.  */
  if (YY_parse_CHAR != YYEOF)
    YY_parse_CHAR = YYEMPTY;

  *++yyvsp = YY_parse_LVAL;
#ifdef YY_parse_LSP_NEEDED
  *++yylsp = YY_parse_LLOC;
#endif

  /* count tokens shifted since error; after three, turn off error status.  */
  if (yyerrstatus) yyerrstatus--;

  yystate = yyn;
  YYGOTO(yynewstate);

/* Do the default action for the current state.  */
YYLABEL(yydefault)

  yyn = yydefact[yystate];
  if (yyn == 0)
    YYGOTO(yyerrlab);

/* Do a reduction.  yyn is the number of a rule to reduce with.  */
YYLABEL(yyreduce)
  yylen = yyr2[yyn];
  if (yylen > 0)
    yyval = yyvsp[1-yylen]; /* implement default value of the action */

#if YY_parse_DEBUG != 0
  if (YY_parse_DEBUG_FLAG)
    {
      int i;

      fprintf (stderr, "Reducing via rule %d (line %d), ",
	       yyn, yyrline[yyn]);

      /* Print the symbols being reduced, and their result.  */
      for (i = yyprhs[yyn]; yyrhs[i] > 0; i++)
	fprintf (stderr, "%s ", yytname[yyrhs[i]]);
      fprintf (stderr, " -> %s\n", yytname[yyr1[yyn]]);
    }
#endif


 #line 839 "/usr/share/bison++/bison.cc"

  switch (yyn) {

case 5:
#line 178 "parser.y"
{
			 _low_domainName = yyvsp[-1].ident;
		       ;
    break;}
case 6:
#line 182 "parser.y"
{
			 idMatchArgsVars( initialSituation, NULL );
			 idMatchArgsVars( goalSituation, NULL );
		       ;
    break;}
case 7:
#line 187 "parser.y"
{
			 /* how much parameters can an schema have? */
			 for( schema_t *sch = schemas; sch != NULL; sch = sch->next )
			   {
			     int i;
			     idList_t *var;
			     for( var = sch->vars, i = 0; var != NULL; var = var->next, ++i );
			     maxParameters = MAX(maxParameters,i);
			   }
			 generateNames();
		       ;
    break;}
case 8:
#line 199 "parser.y"
{
			 domainParsed = 1;
		       ;
    break;}
case 16:
#line 218 "parser.y"
{
			 checkRequirement( yyvsp[0].integer );
		       ;
    break;}
case 17:
#line 222 "parser.y"
{
			 checkRequirement( yyvsp[0].integer );
		       ;
    break;}
case 18:
#line 228 "parser.y"
{
			 yyval.integer = TYPING;
		       ;
    break;}
case 19:
#line 232 "parser.y"
{
			 yyval.integer = CONDITIONAL_EFFECTS;
		       ;
    break;}
case 20:
#line 236 "parser.y"
{
			 yyval.integer = NEGATIVE_PRECONDITIONS;
		       ;
    break;}
case 21:
#line 240 "parser.y"
{
			 yyval.integer = EQUALITY;

			 /* create the equal predicate */
			 formula_t *pred = (formula_t*)malloc( sizeof( formula_t ) );
			 pred->type = ATOMIC_FORMULA;
			 pred->u.atomic.id = ++_low_numberPredicates;
			 pred->u.atomic.neg = 0;
			 pred->u.atomic.equal = 1;
			 pred->u.atomic.name = strdup( "=" );
			 predicates[pred->u.atomic.name] = pred;
		       ;
    break;}
case 22:
#line 253 "parser.y"
{
			 yyval.integer = STRIPS;
		       ;
    break;}
case 25:
#line 266 "parser.y"
{
			 yyval.idlist = (idList_t*)malloc( sizeof( idList_t ) );
			 yyval.idlist->id = 0;
			 yyval.idlist->name = yyvsp[0].ident;
			 yyval.idlist->type = NULL;
			 yyval.idlist->next = NULL;
		       ;
    break;}
case 26:
#line 274 "parser.y"
{
			 yyval.idlist = yyvsp[-1].idlist;
		       ;
    break;}
case 30:
#line 287 "parser.y"
{
			 for( idList_t *id = yyvsp[0].idlist; id != NULL; id = id->next )
			   objects[id->name] = id;
		       ;
    break;}
case 33:
#line 299 "parser.y"
{
			 for( idList_t *id = yyvsp[-2].idlist; id != NULL; id = id->next )
			   {
			     id->type = yyvsp[0].idlist;
			     types[id->name] = id;
			   }
		       ;
    break;}
case 34:
#line 307 "parser.y"
{
			 for( idList_t *id = yyvsp[-2].idlist; id != NULL; id = id->next )
			   {
			     id->type = yyvsp[0].idlist;
			     types[id->name] = id;
			   }
		       ;
    break;}
case 35:
#line 317 "parser.y"
{
			 for( idList_t *id = yyvsp[-2].idlist; id != NULL; id = id->next )
			   {
			     id->type = yyvsp[0].idlist;
			     objects[id->name] = id;
			     //xxxx printf( "object %s has id %d\n", id->name, id->id );
			   }
		       ;
    break;}
case 36:
#line 326 "parser.y"
{
			 for( idList_t *id = yyvsp[-2].idlist; id != NULL; id = id->next )
			   {
			     id->type = yyvsp[0].idlist;
			     objects[id->name] = id;
			     //xxxx printf( "object %s has id %d\n", id->name, id->id );
			   }
		       ;
    break;}
case 37:
#line 337 "parser.y"
{
			 idList_t *name;
			 for( name = yyvsp[-3].idlist; name->next != NULL; name = name->next )
			   name->type = yyvsp[-1].idlist;
			 name->type = yyvsp[-1].idlist;
			 name->next = yyvsp[0].idlist;
			 yyval.idlist = yyvsp[-3].idlist;
		       ;
    break;}
case 38:
#line 346 "parser.y"
{
			 for( idList_t *name = yyvsp[-2].idlist; name != NULL; name = name->next )
			   name->type = yyvsp[0].idlist;
			 yyval.idlist = yyvsp[-2].idlist;
		       ;
    break;}
case 39:
#line 354 "parser.y"
{
			 yyval.idlist = (idList_t*)malloc( sizeof( idList_t ) );
			 yyval.idlist->id = 0;
			 yyval.idlist->name = yyvsp[0].ident;
			 yyval.idlist->type = NULL;
			 yyval.idlist->next = yyvsp[-1].idlist;
		       ;
    break;}
case 40:
#line 362 "parser.y"
{
			 yyval.idlist = (idList_t*)malloc( sizeof( idList_t ) );
			 yyval.idlist->id = 0;
			 yyval.idlist->name = yyvsp[0].ident;
			 yyval.idlist->type = NULL;
			 yyval.idlist->next = NULL;
		       ;
    break;}
case 41:
#line 372 "parser.y"
{
			 yyval.idlist = (idList_t*)malloc( sizeof( idList_t ) );
			 yyval.idlist->id = ++numberObjects;
			 yyval.idlist->name = yyvsp[0].ident;
			 yyval.idlist->type = NULL;
			 yyval.idlist->next = yyvsp[-1].idlist;
			 //objects[$$->name] = $$;
		       ;
    break;}
case 42:
#line 381 "parser.y"
{
			 yyval.idlist = (idList_t*)malloc( sizeof( idList_t ) );
			 yyval.idlist->id = ++numberObjects;
			 yyval.idlist->name = yyvsp[0].ident;
			 yyval.idlist->type = NULL;
			 yyval.idlist->next = NULL;
			 //objects[$$->name] = $$;
		       ;
    break;}
case 43:
#line 392 "parser.y"
{
			 yyval.idlist = (idList_t*)malloc( sizeof( idList_t ) );
			 yyval.idlist->id = 0;
			 yyval.idlist->name = yyvsp[-1].ident;
			 yyval.idlist->type = NULL;
			 yyval.idlist->next = yyvsp[0].idlist;
		       ;
    break;}
case 44:
#line 400 "parser.y"
{  
			 yyval.idlist = NULL;
		       ;
    break;}
case 46:
#line 409 "parser.y"
{
			 yyval.ident = (char*)malloc( strlen( yyvsp[0].ident ) + 2 );
			 yyval.ident[0] = '\0';
			 strcat( yyval.ident, "?" );
			 strcat( yyval.ident, yyvsp[0].ident );
			 free( yyvsp[0].ident );
		       ;
    break;}
case 50:
#line 428 "parser.y"
{
			 formula_t *pred = (formula_t*)malloc( sizeof( formula_t ) );
			 pred->type = ATOMIC_FORMULA;
			 pred->u.atomic.id = ++_low_numberPredicates;
			 pred->u.atomic.neg = 0;
			 pred->u.atomic.name = yyvsp[-2].ident;
			 pred->u.atomic.equal = 0;
			 pred->u.atomic.args = yyvsp[-1].idlist;
			 predicates[pred->u.atomic.name] = pred;
			 assert( pred->u.atomic.name != 0 );
			 // AQUI!!!
			 for( str2wff_t::iterator it = predicates.begin(); 
			      it != predicates.end(); 
			      it++ )
			   assert( it->first != 0 );
			 cout << "predicates size = " << predicates.size() 
			      << " for name = " << predicates[pred->u.atomic.name]->u.atomic.name << endl;
		       ;
    break;}
case 52:
#line 450 "parser.y"
{
			 yyval.ident = "=";
		       ;
    break;}
case 57:
#line 465 "parser.y"
{
			 yyval.integer = ACTION;
		       ;
    break;}
case 58:
#line 472 "parser.y"
{
			 formula_t *f1, *f2, *f3;

			 schema_t *schema = (schema_t*)malloc( sizeof( schema_t ) );
			 schema->name = yyvsp[-1].ident;
			 schema->vars = NULL;
			 schema->prec = NULL;
			 schema->effect = NULL;
			 schema->next = NULL;

			 bool saw_effect = false, saw_observe = false;
			 for( body_t *body = yyvsp[0].body; body != NULL; body = body->next )
			   switch( body->type )
			     {
			     case PARAMETERS:
			       schema->vars = body->u.parameters;
			       break;
			     case PRECONDITION:
			       schema->prec = body->u.formula;
			       break;
			     case EFFECT:
			       saw_effect= true;
			       schema->is_observation = false;
			       for( f1 = body->u.formula; f1 != NULL; f1 = f1->u.flist.next )
				 {
				   f2 = (formula_t*)malloc( sizeof( formula_t ) );
				   f2->type = LIST_FORMULA;
				   f2->u.flist.formula = unfoldQuantifiers( f1->u.flist.formula );
				   f2->u.flist.formula = linearizeEffect( f2->u.flist.formula, f3 );
				   f2->u.flist.next = schema->effect;
				   schema->effect = f2;
				 }
			       break;
			     case OBSERVE:
			       saw_observe = true;
			       schema->is_observation = true;
			       observation_detected = true;
			       for( f1 = body->u.formula; f1 != NULL; f1 = f1->u.flist.next )
				 {
				   f2 = (formula_t*)malloc( sizeof( formula_t ) );
				   f2->type = LIST_FORMULA;
				   f2->u.flist.formula = unfoldQuantifiers( f1->u.flist.formula );
				   f2->u.flist.formula = linearizeEffect( f2->u.flist.formula, f3 );
				   f2->u.flist.next = schema->effect;
				   schema->effect = f2;
				 }
			       break;
			     }

			 assert( !saw_effect || !saw_observe );

			 /* if no effect, insert the empty effect */
			 if( !schema->effect )
			   {
			     f2 = (formula_t*)malloc( sizeof( formula_t ) );
			     f2->type = EMPTY_FORMULA;
			     schema->effect = (formula_t*)malloc( sizeof( formula_t ) );
			     schema->effect->type = LIST_FORMULA;
			     schema->effect->u.flist.formula = f2;
			     schema->effect->u.flist.next = NULL;
			   }

			 /* check and identify predicates and vars */
			 idMatchArgsVars( schema->prec, schema->vars );
			 idMatchArgsVars( schema->effect, schema->vars );
			 /* printSchema( stdout, schema ); printf( "\n" ); */

			 /* link schemas */
			 schema->next = schemas;
			 schemas = schema;

			 /* insert schema into schemaTable */
			 _low_schemaTable[_low_numberSchema++] = schema;
		       ;
    break;}
case 59:
#line 549 "parser.y"
{
			 yyvsp[0].body->next = yyvsp[-1].body;
			 yyval.body = yyvsp[0].body;
		       ;
    break;}
case 60:
#line 554 "parser.y"
{
			 yyval.body = NULL;
		       ;
    break;}
case 61:
#line 560 "parser.y"
{
			 yyval.body = (body_t*)malloc( sizeof( body_t ) );
			 yyval.body->type = PARAMETERS;
			 yyval.body->u.parameters = yyvsp[-1].idlist;
		       ;
    break;}
case 62:
#line 566 "parser.y"
{
			 yyval.body = (body_t*)malloc( sizeof( body_t ) );
			 yyval.body->type = PRECONDITION;
			 yyval.body->u.formula = yyvsp[0].formula;
		       ;
    break;}
case 63:
#line 572 "parser.y"
{
			 yyval.body = (body_t*)malloc( sizeof( body_t ) );
			 yyval.body->type = EFFECT;
			 yyval.body->u.formula = yyvsp[0].formula;
		       ;
    break;}
case 64:
#line 578 "parser.y"
{
			 yyval.body = (body_t*)malloc( sizeof( body_t ) );
			 yyval.body->type = OBSERVE;
			 yyval.body->u.formula = yyvsp[0].formula;
		       ;
    break;}
case 65:
#line 586 "parser.y"
{
			 int i;
			 idList_t *var;
			 for( i = 1, var = yyvsp[0].idlist; var != NULL; var = var->next )
			   var->id = i++;
			 yyval.idlist = yyvsp[0].idlist;
		       ;
    break;}
case 66:
#line 596 "parser.y"
{
			 formula_t *def = (formula_t*)malloc( sizeof( formula_t ) );
			 def->type = DEFINED_FORMULA;
			 for( body_t *body = yyvsp[0].body; body != NULL; body = body->next )
			   switch( body->type )
			     {
			     case PARAMETERS:
			       def->u.lambda.vars = body->u.parameters;
			       break;
			     case FORMULA:
			       def->u.lambda.formula = body->u.formula;
			       break;
			     }

			 /* check and identify predicates and vars */
			 idMatchArgsVars( def->u.lambda.formula, def->u.lambda.vars );

			 /* insert into defined table */
			 defined[yyvsp[-1].ident] = def;
			 /*
			   printf( "defined %s = ", $2 );
			   printFormula( stdout, def->u.lambda.formula );
			   printf( "\n" );
			 */
		       ;
    break;}
case 67:
#line 624 "parser.y"
{
			 yyvsp[0].body->next = yyvsp[-1].body;
			 yyval.body = yyvsp[0].body;
		       ;
    break;}
case 68:
#line 629 "parser.y"
{
			 yyval.body = NULL;
		       ;
    break;}
case 69:
#line 635 "parser.y"
{
			 yyval.body = (body_t*)malloc( sizeof( body_t ) );
			 yyval.body->type = PARAMETERS;
			 yyval.body->u.parameters = yyvsp[-1].idlist;
		       ;
    break;}
case 70:
#line 641 "parser.y"
{
			 yyval.body = (body_t*)malloc( sizeof( body_t ) );
			 yyval.body->type = FORMULA;
			 yyval.body->u.formula = yyvsp[0].formula;
		       ;
    break;}
case 72:
#line 650 "parser.y"
{
			 yyvsp[-1].formula->u.atomic.neg = 1;
			 yyval.formula = yyvsp[-1].formula;
		       ;
    break;}
case 74:
#line 658 "parser.y"
{
			 if( yyvsp[-1].formula->type == ATOMIC_FORMULA )
			   {
			     yyvsp[-1].formula->u.atomic.neg = (yyvsp[-1].formula->u.atomic.neg+1)%2;
			     yyval.formula = yyvsp[-1].formula;
			   }
			 else
			   {
			     yyval.formula = (formula_t*)malloc( sizeof( formula_t ) );
			     yyval.formula->type = NOT_FORMULA;
			     yyval.formula->u.formula = yyvsp[-1].formula;
			   }
		       ;
    break;}
case 75:
#line 672 "parser.y"
{
			 yyval.formula = (formula_t*)malloc( sizeof( formula_t ) );
			 yyval.formula->type = UNKNOWN_FORMULA;
			 yyval.formula->u.formula = yyvsp[-1].formula;
		       ;
    break;}
case 76:
#line 678 "parser.y"
{
			 yyval.formula = (formula_t*)malloc( sizeof( formula_t ) );
			 yyval.formula->type = AND_FORMULA;
			 yyval.formula->u.formula = yyvsp[-1].formula;
		       ;
    break;}
case 77:
#line 684 "parser.y"
{
			 yyval.formula = (formula_t*)malloc( sizeof( formula_t ) );
			 yyval.formula->type = OR_FORMULA;
			 yyval.formula->u.formula = yyvsp[-1].formula;
		       ;
    break;}
case 78:
#line 690 "parser.y"
{
			 yyval.formula = (formula_t*)malloc( sizeof( formula_t ) );
			 yyval.formula->type = ONEOF_FORMULA;
			 yyval.formula->u.formula = yyvsp[-1].formula;
		       ;
    break;}
case 79:
#line 696 "parser.y"
{
			 yyval.formula = (formula_t*)malloc( sizeof( formula_t ) );
			 yyval.formula->type = FORALL_FORMULA;
			 yyval.formula->u.lambda.vars = yyvsp[-3].idlist;
			 yyval.formula->u.lambda.formula = yyvsp[-1].formula;
		       ;
    break;}
case 80:
#line 705 "parser.y"
{
			 yyval.formula = (formula_t*)malloc( sizeof( formula_t ) );
			 yyval.formula->type = LIST_FORMULA;
			 yyval.formula->u.flist.formula = yyvsp[0].formula;
			 yyval.formula->u.flist.next = yyvsp[-1].formula;
		       ;
    break;}
case 81:
#line 712 "parser.y"
{
			 yyval.formula = (formula_t*)malloc( sizeof( formula_t ) );
			 yyval.formula->type = LIST_FORMULA;
			 yyval.formula->u.flist.formula = yyvsp[0].formula;
			 yyval.formula->u.flist.next = NULL;
		       ;
    break;}
case 82:
#line 721 "parser.y"
{
			 yyval.formula = (formula_t*)malloc( sizeof( formula_t ) );
			 yyval.formula->type = ATOMIC_FORMULA;
			 yyval.formula->u.atomic.id = -1;
			 yyval.formula->u.atomic.neg = 0;
			 yyval.formula->u.atomic.equal = 0;
			 yyval.formula->u.atomic.name = yyvsp[-2].ident;
			 yyval.formula->u.atomic.args = yyvsp[-1].idlist;
		       ;
    break;}
case 83:
#line 731 "parser.y"
{
			 instantiation_t *inst;
			 str2wff_t::iterator it;
			 it = defined.find( yyvsp[-2].ident );
			 inst = buildInstantiation( (*it).second->u.lambda.vars, yyvsp[-1].idlist );
			 yyval.formula = copyReplaceFormula( (*it).second->u.lambda.formula, inst );
		       ;
    break;}
case 84:
#line 741 "parser.y"
{
			 yyval.idlist = (idList_t*)malloc( sizeof( idList_t ) );
			 yyval.idlist->id = 0;
			 yyval.idlist->name = yyvsp[-1].ident;
			 yyval.idlist->type = NULL;
			 yyval.idlist->next = yyvsp[0].idlist;
		       ;
    break;}
case 85:
#line 749 "parser.y"
{  
			 yyval.idlist = NULL;
		       ;
    break;}
case 88:
#line 760 "parser.y"
{
			 yyval.formula = (formula_t*)malloc( sizeof( formula_t ) );
			 yyval.formula->type = LIST_FORMULA;
			 yyval.formula->u.flist.formula = yyvsp[0].formula;
			 yyval.formula->u.flist.next = yyvsp[-1].formula;
		       ;
    break;}
case 89:
#line 767 "parser.y"
{
			 yyval.formula = (formula_t*)malloc( sizeof( formula_t ) );
			 yyval.formula->type = LIST_FORMULA;
			 yyval.formula->u.flist.formula = yyvsp[0].formula;
			 yyval.formula->u.flist.next = NULL;
		       ;
    break;}
case 90:
#line 774 "parser.y"
{
			 yyval.formula = (formula_t*)malloc( sizeof( formula_t ) );
			 yyval.formula->type = LIST_FORMULA;
			 yyval.formula->u.flist.formula = yyvsp[0].formula;
			 yyval.formula->u.flist.next = NULL;
		       ;
    break;}
case 91:
#line 784 "parser.y"
{
			 yyval.formula = yyvsp[-1].formula;
		       ;
    break;}
case 92:
#line 788 "parser.y"
{
			 yyval.formula = (formula_t*)malloc( sizeof( formula_t ) );
			 yyval.formula->type = EMPTY_FORMULA;
		       ;
    break;}
case 93:
#line 796 "parser.y"
{
			 yyval.formula = (formula_t*)malloc( sizeof( formula_t ) );
			 yyval.formula->type = LIST_FORMULA;
			 yyval.formula->u.flist.formula = yyvsp[0].formula;
			 yyval.formula->u.flist.next = yyvsp[-1].formula;
		       ;
    break;}
case 94:
#line 803 "parser.y"
{
			 yyval.formula = (formula_t*)malloc( sizeof( formula_t ) );
			 yyval.formula->type = LIST_FORMULA;
			 yyval.formula->u.flist.formula = yyvsp[0].formula;
			 yyval.formula->u.flist.next = NULL;
		       ;
    break;}
case 96:
#line 814 "parser.y"
{
			 yyval.formula = (formula_t*)malloc( sizeof( formula_t ) );
			 yyval.formula->type = SET_FORMULA;
			 yyval.formula->u.fset.literal = yyvsp[-2].formula;
			 yyval.formula->u.fset.formula = yyvsp[-1].formula;
		       ;
    break;}
case 97:
#line 821 "parser.y"
{
			 yyval.formula = (formula_t*)malloc( sizeof( formula_t ) );
			 yyval.formula->type = AND_FORMULA;
			 yyval.formula->u.formula = yyvsp[-1].formula;
		       ;
    break;}
case 98:
#line 827 "parser.y"
{
			 yyval.formula = (formula_t*)malloc( sizeof( formula_t ) );
			 yyval.formula->type = FORALL_EFFECT;
			 yyval.formula->u.lambda.vars = yyvsp[-3].idlist;
			 yyval.formula->u.lambda.formula = yyvsp[-1].formula;
		       ;
    break;}
case 99:
#line 834 "parser.y"
{
			 yyval.formula = (formula_t*)malloc( sizeof( formula_t ) );
			 if( yyvsp[-2].formula->type != OR_FORMULA )
			   {
			     yyval.formula->type = WHEN_EFFECT;
			     yyval.formula->u.when.formula = yyvsp[-2].formula;
			     yyval.formula->u.when.effect = yyvsp[-1].formula;
			   }
			 else
			   {
			     yyval.formula->type = AND_FORMULA;
			     formula_t* cont = (formula_t*)malloc( sizeof( formula_t ) );
			     yyval.formula->u.formula = cont;
			     formula_t* init = yyvsp[-2].formula->u.formula;
			     assert( init != NULL );
			     while( init != NULL )
			       {
				 assert( init->type == LIST_FORMULA );
				 cont->type = LIST_FORMULA;
				 // new When...
				 formula_t* newWhen = (formula_t*)malloc( sizeof( formula_t ) );
				 cont->u.flist.formula = newWhen;

				 newWhen->type = WHEN_EFFECT;
				 newWhen->u.when.formula = init->u.flist.formula;
				 newWhen->u.when.effect = copyReplaceFormula( yyvsp[-1].formula, NULL );

				 init = init->u.flist.next;
				 if( init != NULL )
				   {
				     cont->u.flist.next = (formula_t*)malloc( sizeof( formula_t ) );
				     cont = cont->u.flist.next;
				   }
				 else
				   cont->u.flist.next = NULL;
			       }
			   }
		       ;
    break;}
case 100:
#line 875 "parser.y"
{
			 yyval.formula = (formula_t*)malloc( sizeof( formula_t ) );
			 yyval.formula->type = LIST_FORMULA;
			 yyval.formula->u.flist.formula = yyvsp[0].formula;
			 yyval.formula->u.flist.next = yyvsp[-1].formula;
		       ;
    break;}
case 101:
#line 882 "parser.y"
{
			 yyval.formula = (formula_t*)malloc( sizeof( formula_t ) );
			 yyval.formula->type = LIST_FORMULA;
			 yyval.formula->u.flist.formula = yyvsp[0].formula;
			 yyval.formula->u.flist.next = NULL;
		       ;
    break;}
case 103:
#line 893 "parser.y"
{
			 yyval.formula = (formula_t*)malloc( sizeof( formula_t ) );
			 yyval.formula->type = AND_FORMULA;
			 yyval.formula = yyvsp[-1].formula;
		       ;
    break;}
case 104:
#line 908 "parser.y"
{
			 _low_problemName = yyvsp[-1].ident;
		       ;
    break;}
case 105:
#line 912 "parser.y"
{
			 idMatchArgsVars( initialSituation, NULL );
			 idMatchArgsVars( goalSituation, NULL );
			 generateNames();
		       ;
    break;}
case 111:
#line 927 "parser.y"
{
			 structural = yyvsp[-1].formula;
                       ;
    break;}
case 112:
#line 931 "parser.y"
{
			 initialSituation = yyvsp[-1].formula;
                       ;
    break;}
case 113:
#line 935 "parser.y"
{
			 goalSituation = yyvsp[-1].formula;
                       ;
    break;}
case 116:
#line 942 "parser.y"
{;
    break;}
case 118:
#line 947 "parser.y"
{
			 yyval.formula = (formula_t*)malloc( sizeof( formula_t ) );
			 yyval.formula->type = KNOW_FORMULA;
			 yyval.formula->u.formula = yyvsp[-1].formula;
		       ;
    break;}
case 119:
#line 953 "parser.y"
{
			 yyval.formula = (formula_t*)malloc( sizeof( formula_t ) );
			 yyval.formula->type = CERTAINTY_FORMULA;
		       ;
    break;}
case 120:
#line 958 "parser.y"
{
			 yyval.formula = (formula_t*)malloc( sizeof( formula_t ) );
			 yyval.formula->type = EMPTY_FORMULA;
		       ;
    break;}
}

#line 839 "/usr/share/bison++/bison.cc"
   /* the action file gets copied in in place of this dollarsign  */
  yyvsp -= yylen;
  yyssp -= yylen;
#ifdef YY_parse_LSP_NEEDED
  yylsp -= yylen;
#endif

#if YY_parse_DEBUG != 0
  if (YY_parse_DEBUG_FLAG)
    {
      short *ssp1 = yyss - 1;
      fprintf (stderr, "state stack now");
      while (ssp1 != yyssp)
	fprintf (stderr, " %d", *++ssp1);
      fprintf (stderr, "\n");
    }
#endif

  *++yyvsp = yyval;

#ifdef YY_parse_LSP_NEEDED
  yylsp++;
  if (yylen == 0)
    {
      yylsp->first_line = YY_parse_LLOC.first_line;
      yylsp->first_column = YY_parse_LLOC.first_column;
      yylsp->last_line = (yylsp-1)->last_line;
      yylsp->last_column = (yylsp-1)->last_column;
      yylsp->text = 0;
    }
  else
    {
      yylsp->last_line = (yylsp+yylen-1)->last_line;
      yylsp->last_column = (yylsp+yylen-1)->last_column;
    }
#endif

  /* Now "shift" the result of the reduction.
     Determine what state that goes to,
     based on the state we popped back to
     and the rule number reduced by.  */

  yyn = yyr1[yyn];

  yystate = yypgoto[yyn - YYNTBASE] + *yyssp;
  if (yystate >= 0 && yystate <= YYLAST && yycheck[yystate] == *yyssp)
    yystate = yytable[yystate];
  else
    yystate = yydefgoto[yyn - YYNTBASE];

  YYGOTO(yynewstate);

YYLABEL(yyerrlab)   /* here on detecting error */

  if (! yyerrstatus)
    /* If not already recovering from an error, report this error.  */
    {
      ++YY_parse_NERRS;

#ifdef YY_parse_ERROR_VERBOSE
      yyn = yypact[yystate];

      if (yyn > YYFLAG && yyn < YYLAST)
	{
	  int size = 0;
	  char *msg;
	  int x, count;

	  count = 0;
	  /* Start X at -yyn if nec to avoid negative indexes in yycheck.  */
	  for (x = (yyn < 0 ? -yyn : 0);
	       x < (sizeof(yytname) / sizeof(char *)); x++)
	    if (yycheck[x + yyn] == x)
	      size += strlen(yytname[x]) + 15, count++;
	  msg = (char *) malloc(size + 15);
	  if (msg != 0)
	    {
	      strcpy(msg, "parse error");

	      if (count < 5)
		{
		  count = 0;
		  for (x = (yyn < 0 ? -yyn : 0);
		       x < (sizeof(yytname) / sizeof(char *)); x++)
		    if (yycheck[x + yyn] == x)
		      {
			strcat(msg, count == 0 ? ", expecting `" : " or `");
			strcat(msg, yytname[x]);
			strcat(msg, "'");
			count++;
		      }
		}
	      YY_parse_ERROR(msg);
	      free(msg);
	    }
	  else
	    YY_parse_ERROR ("parse error; also virtual memory exceeded");
	}
      else
#endif /* YY_parse_ERROR_VERBOSE */
	YY_parse_ERROR("parse error");
    }

  YYGOTO(yyerrlab1);
YYLABEL(yyerrlab1)   /* here on error raised explicitly by an action */

  if (yyerrstatus == 3)
    {
      /* if just tried and failed to reuse lookahead token after an error, discard it.  */

      /* return failure if at end of input */
      if (YY_parse_CHAR == YYEOF)
	YYABORT;

#if YY_parse_DEBUG != 0
      if (YY_parse_DEBUG_FLAG)
	fprintf(stderr, "Discarding token %d (%s).\n", YY_parse_CHAR, yytname[yychar1]);
#endif

      YY_parse_CHAR = YYEMPTY;
    }

  /* Else will try to reuse lookahead token
     after shifting the error token.  */

  yyerrstatus = 3;              /* Each real token shifted decrements this */

  YYGOTO(yyerrhandle);

YYLABEL(yyerrdefault)  /* current state does not do anything special for the error token. */

#if 0
  /* This is wrong; only states that explicitly want error tokens
     should shift them.  */
  yyn = yydefact[yystate];  /* If its default is to accept any token, ok.  Otherwise pop it.*/
  if (yyn) YYGOTO(yydefault);
#endif

YYLABEL(yyerrpop)   /* pop the current state because it cannot handle the error token */

  if (yyssp == yyss) YYABORT;
  yyvsp--;
  yystate = *--yyssp;
#ifdef YY_parse_LSP_NEEDED
  yylsp--;
#endif

#if YY_parse_DEBUG != 0
  if (YY_parse_DEBUG_FLAG)
    {
      short *ssp1 = yyss - 1;
      fprintf (stderr, "Error: state stack now");
      while (ssp1 != yyssp)
	fprintf (stderr, " %d", *++ssp1);
      fprintf (stderr, "\n");
    }
#endif

YYLABEL(yyerrhandle)

  yyn = yypact[yystate];
  if (yyn == YYFLAG)
    YYGOTO(yyerrdefault);

  yyn += YYTERROR;
  if (yyn < 0 || yyn > YYLAST || yycheck[yyn] != YYTERROR)
    YYGOTO(yyerrdefault);

  yyn = yytable[yyn];
  if (yyn < 0)
    {
      if (yyn == YYFLAG)
	YYGOTO(yyerrpop);
      yyn = -yyn;
      YYGOTO(yyreduce);
    }
  else if (yyn == 0)
    YYGOTO(yyerrpop);

  if (yyn == YYFINAL)
    YYACCEPT;

#if YY_parse_DEBUG != 0
  if (YY_parse_DEBUG_FLAG)
    fprintf(stderr, "Shifting error token, ");
#endif

  *++yyvsp = YY_parse_LVAL;
#ifdef YY_parse_LSP_NEEDED
  *++yylsp = YY_parse_LLOC;
#endif

  yystate = yyn;
  YYGOTO(yynewstate);
/* end loop, in which YYGOTO may be used. */
  YYENDGOTO
}

/* END */

 #line 1038 "/usr/share/bison++/bison.cc"
#line 964 "parser.y"


void
yyerror( char const *s )
{
  printf( "%s:%d: %s\n", _low_yyfile, lineno, s );
}

static void
checkRequirement( int req )
{
  switch( req )
    {
    case EQUALITY:
      _low_requirements = _low_requirements | REQ_EQUALITY;
      break;
    case TYPING:
      _low_requirements = _low_requirements | REQ_TYPING;
      break;
    case STRIPS:
      _low_requirements = _low_requirements | REQ_STRIPS;
      break;
    case CONDITIONAL_EFFECTS:
      _low_requirements = _low_requirements | REQ_CONDITIONAL_EFFECTS;
      break;
    case NEGATIVE_PRECONDITIONS:
      _low_requirements = _low_requirements | REQ_NEGATIVE_PRECONDITIONS;
      break;
    default:
      printf( "parser(checkRequirement): not supported requirement %d\n", req );
    }
}

void
printAtomicFormulaPDDL( ostream& o, formula_t *formula )
{
  if( formula != NULL )
    {
      // negation?
      if( formula->u.atomic.neg == 1 )
	o << "(not ";
      o << "(";
      // print name
      o << (formula->u.atomic.equal==1?"=":formula->u.atomic.name);

      // args
      if( formula->u.atomic.args != NULL )
	{
	  o << "_";
	  for( idList_t *arg = formula->u.atomic.args; arg != NULL; arg = arg->next )
	    o << arg->name << (arg->next != NULL ? "_" : ")");
	}
      else
	o << ")";

      if( formula->u.atomic.neg == 1 )
	o << ")";
    }
}


void
printAtomicFormulaPDDLTrans( ostream& o, formula_t *formula, string (*trans)(int) )
{
  int atom = atomId( formula, 0 );
  o << trans(formula->u.atomic.neg?-atom:atom);
}

void
printAtomicFormula( FILE *file, formula_t *formula )
{
  if( formula != NULL )
    {
      // negation?
      if( formula->u.atomic.neg == 1 )
	fprintf( file, "(not " );

      // print name
      fprintf( file, "(%s ", (formula->u.atomic.equal==1?"=":formula->u.atomic.name) );

      // args
      if( formula->u.atomic.args != NULL )
	for( idList_t *arg = formula->u.atomic.args; arg != NULL; arg = arg->next )
	  fprintf( file, "%s%s", arg->name, (arg->next != NULL ? " " : ")") );
      else
	fprintf( file, ")" );

      if( formula->u.atomic.neg == 1 )
	fprintf( file, ")" );
    }
}

void
printFormula( FILE *file, formula_t *formula )
{
  formula_t *f;
  if( formula == NULL )
    fprintf( file, "(null)" );
  else
    {
      switch( formula->type )
	{
	case ATOMIC_FORMULA:
	  printAtomicFormula( file, formula );
	  break;
	case AND_FORMULA:
	  fprintf( file, "(and " );
	  printFormula( file, formula->u.formula );
	  fprintf( file, ")" );
	  break;
	case OR_FORMULA:
	  fprintf( file, "(or " );
	  printFormula( file, formula->u.formula );
	  fprintf( file, ")" );
	  break;
	case ONEOF_FORMULA:
	  fprintf( file, "(oneof " );
	  printFormula( file, formula->u.formula );
	  fprintf( file, ")" );
	  break;
	case NOT_FORMULA:
	  fprintf( file, "(not " );
	  printFormula( file, formula->u.formula );
	  fprintf( file, ")" );
	  break;
	case UNKNOWN_FORMULA:
	  fprintf( file, "(unknown " );
	  printFormula( file, formula->u.formula );
	  fprintf( file, ")" );
	  break;
	case FORALL_FORMULA:
	case FORALL_EFFECT:
	  fprintf( file, "(forall (" );
	  for( idList_t *var = formula->u.lambda.vars; var != NULL; var = var->next )
	    fprintf( file, "%s%s", var->name, (var->next != NULL ? " " : "") );
	  fprintf( file, ") " );
	  printFormula( file, formula->u.lambda.formula );
	  fprintf( file, ")" );
	  break;
	case LIST_FORMULA:
	  fprintf( file, "[" );
	  for( f = formula; f != NULL; f = f->u.flist.next )
	    {
	      printFormula( file, f->u.flist.formula );
	      if( f->u.flist.next != NULL )
		fprintf( file, " " );
	    }
	  fprintf( file, "]" );
	  break;
	case EMPTY_FORMULA:
	  fprintf( file, ":empty:" );
	  break;
	case CERTAINTY_FORMULA:
	  fprintf( file, ":certainty:" );
	  break;
	case ADD_FORMULA:
	  fprintf( file, "(+ " );
	  printFormula( file, formula->u.formula );
	  fprintf( file, ")" );
	  break;
	case KNOW_FORMULA:
	  fprintf( file, "(know " );
	  printFormula( file, formula->u.formula );
	  fprintf( file, ")" );
	  break;
	case WHEN_EFFECT:
	  fprintf( file, "\n(when " );
	  printFormula( file, formula->u.when.formula );
	  fprintf( file, " " );
	  printFormula( file, formula->u.when.effect );
	  fprintf( file, ")" );
	  break;
	default:
	  printf( "parse(printFormula): unexpected formula type %d\n", formula->type );
	  break;
	}
    }
}


void
printFormulaPDDL( ostream& out, formula_t *formula )
{
  formula_t *f;
  if( formula == NULL )
    out << "(null)";
  else
    {
      switch( formula->type )
	{
	case ATOMIC_FORMULA:
	  printAtomicFormulaPDDL( out, formula );
	  break;
	case AND_FORMULA:
	  out << "(and ";
	  printFormulaPDDL( out, formula->u.formula );
	  out << ")";
	  break;
	case OR_FORMULA:
	  out << "(or ";
	  printFormulaPDDL( out, formula->u.formula );
	  out << ")";
	  break;
	case ONEOF_FORMULA:
	  out << "(oneof ";
	  printFormulaPDDL( out, formula->u.formula );
	  out << ")";
	  break;
	case NOT_FORMULA:
	  out << "(not ";
	  printFormulaPDDL( out, formula->u.formula );
	  out << ")";
	  break;
	case UNKNOWN_FORMULA:
	  out << "(unknown ";
	  printFormulaPDDL( out, formula->u.formula );
	  out << ")";
	  break;
	case FORALL_FORMULA:
	case FORALL_EFFECT:
	  out << "(forall (";
	  for( idList_t *var = formula->u.lambda.vars; var != NULL; var = var->next )
	    out << var->name << (var->next != NULL ? " " : "");
	  out << ") ";
	  printFormulaPDDL( out, formula->u.lambda.formula );
	  out << ")";
	  break;
	case LIST_FORMULA:
	  {
	    // out << "(and ";
	  for( f = formula; f != NULL; f = f->u.flist.next )
	    {
	      printFormulaPDDL( out, f->u.flist.formula );
	      if( f->u.flist.next != NULL )
		out << " ";
	    }
	  //out << ")";
	  }
	  break;
	case EMPTY_FORMULA:
	  out << ":empty:";
	  break;
	case CERTAINTY_FORMULA:
	  out << ":certainty:";
	  break;
	case ADD_FORMULA:
	  out << "(+ ";
	  printFormulaPDDL( out, formula->u.formula );
	  out << ")";
	  break;
	case KNOW_FORMULA:
	  out << "(know ";
	  printFormulaPDDL( out, formula->u.formula );
	  out << ")";
	  break;
	case WHEN_EFFECT:
	  out << "\n(when ";
	  printFormulaPDDL( out, formula->u.when.formula );
	  out << " ";
	  out << "(and ";
	  printFormulaPDDL( out, formula->u.when.effect );
	  out << ")";
	  out << ")";
	  break;
	default:
	  printf( "parse(printFormulaPDDL): unexpected formula type %d\n", formula->type );
	  break;
	}
    }
}

void
printFormulaPDDLTrans( ostream& out, formula_t *formula, string (*trans)(int) )
{
  formula_t *f;
  if( formula == NULL )
    out << "(null)";
  else
    {
      switch( formula->type )
	{
	case ATOMIC_FORMULA:
	  printAtomicFormulaPDDLTrans( out, formula, trans );
	  break;
	case AND_FORMULA:
	  out << "(and ";
	  printFormulaPDDLTrans( out, formula->u.formula, trans );
	  out << ")";
	  break;
	case OR_FORMULA:
	  out << "(or ";
	  printFormulaPDDLTrans( out, formula->u.formula, trans );
	  out << ")";
	  break;
	case ONEOF_FORMULA:
	  out << "(oneof ";
	  printFormulaPDDLTrans( out, formula->u.formula, trans );
	  out << ")";
	  break;
	case NOT_FORMULA:
	  out << "(not ";
	  printFormulaPDDLTrans( out, formula->u.formula, trans );
	  out << ")";
	  break;
	case UNKNOWN_FORMULA:
	  out << "(unknown ";
	  printFormulaPDDLTrans( out, formula->u.formula, trans );
	  out << ")";
	  break;
	case FORALL_FORMULA:
	case FORALL_EFFECT:
	  out << "(forall (";
	  for( idList_t *var = formula->u.lambda.vars; var != NULL; var = var->next )
	    out << var->name << (var->next != NULL ? " " : "");
	  out << ") ";
	  printFormulaPDDLTrans( out, formula->u.lambda.formula, trans );
	  out << ")";
	  break;
	case LIST_FORMULA:
	  {
	    // out << "(and ";
	  for( f = formula; f != NULL; f = f->u.flist.next )
	    {
	      printFormulaPDDLTrans( out, f->u.flist.formula, trans );
	      if( f->u.flist.next != NULL )
		out << " ";
	    }
	  //out << ")";
	  }
	  break;
	case EMPTY_FORMULA:
	  out << ":empty:";
	  break;
	case CERTAINTY_FORMULA:
	  out << ":certainty:";
	  break;
	case ADD_FORMULA:
	  out << "(+ ";
	  printFormulaPDDLTrans( out, formula->u.formula, trans );
	  out << ")";
	  break;
	case KNOW_FORMULA:
	  out << "(know ";
	  printFormulaPDDLTrans( out, formula->u.formula, trans );
	  out << ")";
	  break;
	case WHEN_EFFECT:
	  out << "\n(when ";
	  printFormulaPDDLTrans( out, formula->u.when.formula, trans );
	  out << " ";
	  out << "(and ";
	  printFormulaPDDLTrans( out, formula->u.when.effect, trans );
	  out << ")";
	  out << ")";
	  break;
	default:
	  printf( "parse(printFormulaPDDLTrans): unexpected formula type %d\n", formula->type );
	  break;
	}
    }
}

void
printInitialPDDL( ostream& out, formula_t *formula )
{
  formula_t *f;
  if( formula == NULL )
    out << "(null)";
  else
    {
      switch( formula->type )
	{
	case ATOMIC_FORMULA:
	  printAtomicFormulaPDDL( out, formula );
	  break;
	case AND_FORMULA:
	  out << "(and ";
	  printInitialPDDL( out, formula->u.formula );
	  out << ")";
	  break;
	case OR_FORMULA:
	  out << "(or ";
	  printInitialPDDL( out, formula->u.formula );
	  out << ")";
	  break;
	case ONEOF_FORMULA:
/* 	  out << "(oneof "; */
/* 	  printInitialPDDL( out, formula->u.formula ); */
/* 	  out << ")"; */
	  break;
	case NOT_FORMULA:
	  out << "(not ";
	  printInitialPDDL( out, formula->u.formula );
	  out << ")";
	  break;
	case UNKNOWN_FORMULA:
/* 	  out << "(unknown "; */
/* 	  printInitialPDDL( out, formula->u.formula ); */
/* 	  out << ")"; */
	  break;
	case FORALL_FORMULA:
	case FORALL_EFFECT:
	  out << "(forall (";
	  for( idList_t *var = formula->u.lambda.vars; var != NULL; var = var->next )
	    out << var->name << (var->next != NULL ? " " : "");
	  out << ") ";
	  printInitialPDDL( out, formula->u.lambda.formula );
	  out << ")";
	  break;
	case LIST_FORMULA:
	  {
	    // out << "(and ";
	  for( f = formula; f != NULL; f = f->u.flist.next )
	    {
	      printInitialPDDL( out, f->u.flist.formula );
	      if( f->u.flist.next != NULL )
		out << " ";
	    }
	  //out << ")";
	  }
	  break;
	case EMPTY_FORMULA:
	  out << ":empty:";
	  break;
	case CERTAINTY_FORMULA:
	  out << ":certainty:";
	  break;
	case ADD_FORMULA:
	  out << "(+ ";
	  printInitialPDDL( out, formula->u.formula );
	  out << ")";
	  break;
	case KNOW_FORMULA:
	  out << "(know ";
	  printInitialPDDL( out, formula->u.formula );
	  out << ")";
	  break;
	case WHEN_EFFECT:
	  out << "\n(when ";
	  printInitialPDDL( out, formula->u.when.formula );
	  out << " ";
	  out << "(and ";
	  printInitialPDDL( out, formula->u.when.effect );
	  out << ")";
	  out << ")";
	  break;
	default:
	  printf( "parse(printInitialPDDL): unexpected formula type %d\n", formula->type );
	  break;
	}
    }
}

bool
isSimpleFormula( formula_t* formula )
{
  if( formula == NULL ) return false;
  switch( formula->type )
    {
    case ATOMIC_FORMULA:
      return true;
      break;
    default:
      return false;
    }
}

bool
isDISJUNCTION( formula_t *formula, bool accept_or = false )
{
  if( formula == NULL )
    return false;
  else
    {
      switch( formula->type )
	{
	case ATOMIC_FORMULA:
	  return true;
	case OR_FORMULA:
	  if( !accept_or )
	    return false;
	case ONEOF_FORMULA:
	  {
	    formula_t* f = formula->u.formula;
	    bool val = true;
	    for( f = formula; f != NULL; f = f->u.flist.next )
	      val = val && isSimpleFormula( f->u.flist.formula );
	    return val;
	  }
	case UNKNOWN_FORMULA:
 	  return isSimpleFormula( formula->u.formula );

	case LIST_FORMULA:
	case AND_FORMULA:
	case NOT_FORMULA: // Not only for vars
	case FORALL_FORMULA:
	case FORALL_EFFECT:
	  return false;
	case EMPTY_FORMULA:
	case CERTAINTY_FORMULA:
	case ADD_FORMULA:
	case KNOW_FORMULA:
	case WHEN_EFFECT:
	default:
	  printf( "parse(isDISJUNCTION): unexpected formula type %d\n", formula->type );
	  exit(1);
	}
    }
}

bool
isCNF( formula_t *formula, bool accept_or = false )
{
  formula_t *f;
  if( formula == NULL )
    return false;
  else
    {
      switch( formula->type )
	{
	case LIST_FORMULA:
	  {
	    bool val = true;
	    for( f = formula; f != NULL; f = f->u.flist.next )
	      val = val && isDISJUNCTION( f->u.flist.formula, accept_or );
	    return val;
	  }
	case AND_FORMULA:
	  return isCNF( formula->u.formula, accept_or );
	case ATOMIC_FORMULA:
	case OR_FORMULA:
	case ONEOF_FORMULA:
	case UNKNOWN_FORMULA:
 	  return isDISJUNCTION( formula->u.formula, accept_or );

	case NOT_FORMULA: // Not only for vars
	case FORALL_FORMULA:
	case FORALL_EFFECT:
	  return false;
	case EMPTY_FORMULA:
	case CERTAINTY_FORMULA:
	case ADD_FORMULA:
	case KNOW_FORMULA:
	case WHEN_EFFECT:
	default:
	  printf( "parse(isCNF): unexpected formula type %d\n", formula->type );
	  exit(1);
	}
    }
}

int
getSimpleFormula( formula_t* formula )
{
  if( formula == NULL ) return 0;
  switch( formula->type )
    {
    case ATOMIC_FORMULA:
      if( !formula->u.atomic.equal )
	{
	  int atom = atomId( formula, NULL );
	  assert( atom > 0 ); // Atom doesn't exist
	  atom = (formula->u.atomic.neg?-1:1) * atom;
	  return atom;
	}
    default:
      printf( "parse(getSimpleFormula): unexpected formula type %d\n", formula->type );
      exit(1);
    }
}

// do not accept not({and|or} ..)
// neither (or ... )
static void
collectConjFormulaAtoms( formula_t* formula, int* parameters, std::set<int> &atoms )
{
  if( formula == NULL ) return;
  switch( formula->type )
    {
    case ATOMIC_FORMULA:
      if( !formula->u.atomic.equal )
	{
	  int atom = atomId( formula, parameters );
	  if( atom <= 0 ) return; // Atom doesn't exist
	  atom = (formula->u.atomic.neg?-1:1)*atom;
	  atoms.insert( atom );
	}
      break;
    case LIST_FORMULA:
      collectConjFormulaAtoms( formula->u.flist.formula, parameters, atoms );
      collectConjFormulaAtoms( formula->u.flist.next, parameters, atoms );
      break;

    case AND_FORMULA:
    case NOT_FORMULA: 
    case UNKNOWN_FORMULA:
    case ONEOF_FORMULA:
    case OR_FORMULA:
    default:
      printf( "parser(collectConjFormulaAtoms): unexpected formula type %d\n", formula->type );
      break;
    }
}

#ifdef USE_CLAUSE

void
getDISJUNCTION( formula_t *formula, clauses& c_or, clauses& c_oneof, 
		set<int>& literals, bool accept_or = false )
{
  formula_t *f;
  if( formula == NULL )
    return;
  else
    {
      switch( formula->type )
	{
	case ATOMIC_FORMULA:
	  {
	    int lit = getSimpleFormula(formula);
	    assert( lit != 0 );
	    literals.insert( lit );
	  }
	  break;
	case OR_FORMULA:
	  assert( accept_or );
	case ONEOF_FORMULA:
	  {
	    formula_t* f = formula->u.formula;
	    clause c;
	    collectConjFormulaAtoms( f, NULL, c );
	    if( formula->type == ONEOF_FORMULA )
	      c_oneof.insert(c);
	    else
	      c_or.insert(c);
	    break;
	    for( f = formula; f != NULL; f = f->u.flist.next )
	      {
		int lit = getSimpleFormula( f->u.flist.formula );
		assert( lit != 0 );
		c.insert(lit);
	      }
	  }
	  break;
	case UNKNOWN_FORMULA:
	  break;
	case LIST_FORMULA:
	  {
	    formula_t* f = formula->u.formula;
	    for( f = formula; f != NULL; f = f->u.flist.next )
	      getDISJUNCTION( f->u.flist.formula, c_or, c_oneof, literals, accept_or );
	  }
	  break;

	case AND_FORMULA:
	case NOT_FORMULA: // Not only for vars
	case FORALL_FORMULA:
	case FORALL_EFFECT:
	case EMPTY_FORMULA:
	case CERTAINTY_FORMULA:
	case ADD_FORMULA:
	case KNOW_FORMULA:
	case WHEN_EFFECT:
	default:
	  printf( "parse(getDISJUNCTION): unexpected formula type %d\n", formula->type );
	  exit(1);
	}
    }
}

void
getCNF( formula_t *formula, clauses& c_or, clauses& c_oneof, set<int>& literals, bool accept_or = false )
{
  formula_t *f;
  if( formula == NULL )
    return;
  else
    {
      switch( formula->type )
	{
	case LIST_FORMULA:
	  for( f = formula; f != NULL; f = f->u.flist.next )
	    getCNF( f->u.flist.formula, c_or, c_oneof, literals, accept_or );
	  break;
	case AND_FORMULA:
	  getCNF( formula->u.formula, c_or, c_oneof, literals, accept_or );
	  break;
	case ATOMIC_FORMULA:
	case OR_FORMULA:
	case ONEOF_FORMULA:
	case UNKNOWN_FORMULA:
	  getDISJUNCTION( formula, c_or, c_oneof, literals, accept_or );
	  break;

	case NOT_FORMULA: // Not only for vars
	case FORALL_FORMULA:
	case FORALL_EFFECT:
	case EMPTY_FORMULA:
	case CERTAINTY_FORMULA:
	case ADD_FORMULA:
	case KNOW_FORMULA:
	case WHEN_EFFECT:
	default:
	  printf( "parse(getCNF): unexpected formula type %d\n", formula->type );
	  exit(1);
	}
    }
}

#endif

void
collectFormulaUncertainty( formula_t *formula, std::vector<formula_t*>& formulas )
{
  formula_t *f;
  if( formula != NULL )
    {
      switch( formula->type )
	{
	case EMPTY_FORMULA:
	case CERTAINTY_FORMULA:
	case ATOMIC_FORMULA:
	  // discard
	  break;
	case AND_FORMULA:
	  collectFormulaUncertainty( formula->u.formula, formulas );
	  break;
	case ONEOF_FORMULA:
	case OR_FORMULA:
	  for( f = formula->u.formula; f != NULL; f = f->u.flist.next )
	    if(!isSimpleFormula( f->u.flist.formula ))
	      {
		printf( "ERROR: collectFormulaUncertainty: complex formula inside ONEOF or OR\n");
		exit(1);
	      }
	  formulas.push_back( formula );
	  break;
	case UNKNOWN_FORMULA:
	  // CFF benchmarks includes unknown for every unknown atom
	  // instead follow conformant planning competition 2006
	  formulas.push_back( formula );
	  break;
	case LIST_FORMULA:
	  for( f = formula; f != NULL; f = f->u.flist.next )
	    collectFormulaUncertainty( f->u.flist.formula, formulas );
	  break;
	case FORALL_FORMULA:
	case FORALL_EFFECT:
	case ADD_FORMULA:
	case WHEN_EFFECT:
	case KNOW_FORMULA:
	case NOT_FORMULA: // Not of atoms are atoms. Other NOT are not allowed
	default:
	  printf( "ERROR: collectFormulaUncertainty: unexpected formula type %d\n", formula->type );
	  exit(1);
	}
    }
}

void
printSchema( FILE *file, schema_t *schema )
{
  fprintf( file, "BEGIN-SCHEMA %s:\n", schema->name );
  fprintf( file, "  PARAMETERS = " );
  for( idList_t *id = schema->vars; id != NULL; id = id->next )
    fprintf( file, "%s ", id->name );
  fprintf( file, "\n  PRECONDITION = " );
  printFormula( file, schema->prec );
  fprintf( file, "\n  EFFECT = " );
  printFormula( file, schema->effect );
  fprintf( file, "\nEND-SCHEMA\n" );
}


static void
generateNames( void )
{
  str2wff_t::iterator it;
  map<const char*,idList_t*,ltstr>::iterator it2;

  _low_schemaName = (char**)calloc( _low_numberSchema, sizeof( char* ) );
  _low_objectName = (char**)calloc( numberObjects, sizeof( char* ) );
  _low_predicateName = (char**)calloc( _low_numberPredicates, sizeof( char* ) );

  for( int i = 0; i < _low_numberSchema; ++i )
    _low_schemaName[i] = strdup( _low_schemaTable[i]->name );

  for( it = predicates.begin(); it != predicates.end(); ++it )
    {
      _low_predicateName[(*it).second->u.atomic.id-1] = strdup( (*it).second->u.atomic.name );
      //xxxx printf( "name for p%d = \"%s\"\n", (*it).second->u.atomic.id, (*it).second->u.atomic.name );
    }

  for( it2 = objects.begin(); it2 != objects.end(); ++it2 )
    _low_objectName[(*it2).second->id-1] = strdup( (*it2).second->name );
}

vector<formula_t* > later_formula;
vector<idList_t *> later_object;


// Rescue unbounded predicates and objects
void
rescue_later()
{
  for( vector<formula_t*>::iterator it3 = later_formula.begin(); it3 != later_formula.end(); ++it3 )
    {
      formula_t* formula = *it3;
      str2wff_t::iterator it =
	predicates.find( formula->u.atomic.name );
      if( it == predicates.end() )
	{
	  printf( "FALTAL: parser(idMatchArgsVars): no predicate for %s\n", formula->u.atomic.name );
	  exit(1);
	}
      else
	{
	  formula->u.atomic.id = (*it).second->u.atomic.id;
	  formula->u.atomic.equal = (*it).second->u.atomic.equal;
	}	
    }
  for( vector<idList_t*>::iterator it3 = later_object.begin(); it3 != later_object.end(); ++it3 )
    {
      idList_t *arg = *it3;
      map<const char*,idList_t*,ltstr>::iterator it2 = 
	objects.find( arg->name );
      if( it2 == objects.end() )
	{
	  printf( "FATAL: parser(idMatchArgsVars): no object for %s\n", arg->name );
	  exit(1);
	}
      else
	arg->id = (*it2).second->id;
    }
}

static void
idMatchArgsVars( formula_t *formula, idList_t *vars )
{
  idList_t *arg, *var;
  str2wff_t::iterator it;
  map<const char*,idList_t*,ltstr>::iterator it2;

  if( formula != NULL )
    switch( formula->type )
      {
      case ATOMIC_FORMULA:
	for( str2wff_t::iterator it3 = predicates.begin(); 
	     it3 != predicates.end(); 
	     it3++ )
	  assert( it3->first != 0 );
	assert( formula->u.atomic.name != 0 );
	it = predicates.find( formula->u.atomic.name );
	if( it == predicates.end() )
	  {
	    printf( "parser(idMatchArgsVars): no predicate for %s\n", formula->u.atomic.name );
	    later_formula.push_back( formula );
	  }
	else
	  {
	    formula->u.atomic.id = (*it).second->u.atomic.id;
	    formula->u.atomic.equal = (*it).second->u.atomic.equal;
	  }

	for( arg = formula->u.atomic.args; arg != NULL; arg = arg->next )
	  if( arg->name[0] == '?' )
	    {
	      for( var = vars; var != NULL; var = var->next )
		if( !strcasecmp( arg->name, var->name ) )
		  {
		    arg->id = var->id;
		    break;
		  }
	      if( var == NULL )
		printf( "parser(idMatchArgsVars): no variable for %s\n", arg->name );
	    }
	  else
	    {
	      it2 = objects.find( arg->name );
	      if( it2 == objects.end() )
		{ 
		  printf( "parser(idMatchArgsVars): no object for %s\n", arg->name );
		  later_object.push_back( arg );
		  if(0){
		  cout << "Objects: ";
		  for( it2 = objects.begin(); it2 != objects.end(); ++it2 )
		    cout<< it2->second->name << " ";
		  cout << endl;
		  }
		}
	      else
		arg->id = (*it2).second->id;
	    }
	break;
      case AND_FORMULA:
      case OR_FORMULA:
      case NOT_FORMULA:
      case ADD_FORMULA:
      case KNOW_FORMULA:
      case ONEOF_FORMULA:
      case UNKNOWN_FORMULA:
	idMatchArgsVars( formula->u.formula, vars );
	break;
      case FORALL_FORMULA:
      case FORALL_EFFECT:
	// extend environment and make recursive call
	for( var = formula->u.lambda.vars; var->next != NULL; var = var->next );
	assert( (var != NULL) && (var->next == NULL) );
	var->next = vars;
	idMatchArgsVars( formula->u.lambda.formula, formula->u.lambda.vars );
	var->next = NULL;
	break;
      case LIST_FORMULA:
	idMatchArgsVars( formula->u.flist.formula, vars );
	idMatchArgsVars( formula->u.flist.next, vars );
	break;
      case EMPTY_FORMULA:
      case CERTAINTY_FORMULA:
	break;
      case SET_FORMULA:
	idMatchArgsVars( formula->u.fset.literal, vars );
	idMatchArgsVars( formula->u.fset.formula, vars );
	break;
      case WHEN_EFFECT:
	idMatchArgsVars( formula->u.when.formula, vars );
	idMatchArgsVars( formula->u.when.effect, vars );
	break;
      default:
	printf( "parse(idMatchArgsVars): unexpected formula type %d\n", formula->type );
	break;
      }
}

static bool
isOfType( idList_t *type1, idList_t *type2 )
{
  if( type1 == NULL && type2 == NULL )
    return true;
  if( type1 == NULL || type2 == NULL )
    return false;
  if( !strcasecmp( type1->name, type2->name ) )
    return( true );
  else
    {
      map<const char*,idList_t*,ltstr>::iterator it;
      for( idList_t *t1 = type1; t1 != NULL; t1 = t1->next )
	if( (it = types.find( t1->name )) != types.end() )
	  {
	      for( idList_t *t2 = (*it).second->type; t2 != NULL; t2 = t2->next )
		if( isOfType( t2, type2 ) )
		  return( true );
	    }
      return( false );
    }
}

static instantiation_t *
buildInstantiation( idList_t *vars, idList_t *args )
{
  if( !vars && !args )
    {
      return( NULL );
    }
  else if( vars && args )
    {
      instantiation_t *inst = (instantiation_t*)malloc( sizeof( instantiation_t ) );
      inst->var = vars;
      inst->val = args;
      inst->next = buildInstantiation( vars->next, args->next );
      return( inst );
    }
  else
    {
      printf( "parse(buildInstantiation): wrong number or arguments\n" );
      return( NULL );
    }
}

static formula_t *
copyReplaceAtomicFormula( formula_t *formula, instantiation_t *instantiation )
{
  instantiation_t *inst;
  idList_t *arg, *prevArg, *newArg;

  formula_t *result = (formula_t*)malloc( sizeof( formula_t ) );
  *result = *formula;
  result->u.atomic.args = NULL;

  // copy/replace arguments
  prevArg = NULL;
  for( arg = formula->u.atomic.args; arg != NULL; arg = arg->next )
    {
      newArg = (idList_t*)malloc( sizeof( idList_t ) );
      for( inst = instantiation; inst != NULL; inst = inst->next )
	if( !strcasecmp( arg->name, inst->var->name ) )
	  break;
      *newArg = *(inst==NULL?arg:inst->val);
      newArg->next = NULL;

      // link it
      if( prevArg == NULL )
	result->u.atomic.args = newArg;
      else
	prevArg->next = newArg;
      prevArg = newArg;
    }
  return( result );
}

static formula_t *
copyReplaceFormula( formula_t *formula, instantiation_t *inst )
{
  formula_t *result = NULL;
  if( formula != NULL )
    {
      switch( formula->type )
	{
	case ATOMIC_FORMULA:
	  result = copyReplaceAtomicFormula( formula, inst );
	  break;
	case AND_FORMULA:
	case OR_FORMULA:
	case NOT_FORMULA:
	case ADD_FORMULA:
	case KNOW_FORMULA:
	case ONEOF_FORMULA:
	case UNKNOWN_FORMULA:
	  result = (formula_t*)malloc( sizeof( formula_t ) );
	  *result = *formula;
	  result->u.formula = copyReplaceFormula( formula->u.formula, inst );
	  break;
	case FORALL_FORMULA:
	case FORALL_EFFECT:
	  result = (formula_t*)malloc( sizeof( formula_t ) );
	  *result = *formula;
	  result->u.lambda.formula = copyReplaceFormula( formula->u.lambda.formula, inst );
	  break;
	case LIST_FORMULA:
	  result = (formula_t*)malloc( sizeof( formula_t ) );
	  *result = *formula;
	  result->u.flist.formula = copyReplaceFormula( formula->u.flist.formula, inst );
	  result->u.flist.next = copyReplaceFormula( formula->u.flist.next, inst );
	  break;
	default:
	  result = formula;
	  break;
	}
    }
  return( result );
}

static formula_t *
instantiateFormula( formula_t* formula, idList_t* vars, instantiation_t* inst, formula_t *result )
{
  map<const char*,idList_t*,ltstr>::iterator it;
  if( vars == NULL )
    {
      formula_t *aux = (formula_t*)malloc( sizeof( formula_t ) );
      aux->type = LIST_FORMULA;
      aux->u.flist.formula = unfoldQuantifiers( copyReplaceFormula( formula, inst ) );
      aux->u.flist.next = result;
      result = aux;
    }
  else
    {
      instantiation_t newInst;
      newInst.next = inst;
      newInst.var = vars;
      for( it = objects.begin(); it != objects.end(); ++it )
	if( isOfType( (*it).second->type, vars->type ) )
	  {
	    newInst.val = (*it).second;
	    result = instantiateFormula( formula, vars->next, &newInst, result );
	  }
    }
  return( result );
}

static formula_t *
unfoldQuantifiers( formula_t *formula )
{
  formula_t *result = NULL;
  if( formula != NULL )
    {
      result = formula;
      switch( formula->type )
	{
	case ATOMIC_FORMULA:
	  break;
	case AND_FORMULA:
	case OR_FORMULA:
	case NOT_FORMULA:
	case ADD_FORMULA:
	case KNOW_FORMULA:
	case ONEOF_FORMULA:
	case UNKNOWN_FORMULA:
	  result->u.formula = unfoldQuantifiers( formula->u.formula );
	  break;
	case FORALL_FORMULA:
	case FORALL_EFFECT:
	  result = (formula_t*)malloc( sizeof( formula_t ) );
	  result->type = AND_FORMULA;
	  result->u.formula = instantiateFormula( formula->u.lambda.formula, formula->u.lambda.vars, NULL, NULL );
	  break;
	case LIST_FORMULA:
	  result->u.flist.formula = unfoldQuantifiers( result->u.flist.formula );
	  result->u.flist.next = unfoldQuantifiers( result->u.flist.next );
	  break;
	case SET_FORMULA:
	  result->u.fset.formula = unfoldQuantifiers( formula->u.fset.formula );
	  break;
	case WHEN_EFFECT:
	  result->u.when.formula = unfoldQuantifiers( formula->u.when.formula );
	  result->u.when.effect = unfoldQuantifiers( formula->u.when.effect );
	  break;
	default:
	  printf( "parse(unfoldQuantifiers): unexpected formula type %d\n", formula->type );
	  break;
	}
    }
  return( result );
}

static formula_t *
linearizeEffect( formula_t *formula, formula_t* &tail )
{
  formula_t *aux, *result;
  result = tail = NULL;
  if( formula != NULL )
    switch( formula->type )
      {
      case ATOMIC_FORMULA:
      case EMPTY_FORMULA:
      case SET_FORMULA:
      case WHEN_EFFECT:
	result = (formula_t*)malloc( sizeof( formula_t ) );
	result->type = LIST_FORMULA;
	result->u.flist.formula = formula;
	result->u.flist.next = NULL;
	tail = result;
	break;
      case AND_FORMULA:
	result = linearizeEffect( formula->u.formula, tail );
	break;
      case LIST_FORMULA:
	result = linearizeEffect( formula->u.flist.formula, aux );
	aux->u.flist.next = linearizeEffect( formula->u.flist.next, tail );
	if( tail == NULL )
	  tail = aux;
	break;
      default:
	printf( "parse(linearizeEffect): unexpected formula type %d\n", formula->type );
	break;
      }
  return( result );
}

// return -1 if parameters are not instantiated
static int
atomId( formula_t *literal, int* parameters )
{
  static int arguments[MAXPARAMETERS];

  // argument extraction
  int *p = arguments;
  *p++ = literal->u.atomic.id;
  for( idList_t *arg = literal->u.atomic.args; arg != NULL; arg = arg->next )
    if( arg->name[0] == '?' )
      {
	assert( arg->id > 0 );
	if( parameters[arg->id] <= 0 )
	  return -1; // Atom does not exist
	*p++ = parameters[arg->id];
      }
    else
      *p++ = arg->id;
  *p = -1;

  // generate atomId
  return( readAtomHash( arguments )->idx );
}


void
generateAtoms( void )
{
  formula_t *formula;
  str2wff_t::iterator it;

  for( it = predicates.begin(); it != predicates.end(); ++it )
    if( (*it).second->u.atomic.equal == 0 )
      {
	// generate instantiations and insert into atom hash
	formula = instantiateFormula( (*it).second, (*it).second->u.atomic.args, NULL, NULL );
	while( formula != NULL )
	  {
	    atomId( formula->u.flist.formula, NULL );
	    formula = formula->u.flist.next;
	  }
      }
}

void
generateVarsAndValues( void )
{
  int i, j, k;
  idList_t *var;
  map<const char*,idList_t*,ltstr>::iterator it;

  // vars
  _low_vars = (int**)calloc( _low_numberSchema, sizeof( int* ) );
  for( i = 0; i < _low_numberSchema; ++i )
    {
      _low_vars[i] = (int*)calloc( maxParameters + 1, sizeof( int ) );
      for( var = _low_schemaTable[i]->vars, j = 0; var != NULL; var = var->next, ++j )
	_low_vars[i][j] = var->id;
    }

  // values
  _low_values = (int**)calloc( _low_numberSchema * (maxParameters + 1), sizeof( int* ) );
  for( i = 0; i < _low_numberSchema * maxParameters; ++i )
    _low_values[i] = (int*)calloc( numberObjects+1, sizeof( int ) );
  for( i = 0; i < _low_numberSchema; ++i )
    for( var = _low_schemaTable[i]->vars; var != NULL; var = var->next )
      {
	k = 0;
	if( var->type == NULL )
	  {
	    for( it = objects.begin(); it != objects.end(); ++it )
	      _low_values[_low_numberSchema*(var->id-1) + i][k++] = (*it).second->id;
	  }
	else
	  {
	    if( !(_low_requirements & REQ_TYPING) )
	      printf( "parser(generateVarsAndValues): using types without :typing requirements.\n" );
	    for( it = objects.begin(); it != objects.end(); ++it )
	      if( !strcasecmp( var->type->name, (*it).second->type->name ) ||
		  isOfType( (*it).second->type, var->type ) )
		_low_values[_low_numberSchema*(var->id-1) + i][k++] = (*it).second->id;
	  }
      }
}

static nnf::node
generateEffect( nnf::Manager *man, nnf::node avar, formula_t *formula, int *parameters, lit_effect_t &frame )
{
  nnf::node res, tmp1, tmp2, tmp3;
  lit_effect_t t_frame;
  assert( (avar != (unsigned)-1) || (formula->type != WHEN_EFFECT) );

  switch( formula->type )
    {
    case LIST_FORMULA:
      res = nnf::make_value( man, true );
      for( formula_t *eff = formula; eff != 0; eff = eff->u.flist.next )
	{
	  tmp1 = generateEffect( man, avar, eff->u.flist.formula, parameters, frame );
	  tmp2 = nnf::make_and( man, res, tmp1 );
	  man->unregister_use( res );
	  man->unregister_use( tmp1 );
	  res = tmp2;
	}
      break;
    case ATOMIC_FORMULA:
      // CNF = action => lit = -action || lit
      tmp1 = generateAtomicFormula( man, formula, parameters, true );
      if( avar != (unsigned)-1 )
	res = nnf::make_or( man, avar, tmp1 );
      else
	{
	  res = tmp1;
	  man->register_use( tmp1 );
	}
      frame.push_back( std::make_pair( (formula_t*)0, std::make_pair( nnf::make_value(man,true), tmp1 ) ) );
      break;
    case SET_FORMULA:
      assert( 0 );
      break;
    case WHEN_EFFECT:
      // CNF:  action & condition => lit  <=>  -action || -condition || lit
      tmp1 = generateFormula( man, formula->u.when.formula, parameters, false );
      tmp2 = nnf::make_not( man, tmp1 );
      tmp3 = nnf::make_or( man, avar, tmp2 );
      man->unregister_use( tmp2 );
      tmp2 = generateEffect( man, (unsigned)-1, formula->u.when.effect, parameters, t_frame );
      res = nnf::make_or( man, tmp3, tmp2 );
      man->unregister_use( tmp3 );
      man->unregister_use( tmp2 );
      tmp2 = nnf::make_cnf( man, res );
      man->unregister_use( res );
      res = tmp2;
      for( size_t i = 0; i < t_frame.size(); ++i )
	{
	  man->register_use( tmp1 );
	  frame.push_back( std::make_pair( formula->u.when.formula, std::make_pair(tmp1,t_frame[i].second.second) ) );
	  man->unregister_use( t_frame[i].second.first );
	}
      man->unregister_use( tmp1 );
      break;
    default:
      res = nnf::make_value( man, true );
      printf( "parse(generateEffect): unexpected formula type %d\n", formula->type );
      break;
    }
  return( res );
}

static void
collectEffectAtoms( formula_t *formula, int *parameters, std::vector<int> &atoms, std::vector<int> *atoms_conds )
{
  switch( formula->type )
    {
    case LIST_FORMULA:
      for( formula_t *eff = formula; eff != 0; eff = eff->u.flist.next )
	collectEffectAtoms( eff->u.flist.formula, parameters, atoms, atoms_conds );
      break;
    case ATOMIC_FORMULA:
      collectFormulaAtoms( formula, parameters, atoms );
      break;
    case WHEN_EFFECT:
      if( atoms_conds )
	collectFormulaAtoms( formula->u.when.formula, parameters, *atoms_conds );
      collectEffectAtoms( formula->u.when.effect, parameters, atoms, atoms_conds );
      break;
    default:
      printf( "parse(collectEffectAtoms): unexpected formula type %d\n", formula->type );
      break;
    }
}

static void
collectUncondEffectAtoms( formula_t *formula, int *parameters, std::vector<int> &atoms )
{
  switch( formula->type )
    {
    case LIST_FORMULA:
      for( formula_t *eff = formula; eff != 0; eff = eff->u.flist.next )
	collectUncondEffectAtoms( eff->u.flist.formula, parameters, atoms );
      break;
    case ATOMIC_FORMULA:
      collectFormulaAtoms( formula, parameters, atoms );
      break;
    case AND_FORMULA:
      collectUncondEffectAtoms( formula->u.formula, parameters, atoms );
      printf( "CHECK: pass through AND in collectEffectAtoms\n" );
      break;
    case SET_FORMULA:
      assert( 0 );
      break;
    case WHEN_EFFECT:
      break;
    default:
      printf( "parse(collectEffectAtoms): unexpected formula type %d\n", formula->type );
      break;
    }
}
void
mapWhenEffects( formula_t *formula, int *parameters, std::vector<formula_t*> &clist )
{
  switch( formula->type )
    {
    case LIST_FORMULA:
      for( formula_t *eff = formula; eff != 0; eff = eff->u.flist.next )
	mapWhenEffects( eff->u.flist.formula, parameters, clist );
      break;
    case ATOMIC_FORMULA:
      break;
    case SET_FORMULA:
      assert( 0 );
      break;
    case WHEN_EFFECT:
      clist.push_back( formula->u.when.formula );
      mapWhenEffects( formula->u.when.effect, parameters, clist );
      break;
    default:
      printf("parse(mapWhenEffects): unexpected formula type %d\n", formula->type);
      break;
    }
}

int
equalityValue( formula_t *formula, int *parameters )
{
  int val[2];
  idList_t *arg[2];
  arg[0] = formula->u.atomic.args;
  arg[1] = formula->u.atomic.args->next;
  for( int i = 0; i < 2; ++i )
    {
      if( arg[i]->name[0] == '?' )
	{
	  assert( arg[i]->id > 0 );
	  if( parameters[arg[i]->id] <= 0 )
	    return -1; // Atom does not exist
	  val[i] = parameters[arg[i]->id];
	}
      else
	val[i] = arg[i]->id;
    }
  return( val[0] == val[1] );
}

static nnf::node
generateAtomicFormula( nnf::Manager *man, formula_t *formula, int *parameters, bool future )
{
  if( formula->u.atomic.equal == 1 )
    {
      bool test = equalityValue( formula, parameters );
      if( formula->u.atomic.neg ) test = !test;
      return( nnf::make_value( man, (test?true:false) ) );
    }
  else
    {
      int atom = atomId( formula, parameters );
      if( reachable.find( atom ) == reachable.end() )
	return( nnf::make_value( man, true ) ); // can only happen if formula is init
      else
	{
	  atom = reachable[atom];
	  atom = (future?atom+time_shift:atom)<<1; // present or future?
	  atom = (formula->u.atomic.neg?1+atom:atom);
	  return( nnf::make_variable( man, atom ) );
	}
    }
}

nnf::node
generateFormula( nnf::Manager *man, formula_t* formula, int* parameters, bool future )
{
  nnf::node res, tmp1, tmp2;
  if( formula == NULL ) return( nnf::make_value( man, true ) );
  switch( formula->type )
    {
    case ATOMIC_FORMULA:
      res = generateAtomicFormula( man, formula, parameters, future );
      break;
    case OR_FORMULA:
    case AND_FORMULA:
      res = nnf::make_value( man, (formula->type!=OR_FORMULA) );
      for( formula_t *f = formula->u.formula; f != NULL; f = f->u.flist.next )
	{
	  tmp1 = generateFormula( man, f->u.flist.formula, parameters, future );
	  if( formula->type == OR_FORMULA )
	    tmp2 = nnf::make_or( man, res, tmp1 );
	  else
	    tmp2 = nnf::make_and( man, res, tmp1 );
	  man->unregister_use( res );
	  man->unregister_use( tmp1 );
	  res = tmp2;
	}
      break;
    case LIST_FORMULA: // Verify it
      res = nnf::make_value( man, true );
      for( formula_t *f = formula; f != 0; f = f->u.flist.next ) 
	{
	  tmp1 = generateFormula( man, f->u.flist.formula, parameters, future );
	  tmp2 = nnf::make_and( man, res, tmp1 );
	  man->unregister_use( res );
	  man->unregister_use( tmp1 );
	  res = tmp2;
	}
      break;
    case NOT_FORMULA:
      tmp1 = generateFormula( man, formula->u.formula, parameters, future );
      res = nnf::make_not( man, tmp1 );
      man->unregister_use( tmp1 );
      break;
      // OJO: COMPLETAR!
    case ONEOF_FORMULA:
    case UNKNOWN_FORMULA:
      res = nnf::make_value( man, true );
      printf( "don't generate formula for ONEOF or UNKNOWN yet. Type %d\n", formula->type );
      break;
    default:
      res = nnf::make_value( man, true );
      printf( "parser(generateFormula): unexpected formula type %d\n", formula->type );
      //assert( 0 != 0 );
      break;
    }
  return( res );
}

static void
collectFormulaEquals( formula_t* formula, int* parameters, std::vector<formula_t*> &equals )
{
  if( formula == NULL ) return;
  switch( formula->type )
    {
    case ATOMIC_FORMULA:
      if( formula->u.atomic.equal )
	equals.push_back(formula);
      break;
    case AND_FORMULA:
      for( formula_t *f = formula->u.formula; f != NULL; f = f->u.flist.next )
	collectFormulaEquals( f->u.flist.formula, parameters, equals );
      break;
    case NOT_FORMULA:
      collectFormulaEquals( formula->u.formula, parameters, equals );
      break;
    case LIST_FORMULA:
      collectFormulaEquals( formula->u.flist.formula, parameters, equals );
      collectFormulaEquals( formula->u.flist.next, parameters, equals );
      break;
    case UNKNOWN_FORMULA:
    case OR_FORMULA:
    case ONEOF_FORMULA:
    default:
      printf( "parser(collectFormulaEquals): unexpected formula type %d\n", formula->type );
      break;
    }
}

// Collect atom already instantiated
static void
collectFormulaAtoms( formula_t* formula, int* parameters, std::vector<int> &atoms )
{
  if( formula == NULL ) return;
  switch( formula->type )
    {
    case ATOMIC_FORMULA:
      if( !formula->u.atomic.equal )
	{
	  int atom = atomId( formula, parameters );
	  if( atom <= 0 ) return; // Atom doesn't exist
	  atom = (formula->u.atomic.neg?1+(atom<<1):(atom<<1));
	  atoms.push_back( atom );
	}
      break;
    case OR_FORMULA:
    case AND_FORMULA:
    case ONEOF_FORMULA:
      for( formula_t *f = formula->u.formula; f != NULL; f = f->u.flist.next )
	collectFormulaAtoms( f->u.flist.formula, parameters, atoms );
      break;
    case UNKNOWN_FORMULA:
      collectFormulaAtoms( formula->u.formula, parameters, atoms );
      break;
    case LIST_FORMULA:
      collectFormulaAtoms( formula->u.flist.formula, parameters, atoms );
      collectFormulaAtoms( formula->u.flist.next, parameters, atoms );
      break;
    case NOT_FORMULA:
    default:
      printf( "parser(collectFormulaAtoms): unexpected formula type %d\n", formula->type );
      break;
    }
}

void
collectAllAtoms( formula_t* formula, int* parameters, std::vector<int> &atoms )
{
  if( formula == NULL ) return;
  switch( formula->type )
    {
    case LIST_FORMULA:
      for( formula_t *f = formula; f != 0; f = f->u.flist.next )
	collectAllAtoms( f->u.flist.formula, parameters, atoms );
      break;
    case ATOMIC_FORMULA:
      if( !formula->u.atomic.equal )
	{
	  int atom = atomId( formula, parameters );
	  atom = (formula->u.atomic.neg?1+(atom<<1):(atom<<1));
	  atoms.push_back( atom );
	}
      break;
    case OR_FORMULA:
    case AND_FORMULA:
    case ONEOF_FORMULA:
      for( formula_t *f = formula->u.formula; f != NULL; f = f->u.flist.next )
	collectAllAtoms( f->u.flist.formula, parameters, atoms );
      break;
    case NOT_FORMULA:
    case UNKNOWN_FORMULA:
      collectAllAtoms( formula->u.formula, parameters, atoms );
      break;
    case SET_FORMULA:
      assert( 0 );
      break;
    case WHEN_EFFECT:
      collectAllAtoms( formula->u.when.formula, parameters, atoms );
      collectAllAtoms( formula->u.when.effect, parameters, atoms );
      break;
    default:
      printf( "parser(collectAllAtoms): unexpected formula type %d\n", formula->type );
      break;
    }
}

void
generateSchema( nnf::Manager *man, nnf::node action, schema_t* schema, int* parameters )
{
  // need to generate cnfs for precondition and effects (frame will do elsewhere)
  // ASSUMPTION: avar is negative action literal 

  // CNF(prec) = prec || !action
  // ASSUMPTION: precondition formula is in positive form
  nnf::node tmp1 = generateFormula( man, schema->prec, parameters, false );
  nnf::node tmp2 = nnf::make_or( man, action, tmp1 );
  man->unregister_use( tmp1 );
  nnf::node prec = nnf::make_cnf( man, tmp2 );
  man->unregister_use( tmp2 );

  // cnf for effectstrue if action is 
  _low_operator.frame_->clear();
  nnf::node effect = generateEffect( man, action, schema->effect, parameters, *_low_operator.frame_ );
  tmp1 = nnf::make_and( man, prec, effect );
  man->unregister_use( prec );
  man->unregister_use( effect );
  _low_operator.cnf_ = tmp1;
}

// Return false can't be executed (typically, equals on precods)
// Return only atoms instatiated by parameters
bool
operatorAtoms( schema_t *schema, int *parameters, 
	       std::set<int> &prec, std::set<int> &add, std::set<int> &del,
	       std::set<int>* reachable_atoms = 0, 
	       std::set<int>* neg_prec = 0,  
	       std::set<int>* conds = 0 )
{
  std::vector<int> atoms_vec;
  collectPlainFormulaAtoms( schema->prec, parameters, atoms_vec );
  for( size_t i = 0; i < atoms_vec.size(); ++i )
    {
      if( atoms_vec[i] % 2 ) 
	{
	  if( reachable_atoms != 0 &&
	      reachable_atoms->count( atoms_vec[i] >> 1 ) )
	    return false;
	  if(neg_prec != 0) neg_prec->insert( atoms_vec[i] >> 1 );
	}
      else
	prec.insert( atoms_vec[i] >> 1 );
    }

  // Check if equals agree...
  std::vector<formula_t*> equals;
  collectFormulaEquals( schema->prec, parameters, equals );
  for( size_t i = 0; i < equals.size(); ++i )
    {
      assert( equals[i]->type = ATOMIC_FORMULA &&
	      equals[i]->u.atomic.equal == 1 );
      int test = equalityValue( equals[i], parameters );
      if( test != -1 )
	{
	  if( equals[i]->u.atomic.neg ) test = !test;
	  if( !test )
	    return false;
	}
    }
    
  atoms_vec.clear();
  vector<int> atoms_conds;
  if( conds )
    collectEffectAtoms( schema->effect, parameters, atoms_vec, &atoms_conds );    
  else
    collectEffectAtoms( schema->effect, parameters, atoms_vec );
  for( size_t i = 0; i < atoms_vec.size(); ++i )
    {
      if( atoms_vec[i] % 2 )
	del.insert( atoms_vec[i]>>1 );
      else
	add.insert( atoms_vec[i]>>1 );
    }
  if(conds)
    for( size_t i = 0; i < atoms_conds.size(); ++i )
      {
	if( atoms_conds[i] % 2 )
	  conds->insert( -int(atoms_conds[i]>>1) );
	else
	  conds->insert( atoms_conds[i]>>1 );
      }
  return true;
}



// do not accept not({and|or} ..)
// neither (or ... )
static void
collectPlainFormulaAtoms( formula_t* formula, int* parameters, std::vector<int> &atoms )
{
  if( formula == NULL ) return;
  switch( formula->type )
    {
    case ATOMIC_FORMULA:
      if( !formula->u.atomic.equal )
	{
	  int atom = atomId( formula, parameters );
	  if( atom <= 0 ) return; // Atom doesn't exist
	  atom = (formula->u.atomic.neg?1+(atom<<1):(atom<<1));
	  atoms.push_back( atom );
	}
      break;
    case AND_FORMULA:
      for( formula_t *f = formula->u.formula; f != NULL; f = f->u.flist.next )
	collectPlainFormulaAtoms( f->u.flist.formula, parameters, atoms );
      break;
    case NOT_FORMULA: 
      if ( formula->u.formula->type != ATOMIC_FORMULA )
	{
	  printf( "parser(collectPlainFormulaAtoms): not of a non atomic formula\n");
	  exit(1);
	}
      collectPlainFormulaAtoms( formula->u.formula, parameters, atoms );
      break;
    case LIST_FORMULA:
      collectPlainFormulaAtoms( formula->u.flist.formula, parameters, atoms );
      collectPlainFormulaAtoms( formula->u.flist.next, parameters, atoms );
      break;
    case UNKNOWN_FORMULA:
    case ONEOF_FORMULA:
    case OR_FORMULA:
    default:
      printf( "parser(collectPlainFormulaAtoms): unexpected formula type %d\n", formula->type );
      break;
    }
}

void
collectPlainFormulaCertainAtoms( formula_t* formula, std::set<int> &atoms )
{
  if( formula == NULL ) return;
  switch( formula->type )
    {
    case ATOMIC_FORMULA:
      if( !formula->u.atomic.equal )
	{
	  int atom = atomId( formula, 0 );
	  int a = (formula->u.atomic.neg?-int(atom):int(atom));
	  atoms.insert( a );
	}
      break;
    case AND_FORMULA:
      for( formula_t *f = formula->u.formula; f != NULL; f = f->u.flist.next )
	collectPlainFormulaCertainAtoms( f->u.flist.formula, atoms );
      break;
    case NOT_FORMULA: 
      if ( formula->u.formula->type != ATOMIC_FORMULA )
	{
	  printf( "parser(collectPlainFormulaCertainAtoms): not of a non atomic formula\n");
	  exit(1);
	}
      collectPlainFormulaCertainAtoms( formula->u.formula, atoms );
      break;
    case LIST_FORMULA:
      collectPlainFormulaCertainAtoms( formula->u.flist.formula, atoms );
      collectPlainFormulaCertainAtoms( formula->u.flist.next, atoms );
      break;
    case UNKNOWN_FORMULA:
    case ONEOF_FORMULA:
    case OR_FORMULA:
      break;
    default:
      printf( "parser(collectPlainFormulaCertainAtoms): unexpected formula type %d\n", formula->type );
      break;
    }
}

// Some atoms that appear for sure on every model (simplest case)
void
collectPlainFormulaPosAtoms( formula_t* formula, std::set<int> &atoms )
{
  if( formula == NULL ) return;
  switch( formula->type )
    {
    case ATOMIC_FORMULA:
      if( !formula->u.atomic.equal )
	{
	  int atom = atomId( formula, 0 );
	  int a = (formula->u.atomic.neg?-int(atom):int(atom));
	  atoms.insert( a );
	}
      break;
    case AND_FORMULA:
      for( formula_t *f = formula->u.formula; f != NULL; f = f->u.flist.next )
	collectPlainFormulaPosAtoms( f->u.flist.formula, atoms );
      break;
      break;
    case LIST_FORMULA:
      collectPlainFormulaPosAtoms( formula->u.flist.formula, atoms );
      collectPlainFormulaPosAtoms( formula->u.flist.next, atoms );
      break;
    case NOT_FORMULA: 
    case UNKNOWN_FORMULA:
    case OR_FORMULA:
    case ONEOF_FORMULA:
      break;
    default:
      printf( "parser(collectPlainFormulaPosAtoms): unexpected formula type %d\n", formula->type );
      break;
    }
}


bool
isComplexFormula2( formula_t* formula )
{
  bool val = false;
  if( formula == NULL ) return false;
  switch( formula->type )
    {
    case ATOMIC_FORMULA:
      return false;
      break;
    case ONEOF_FORMULA:
    case AND_FORMULA:
      for( formula_t *f = formula->u.formula; f != NULL; f = f->u.flist.next )
	val = val || isComplexFormula2( f->u.flist.formula );
      break;
    case UNKNOWN_FORMULA:
      val = val || isComplexFormula2( formula->u.formula );
    case NOT_FORMULA: 
      if ( formula->u.formula->type == ATOMIC_FORMULA )
	return false;
      else
	return true;
      break;
    case LIST_FORMULA:
      val = val || isComplexFormula2( formula->u.flist.formula );
      val = val || isComplexFormula2( formula->u.flist.next );
      break;
    case OR_FORMULA:
      return true;
    }
  return val;
}

bool
isComplexFormula( formula_t* formula )
{
  bool val = false;
  if( formula == NULL ) return false;
  switch( formula->type )
    {
    case ATOMIC_FORMULA:
      return false;
      break;
    case AND_FORMULA:
      for( formula_t *f = formula->u.formula; f != NULL; f = f->u.flist.next )
	val = val || isComplexFormula( f->u.flist.formula );
      break;
    case NOT_FORMULA: 
      if ( formula->u.formula->type == ATOMIC_FORMULA )
	return false;
      else
	return true;
      break;
    case LIST_FORMULA:
      val = val || isComplexFormula( formula->u.flist.formula );
      val = val || isComplexFormula( formula->u.flist.next );
      break;
    case UNKNOWN_FORMULA:
    case ONEOF_FORMULA:
    case OR_FORMULA:
      return true;
    }
  return val;
}

static int
collectCondEffectAtoms( formula_t *formula, int *parameters,  
			std::vector<int>& atoms, Act &act, vector<int>* r2a,
			const std::set<int>* reachable_atoms,
			const std::set<int>* static_positive_atoms = 0 )
{
  int total = 0;
  const bool debugit = false;

  switch( formula->type )
    {
    case LIST_FORMULA:
      for( formula_t *eff = formula; eff != 0; eff = eff->u.flist.next )
	total += collectCondEffectAtoms( eff->u.flist.formula, parameters, atoms, act, r2a,
					 reachable_atoms,
					 static_positive_atoms );
      break;
    case ATOMIC_FORMULA:
      break;
    case SET_FORMULA:
      assert( 0 );
      break;
    case WHEN_EFFECT:
      {
	total = 1;
	When w;
	atoms.clear();
	collectPlainFormulaAtoms( formula->u.when.formula, parameters, atoms );
	for( size_t i = 0; i < atoms.size(); ++i )
	  {
	    size_t old_a = atoms[i]>>1;
	    size_t a = 0;
	    if( r2a )
	      {
		if( (atoms[i]>>1) >= r2a->size() )
		  {
		    cout << "av = " <<  (atoms[i]>>1) 
			 << ", r2a = " << r2a->size() << endl;
		  }
		assert( (atoms[i]>>1) < r2a->size() );
		a = (*r2a)[atoms[i]>>1];
	      }
	    else
	      a = old_a;
	    if(debugit)
	      cout << "in When: considering condition atom " << (atoms[i] % 2?-1:1)*old_a 
		   << ". new value = " << a << endl;
	    if( atoms[i] % 2 )
	      {
		// Can't be made positive
		if( static_positive_atoms && static_positive_atoms->count( old_a ) > 0 )
		  {
		    if(debugit)
		      cout << "rejecting because atom " << old_a  << " is static " << endl;
		    // Isn't right
		    //act.conds.pop_back();
		    return 0;
		  }
		w.prec.insert( -a );
	      }
	    else
	      {
		// Adding non-static atoms
		if( !static_positive_atoms || static_positive_atoms->count( old_a ) == 0 ) 
		  {
		    if( reachable_atoms && reachable_atoms->count( old_a ) == 0 ) 
		      {
			if(debugit)
			  cout << "rejecting because can't reach atom " << old_a << endl;
			return 0;
		      }
		    w.prec.insert( a );
		    if(debugit)
		      cout << "Adding atom " << a << endl;
		  }
		else if(debugit)
		  cout << "rejecting because is static and positive " << old_a << endl;
	      }
	  }
	if(debugit)
	  cout << "Prec of condition size: " << w.prec.size() << endl;
	atoms.clear();
	collectPlainFormulaAtoms( formula->u.when.effect, parameters, atoms );
	  for( size_t i = 0; i < atoms.size(); ++i )
	    {
	      if( r2a && (atoms[i]>>1) >= r2a->size() )
		{
		  cout << "av = " <<  (atoms[i]>>1) 
		       << ", r2a = " << r2a->size() << endl;
		  assert( (atoms[i]>>1) < r2a->size() );
		}
	      size_t a;
	      if( r2a )
		a = (*r2a)[atoms[i]>>1];
	      else
		a = atoms[i]>>1;
	      if( atoms[i] % 2 )
		w.eff.insert( -a );
	      else
		w.eff.insert( a );
	      if(debugit)
		cout << "in When: considering effect atom " << (atoms[i] % 2?-1:1)*(atoms[i]>>1)
		     << ". new value = " << a << endl;
	    }
	atoms.clear();
	if( w.prec.size() == 0 )
	  for( set<int>::iterator e = w.eff.begin();
	       e != w.eff.end(); ++e )
	    act.eff.insert(*e);
	else
	  act.addWhen(w);
	if(debugit)
	  {
	    cout << "now action is ";
	    act.dump(cout);
	  }
      }
      break;
    default:
      printf( "parse(collectCondEffectAtoms): unexpected formula type %d\n", formula->type );
      break;
    }
  return total;
}

bool
operatorAtomsWhen( schema_t *schema, int *parameters, Act &act, vector<int>* r2a,
		   const std::set<int>& reachable_atoms,
		   const std::set<int>* static_positive_atoms = 0 )
{
  const bool debugit = false;

  std::vector<int> atoms_vec;
  collectPlainFormulaAtoms( schema->prec, parameters, atoms_vec );
  for( size_t i = 0; i < atoms_vec.size(); ++i )
    {
      int old_a = atoms_vec[i]>>1;
      size_t a = 0;
      if( r2a ) 
	{
	  if( (atoms_vec[i]>>1) >= r2a->size() )
	    {
	      cerr << "FATAL ERROR: av = " <<  (atoms_vec[i]>>1) 
		   << ", r2a = " << r2a->size() << endl;
	    }
	  assert( (atoms_vec[i]>>1) < r2a->size() );
	  a = (*r2a)[atoms_vec[i]>>1];
	}
      else
	a = old_a;
      if(debugit)
	cout << "considering atom " << (atoms_vec[i] % 2?-1:1)*old_a << ". new value = " << a << endl;
      if( atoms_vec[i] % 2 )
	{
	  // Can't be made positive
	  if( static_positive_atoms && static_positive_atoms->count( old_a ) > 0 )
	    {
	      if(debugit)
		cout << "rejecting because atom " << old_a << endl;
	      return false;
	    }

	  if( reachable_atoms.count( old_a ) != 0 )
	    { // Can be made positive, so we can't remove it
	      cerr << "FATAL ERROR: Non-static negative preconditions not supported. Final check" << endl;
	      exit(1);
	    }
	}
      else
	{
	  if( !static_positive_atoms || static_positive_atoms->count( old_a ) == 0 ) 
	    {
	      if(debugit)
		cout << "Adding atom " << a << endl;
	      act.prec.insert( a );
	    }
	}
    }
  if(debugit)
    cout << "Prec of action size: " << act.prec.size() << endl;

  atoms_vec.clear();
  collectUncondEffectAtoms( schema->effect, parameters, atoms_vec );
  for( size_t i = 0; i < atoms_vec.size(); ++i )
    {
      if( r2a && (atoms_vec[i]>>1) >= r2a->size() )
	{
	  cout << "av = " <<  (atoms_vec[i]>>1) 
	       << ", r2a = " << r2a->size() << endl;
	  assert( (atoms_vec[i]>>1) < r2a->size() );
	}

      size_t a;
      if( r2a )
	a = (*r2a)[atoms_vec[i]>>1];
      else
	a = atoms_vec[i]>>1;

      if( atoms_vec[i] % 2 )
	act.eff.insert( -a );
      else
	act.eff.insert( a );
    }
  int added = collectCondEffectAtoms( schema->effect, parameters, atoms_vec, act, r2a, 
				      &reachable_atoms, static_positive_atoms );
  if( act.eff.size() == 0 && added == 0 )
    return false; // Do nothing
  else
    return true;
}

void
operatorAtoms( schema_t *schema, int *parameters, std::set<int> &atoms )
{
  std::vector<int> atoms_vec;
  collectAllAtoms( schema->prec, parameters, atoms_vec );
  collectAllAtoms( schema->effect, parameters, atoms_vec );
  for( size_t i = 0; i < atoms_vec.size(); ++i )
    atoms.insert( atoms_vec[i] >> 1 );
}

void
formulaAtomsPos( formula_t *formula, int *parameters, int phase, std::set<int> &atoms )
{
  std::vector<int> atoms_vec;
  collectFormulaAtoms( formula, parameters, atoms_vec );
  for( size_t i = 0; i < atoms_vec.size(); ++i )
    if( (atoms_vec[i] % 2) == phase )
      atoms.insert( atoms_vec[i] >> 1 );
}

void
formulaAtoms( formula_t *formula, int *parameters, std::set<int> &atoms )
{
  std::vector<int> atoms_vec;
  collectFormulaAtoms( formula, parameters, atoms_vec );
  for( size_t i = 0; i < atoms_vec.size(); ++i )
    atoms.insert( atoms_vec[i] >> 1 );
}

void
formulaLiterals( formula_t *formula, int *parameters, std::set<int> &atoms )
{
  std::vector<int> atoms_vec;
  collectFormulaAtoms( formula, parameters, atoms_vec );
  for( size_t i = 0; i < atoms_vec.size(); ++i )
    if( atoms_vec[i] % 2) 
      atoms.insert( -(atoms_vec[i] >> 1) );
    else
      atoms.insert( atoms_vec[i] >> 1 );
}
