text: /*
   * All of the documentation and software included in the
   * Alchemy Software is copyrighted by Stanley Kok, Parag
   * Singla, Matthew Richardson, Pedro Domingos, Marc
   * Sumner, Hoifung Poon, and Daniel Lowd.
   * 
   * Copyright [2004-07] Stanley Kok, Parag Singla, Matthew
   * Richardson, Pedro Domingos, Marc Sumner, Hoifung
   * Poon, and Daniel Lowd. All rights reserved.
   * 
   * Contact: Pedro Domingos, University of Washington
   * (pedrod@cs.washington.edu).
   * 
   * Redistribution and use in source and binary forms, with
   * or without modification, are permitted provided that
   * the following conditions are met:
   * 
   * 1. Redistributions of source code must retain the above
   * copyright notice, this list of conditions and the
   * following disclaimer.
   * 
   * 2. Redistributions in binary form must reproduce the
   * above copyright notice, this list of conditions and the
   * following disclaimer in the documentation and/or other
   * materials provided with the distribution.
   * 
   * 3. All advertising materials mentioning features or use
   * of this software must display the following
   * acknowledgment: "This product includes software
   * developed by Stanley Kok, Parag Singla, Matthew
   * Richardson, Pedro Domingos, Marc Sumner, Hoifung
   * Poon, and Daniel Lowd in the Department of Computer Science and
   * Engineering at the University of Washington".
   * 
   * 4. Your publications acknowledge the use or
   * contribution made by the Software to your research
   * using the following citation(s): 
   * Stanley Kok, Parag Singla, Matthew Richardson and
   * Pedro Domingos (2005). "The Alchemy System for
   * Statistical Relational AI", Technical Report,
   * Department of Computer Science and Engineering,
   * University of Washington, Seattle, WA.
   * http://www.cs.washington.edu/ai/alchemy.
   * 
   * 5. Neither the name of the University of Washington nor
   * the names of its contributors may be used to endorse or
   * promote products derived from this software without
   * specific prior written permission.
   * 
   * THIS SOFTWARE IS PROVIDED BY THE UNIVERSITY OF WASHINGTON
   * AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED
   * WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
   * WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR
   * PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE UNIVERSITY
   * OF WASHINGTON OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT,
   * INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
   * DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
   * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR
   * PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
   * ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
   * LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
   * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN
   * IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
   * 
   */
  #ifndef FOLHELPER_H_JUL_21_2005
  #define FOLHELPER_H_JUN_21_2005
  
  // dl library used for dynamically loading linked-in functions
  #include <dlfcn.h>
  #include <stdio.h>
  #include <stdlib.h>
  #include <assert.h>
  #include <signal.h>
  #include <ext/hash_set>
  #include <stack>
  #include <iostream>
  #include <fstream>
  #include <sstream>
  #include "strfifolist.h"
  #include "predicate.h"
  #include "function.h"
  #include "clause.h"
  #include "clausefactory.h"
  #include "hashstring.h"
  #include "database.h"
  #include "listobj.h"
  #include "timer.h"
  #include "internals.h"
  
  //NOTE: When a variable is added, please init it in zzinit() and destroy it 
  //      in zzcleanUp(). Add it in zzreset() if it has to be reinitialized before
  //      a new clause is parsed.
  
  
    //Each hard clause derived from a hard formula is given a weight that is twice
    //that of the maximum soft clause weight. You can change this value by setting
    //HARD_WEIGHT_MULTIPLIER below. If you wish to set the hard clause weight to
    //a specific value, you can set HARD_WEIGHT below. 
    //If HARD_WEIGHT is DBL_MIN, HARD_WEIGHT_MULTIPLIER is used instead of 
    //HARD_WEIGHT; otherwise the latter is used.
  const double HARD_WEIGHT_MULTIPLIER = 2;
  const double HARD_WEIGHT = DBL_MIN;
  
    // If the variables are assigned some initial values, ensure they are are
    // similarly assigned in zzinit(). Also set any data structure to its initial 
    // state in zzinit()
  const int ZZ_MAX_ERRORS = 50;
  
  // Start of variable names generated by replacement of functions
  const char* ZZ_FUNCVAR_PREFIX = "funcVar";
  
  // Name of shared object file for linked-in functions
  const char* ZZ_FUNCTION_SO_FILE = "functions.so";
  
    // a copy of the user-specified MLN file is created & appended with this str
  const char* ZZ_TMP_FILE_POSTFIX = "_tmpalchemy.mln";
  
    // prepend to a file containing query predicates
  const char* zzdefaultPredName = "SKPRED";
  const char* zzdefaultFuncName = "SKFUNC";
  const char* zzdefaultTypeName = "SKTYPE";
  const char* zzdefaultVarName  = "SKVAR";
  
  bool zzstoreGroundPreds = false; //set to true for testing only
    //constants must be declared before being used
  bool zzconstantMustBeDeclared = false;
    // read weight that is specified for a hard formula
  bool zzreadHardClauseWts = false;
    //used in follex.y to allow predicate definitions to be on the same line
  bool zzafterRtParen;
  
  bool zzisParsing; //indicates whether a file is currently being parsed
  double zzdefaultWt; // default wt of a formula if no wt or . is specified
    //a formula must begin with a weight or end with full stop
  bool zzmustHaveWtOrFullStop;
    // indicates whether weights should be flipped when a clause is flipped.
    // This should be true for inference and false for learning.
  bool zzflipWtsOfFlippedClause;
  bool zzwarnDuplicates;
  string zzinFileName;
  char zzerrMsg[1024];
  
  int zzcount;  // to be appended to names of default pred, type etc.
  int zzline, zzcolumn;
  int zznumCharRead;
  int zznumErrors;
  bool zzok;
  MLN* zzmln;
  Domain* zzdomain;
  int zznumEofSeen; // num of times EOF seen
  StrFifoList zztokenList;
  
  char* zztypeName;
  PredicateTemplate* zzpredTemplate;
  FunctionTemplate* zzfuncTemplate;
  Predicate* zzpred;
  Function* zzfunc;
  stack<Function*> zzfuncStack;
  stack<ListObj*> zzfuncConjStack;
  double* zzwt;
  bool zzisNegated;
  bool zzisAsterisk;
  bool zzisPlus;
  bool zzhasFullStop;
  int zznumAsterisk;
  char zztrueFalseUnknown;
  string zzformulaStr;
  string zzfuncConjStr;
  bool zzparseGroundPred;
  stack<ListObj*> zzformulaListObjs;  //used by formulas with connectives
  stack<ListObj*> zzpredFuncListObjs; // used by predicates and functions
  hash_map<int, PredicateHashArray*> zzpredIdToGndPredMap;
  
  // Used to check if there is a function definition
  int zzfdnumPreds;
  int zzfdnumFuncs;
  int zzfdnumVars;
  int zzfuncVarCounter = 0;
  //bool zzfdisEqualPred;
  string zzfdfuncName;
  Array<string> zzfdfuncConstants;
  string zzfdconstName;
  // Used in function definitions to store the return value and type
  char* zztmpReturnConstant;
  bool zztmpReturnNum;
  
  // Used to store first number in numeric declarations
  int zzinitialNumDeclaration;
  
  // Set to true if using linked-in predicates
  bool zzusingLinkedPredicates;
  // Set to true if using linked-in functions
  bool zzusingLinkedFunctions;
  
  // Needed to hold list object information while function is replaced
  ListObj* zzoldFuncLo; 
  Timer zztimer;
  
  // Holds the internally implemented predicates and their types (see zzinit())
  Array<Array<const char*> > zzinternalPredicates;
  // Holds the internally implemented functions and their types (see zzinit())
  Array<Array<const char*> > zzinternalFunctions;
  
  // If an infix predicate is encountered then the name of it is stored here
  char* zzinfixPredName;
  // If an infix function is encountered then the name of it is stored here
  char* zzinfixFuncName;
  
  ///////// store '=' preds for which the types on both sides are unknown //////
  struct ZZUnknownEqPredInfo
  {
    ZZUnknownEqPredInfo(const string& name, const string& lhs, const string& rhs)
      :name_(name), lhs_(lhs), rhs_(rhs) {}
  
    string name_; //e.g. SK_EQUAL_1
      // variable name on left and right hand side  
    string lhs_;
    string rhs_; 
  };
  
  ///// store internal preds for which the types on both sides are unknown //////
  struct ZZUnknownIntPredInfo
  {
    ZZUnknownIntPredInfo(const string& name, const string& lhs, const string& rhs)
      :name_(name), lhs_(lhs), rhs_(rhs) {}
  
    string name_; //e.g. greaterThan_1
      // variable name on left and right hand side  
    string lhs_;
    string rhs_; 
  };
  
  /////// store internal funcs for which at least one term type is unknown //////
  struct ZZUnknownIntFuncInfo
  {
    ZZUnknownIntFuncInfo(const string& name, const Array<string>& vnames)
      :name_(name), vnames_(vnames) {}
  
    string name_; //e.g. plus_1
      // variable names
    Array<string> vnames_;
  };
  
    // counts the number of '=' predicates for which both LHS and RHS are unknown
  int zzeqTypeCounter; 
    // counts the number of internal predicates for which both LHS and RHS are
    // unknown
  int zzintPredTypeCounter; 
    // counts the number of internal functions for which at least one term type is
    // unknown
  int zzintFuncTypeCounter; 
  
    // list of '=' predicates for which both LHS and RHS are unknown
  list<ZZUnknownEqPredInfo> zzeqPredList;
    // list of internal predicates for which both LHS and RHS are unknown
  list<ZZUnknownIntPredInfo> zzintPredList;
    // list of internal functions for which at least one term type is unknown
  list<ZZUnknownIntFuncInfo> zzintFuncList;
  
    
  /////////// store state necessary to support "#include" statement //////////
  
  struct ZZFileState
  {
    ZZFileState(FILE* const & file, const string& inFileName, 
                const int& numCharRead, const int& line, const int& column) 
      : file_(file), inFileName_(inFileName), numCharRead_(numCharRead), 
        line_(line), column_(column) {}
  
    FILE* file_;
    string inFileName_;
    int numCharRead_;
    int line_;
    int column_;
  };
  
  stack<ZZFileState> zzinStack; 
  
  ///////////// ensure variable name, id, and type consistency ////////////////
  
  int zzvarCounter;
  int zzanyTypeId;
  
  struct ZZVarIdType
  {
    ZZVarIdType() : id_(0), typeId_(0) {}
  
    ZZVarIdType(const ZZVarIdType& varIdType)
      : id_(varIdType.id_), typeId_(varIdType.typeId_) {}
   
    ZZVarIdType(const int& varId, const int& typeId) 
      : id_(varId), typeId_(typeId) {}
  
    int id_;
    int typeId_;
  };
  
  
    // contains variables names
  typedef hash_map<const string, ZZVarIdType, HashString, EqualString> 
    ZZVarNameToIdMap;
  
  ZZVarNameToIdMap zzvarNameToIdMap;
  
    // contains mappings of functions to funcVars which replace them
  typedef hash_map<Function*, string, HashFunction, EqualFunction> 
    ZZFuncToFuncVarMap;
    
  ZZFuncToFuncVarMap zzfuncToFuncVarMap;
  
  
    // maps a variable name to a new one that has its scope number appended
  typedef hash_map<string, string, HashString, EqualString> StringToStringMap;
  
  int zzscopeCounter; // identifies a scope
  
    // using a list so that we can iterate through the elements in the stack
    // the front and back correspond to the the top and bottom of a stack
  typedef list< pair<StringToStringMap*,int> > ZZOldNewVarList;
  ZZOldNewVarList zzoldNewVarList;
  
  
    // since plus variables e.g. x in P(+x,y) cannot be explicitly 
    // universally/existentially quantified, they must exist within the scope of
    // the entire formula
  typedef hash_map<string, int, HashString, EqualString> StringToIntMap;
  StringToIntMap zzplusVarMap;
  
  
  ////////// store the information about a formula for later processsing ////////
  struct ZZFormulaInfo
  {
    ZZFormulaInfo(const ListObj* const & fformula, const string& fformulaStr,
                  const int& nnumPreds, const double* const & wwt, 
                  const double& ddefaultWt, const Domain* const& ddomain, 
                  MLN* const & mmln, const ZZVarNameToIdMap& vvarNameToIdMap,
                  const StringToIntMap& pplusVarMap, const int& nnumAsterisk,
                  const bool& hhasFullStop, 
                  const bool& rreadHardClauseWts,
                  const bool& mmustHaveWtOrFullStop)
      : formula(fformula), formulaStr(fformulaStr), numPreds(nnumPreds), 
        defaultWt(ddefaultWt), domain(ddomain), mln(mmln), 
        numAsterisk(nnumAsterisk), hasFullStop(hhasFullStop), 
        readHardClauseWts(rreadHardClauseWts),
        mustHaveWtOrFullStop(mmustHaveWtOrFullStop)
  
    {
      wt = (wwt) ? new double(*wwt) : NULL;
      
      ZZVarNameToIdMap::const_iterator it = vvarNameToIdMap.begin();
      for (; it != vvarNameToIdMap.end(); it++)
        varNameToIdMap[(*it).first] = ZZVarIdType((*it).second);
  
      StringToIntMap::const_iterator itt = pplusVarMap.begin();
      for (; itt != pplusVarMap.end(); itt++)
        plusVarMap[(*itt).first] = (*itt).second;
    }
  
    ~ZZFormulaInfo() { if (wt) delete wt; }
  
    const ListObj* formula;
    const string formulaStr;
    const int numPreds;
    const double* wt;
    const double defaultWt;
    const Domain* domain;
    MLN* mln;
    ZZVarNameToIdMap varNameToIdMap;
    StringToIntMap plusVarMap;
    const int numAsterisk;
    const bool hasFullStop;
    const bool readHardClauseWts;
    const bool mustHaveWtOrFullStop;
  };
  
  Array<ZZFormulaInfo*> zzformulaInfos;
  
  
  ///////////////////////////////////////////////////////////////////////
  
  string rmTmpPostfix(const string& filename)
  {
    unsigned int postfixLen = strlen(ZZ_TMP_FILE_POSTFIX);
    if (filename.length() < postfixLen) return filename;
    if (filename.compare(filename.length() - postfixLen, postfixLen, 
                         ZZ_TMP_FILE_POSTFIX, postfixLen)==0)
      return filename.substr(0, filename.length() - postfixLen); 
    else
      return filename;
  }
  
  
  void yyerror(char const * err) 
  {
    string errStr = err;
    if (strncmp(err,"parse error, unexpected '(', expecting '='",42)==0)
      errStr.append("Have you declared the predicate/function preceding '('");
  
    if (zzisParsing)
      printf("ERROR in %s: line %d, col %d: %s\n", 
             rmTmpPostfix(zzinFileName).c_str(),zzline, zzcolumn, errStr.c_str());
    else
      printf("ERROR occurs after parsing %s: %s\n", 
             rmTmpPostfix(zzinFileName).c_str(), errStr.c_str());
  
    zzok=false;
    if (++zznumErrors == ZZ_MAX_ERRORS)
    {
      cout << "Num of errors = " << zznumErrors 
           << ". Exceeded maximum number of errors." << endl;
      exit(-1);
    }
  }
  
  
  void zzerr(const char* const & str) { yyerror(str); }
  
  
  void zzerr(const char* const & str, const char* const & token)
  {
    sprintf(zzerrMsg, str, token);
    yyerror(zzerrMsg);
  }
  
  
  void zzerr(const char* const & str, const char* const & token1, 
             const char* const & token2)
  {
    sprintf(zzerrMsg, str, token1, token2);
    yyerror(zzerrMsg);
  }
  
  
  void zzerr(const char* const & str, const char* const & token1, 
             const char* const & token2, const char* const & token3)
  {
    sprintf(zzerrMsg, str, token1, token2, token3);
    yyerror(zzerrMsg);
  }
  
  
  void zzerr(const char* const & str, const char* const & token1, 
             const int& token2, const int& token3)
  {
    sprintf(zzerrMsg, str, token1, token2, token3);
    yyerror(zzerrMsg);
  }
  
  
  void zzwarn(const char* const & str)
  {
    if (zzisParsing)
      printf("WARNING in %s: line %d, col %d: %s\n", 
             rmTmpPostfix(zzinFileName).c_str(), zzline, zzcolumn, str);
    else
      printf("WARNING after parsing %s: %s\n", 
             rmTmpPostfix(zzinFileName).c_str(), str);
  }
  
  
  void zzwarn(const char* const & str, const char* const & token)
  {
    sprintf(zzerrMsg, str, token);
    zzwarn(zzerrMsg);
  }
  
  
  void zzexit(const char* const & str)
  {
    zzerr(str);
    exit(-1);
  }
  
  
  void zzexit(const char* const & str, const char* const & token)
  {
    zzerr(str,token);
    exit(-1);
  }
  
  
  void zzassert(const bool& condn, const char* const & str)
  {
    string s("assertion failed! ");
    s.append(str);
    if (!condn) zzexit(s.c_str()); 
  }
  
  
  void zzmsg(const char* const & str)
  {
    if (zzisParsing)
      printf("in %s: line %d, col %d: %s\n", 
             rmTmpPostfix(zzinFileName).c_str(), zzline, zzcolumn, str);
    else
      printf("after parsing %s: %s\n", rmTmpPostfix(zzinFileName).c_str(), str);
  }
  
  
  void zzmsg(const char* const & str, const char* const & token)
  {
    sprintf(zzerrMsg, str, token);
    zzmsg(zzerrMsg);
  }
  
  
  ///////////////////////// manage variable ids ////////////////////////
  
  string zzgetNewVarName(const char* const & varName)
  {
    ZZOldNewVarList::iterator it = zzoldNewVarList.begin();
    for (; it != zzoldNewVarList.end(); it++)
    {
      StringToStringMap* oldNewVarMap = (*it).first;
      StringToStringMap::iterator mit;
      if ((mit = oldNewVarMap->find(varName)) != oldNewVarMap->end())
        return (*mit).second;
    }
    return string(varName);
  }
  
  
    // returns var id (negative number) or 0 if varName is of wrong type
  int zzgetVarId(const char* const& varName, const int& varTypeId,
                 int& expectedTypeId)
  {
    string vname = varName;
  
      // search last element (which corresponds to the scope of the entire formula
    ZZVarNameToIdMap::iterator mit;
    if ((mit = zzvarNameToIdMap.find(vname)) == zzvarNameToIdMap.end())
    {
      ZZVarIdType v(--zzvarCounter, varTypeId);
      zzvarNameToIdMap[vname] = v;
      return v.id_;
    }
  
    ZZVarIdType& varIdType = (*mit).second;
    int typeId = varTypeId; //avoid confusion later
  
    if (varIdType.typeId_ == zzanyTypeId)
    {
      varIdType.typeId_ = typeId;
      expectedTypeId = varIdType.typeId_;
      return varIdType.id_;
    }
  
    if (typeId != zzanyTypeId && typeId != varIdType.typeId_) 
    {
      expectedTypeId = varIdType.typeId_;
      return 0;
    }
    return varIdType.id_;  
  }
  
  
  int zzgetVarTypeId(const char* const& varName)
  {
    ZZVarNameToIdMap::iterator mit;
    if ((mit = zzvarNameToIdMap.find(string(varName))) != zzvarNameToIdMap.end())
      return (*mit).second.typeId_;
    return -1;
  }
  
  
  void zzcheckVarNameToIdMap()
  {
    ZZVarNameToIdMap::iterator it = zzvarNameToIdMap.begin();
    for (;it != zzvarNameToIdMap.end(); it++)
      if ((*it).second.typeId_ == zzanyTypeId)
        zzerr("Variable %s has unknown type.", (*it).first.c_str()); 
  }
  
  
    // returns var id (negative number) or 0 if varName is of wrong type
  bool zzvarIsQuantified(const char* const& varName)
  {
    ZZOldNewVarList::iterator it = zzoldNewVarList.begin();
    for (; it != zzoldNewVarList.end(); it++)
    {
      StringToStringMap* oldNewVarMap = (*it).first;
      StringToStringMap::iterator mit;
      if ((mit = oldNewVarMap->find(varName)) != oldNewVarMap->end())
        return true;
    }
    return false;
  }
  
  
     // Caller must delete the returned VarTypeMap
  VarTypeMap* zzcreateVarTypeMap(const ZZVarNameToIdMap& map)
  {
    VarTypeMap* vtMap = new VarTypeMap;
    ZZVarNameToIdMap::const_iterator it = map.begin();
    for (; it != map.end(); it++)
      (*vtMap)[(*it).first] =(*it).second.typeId_;
    return vtMap;
  }
  
  
  void zzsetPlusVarTypeId()
  {
    StringToIntMap::iterator mit = zzplusVarMap.begin();
    for (; mit != zzplusVarMap.end(); mit++)
    {
      string plusVarName = (*mit).first;
      ZZVarNameToIdMap::iterator typeIt = zzvarNameToIdMap.find(plusVarName);
      zzassert(typeIt != zzvarNameToIdMap.end(),
               "expect typeIt != zzvarNameToIdMap.end()");
      //commented out: done in zzcheckVarNameToIdMap()
      //zzassert((*mit).second.typeId_ > 0,"expect typedId > 0");
      (*mit).second = (*typeIt).second.typeId_;
    }
  }
  
  
  ////////////////////////// predicate functions ////////////////////////
  
  
  /**
   * Checks if the name of a function is that of an internal function.
   * 
   * @param funcname Name of function to be checked
   * 
   * @return true, if name of function found, otherwise false
   */
  bool zzisInternalFunction(const char* funcname)
  {
    for (int i = 0; i < zzinternalFunctions.size(); i++)
    	if (strcmp(funcname, zzinternalFunctions[i][0]) == 0)
    	  return true;
  
    return false;
  }
  
  // Returns the index of internal function with name funcname if found,
  // otherwise 0
  int zzfindInternalFunction(const char* funcname)
  {
    for (int i = 0; i < zzinternalFunctions.size(); i++)
      if (strcmp(funcname, zzinternalFunctions[i][0]) == 0)
        return i;
    return -1;
  }
  
  /**
   * Checks if the name of a predicate is that of an internal predicate.
   * 
   * @param predname Name of predicate to be checked
   * 
   * @return true, if name of predicate found, otherwise false
   */
  bool zzisInternalPredicate(const char* predname)
  {
    for (int i = 0; i < zzinternalPredicates.size(); i++)
    	if (strcmp(predname, zzinternalPredicates[i][0]) == 0)
    	  return true;
  
    return false;
  }
  
  // Returns the index of internal predicate with name predname if found,
  // otherwise 0
  int zzfindInternalPredicate(const char* predname)
  {
    for (int i = 0; i < zzinternalPredicates.size(); i++)
      if (strcmp(predname, zzinternalPredicates[i][0]) == 0)
        return i;
    return -1;
  }
  
  /**
   * Checks if the name of a function is that of a linked-in function.
   * 
   * @param funcname Name of function to be checked
   * @param handle handle obtained from dlopen() on a file name
   * 
   * @return true, if name of function found, otherwise false
   */
  bool zzisLinkedFunction(const char* funcname, void* handle)
  {
    char *error;
  
    dlerror();    // Clear any existing error
    dlsym(handle, funcname);
    if ((error = dlerror()) != NULL) return false;
  
    return true;
  }
  
  /**
   * Checks if the name of a predicate is that of a linked-in predicate.
   * 
   * @param predname Name of predicate to be checked
   * @param handle handle obtained from dlopen() on a file name
   * 
   * @return true, if name of predicate found, otherwise false
   */
  bool zzisLinkedPredicate(const char* predname, void* handle)
  {
    char *error;
  
    dlerror();    // Clear any existing error
    dlsym(handle, predname);
    if ((error = dlerror()) != NULL) return false;
  
    return true;
  }	
  
  void zzsetEqPredTypeName(const int& typeId)
  {  
    const char * typeName = zzdomain->getTypeName(typeId);
    string eqPredName = PredicateTemplate::createEqualPredTypeName(typeName);
    const PredicateTemplate* t =
      zzdomain->getPredicateTemplate(eqPredName.c_str());
    zzpred->setTemplate((PredicateTemplate*)t);
    zzassert(t != NULL,
             "expect equal pred template != NULL");
    ListObj* predlo = zzpredFuncListObjs.top(); 
    predlo->replace(PredicateTemplate::EQUAL_NAME, eqPredName.c_str());
  }
  
  
  int zzgetTypeId(const Term* const & t, const char* const & varName)
  {
    int termType = t->getType();
    if (termType == Term::FUNCTION) 
      return t->getFunction()->getRetTypeId();
   
    if (termType == Term::CONSTANT) 
      return zzdomain->getConstantTypeId(t->getId());
  
    if (termType == Term::VARIABLE) 
    {
      ZZVarNameToIdMap::iterator mit = zzvarNameToIdMap.find(varName);
      if (mit != zzvarNameToIdMap.end()) return (*mit).second.typeId_;
      return zzanyTypeId;
    }
    zzassert(false, "expect FUNCTION, VARIABLE, CONSTANT");
    return -1;
  }
  
  
  void zzdetermineEqPredTypes(ListObj* const & formula)
  {
    unsigned int prevSize = 0;
    while (zzeqPredList.size() != prevSize)
    {
      prevSize = zzeqPredList.size();
      list<ZZUnknownEqPredInfo>::iterator lit, remIt ;
      for (lit = zzeqPredList.begin(); lit != zzeqPredList.end(); lit++)
      {
        ZZUnknownEqPredInfo& uepi = (*lit);
        string lvarName = uepi.lhs_;
        string rvarName = uepi.rhs_;
        int lTypeId = zzgetVarTypeId(lvarName.c_str());
        int rTypeId = zzgetVarTypeId(rvarName.c_str());
  
        if (lTypeId > 0 && rTypeId > 0) //if both types are known
        {
          if (lTypeId != rTypeId)
            zzerr("The types of %s and %s on the left and right of "
                  "'=' must match.", lvarName.c_str(), rvarName.c_str());
          const char * typeName = zzdomain->getTypeName(lTypeId);
          string eqPredName 
            = PredicateTemplate::createEqualPredTypeName(typeName);
          formula->replace(uepi.name_.c_str(), eqPredName.c_str());
          remIt = lit; lit++; zzeqPredList.erase(remIt);
          
        }
        else  // if only one type is known
        if ( (lTypeId<=0 && rTypeId>0) || (lTypeId>0 && rTypeId<=0) )
        {
          int knownTypeId = (lTypeId>0) ? lTypeId : rTypeId;
          const char * typeName = zzdomain->getTypeName(knownTypeId);
          string eqPredName 
            = PredicateTemplate::createEqualPredTypeName(typeName);
          formula->replace(uepi.name_.c_str(), eqPredName.c_str());
          const char* unknowVarName = (lTypeId>0) ?  rvarName.c_str() : 
                                                     lvarName.c_str();
          zzvarNameToIdMap[unknowVarName].typeId_ = knownTypeId;
          remIt = lit; lit++; zzeqPredList.erase(remIt);  
        }
      }
    }
    if (zzeqPredList.size() > 0)
    {
      zzerr("The following variables used with the '=' operator have "
           "unknown types");
      list<ZZUnknownEqPredInfo>::iterator lit; 
      for (lit = zzeqPredList.begin(); lit != zzeqPredList.end(); lit++)
        cout << (*lit).lhs_ << " " << (*lit).rhs_ << " ";
      cout << endl;
    }
  }
  
  void zzdetermineIntPredTypes(ListObj* const & formula)
  {
    unsigned int prevSize = 0;
    while (zzintPredList.size() != prevSize)
    {
      prevSize = zzintPredList.size();
      list<ZZUnknownIntPredInfo>::iterator lit, remIt ;
      for (lit = zzintPredList.begin(); lit != zzintPredList.end(); lit++)
      {
        ZZUnknownIntPredInfo& uipi = (*lit);
        string lvarName = uipi.lhs_;
        string rvarName = uipi.rhs_;
  	  string baseName = uipi.name_.substr(0, uipi.name_.find_last_of("_"));
        int lTypeId = zzgetVarTypeId(lvarName.c_str());
        int rTypeId = zzgetVarTypeId(rvarName.c_str());
  
        if (lTypeId > 0 && rTypeId > 0) //if both types are known
        {
          if (lTypeId != rTypeId)
            zzerr("The types of %s and %s on the left and right of "
                  "an internal opreator must match.",
                  lvarName.c_str(), rvarName.c_str());
          const char * typeName = zzdomain->getTypeName(lTypeId);
          string intPredName 
            = PredicateTemplate::createInternalPredTypeName(baseName.c_str(),
                                                            typeName);
          formula->replace(uipi.name_.c_str(), intPredName.c_str());
          remIt = lit; lit++; zzintPredList.erase(remIt);        
        }
        else  // if only one type is known
        if ( (lTypeId<=0 && rTypeId>0) || (lTypeId>0 && rTypeId<=0) )
        {
          int knownTypeId = (lTypeId>0) ? lTypeId : rTypeId;
          const char * typeName = zzdomain->getTypeName(knownTypeId);
          string intPredName 
            = PredicateTemplate::createInternalPredTypeName(baseName.c_str(),
                                                            typeName);
          formula->replace(uipi.name_.c_str(), intPredName.c_str());
          const char* unknowVarName = (lTypeId>0) ?  rvarName.c_str() : 
                                                     lvarName.c_str();
          zzvarNameToIdMap[unknowVarName].typeId_ = knownTypeId;
          remIt = lit; lit++; zzintPredList.erase(remIt);  
        }
      }
    }
    if (zzintPredList.size() > 0)
    {
      zzerr("The following variables used with an internal operator have "
           "unknown types");
      list<ZZUnknownIntPredInfo>::iterator lit; 
      for (lit = zzintPredList.begin(); lit != zzintPredList.end(); lit++)
        cout << (*lit).lhs_ << " " << (*lit).rhs_ << " ";
      cout << endl;
    }
  }
  
  void zzdetermineIntFuncTypes(ListObj* const & formula)
  {
    unsigned int prevSize = 0;
    while (zzintFuncList.size() != prevSize)
    {
      prevSize = zzintFuncList.size();
      list<ZZUnknownIntFuncInfo>::iterator lit, remIt ;
      for (lit = zzintFuncList.begin(); lit != zzintFuncList.end(); lit++)
      {
        ZZUnknownIntFuncInfo& uifi = (*lit);
        Array<string> varNames = uifi.vnames_;
  	  string baseName = uifi.name_.substr(0, uifi.name_.find_last_of("_"));
  
  	  bool unknownTypes = false;
        Array<int> typeIds;
        for  (int i = 0; i < varNames.size(); i++)
        {
        	int typeId = zzgetVarTypeId(varNames[i].c_str());
        	typeIds.append(typeId);
  		if (typeId <= 0)
  		{
  		  unknownTypes = true;
  		}
        }
  
        if (!unknownTypes) //if both types are known
        {
          Array<string> typeNames;
          for (int i = 0; i < typeIds.size(); i++)
          {
            string typeName = zzdomain->getTypeName(typeIds[i]);
            typeNames.append(typeName);
          }
          string intPredFromFuncName 
            = FunctionTemplate::createInternalFuncTypeName(baseName.c_str(),
                                                           typeNames);
          formula->replace(uifi.name_.c_str(), intPredFromFuncName.c_str());
          remIt = lit; lit++; zzintFuncList.erase(remIt);
        }
      }
    }
    if (zzintFuncList.size() > 0)
    {
      zzerr("The following variables used with an internal function have "
           "unknown types");
      list<ZZUnknownIntFuncInfo>::iterator lit; 
      for (lit = zzintFuncList.begin(); lit != zzintFuncList.end(); lit++)
      {
        for (int i = 1; i < (*lit).vnames_.size(); i++)
         	cout << (*lit).vnames_[i] << " ";
      }
      cout << endl;
    }
  }
  
  
  bool zzcheckRightTypeAndGetVarId(const int& typeId, const char* const& varName,
                                   int& varId)
  {
      // check that the variable is of the right type
    int expectedTypeId = -1;
    varId = zzgetVarId(varName, typeId, expectedTypeId);
    if (varId == 0)
    {
      const char* expName = zzdomain->getTypeName(typeId);
      const char* unexpName = zzdomain->getTypeName(expectedTypeId);
      zzerr("Variable %s is of the wrong type. Expected %s but given %s", 
            varName, expName, unexpName);
      return false;
    }
    return true;
  }
  
  void zzaddType(const char* const& typeName, 
                 PredicateTemplate* const& predTemplate, 
                 FunctionTemplate* const& funcTemplate,
                 bool isUnique, const Domain* const & domain)
  {
    if (isUnique && funcTemplate != NULL)
    {
      zzerr("Function parameter (%s) cannot be existentially and uniquely "
            "quantified",typeName);
      isUnique = false;
    }
  
    if (predTemplate != NULL)
    { 
      bool ok = predTemplate->appendTermType(typeName, isUnique, domain);
      if(!ok) zzexit("Term type %s should have been declared.", typeName);
    }
    else 
    if (funcTemplate != NULL) 
    {
      bool ok = funcTemplate->appendTermType(typeName, isUnique, domain);
      if (!ok) zzexit("Term type %s should have been declared.", typeName);
    }
  }
  
  
  int zzaddTypeToDomain(Domain* const & domain, const char* const & typeName)
  {
    int typeId = domain->addType(typeName);
    
    if (typeName != PredicateTemplate::ANY_TYPE_NAME)
    {
        // create a PredicateTemplate to represent '=' (equality pred) for type
      string ptName = PredicateTemplate::createEqualPredTypeName(typeName);
      if (domain->getPredicateTemplate(ptName.c_str()) == NULL)
      {
        PredicateTemplate* pt = new PredicateTemplate();
        pt->setName(ptName.c_str());
        pt->appendTermType(typeName, false, domain);
        pt->appendTermType(typeName, false, domain);
        int id = domain->addPredicateTemplate(pt);
        zzassert(id >= 0, "expect pred template id >= 0");
        pt->setId(id);
      }
      
        // create a PredicateTemplate for each internal pred. for this type
  /*
      Array<string> ptNames =
        PredicateTemplate::createInternalPredTypeNames(typeName);
  	for (int i = 0; i < ptNames.size(); i++)
  	{
  	  string ptName = ptNames[i];
  	  if (domain->getPredicateTemplate(ptName.c_str()) == NULL)
        {
        	PredicateTemplate* pt = new PredicateTemplate();
        	pt->setName(ptName.c_str());
        	pt->appendTermType(typeName, false, domain);
        	pt->appendTermType(typeName, false, domain);
        	int id = domain->addPredicateTemplate(pt);
        	zzassert(id >= 0, "expect pred template id >= 0");
        	pt->setId(id);
        }
  	}
  */
    }
  
    return typeId;
  }
  
  void zzcreatePred(Predicate*& pred, const char* const & predName)
  {
    const PredicateTemplate* t = zzdomain->getPredicateTemplate(predName);
    if (t==NULL)
    {
    	int index = zzfindInternalPredicate(predName);
    	// Internal predicates are declared on the fly
      if (index >= 0)
      {
        zzassert(zzdomain->getFunctionId(predName) < 0, 
      	       "not expecting pred name to be declared as a function name");
    	  PredicateTemplate* ptemplate = new PredicateTemplate();
    	  ptemplate->setName(predName);
   	
    	  // Add types
    	  for (int j = 1; j < zzinternalPredicates[index].size(); j++)
    	  {
    	    int id;
    	    const char* ttype = zzinternalPredicates[index][j];
    	    if (!zzdomain->isType(ttype))
    	    {
  		  id = zzaddTypeToDomain(zzdomain, ttype);
    		  zzassert(id >= 0, "expecting var id >= 0");
    	    }
    	    zzaddType(ttype, ptemplate, NULL, false, zzdomain);
  	    //delete [] ttype;
    	  }
    	
     	  // Add template to domain
    	  zzassert(ptemplate, "not expecting ptemplate==NULL");
  	  int id = zzdomain->addPredicateTemplate(ptemplate);
    	  zzassert(id >= 0, "expecting pred template id >= 0");
    	  ptemplate->setId(id);
  	  zzassert(pred == NULL, "expect pred == NULL");
    	  pred = new Predicate(ptemplate);
    	  return; 
      }
      else
    	  zzexit("Predicate %s should have been declared.", predName);
    }
      // commented out because when zzcreatePred is called predicate has already 
      // been declared
    //if (t == NULL) 
    //{
    //  zzerr("Failed to find predicate %s. Have you declared it?", predName);
    //    // create a fake predicate template and attempt to recover
    //  char buf[32];
    //  sprintf(buf, "%s%d", zzdefaultPredName, zzcount++); 
    //  zzpredTemplate = new PredicateTemplate();
    //  zzpredTemplate->setDomain(zzdomain);
    //  zzpredTemplate->setName(buf);
    //  int id = zzdomain->addPredicateTemplate(zzpredTemplate);
    //  zzassert(id >= 0, "expect id >= 0");
    //  zzpredTemplate->setId(id);
    //  for (int i = 0; i < 20; i++)
    //  {
    //    sprintf(buf, "%s%d",zzdefaultTypeName, zzcount++); 
    //    bool ok = zzpredTemplate->appendTermType(buf, false, zzdomain);
    //    if(!ok) zzexit("");
    //  }
    //  t = zzpredTemplate;
    //  zzpredTemplate = NULL;
    //}
  
    zzassert(pred == NULL, "expect pred == NULL");
    pred = new Predicate(t); 
  }
  
  
  
  void zzcheckPredNumTerm(Predicate*& pred)
  {
    int exp, unexp;
    if ((unexp=pred->getNumTerms()) != (exp=pred->getTemplate()->getNumTerms()))
    {
      zzerr("Wrong number of terms for predicate %s. Expected %d but given %d", 
            pred->getName(), exp, unexp);
    
      char buf[128];
        // try to recover
      for (int i = unexp; i < exp; i++)
      {
        sprintf(buf, "%s%d", zzdefaultVarName, zzcount++); 
        int typeId = pred->getTermTypeAsInt(i);
        int varId;
        bool rightType = zzcheckRightTypeAndGetVarId(typeId, buf, varId);
        if (!rightType) zzexit("");
        pred->appendTerm(new Term(varId, (void*)pred, true));
      }
    }
  }
  
  
  void zzpredAppendConstant(Predicate* const& pred, const int& constId,
                            const char* const & constName)
  {    
      // if exceeded the number of terms
    int exp, unexp;
    if ((unexp=pred->getNumTerms()) == (exp=pred->getTemplate()->getNumTerms()))
    {
      zzerr("Wrong number of terms for predicate %s. Expected %d but given >%d", 
            pred->getName(), exp, unexp);
      return;
    }
  
      // if this is not '=' predicate with unknown types
    if (!(strcmp(pred->getName(),PredicateTemplate::EQUAL_NAME) == 0) &&
    	  !(strcmp(pred->getTermTypeAsStr(pred->getNumTerms()),
                 PredicateTemplate::ANY_TYPE_NAME) == 0))
    {
        // Check that constant has same type as that of predicate term
      int typeId = pred->getTermTypeAsInt(pred->getNumTerms());
      int unexpId; 
      if (typeId != (unexpId=zzdomain->getConstantTypeId(constId)))
      {
        const char* expName = zzdomain->getTypeName(typeId);
        const char* unexpName = zzdomain->getTypeName(unexpId);
        zzerr("Constant %s is of the wrong type. Expected %s but "
              "given %s", constName, expName, unexpName);
        return;
      }
    }
    
      // at this point, we have the right num of terms and right constant types
    if (pred != NULL) pred->appendTerm(new Term(constId, (void*)pred, true));
  }
  
  
  ////////////////////////// function functions ////////////////////////
  
  void zzconsumeToken(StrFifoList& tokenList, const char* c)
  {
    const char* tok = tokenList.removeLast();
    if (strcmp(tok, c)!=0)
    {
      cout << "token = '" << tok << "', '" << c << "'" << endl;
      zzassert(strcmp(tok, c)==0, "expect strcmp(tok,c)==0");
    }
    delete [] tok;
  }
  
  
  void zzcreateFunc(Function*& func, const char* const & funcName)
  {
    const FunctionTemplate* t = zzdomain->getFunctionTemplate(funcName);
    if (t==NULL)
    {
    	// Internal functions are declared on the fly
      int index;
  	if ((index = zzfindInternalFunction(funcName)) >= 0)
   	{
        zzassert(zzfuncTemplate==NULL, "expecting zzfuncTemplate==NULL");
  	  zzfuncTemplate = new FunctionTemplate();
  
  	  // We are creating a new predicate as well
    	  zzassert(zzpredTemplate==NULL,"expecting zzpredTemplate==NULL");
    	  zzpredTemplate = new PredicateTemplate();
  
  	  zzassert(zzdomain->getPredicateId(funcName) < 0, 
      	       "not expecting func name to be declared as pred name");
    	  zzassert(zzfuncTemplate,"expecting zzfuncTemplate!=NULL");
  	  zzfuncTemplate->setName(funcName);
  
  	  // Predicate name is PredicateTemplate::ZZ_RETURN_PREFIX + function name
  	  char* predName;
  	  predName = (char *)malloc((strlen(PredicateTemplate::ZZ_RETURN_PREFIX) +
    		    					strlen(funcName) + 1)*sizeof(char));
   	  strcpy(predName, PredicateTemplate::ZZ_RETURN_PREFIX);
  	  strcat(predName, funcName);
      	
  	  // Check that predicate has not been declared a function
  	  zzassert(zzdomain->getFunctionId(predName) < 0, 
    		       "not expecting pred name to be declared as a function name");
    	  zzassert(zzpredTemplate,"expecting zzpredTemplate!=NULL");
   	  zzpredTemplate->setName(predName);
  	  delete [] predName;  
    	
    	  // Add return type
    	  const char* retTypeName = zzinternalFunctions[index][1];
  
  	  if (!zzdomain->isType(retTypeName))
    	  {
     	    int id = zzaddTypeToDomain(zzdomain, retTypeName);
          zzassert(id >= 0, "expecting retTypeName's id >= 0");
    	  }
  
  	  zzfuncTemplate->setRetTypeName(retTypeName,zzdomain);
    	  // We are creating a new predicate as well
  	  zzaddType(retTypeName, zzpredTemplate, NULL, false, zzdomain);
    
    	  // Add types
    	  for (int j = 2; j < zzinternalFunctions[index].size(); j++)
    	  {
    	    int id;
    	    const char* ttype = zzinternalFunctions[index][j];
    	    if (!zzdomain->isType(ttype))
    	    {
  		  id = zzaddTypeToDomain(zzdomain, ttype);
    		  zzassert(id >= 0, "expecting var id >= 0");
    	    }
    	    zzaddType(ttype, zzpredTemplate, NULL, false, zzdomain);
  	    // Add the type to the function too
  	    zzaddType(ttype, NULL, zzfuncTemplate, false, zzdomain);
    	  }
  
  	  // Add templates to domain
  	  zzassert(zzfuncTemplate, "expecting zzfuncTemplate != NULL");
  	  int id = zzdomain->addFunctionTemplate(zzfuncTemplate);
  	  zzassert(id >= 0, "expecting function template's id >= 0");
  	  zzfuncTemplate->setId(id);
  
  	  zzassert(zzpredTemplate, "not expecting zzpredTemplate==NULL");
  	  int predId = zzdomain->addPredicateTemplate(zzpredTemplate);
  	  zzassert(predId >= 0, "expecting pred template id >= 0");
  	  zzpredTemplate->setId(predId);
  
  	  zzassert(func == NULL, "expect func == NULL");
    	  func = new Function(zzfuncTemplate);
  	  zzfuncTemplate = NULL;
  	  zzpredTemplate = NULL;
  	  return;
  	}
    	else
      	zzexit("Function %s should have been declared.", funcName);
    }
    //if (t == NULL) 
    //{
    //  zzerr("Failed to find function %s. Have you declared it?", funcName);
    //    // create a fake predicate template and attempt to recover
    //  char buf[32];
    //  sprintf(buf, "%s%d", zzdefaultFuncName, zzcount++); 
    //  zzfuncTemplate = new FunctionTemplate();
    //  zzfuncTemplate->setDomain(zzdomain);
    //  zzfuncTemplate->setRetTypeName(PredicateTemplate::ANY_TYPE_NAME);
    //  zzfuncTemplate->setName(buf);
    //  int id = zzdomain->addFunctionTemplate(zzfuncTemplate);
    //  zzassert(id >= 0, "expect id >= 0");
    //  zzfuncTemplate->setId(id);
    //  for (int i = 0; i < 20; i++)
    //  {
    //    sprintf(buf, "%s%d",zzdefaultTypeName, zzcount++); 
    //    bool ok = zzfuncTemplate->appendTermType(buf, false, zzdomain);
    //    if(!ok) zzexit("");
    //  }
    //  t = zzfuncTemplate;
    //  zzfuncTemplate = NULL;
    //}
  
    zzassert(func == NULL, "expect func == NULL");
    func = new Function(t);
  }
  
  
  void zzcheckFuncNumTerm(Function*& func)
  {
    int exp, unexp;
    if ((unexp=func->getNumTerms()) != (exp=func->getTemplate()->getNumTerms()))
    {
      zzerr("Wrong number of terms for func %s. Expected %d but given %d", 
            func->getName(), exp, unexp);
    
      char buf[128];
        // try to recover
      for (int i = unexp; i < exp; i++)
      {
        sprintf(buf, "%s%d", zzdefaultVarName, zzcount++); 
        int typeId = func->getTermTypeAsInt(i);
        int varId;
        bool rightType = zzcheckRightTypeAndGetVarId(typeId, buf, varId);
        if (!rightType) zzexit("");
        func->appendTerm(new Term(varId, (void*)func, false));
      }
    }
  }
  
  
  void zzfuncAppendConstant(Function* const& func, const int& constId,
                            const char* const & constName)
  {    
      // if exceeded the number of terms
    int exp, unexp;
    if ((unexp=func->getNumTerms()) == (exp=func->getTemplate()->getNumTerms()))
    {
      zzerr("Wrong number of terms for function %s. Expected %d but given > %d", 
            func->getName(), exp, unexp);
      return;
    }
  
    if (!(strcmp(func->getTermTypeAsStr(func->getNumTerms()),
                 PredicateTemplate::ANY_TYPE_NAME)==0))
    {
  	  // Check that constant has same type as that of predicate term
    	int typeId = func->getTermTypeAsInt(func->getNumTerms());
    	int unexpId; 
    	if (typeId != (unexpId=zzdomain->getConstantTypeId(constId)))
    	{
        const char* expName = zzdomain->getTypeName(typeId);
        const char* unexpName = zzdomain->getTypeName(unexpId);
        zzerr("Constant %s is of the wrong type. Expected %s but given %s", 
              constName, expName, unexpName);
        return;
    	}
    }
      // at this point, we have the right num of term and right constant type
    if (func != NULL) func->appendTerm(new Term(constId, (void*)func, false));
  }
  
  
  /////////////////////// create clause from list obj//////////////////////////
  
  void zzpermuteAsteriskedPreds(const int& numAsterisk, 
                                const ListObj* const & formula,
                                const string& formulaStr,
                                Array<ListObj*>& clauses,
                                Array<string>& formulaStrs)
  {
    clauses.clear();
    formulaStrs.clear();
    if (numAsterisk == 0) 
    { 
      clauses.append( new ListObj(formula)); 
      formulaStrs.append(formulaStr);
      return; 
    }
  
    Array<int> astIdxs;
    for (unsigned int i = 0; i < formulaStr.length(); i++)
      if (formulaStr.at(i) == '*') astIdxs.append(i);
    assert(astIdxs.size() == numAsterisk);
  
      // add numAsterisk number of [false][true] to ArraysAccessor
    ArraysAccessor<bool> acc;
    for (int i = 0; i < numAsterisk; i++)
    {
      Array<bool>* a = new Array<bool>(2); 
      a->append(false); a->append(true);
      acc.appendArray(a);
    }
  
    Array<bool> bArr;
    while (acc.getNextCombination(bArr))
    {
        // create a copy of the formula
      clauses.append(new ListObj(formula));
      int idx = 0;    
      clauses[clauses.size()-1]->replaceAsterisk(bArr, idx);
  
      string s = formulaStr;
      assert(bArr.size() == astIdxs.size());
      for (int j = 0; j < bArr.size(); j++)
        s.at(astIdxs[j]) = (bArr[j]) ? ' ' : '!';
  
      formulaStrs.append(s);
    }
  
    acc.deleteArraysAndClear();
  }
  
  
  void zzgetDisjunctions(const ListObj* const & lo, Array<ListObj*>& clauses)
  {
    const Array<ListObj*>& lobjs = lo->getList();
    
    if ((lobjs[0]->getStr())[0] != '^')
    {
      clauses.append((ListObj*)lo);
      return;
    }
    
    for (int i = 1; i < lobjs.size(); i++)
      clauses.append(lobjs[i]);
  }
  
    // Checks if name starts with upper case or " (string constant)
  const bool zzisConstant(const char* const & name)
  {
    return (isupper(name[0]) || name[0] == '"');
  }
  
  Function* zzcreateFunc(const ListObj* const & lo)
  {
    const Array<ListObj*>& termlo = lo->getList();
    const char* funcName = termlo[0]->getStr();
    Function* func = NULL;
    zzcreateFunc(func, funcName);
    for (int i = 1; i < termlo.size(); i++)
    {
      if (termlo[i]->isStr())  // if is a constant or variable
      {
        const char* name = termlo[i]->getStr();
        //if (isupper(name[0]))  // if is a constant
        if (zzisConstant(name))  // if is a constant
        {
          int constId = zzdomain->getConstantId(name);
          if (constId < 0) 
            zzexit("zzcreateFunc(): failed to find constant %s. "
                   "Have you declared it?", name);
          zzfuncAppendConstant(func, constId, name);
        }
        else  // is a variable
        {
          if (func->getNumTerms() == func->getTemplate()->getNumTerms())
            zzexit("zzcreateFunc(): Function %s has too many terms", 
                   func->getName());
  
            // check the type of the term that is to be added
          int typeId = func->getTermTypeAsInt(func->getNumTerms());
          int expectedTypeId; 
          int varId = zzgetVarId(name,typeId, expectedTypeId);
  
          if (varId==0) 
            zzexit("zzcreateFunc(): failed to create term, variable %s has wrong "
                   "type", name);
          func->appendTerm(new Term(varId, (void*)func, false));        
        }
      }
      else // is a function
      {
          //push onto stack
        Function* termFunc = zzcreateFunc(termlo[i]);    
        Term* newTerm = new Term(termFunc, (void*)func, false);
        termFunc->setParent(newTerm);
        func->appendTerm(newTerm);
      }
    }
    
    zzcheckFuncNumTerm(func);
    return func;
  } 
  
  
  Predicate* zzcreatePred(const ListObj* const & lo)
  {
    const Array<ListObj*>& termlo = lo->getList();
    const char* predName = termlo[0]->getStr();
    Predicate* pred = NULL;
    zzcreatePred(pred, predName);
    for (int i = 1; i < termlo.size(); i++)
    {
      if (termlo[i]->isStr())  // if is a constant or variable
      {
        const char* name = termlo[i]->getStr();
        //if (isupper(name[0]))  // if is a constant
        if (zzisConstant(name))  // if is a constant
        {
          int constId = zzdomain->getConstantId(name);
          if (constId < 0) 
            zzexit("zzcreatePred(): failed to find constant %s. "
                   "Have you declared it?", name);
          zzpredAppendConstant(pred, constId, name);
        }
        else  // is a variable
        {
          if (pred->getNumTerms() == pred->getTemplate()->getNumTerms())
            zzexit("zzcreatePred(): Predicate %s has too many terms", 
                   pred->getName());
  
            // check the type of the term that is to be added
          int typeId = pred->getTermTypeAsInt(pred->getNumTerms());
          int expectedTypeId;
          int varId = zzgetVarId(name,typeId,expectedTypeId);
  
          if (varId==0) 
            zzexit("zzcreatePred(): failed to create term, variable %s has wrong "
                   "type", name);
          pred->appendTerm(new Term(varId, (void*)pred, true));        
        }
      }
      else // is a function
      {
        Function* func = zzcreateFunc(termlo[i]);
        Term* newTerm = new Term(func, (void*)pred, true);
        func->setParent(newTerm);
        pred->appendTerm(newTerm);
      }
    }
    
    zzcheckPredNumTerm(pred);
    return pred;
  } 
  
  
  void zzcreateClause(const ListObj* const & lo, Clause* const & clause)
  {
    zzvarCounter = 0;
    zzvarNameToIdMap.clear();
  
    const Array<ListObj*>& clauselo = lo->getList();
    if (strcmp(clauselo[0]->getStr(), "v")==0)
    {
      for (int i = 1; i < clauselo.size(); i++)
      {
        const Array<ListObj*>& predlo = clauselo[i]->getList();
        Predicate* pred;
  
        if ((predlo[0]->getStr())[0] == '!')
        {
          pred = zzcreatePred(predlo[1]);
          pred->setSense(false);
        }
        else
          pred = zzcreatePred(clauselo[i]);
        pred->setParent(clause);
        clause->appendPredicate(pred);
      }
    }
    else
    {
      Predicate* pred;
      if (((*lo)[0]->getStr())[0] == '!')
      {
        pred = zzcreatePred((*lo)[1]);
        pred->setSense(false);
      }
      else
        pred = zzcreatePred(lo);
      pred->setParent(clause);
      clause->appendPredicate(pred);
    }
  
    zzcheckVarNameToIdMap();
  }
  
  
    // clauses are those that occur together in CNF
  void zzcreateClauses(const ListObj* const & lo, Array<Clause*>& clauses,
                       Clause*& flippedClause)
  {
    flippedClause = NULL;
      // clauseOfUnitPreds contains the predicates of unit clauses
      // e.g if the cnf formula is P(x) ^ Q(x) ^ (P(y) v Q(y))
      // then clauseOfUnitPreds is !P(x) v !Q(x)
    Clause* clauseOfUnitPreds = new Clause;
    ListObj* unitPreds = new ListObj; ListObj orr("v"); unitPreds->append(&orr);
    Array<ListObj*> disjunctions;
    zzgetDisjunctions(lo, disjunctions);
    for (int i = 0; i < disjunctions.size(); i++)
    {
      Clause* clause = new Clause();
      zzcreateClause(disjunctions[i], clause);
      if (clause->getNumPredicates() > 1)
        clauses.append(clause);
      else
      {
        unitPreds->append(disjunctions[i]);
        delete clause;
      }
    }
  
    if (unitPreds->size() > 1) zzcreateClause(unitPreds, clauseOfUnitPreds);
    unitPreds->clear();
    delete unitPreds;
  
    if (clauseOfUnitPreds->getNumPredicates() > 1)
    {
      for (int i = 0; i < clauseOfUnitPreds->getNumPredicates(); i++)
        ((Predicate*)clauseOfUnitPreds->getPredicate(i))->invertSense();
      clauses.append(clauseOfUnitPreds);
      flippedClause = clauseOfUnitPreds;
    }
    else
    if (clauseOfUnitPreds->getNumPredicates() == 1) 
    {
        //if these is only one unit pred, then don't invert its sense
      clauses.append(clauseOfUnitPreds);
    }
    else
      delete clauseOfUnitPreds;
  }
  
  
  /**
   * Creates blocks in a domain based on existentially and uniquely quantified
   * variables (the ! operator). All predicates are examined if they have been marked
   * as block predicates.
   * 
   * @param domain Domain in which the blocks are created.
   * 
   * @return Number of blocks created.
   */
  int zzcreateBlocks(const Domain* const & domain)
  {
    int totalNumPreds = 0;
    int numFOPreds = domain->getNumPredicates();
    for (int p = 0; p < numFOPreds; p++)
    {
      const PredicateTemplate* pt = domain->getPredicateTemplate(p);
      const Array<int>* uniqueVarIndexes = pt->getUniqueVarIndexes();
        // If predicate has no blocked vars, then continue
      if (uniqueVarIndexes->size() == 0) continue;
  
      Predicate* pred = domain->createPredicate(p, false);
        // Save variable ids, set unique vars to dummy id, ground pred to generate
        // blocks, then set var ids back to original and add as block to domain
      Array<int> uniqueVarIds;
        // Save var ids
      for (int i = 0; i < pred->getNumTerms(); i++)
      {
        if (uniqueVarIndexes->contains(i))
          uniqueVarIds.append(pred->getTerm(i)->getId());
      }
        // Set dummy id
      for (int i = 0; i < uniqueVarIndexes->size(); i++)
      {
        ((Term*)pred->getTerm((*uniqueVarIndexes)[i]))->setId(0);
      }
        // Ground pred to generate blocks 
      Array<Predicate*> predArr;
      pred->createAllGroundings(domain, predArr);
      int numPreds = predArr.size();
      totalNumPreds += numPreds;
  
      for (int i = 0; i < numPreds; i++)
      {
        Predicate* newPred = predArr[i];
          // Set var ids back to original
        for (int j = 0; j < uniqueVarIndexes->size(); j++)
        {
          Term* t = (Term*)newPred->getTerm((*uniqueVarIndexes)[j]);
          t->setId(uniqueVarIds[j]);
        }
          // Add as block to domain
        int blockIdx = domain->addPredBlock(newPred);
  
        bool trueOne = false;
          // If groundings of this pred occur, then make sure exactly one is true
          // and tell this to the domain
        if ((zzpredIdToGndPredMap.find(pred->getId())) != 
            zzpredIdToGndPredMap.end())
        {
          PredicateHashArray* pha = zzpredIdToGndPredMap[pred->getId()];
          for (int j = 0; j < pha->size(); j++)
          {
            Predicate* gndPred = (*pha)[j];
              // Only one atom in a block can be true
            if (gndPred->getTruthValue() == TRUE &&
                newPred->canBeGroundedAs(gndPred))
            {
              if (domain->getBlockEvidence(blockIdx))
                zzexit("More than one true atom found for mutually "
                       "exclusive and exhaustive variables");
              domain->setBlockEvidence(blockIdx, true);
              domain->setTruePredInBlock(blockIdx, new Predicate(*gndPred));
              trueOne = true;
            }
          }
        }
          // Query pred: There does not have to be a true one
        else
          trueOne = true;
        
          // One pred has to be true
        if (!trueOne)
        {
          zzexit(": No true atom was found for mutually "
                 "exclusive and exhaustive variables");
        }
      }
      delete pred;
    }
    return totalNumPreds;
  }
  
  
  //////////create formulas by grounding variables preceded by a plus///////////
  
  void zzgroundPlusVar(const ListObj* const & formula, const string& formulaStr,
                       const StringToIntMap& varNameToTypeIdMap, 
                       Array<ListObj*>& formulas, Array<string>& formulaStrs,
                       const Domain* const & domain,const Domain* const & domain0)
  {
    formulas.clear();
    formulaStrs.clear();
    if (varNameToTypeIdMap.size()==0) 
    {
      formulas.append(new ListObj(formula));
      formulaStrs.append(formulaStr);
      return; 
    }
  
    Array<Array<int>*> cleanUp;
    ArraysAccessor<int> acc;
    Array<string> varNames;
    StringToIntMap::const_iterator mit = varNameToTypeIdMap.begin();
    for (; mit != varNameToTypeIdMap.end(); mit++)
    {
      int typeId = (*mit).second;
      zzassert(typeId > 0, "expect typeId > 0");
  
      Array<int>* constArr;
      constArr = (Array<int>*) domain->getConstantsByType(typeId);
  
      acc.appendArray(constArr);
      varNames.append((*mit).first);
    }
  
    Array<int> constIds;
    while (acc.getNextCombination(constIds))
    {
      ListObj* gndFormula = new ListObj(formula);
      string s = formulaStr;
  
      zzassert(constIds.size() == varNames.size(),
               "expect constIds.size() == varNames.size()");
      for (int i = 0; i < varNames.size(); i++)
      {
        const char* constName = domain->getConstantName(constIds[i]);
        ListObj::replace(gndFormula, varNames[i].c_str(), constName, domain);
        unsigned int a = s.find("+" + varNames[i]);
        assert(a != string::npos);
        s.replace(a, varNames[i].length() + 1, constName);
      }
      formulas.append(gndFormula);
      formulaStrs.append(s);
    }
    //acc.deleteArraysAndClear();
  
    if (domain0) cleanUp.deleteItemsAndClear();
  }
  
  ////////////////////////////// misc //////////////////////////////////
  
  
  void zzcreateListObjFromTop(stack<ListObj*>& stack, const char* const & op)
  {
    //zzassert(zzformulaListObjs.size()>=1, "expect zzformulaListObjs.size()>=1");  
    zzassert(stack.size() >= 1, "expect stack.size()>=1");  
    ListObj* lo1 = stack.top(); stack.pop();
    ListObj* lo = new ListObj; lo->append(op); lo->append(lo1);
    stack.push(lo);
  }
  
  
  void zzcreateListObjFromTopTwo(stack<ListObj*>& stack, const char* const & op)
  {
    //zzassert(zzformulaListObjs.size()>=2,"expect zzformulaListObjs.size()>=2");  
    zzassert(stack.size()>=2,"expect stack.size()>=2");  
    ListObj* lo1 = stack.top(); stack.pop();
    ListObj* lo2 = stack.top(); stack.pop();
  
    if ((strcmp(op,"v")==0 && lo2->hasOrOp()) || 
        (strcmp(op,"^")==0 && lo2->hasAndOp()))
    {
      lo2->append(lo1);
      stack.push(lo2);
    }
    else
    {
      ListObj* lo = new ListObj; lo->append(op); lo->append(lo2); lo->append(lo1);
      stack.push(lo);
    }
  }
  
  
  void zzcreateListObjFromTopThree(stack<ListObj*>& stack)
  {
    //zzassert(zzformulaListObjs.size()>=3, "expect zzformulaListObjs.size()>=3");  
    zzassert(stack.size()>=3, "expect stack.size()>=3");  
    ListObj* lo1 = stack.top(); stack.pop();
    ListObj* lo2 = stack.top(); stack.pop();
    ListObj* lo3 = stack.top(); stack.pop();
    ListObj* lo = new ListObj; lo->append(lo3); lo->append(lo2); lo->append(lo1);
    stack.push(lo);
  }
  
  
  void zzcreateIntConstant(char* const & buf, const char* const & typeName, 
                         const int& i)
  { sprintf(buf, "C@%s@%d", typeName, i); }
  
    // Checks all types of domain if C@type@intStr is in domain
  bool isIntConstant(const int& i, const Domain* const & domain)
  {
    const Array<const char*>* typeNames = domain->getTypeNames();
    for (int j = 0; j < typeNames->size(); j++)
    {
    	char constName[100];
    	zzcreateIntConstant(constName, (*typeNames)[j], i);
    	if (domain->isConstant(constName)) 
    	{
    	  return true;
    	}
    }
    return false;
  }
  
    // Returns the first type found to have C@type@intStr as a constant
  const char* getIntConstantTypeName(const int& i, const Domain* const & domain)
  { 
    const Array<const char*>* typeNames = domain->getTypeNames();
    for (int j = 0; j < typeNames->size(); j++)
    {
    	char constName[100];
    	zzcreateIntConstant(constName, (*typeNames)[j], i);
    	if (domain->getConstantId(constName) >= 0) return (*typeNames)[j];
    }
    return NULL;
  }
  
  void zzcreateAndCheckIntConstant(const char* const & intStr,
                                   const Function* const & func,
                                   const Predicate* const & pred,
                                   const Domain* const & domain,
                                   char* constName)
  {
    double d = atof(intStr); int i = int(d);
    if (d!=i) zzerr("%s cannot be a term. Only integer terms are allowed",intStr);
    
    const char* typeName = NULL;
    if (func) typeName = func->getTermTypeAsStr(func->getNumTerms());
    else      typeName = pred->getTermTypeAsStr(pred->getNumTerms());
  
    if (typeName == NULL) 
    { zzerr("Too many terms for predicate/function"); constName = NULL; return;}
  
  	// If type name is still open, then try to determine it
    if (strcmp(typeName, PredicateTemplate::ANY_TYPE_NAME)==0)
    {
    	  // Constant may have been previously declared
    	if (isIntConstant(i, domain))
  	  typeName = getIntConstantTypeName(i, domain);
    }
  
    zzcreateIntConstant(constName, typeName, i);
  
    char buf[30]; sprintf(buf,"%f",d);
    if (zzconstantMustBeDeclared && domain->getConstantId(constName) < 0)
      zzerr("Constant %s must be declared before it is used", buf);
  }
  
  
    //ASSUMPTION: users don't define truth values of '=' ground preds e.g. A=A
  void zzaddGndPredsToDb(Database* const & db)
  {
      // Add explicit evidence to db
    int numPreds = zzdomain->getNumPredicates();
    hash_map<int, PredicateHashArray*>::iterator it;
    for (int i = 0; i < numPreds; i++)
    {
      if ((it = zzpredIdToGndPredMap.find(i)) != zzpredIdToGndPredMap.end())
      {
        PredicateHashArray* predHashArray = (*it).second;
        for (int j = 0; j < predHashArray->size(); j++)
          db->addEvidenceGroundPredicate((*predHashArray)[j]);
  
        predHashArray->deleteItemsAndClear();
      }
      else
      {
        //  '=' predicates are handled specially by database
      }
    }
  
      // If the predicate occurs in the mln with a non-evidence atom, then add
      // it to the index in DB
      
      // Keep track of preds already indexed
    Array<Predicate*> indexedPreds;
    
    for (int i = 0; i < zzmln->getNumClauses(); i++)
    {
      const Clause* clause = zzmln->getClause(i);
        // First check if non-evid. pred is in clause
      Array<bool> nonEvidPred(clause->getNumPredicates(), false);
      bool oneNonEvidPred = false;
      for (int j = 0; j < clause->getNumPredicates(); j++)
      {
        Predicate* pred = clause->getPredicate(j);
        if (!db->isClosedWorld(pred->getId()))
        {
          nonEvidPred[j] = true;
          oneNonEvidPred = true;
        }
      }
  
        // If at least one pred is non-evid., then create index for evidence
      if (oneNonEvidPred)
      {
        for (int j = 0; j < clause->getNumPredicates(); j++)
        {
          if (!nonEvidPred[j])
          {
            Predicate* pred = clause->getPredicate(j);
            if (pred->isEqualPred()) continue;
              // Neg. literal means true groundings are added to index which
              // already happened above in addEvidenceGroundPredicate
            if (!pred->getSense())
              continue;
  
            for (int k = 0; k < indexedPreds.size(); k++)
            {
              if (indexedPreds[k]->canBeGroundedAs(pred))
                continue;
            }
              // Add all groundings to index
            indexedPreds.append(pred);
              // Generate groundings to add to index
            Array<Predicate*> predArr;
            pred->createAllGroundings(zzdomain, predArr);
            int numPreds = predArr.size();
            for (int l = 0; l < numPreds; l++)
            {
              Predicate* newPred = predArr[l];
              db->addPredToEvidenceIndex(newPred, pred->getSense());
              delete newPred;
            }
          }
        }
      }
    }
  
    for (unsigned int i = 0; i < zzpredIdToGndPredMap.size(); i++)
      delete zzpredIdToGndPredMap[i]; 
  }
  
  
  void zzcreateBoolArr(int idx, Array<bool>*& curArray,
                       Array<Array<bool>*>& boolArrays)
  {  
    --idx;
  
    Array<bool>* copyArray = new Array<bool>(*curArray);
  
    curArray->append(true);
    copyArray->append(false);
  
    if (idx == 0) 
    {
      boolArrays.append(curArray);
      boolArrays.append(copyArray);
    }
    else
    {
      zzcreateBoolArr(idx, curArray, boolArrays);
      zzcreateBoolArr(idx, copyArray, boolArrays);
    }
  }
  
  
    // vs (variable or string) is the name of the constant
  void zzaddConstantToDomain(const char* const & vs, const char* const & typeName)
  {
    //if it is not a string and it does not begin with an uppercase char
    //if (vs[0] != '"' && !isupper(vs[0]))
    if (!zzisConstant(vs))
    {
      zzerr("Constant %s must begin in uppercase char or be a \"string\".", vs);
      return;
    }
  
    zzassert(typeName != NULL, "expect typeName != NULL");
    int id = zzdomain->addConstant(vs, typeName);
    if (id < 0) zzerr("Failed to add constant %s", vs);
  }
  
  
  void zzaddConstantToPredFunc(const char* const & constName)
  {
      //commented out because a constant can be declared with its first appearance
    //int constId = zzcheckConstantAndGetId(constName);
   
    int constId = zzdomain->getConstantId(constName);
    if (constId < 0) 
    {
      const char* typeName = NULL;
      if (zzfunc) typeName = zzfunc->getTermTypeAsStr(zzfunc->getNumTerms());
      else
      if (zzpred) typeName = zzpred->getTermTypeAsStr(zzpred->getNumTerms());
  
        // May be continuing after a parse error
      if (typeName == NULL) 
      {
        zzwarn("Wrong number of terms.");
        typeName=PredicateTemplate::ANY_TYPE_NAME;
      }
  
      zzaddConstantToDomain(constName, typeName);
      constId = zzdomain->getConstantId(constName);
    }
    if (zzfunc) zzfuncAppendConstant(zzfunc, constId, constName);
    else if (zzpred) zzpredAppendConstant(zzpred, constId, constName);
    else zzexit("No predicate or function is defined.");
  }
  
  
  void zztermIsConstant(const char* const & constName,
                        const char* const & constStr, const bool& appendToFormula)
  {
    int constId = zzdomain->getConstantId(constName);
      //commented out because a constant can be declared with its first appearance
    //if (constId < 0) zzexit("Failed to find constant %s. Have you declared it?",
    //                        constName);
    if (constId < 0) 
    {
      const char* typeName = NULL;
      if (zzfunc) typeName = zzfunc->getTermTypeAsStr(zzfunc->getNumTerms());
      else
      if (zzpred) typeName = zzpred->getTermTypeAsStr(zzpred->getNumTerms());
  
        // May be continuing after a parse error
      if (typeName==NULL) 
      {
        zzwarn("Wrong number of terms.");
        typeName=PredicateTemplate::ANY_TYPE_NAME;
      }
  
      zzaddConstantToDomain(constName, typeName);
      constId = zzdomain->getConstantId(constName);
    }
  
      //always check zzfunc first, as a function can be found inside a predicate
    if (zzfunc != NULL)      
    {
      zzfuncAppendConstant(zzfunc, constId, constName);
      zzpredFuncListObjs.top()->append(constName);
    }
    else 
    if (zzpred != NULL) 
    {
      zzpredAppendConstant(zzpred, constId, constName);
      zzassert(zzpredFuncListObjs.size()==1, 
               "expect zzpredFuncListObjs.size()==1");
      zzpredFuncListObjs.top()->append(constName);
      if (appendToFormula) zzformulaStr.append(constStr);
    }
    else 
      zzexit("No function or predicate to hold constant %s", constName);
  }
  
  
  /**
   * Append a variable to a predicate
   * 
   * @varName The name of the variable being appended
   */
  void zzputVariableInPred(const char* varName, const bool& folDbg)
  {
    if (folDbg >= 1) printf("v_%s ", varName); 
  
    ++zzfdnumVars;
    string newVarName = zzgetNewVarName(varName);
        
    if (zzpred != NULL) 
    {
      bool rightNumTerms = true;
      bool rightType = true;
      int exp, unexp;
        
        // check that we have not exceeded the number of terms
      if ((unexp = zzpred->getNumTerms()) ==
         	(exp = zzpred->getTemplate()->getNumTerms()))
      {
        rightNumTerms = false;
        zzerr("Wrong number of terms for predicate %s. "
              "Expected %d but given %d", zzpred->getName(), exp, unexp+1);
      }
          
      int varId = -1;
      if (rightNumTerms)
      {
          // check that the variable is of the right type
        int typeId = zzpred->getTermTypeAsInt(zzpred->getNumTerms());
        rightType = zzcheckRightTypeAndGetVarId(typeId, newVarName.c_str(), varId);
      }
        
      if (rightNumTerms && rightType)
      {
        zzpred->appendTerm(new Term(varId, (void*)zzpred, true));
        zzpredFuncListObjs.top()->append(newVarName.c_str());
        //zzformulaStr.append(varName);
      }
    }
    else 
      zzexit("No function or predicate to hold variable %s",varName);
  }
  	
  
  void zztermIsVariable(const bool& folDbg)
  {
    const char* varName = zztokenList.removeLast();
    
      // if it is a constant (starts in uppercase or a string)
    if (zzisConstant(varName)) 
    {
      if (folDbg >= 1) printf("c2_%s ", varName); 
      
      if (zzconstantMustBeDeclared)
        zzerr("Constant %s must be declared before it is used", varName);
      zztermIsConstant(varName, varName, true);
      delete [] varName;
    }
    else
    {   //we are dealing with a variable that begins in lowercase    
      if (folDbg >= 1) printf("v_%s ", varName); 
      
      ++zzfdnumVars;
      string newVarName = zzgetNewVarName(varName);
      
        //always check zzfunc first, as a function can be found inside a predicate
      if (zzfunc != NULL)      
      {
        bool rightNumTerms = true;
        bool rightType = true;
        int exp, unexp;
        
          // check that we have not exceeded the number of terms
        if ((unexp = zzfunc->getNumTerms()) ==
            (exp = zzfunc->getTemplate()->getNumTerms()))
        {
          rightNumTerms = false;
          zzerr("Wrong number of terms for function %s. "
                "Expected %d but given %d", zzfunc->getName(), exp, unexp+1);
        }
        
        int varId = -1;      
        if (rightNumTerms)
        {
            // check that the variable is of the right type
          int typeId = zzfunc->getTermTypeAsInt(zzfunc->getNumTerms());
          rightType = zzcheckRightTypeAndGetVarId(typeId, newVarName.c_str(),
                                                  varId);
        }
  
        if (rightNumTerms && rightType)
        {
          zzfunc->appendTerm(new Term(varId, (void*)zzfunc, false));
          zzpredFuncListObjs.top()->append(newVarName.c_str());
          //zzformulaStr.append(varName);
        }
      }
      else 
      if (zzpred != NULL) 
      {
        bool rightNumTerms = true;
        bool rightType = true;
        int exp, unexp;
        
          // check that we have not exceeded the number of terms
        if ((unexp = zzpred->getNumTerms()) ==
            (exp = zzpred->getTemplate()->getNumTerms()))
        {
          rightNumTerms = false;
          zzerr("Wrong number of terms for predicate %s. "
                "Expected %d but given %d", zzpred->getName(), exp, unexp+1);
        }
        
        int varId = -1;
        if (rightNumTerms)
        {         
            // check that the variable is of the right type
          int typeId = zzpred->getTermTypeAsInt(zzpred->getNumTerms());
          rightType = zzcheckRightTypeAndGetVarId(typeId, newVarName.c_str(),
                                                  varId);
        }
        
        if (rightNumTerms && rightType)
        {
          zzpred->appendTerm(new Term(varId, (void*)zzpred, true));
          if (zzpredFuncListObjs.size() != 1) 
            zzerr("There may be a parse error. Have you declared all the "
                  "predicates and functions?");
          zzpredFuncListObjs.top()->append(newVarName.c_str());
          zzformulaStr.append(varName);
        }
      }
      else 
        zzexit("No function or predicate to hold variable %s",varName);
  
  
      if (zzisPlus) 
      {
        //zzisPlus = false; //commented out: set to false in not: rule
          // if variable is explicitly universally/existentially quantified
        if (!zzvarIsQuantified(varName)) // use the old var name
        {
            // we'll set it to the actual type when the entire formula is seen
          zzplusVarMap[newVarName] =  zzanyTypeId;
        }
        else
          zzerr("the '+' operator cannot be applied to variable %s that is "
                "explicitly universally/existentially quantified", varName);
      }
      delete [] varName;
    } //else we are dealing with a variable that begins in lowercase
  }
  
  
  
  void zzcleanUp()
  {
    zzeqPredList.clear();
    zzintPredList.clear();
    zzintFuncList.clear();
    while (!zzinStack.empty()) zzinStack.pop(); 
    zzvarNameToIdMap.clear();
    zzfuncToFuncVarMap.clear();
    zzoldNewVarList.clear();
    zzplusVarMap.clear();
    zztokenList.deleteContentsAndClear();
    while (!zzfuncStack.empty()) zzfuncStack.pop();
    while (!zzfuncConjStack.empty()) zzfuncConjStack.pop();
    while (!zzformulaListObjs.empty()) 
    {
      ListObj* top = zzformulaListObjs.top();
      zzformulaListObjs.pop();
      delete top;
    }
    while (!zzpredFuncListObjs.empty()) 
    {
      ListObj* top = zzpredFuncListObjs.top();
      zzpredFuncListObjs.pop();
      delete top;
    }
      //PredicateHashArray and contents deleted in zzaddGndPredsToDb()
    zzpredIdToGndPredMap.clear();
    zzformulaInfos.clear();
  }
  
  
  void zzinit()
  {
    zzafterRtParen = false;
    zzcount = 0;
    zzline = 0;
    zzcolumn = -1;
    zznumCharRead = 0;
    zznumErrors = 0;
    zzok = true;
    zzmln = NULL;
    zzdomain = NULL;
    zznumEofSeen = 0;
    zzeqTypeCounter = 0;
    zzintPredTypeCounter = 0;
    zzintFuncTypeCounter = 0;
    zzanyTypeId = -1;
    zzerrMsg[0] = '\0';
    zzfdfuncConstants.clear();
    zzusingLinkedFunctions = false;
    zztmpReturnNum = false;
    
    // Add internal predicates
    Array<const char*>* pred;
    pred = new Array<const char*>;
    pred->append("greaterThan");
    //pred->append("int");
    //pred->append("int");
    pred->append(PredicateTemplate::ANY_TYPE_NAME);
    pred->append(PredicateTemplate::ANY_TYPE_NAME);
    zzinternalPredicates.append(*pred);
    delete pred;
    
    pred = new Array<const char*>;
    pred->append("lessThan");
    //pred->append("int");
    //pred->append("int");
    pred->append(PredicateTemplate::ANY_TYPE_NAME);
    pred->append(PredicateTemplate::ANY_TYPE_NAME);
    zzinternalPredicates.append(*pred);
    delete pred;
  
    pred = new Array<const char*>;
    pred->append("greaterThanEq");
    //pred->append("int");
    //pred->append("int");
    pred->append(PredicateTemplate::ANY_TYPE_NAME);
    pred->append(PredicateTemplate::ANY_TYPE_NAME);
    zzinternalPredicates.append(*pred);
    delete pred;
    
    pred = new Array<const char*>;
    pred->append("lessThanEq");
    //pred->append("int");
    //pred->append("int");
    pred->append(PredicateTemplate::ANY_TYPE_NAME);
    pred->append(PredicateTemplate::ANY_TYPE_NAME);
    zzinternalPredicates.append(*pred);
    delete pred;
  
    pred = new Array<const char*>;
    pred->append("substr");
    //pred->append("string");
    //pred->append("string");
    pred->append(PredicateTemplate::ANY_TYPE_NAME);
    pred->append(PredicateTemplate::ANY_TYPE_NAME);
    zzinternalPredicates.append(*pred);
    delete pred;
  
    // Add internal functions
    Array<const char*>* func;
  
    func = new Array<const char*>;
    func->append("succ");
    //func->append("int"); //return type
    //func->append("int");
    func->append(PredicateTemplate::ANY_TYPE_NAME);
    func->append(PredicateTemplate::ANY_TYPE_NAME);
    zzinternalFunctions.append(*func);
    delete func;
    
    func = new Array<const char*>;
    func->append("plus");
    //func->append("int"); //return type
    //func->append("int");
    //func->append("int");
      // return type
    func->append(PredicateTemplate::ANY_TYPE_NAME);
    func->append(PredicateTemplate::ANY_TYPE_NAME);
    func->append(PredicateTemplate::ANY_TYPE_NAME);
    zzinternalFunctions.append(*func);
    delete func;
  
    func = new Array<const char*>;
    func->append("minus");
    //func->append("int"); //return type
    //func->append("int");
    //func->append("int");
      // return type
    func->append(PredicateTemplate::ANY_TYPE_NAME);
    func->append(PredicateTemplate::ANY_TYPE_NAME);
    func->append(PredicateTemplate::ANY_TYPE_NAME);
    zzinternalFunctions.append(*func);
    delete func;
  
    func = new Array<const char*>;
    func->append("times");
    //func->append("int"); //return type
    //func->append("int");
    //func->append("int");
      // return type
    func->append(PredicateTemplate::ANY_TYPE_NAME);
    func->append(PredicateTemplate::ANY_TYPE_NAME);
    func->append(PredicateTemplate::ANY_TYPE_NAME);
    zzinternalFunctions.append(*func);
    delete func;
  
    func = new Array<const char*>;
    func->append("dividedBy");
    //func->append("int"); //return type
    //func->append("int");
    //func->append("int");
      // return type
    func->append(PredicateTemplate::ANY_TYPE_NAME);
    func->append(PredicateTemplate::ANY_TYPE_NAME);
    func->append(PredicateTemplate::ANY_TYPE_NAME);
    zzinternalFunctions.append(*func);
    delete func;
  
    func = new Array<const char*>;
    func->append("mod");
    //func->append("int"); //return type
    //func->append("int");
    //func->append("int");
      // return type
    func->append(PredicateTemplate::ANY_TYPE_NAME);
    func->append(PredicateTemplate::ANY_TYPE_NAME);
    func->append(PredicateTemplate::ANY_TYPE_NAME);
    zzinternalFunctions.append(*func);
    delete func;
  
    func = new Array<const char*>;
    func->append("concat");
    //func->append("string"); //return type
    //func->append("string");
    //func->append("string");
      // return type
    func->append(PredicateTemplate::ANY_TYPE_NAME);
    func->append(PredicateTemplate::ANY_TYPE_NAME);
    func->append(PredicateTemplate::ANY_TYPE_NAME);
    zzinternalFunctions.append(*func);
    delete func;
  }
  
  
  void zzreset()
  {
    zzvarCounter = 0;
    zzscopeCounter = 0;
    zzoldNewVarList.clear();
    zzvarNameToIdMap.clear();
    zzfuncToFuncVarMap.clear();
    zzplusVarMap.clear();
    zzeqPredList.clear();
    zzintPredList.clear();
    zzintFuncList.clear();
  
    zztypeName = NULL;
    zzpredTemplate = NULL;
    zzfuncTemplate = NULL;
    zzpred = NULL;
    zzfunc = NULL;
    while (!zzfuncStack.empty()) zzfuncStack.pop();
    while (!zzfuncConjStack.empty()) zzfuncConjStack.pop();
    if (zzwt) { delete zzwt; zzwt = NULL; }
    zzisNegated = false;
    zzisAsterisk = false;
    zzisPlus = false;
    zzhasFullStop = false;
    zznumAsterisk = 0;
    zztrueFalseUnknown = 't';
    zzformulaStr.clear();
    zzfuncConjStr.clear();
    zzparseGroundPred = false;
    while (!zzformulaListObjs.empty()) 
    {
      ListObj* top = zzformulaListObjs.top();
      zzformulaListObjs.pop();
      delete top;
    }
    while (!zzpredFuncListObjs.empty()) 
    {
      ListObj* top = zzpredFuncListObjs.top();
      zzpredFuncListObjs.pop();
      delete top;
    }
    while (!zzfuncStack.empty()) zzfuncStack.pop();
    while (!zzfuncConjStack.empty()) zzfuncConjStack.pop();
  
    zzfdnumPreds = 0;
    zzfdnumFuncs = 0;
    zzfdnumVars = 0;
  //  zzfdisEqualPred = false;
    zzfdfuncName.clear();
    zzfdfuncConstants.clear();
    zzfdconstName.clear();
    zztmpReturnNum = false;
    zzinfixPredName = NULL;
    zzinfixFuncName = NULL;
  }
  
  
  string zzappend(const char* const & s, const int& i)
  {
    char buf[16];
    sprintf(buf,"%d",i);
    string str;
    return str.append(s).append(buf);
  }
  
  string zzappendWithUnderscore(const char* const & s, const int& i)
  {
    char buf[16];
    sprintf(buf,"%d",i);
    string str;
    return str.append(s).append("_").append(buf);
  }
  
  void zzcheckAllTypesHaveConstants(const Domain* const & domain)
  {
    const Array<const char*>* types = domain->getTypeNames();
    for (int i = 0; i < types->size(); i++)
    {
      if (strcmp((*types)[i],PredicateTemplate::ANY_TYPE_NAME)==0) continue;
      if (strcmp((*types)[i],PredicateTemplate::INT_TYPE_NAME)==0) continue;
      if (strcmp((*types)[i],PredicateTemplate::STRING_TYPE_NAME)==0) continue;
      if (domain->getNumConstantsByType((*types)[i]) <= 0)
        zzerr("type %s has no constant. A type must have at least one constant",
              (*types)[i]);
    }
  }
  
  
  void zzfillClosedWorldArray(Array<bool>& isClosedWorldArr,
                              const bool& allPredsExceptQueriesAreClosedWorld,
                              const StringHashArray* const & openWorldPredNames,
                              const StringHashArray* const & closedWorldPredNames,
                              const StringHashArray* const & queryPredNames)
  {
    if (queryPredNames)
    {
      for (int i = 0; i < queryPredNames->size(); i++) 
      {
        const char* predName = (*queryPredNames)[i].c_str();
        const PredicateTemplate* pt = zzdomain->getPredicateTemplate(predName);
        if (pt == NULL) 
        {
          zzerr("Query predicate %s is not found. Please declare it. "
                "Note that '!' and '?' should not be used with query predicates.",
                predName);
          continue;
        }
        if (pt->isEqualPredicateTemplate())
        {
          zzerr("'=' predicate cannot be a query predicate()");
          exit(-1);
        }
      }
    }
  
    int numPreds = zzdomain->getNumPredicates();
    isClosedWorldArr.growToSize(numPreds, true);
    if (!allPredsExceptQueriesAreClosedWorld)
    {
        // If a predicate has no evidence atoms, it is open-world (unless it's in
        // cwPredNames), if it has evidence atoms, it is closed-world (unless it's
        // in owPredNames).
      for (int i = 0; i < numPreds; i++)
      {
        hash_map<int, PredicateHashArray*>::iterator it;
        for (int i = 0; i < numPreds; i++)
        {
          if ((it = zzpredIdToGndPredMap.find(i)) != zzpredIdToGndPredMap.end())
          {
              // At least one evidence grounding is present
            isClosedWorldArr[i] = true;
          }
          else
          {
              // equality and internal predicates are handled specially by
              // database
            const PredicateTemplate* pt = zzdomain->getPredicateTemplate(i);          
            if (!pt->isEqualPredicateTemplate() &&
                !pt->isInternalPredicateTemplate())
              isClosedWorldArr[i] = false;
            else
              isClosedWorldArr[i] = true;
          }
        }
      }  
    }
    
      // Force these to be open-world
    if (openWorldPredNames)
    {
      for (int i = 0; i < openWorldPredNames->size(); i++) 
      {
        const char* predName = (*openWorldPredNames)[i].c_str();
        int predId = zzdomain->getPredicateId(predName);
        isClosedWorldArr[predId] = false;
      }
    }
      // Force these to be closed-world
    if (closedWorldPredNames)
    {
      for (int i = 0; i < closedWorldPredNames->size(); i++) 
      {
        const char* predName = (*closedWorldPredNames)[i].c_str();
        int predId = zzdomain->getPredicateId(predName);
        isClosedWorldArr[predId] = true;
      }
    } 
      // Queries are always open-world
    if (queryPredNames)
    {
      for (int i = 0; i < queryPredNames->size(); i++) 
      {
        const char* predName = (*queryPredNames)[i].c_str();
        int predId = zzdomain->getPredicateId(predName);
        isClosedWorldArr[predId] = false;
      }
    }
  }
  
  
  void zzappendUnitClausesToMLN(const Domain* const & domain, MLN* const & mln,
                                const double& defaultWt )
  {
    for (int i = 0; i < domain->getNumPredicates(); i++)
    {
      Predicate* pred = domain->createPredicate(i, false);
      if (pred == NULL) continue;
      Clause* clause = ClauseFactory::createUnitClause(pred, false);
      delete pred;
  
      if (clause == NULL) continue;
      if (mln->containsClause(clause)) { delete clause; continue; }
  
      int idx;
      ostringstream oss;
      clause->getPredicate(0)->getTemplate()->printWithStrVar(oss);
      bool app = mln->appendClause(oss.str(), false, clause, defaultWt,false,idx);
      if (app)
      {
        mln->setFormulaNumPreds(oss.str(), 1);
        mln->setFormulaIsHard(oss.str(), false);
        mln->setFormulaPriorMean(oss.str(), defaultWt);
      }
    }
  }
  
  
  void zzappendFormulaClausesToMLN(const ListObj* const & formula,
                                   const string& formulaStr, 
                                   const int& numPreds,
                                   const double* const & wt,
                                   const double& defaultWt,
                                   const Domain* const & domain,
                                   MLN* const & mln,
                                   const ZZVarNameToIdMap& varNameToIdMap,
                                   const StringToIntMap& plusVarMap,
                                   const int& numAsterisk,
                                   const bool& hasFullStop,
                                   const bool& readHardClauseWts,
                                   const bool& mustHaveWtOrFullStop,
                                   Array<int>& hardClauseIdxs,
                                   Array<string>& hardFormulas,
                                   Clause*& flippedClause,
                                   const Domain* const & domain0)
  {
    //cout << "orig formula = " << endl << "\t: " << formulaStr << endl;    
    //cout << "formula      = " << endl << "\t: " << *formula << endl;
  
    VarTypeMap* vtMap = zzcreateVarTypeMap(varNameToIdMap);
    Array<ListObj*> formulas;
    Array<string> formulaStrs;
    zzgroundPlusVar(formula, formulaStr, plusVarMap, formulas, formulaStrs, 
                    domain, domain0);
    delete formula;
  
    for (int f = 0; f < formulas.size(); f++)
    {
      //cout<<"formula (after gnding '+')= "<<endl<<"\t: "<< *(formulas[f])<<endl;
  
      Array<ListObj*> formulas2;
      Array<string> formulaStrs2;
      zzpermuteAsteriskedPreds(numAsterisk, formulas[f], formulaStrs[f], 
                               formulas2, formulaStrs2);
      delete formulas[f];    
  
      for (int g = 0; g < formulas2.size(); g++)
      {
        string formStr = formulaStrs2[g];
  
        //cout << "formula (after *) " << endl << "\t: " << *(formulas2[g])<<endl;
        ListObj* vars = new ListObj;
        bool hasExist = false;
        ListObj* cnf = ListObj::toCNF(formulas2[g], vars, domain, vtMap, hasExist);
        delete formulas2[g];
        //cout << "cnf = " << endl << "\t: " << *cnf << endl;
  
        cnf->cleanUpVars();
        //cout << "cnf (after cleanUp) = " << endl << "\t: " << *cnf << endl;
        
        //commented out: not likely for there to be redundant clauses and is slow
        //replaced with removeRedundantPredicates()
        //cnf->removeRedundantClauses();
  
        cnf->removeRedundantPredicates();
        //cout << "cnf (removed redundant preds) = " <<endl<<"\t: "<<*cnf<<endl;
  
        Array<Clause*> clauses;
        zzcreateClauses(cnf, clauses, flippedClause);
  
          // Output message of cnf size only if more than one
        if (clauses.size() > 1)
          cout << "\tCNF has  " << clauses.size() << " clauses" << endl;
  
        delete cnf; delete vars;
  
        double perClauseWt = 0;
        double formulaWt = 0;
        bool setHardWtLater = false;
  
        if (hasFullStop) // if this is a hard clause/formula
        {
          assert(wt == NULL);
          if (readHardClauseWts)
          {
            if (wt) 
            { perClauseWt = (*wt)/clauses.size(); formulaWt = (*wt); }
            else    
            {   //set weight later to twice of max soft clause wt
              perClauseWt = 1; formulaWt = 1; 
              hardFormulas.append(formStr);
              setHardWtLater = true;
            }                   
          }
          else
          {   //set later to twice of max soft clause wt         
            perClauseWt = 1; formulaWt = 1;
            hardFormulas.append(formStr);
            setHardWtLater = true;
          }
        }
        else
        if (wt)
        { perClauseWt = (*wt)/clauses.size(); formulaWt = *wt; }
        else
        {
          if (mustHaveWtOrFullStop)
            zzerr("a weight or full stop must be specified for:\n%s",
                  formStr.c_str());
          perClauseWt = defaultWt/clauses.size();
          formulaWt = defaultWt;
        }
  
        
        for (int i = 0; i < clauses.size(); i++)
        {
          ////// need a flag zzflipWtOfFlippedClause to indicate whether we should
          ////// flip the sign of the wt of a flipped clause.
          ////// During weight learning, we need not flip the sign because the
          ////// specified wt is a prior mean. During inference, we should flip
          ////// the sign because it's a real wt. This flag would have to 
          ////// be passed in via runYYParser
          double clauseWt = perClauseWt;
          if (flippedClause && flippedClause == clauses[i] 
              && zzflipWtsOfFlippedClause)
            clauseWt = -clauseWt;
  
          int prevIdx;
          bool ok = mln->appendClause(formStr, hasExist, clauses[i], 
                                      clauseWt, hasFullStop, prevIdx);
  
          if (!ok)
          {
            cout << "\tsame clause (derived from another formula) has been added "
                 << "to MLN:\n\t"; 
            const Clause* cl = mln->getClause(prevIdx);          
            cl->printWithoutWt(cout,domain); cout << endl;
            //cout << " derived from current formula:\n\t" << formStr << endl;
          }
  
          if (setHardWtLater) hardClauseIdxs.append(prevIdx);
        }
  
        mln->setFormulaNumPreds(formStr, numPreds);
        mln->setFormulaPriorMean(formStr, formulaWt);
        mln->setFormulaWt(formStr, formulaWt);
        mln->setFormulaIsHard(formStr, hasFullStop);      
  
      } //for (int g = 0; g < formulas2.size(); g++)
    }//for (int f = 0; f < formulas.size(); f++)
    delete vtMap;
  }
  
  
  void zzappendFormulasToMLN(Array<ZZFormulaInfo*>& formulaInfos, 
                             MLN* const & mln, const Domain* const & domain0)
  {
    cout << "converting to CNF:" << endl;
  
    Array<int> hardClauseIdxs;
    Array<string> hardFormulas;
    Clause* flippedClause = NULL;
  
    for (int i = 0; i < formulaInfos.size(); i++)
    {
      double startSec = zztimer.time();
      ZZFormulaInfo* epfi = formulaInfos[i];
      //cout << "formula " << i << ": " << epfi->formulaStr << endl;
      assert(mln == epfi->mln);
      zzappendFormulaClausesToMLN(epfi->formula, epfi->formulaStr, epfi->numPreds,
                                  epfi->wt, epfi->defaultWt, epfi->domain,
                                  epfi->mln, epfi->varNameToIdMap,
                                  epfi->plusVarMap, epfi->numAsterisk,
                                  epfi->hasFullStop,
                                  epfi->readHardClauseWts,
                                  epfi->mustHaveWtOrFullStop,
                                  hardClauseIdxs, hardFormulas, 
                                  flippedClause, domain0);
      delete epfi;
      //cout<<"CNF conversion took ";Timer::printTime(cout,zztimer.time()-startSec);
      //cout<<endl;
    }
    formulaInfos.clear();
  
    //set the weights of hard clauses
    double maxSoftWt = mln->getMaxAbsSoftWt();
    if (maxSoftWt == 0) maxSoftWt = 1;
  
    double hardWt = (HARD_WEIGHT==DBL_MIN) ?  HARD_WEIGHT_MULTIPLIER * maxSoftWt 
                                            : HARD_WEIGHT;
  
    for (int i = 0; i < hardClauseIdxs.size(); i++)
    {
      ////// need a flag zzflipWtOfFlippedClause to indicate whether we should
      ////// flip the sign of the wt of a flipped clause.
      ////// during weight learning, we need not flip the sign because the
      ////// specified wt is a prior mean. During inference, we should flip
      ////// the sign because it's a real wt. This flag would have to 
      ////// be passed in via runYYParser
      double hhardWt = hardWt;
      /*
      if (flippedClause && 
          //flippedClause->same( (Clause*)mln->getClause(hardClauseIdxs[i]) )
          flippedClause == (Clause*)mln->getClause(hardClauseIdxs[i])
          && zzflipWtsOfFlippedClause)
        hhardWt = -hhardWt;
      */
      
        // Weight has been flipped when added to mln. So, if weight
        // is neg. and marked as hard, then need to flip hard weight
      if (zzflipWtsOfFlippedClause &&
          ((Clause*)mln->getClause(hardClauseIdxs[i]))->getWt() < 0)
        hhardWt = -hhardWt;
            
      ((Clause*)mln->getClause(hardClauseIdxs[i]))->setWt(hhardWt);
    }
  
    for (int i = 0; i < hardFormulas.size(); i++)
    {
      mln->setFormulaWt(hardFormulas[i], hardWt);
      mln->setFormulaPriorMean(hardFormulas[i], hardWt);
    }
  }
  
  
  void zzsigHandler(int signo)
  {
    if (zznumErrors > 0) printf("Num of errors detected = %d\n", zznumErrors);
    if (zzisParsing)
      printf("UNRECOVERABLE ERROR in %s: line %d, col %d\n", 
             rmTmpPostfix(zzinFileName).c_str(), zzline, zzcolumn);
    else
      printf("UNRECOVERABLE ERROR after parsing %s\n", 
             rmTmpPostfix(zzinFileName).c_str());
  
    zzok = false;
    signal(signo,SIG_DFL);
  }
  
  /**
   * Compiles a C++ file containing linked-in functions into a shared object file.
   * The old version of the target file is removed, if it exists, then the C++
   * file is compiled. If the old target file can not be removed or if the C++
   * file can not be compiled then the program exits.
   * 
   * @fileName absolute path to file to be compiled.
   */
  void zzcompileFunctions(const char* fileName)
  {
    ifstream infs;
    ofstream outfs;
  
    // First remove any old .so file
    char* removeso;
    removeso = (char *)malloc((strlen("rm -f ") +
    							strlen(ZZ_FUNCTION_SO_FILE) + 1)*sizeof(char));
    strcpy(removeso, "rm -f ");
    strcat(removeso, ZZ_FUNCTION_SO_FILE);
    system(removeso);
  
    // If .so file is still there, then exit  
    infs.open(ZZ_FUNCTION_SO_FILE, ifstream::in);
    infs.close();
    if(!infs.fail())
    {
    	infs.clear(ios::failbit);
  	cout << "Unable to remove " << ZZ_FUNCTION_SO_FILE << endl;
  	exit(-1);
    }
    
    // Compile the file
    char* systemcall;
    systemcall = (char *)malloc((strlen("g++ -fPIC -shared -o ") +
    								strlen(ZZ_FUNCTION_SO_FILE) +
  								strlen(" ") +
  								strlen(fileName) + 1)*sizeof(char));
    strcpy(systemcall, "g++ -fPIC -shared -o ");
    strcat(systemcall, ZZ_FUNCTION_SO_FILE);
    strcat(systemcall, " ");
    strcat(systemcall, fileName);
    system(systemcall);
    
    // If .so file is not there, then exit  
    infs.open(ZZ_FUNCTION_SO_FILE, ifstream::in);
    infs.close();
    if(infs.fail())
    {
    	infs.clear(ios::failbit);
  	cout << "Could not compile function file " << fileName << endl;
  	exit(-1);
    }
    return;
  }
  
  
  /**
   * Inserts one permutation of constants for a function to take as
   * arguments.
   * 
   * @param domain the domain from which the constants are used
   * 
   * @param funccall function call obtained from dlsym() (dynamic library)
   * 
   * @param ftemplate function template present for the function in the
   * given domain
   * 
   * @numTerms number of terms which the function takes
   * 
   * @currentConstants counters for each term, telling us which constant is
   * currently being inserted
   * 
   */
  void zzinsertPermutationOfLinkedFunction(const Domain* const & domain,
                                           void* funccall,
                                           const FunctionTemplate* ftemplate,
                                           int numTerms,
                                           Array<int>* currentConstants)
  {
    string retString;
    string arguments[numTerms];
    string argumentsAsNum[numTerms];
    
    // Find the arguments for the function according to currentConstants
    for (int i = 0; i < numTerms; i++)
    {
      const Array<int>* constantsByType =
        domain->getConstantsByType(ftemplate->getTermTypeAsInt(i));
  
      arguments[i] =
        domain->getConstantName((*constantsByType)[((*currentConstants)[i])]);
  	// If constant is a number, then we have to cut it out of the string
      // C@Type@Number
      unsigned int at = arguments[i].rfind("@");
      if (at != string::npos)
        argumentsAsNum[i] = arguments[i].substr(at+1, arguments[i].length()-at-1);
      else argumentsAsNum[i] = arguments[i];
    }
    
    // Make the function call (max. 5 arguments)
    switch (numTerms)
    {
      case 0:
        retString = (*(string (*)())(funccall))();
        break;
      case 1:
        retString = (*(string (*)(string))(funccall))(argumentsAsNum[0]);
        break;
      case 2:
        retString = (*(string (*)(string, string))(funccall))
                      (argumentsAsNum[0], argumentsAsNum[1]);
        break;
      case 3:
        retString = (*(string (*)(string, string, string))(funccall))
                      (argumentsAsNum[0], argumentsAsNum[1], argumentsAsNum[2]);
        break;
      case 4:
        retString = (*(string (*)(string, string, string, string))(funccall))
                      (argumentsAsNum[0], argumentsAsNum[1], argumentsAsNum[2],
                       argumentsAsNum[3]);
        break;
      case 5:
        retString = (*(string (*)(string, string, string, string, string))
                      (funccall))
                      (argumentsAsNum[0], argumentsAsNum[1], argumentsAsNum[2],
                       argumentsAsNum[3], argumentsAsNum[4]);
        break;
      default:
        cout << "Linked-in functions can take max. 5 arguments\n" << endl;
        return;    
    }
  
    // If a number is returned, then we have to make a constant out of it
    int i;
    istringstream iss(retString);
    char constName[1000];
    if (iss>>i) // We are dealing with an integer
      zzcreateIntConstant(constName, ftemplate->getRetTypeName(), i);
    else
      strcpy(constName, retString.c_str());
  
    // The return value has to be an existing constant of the return type
    int constantId = domain->getConstantId(constName);
    const Array<int>* returnConstants =
      domain->getConstantsByType(ftemplate->getRetTypeId());
    
    if (returnConstants->contains(constantId))
    {
        // Insert the function definition just created  
        // Predicate name is PredicateTemplate::ZZ_RETURN_PREFIX + function name
      char* predName;
      predName = (char *)malloc((strlen(PredicateTemplate::ZZ_RETURN_PREFIX) +
                                 strlen(ftemplate->getName()) + 1)*sizeof(char));
      strcpy(predName, PredicateTemplate::ZZ_RETURN_PREFIX);
      strcat(predName, ftemplate->getName());
      zzcreatePred(zzpred, predName);
      zzpred->setTruthValue(TRUE);
  
        //Add return constant to predicate
      zzpredAppendConstant(zzpred, constantId, constName);
        //Add constant terms to predicate
      for (int i = 0; i < numTerms; i++)
      {
        const char* term = arguments[i].c_str();
        int constId = domain->getConstantId(term);
        zzpredAppendConstant(zzpred, constId, term);
      }
  	
      zzcheckPredNumTerm(zzpred);
      int predId = zzpred->getId();
  
        // Insert mapping of grounding
      hash_map<int,PredicateHashArray*>::iterator it;
      if ((it=zzpredIdToGndPredMap.find(predId)) == zzpredIdToGndPredMap.end())
        zzpredIdToGndPredMap[predId] = new PredicateHashArray;
  
  //cout << "Mapping " << endl;
  //zzpred->printWithStrVar(cout, zzdomain);
  //cout << " " << zzpred->getTruthValue() << endl;
    
      PredicateHashArray* pha = zzpredIdToGndPredMap[predId];
      if (pha->append(zzpred) < 0)
      {
        int a = pha->find(zzpred);
        zzassert(a >= 0, "expecting ground predicate to be found");
        string origTvStr = (*pha)[a]->getTruthValueAsStr();
        (*pha)[a]->setTruthValue(zzpred->getTruthValue());
        string newTvStr = (*pha)[a]->getTruthValueAsStr();
  
        if (zzwarnDuplicates)
        {
          ostringstream oss;
          oss << "Duplicate ground predicate "; zzpred->print(oss, zzdomain); 
          oss << " found. ";
          if (origTvStr.compare(newTvStr) != 0)
            oss << "Changed its truthValue from " << origTvStr << " to "
                << newTvStr << endl;
          zzwarn(oss.str().c_str());
        }
    	  delete zzpred;
      }
  
      delete [] predName;
      zzpred = NULL;
    }
    //delete returnConstants;
  }
  
  /**
   * Inserts all permutations of constants for a function to take as
   * arguments.
   * 
   * @param domain the domain from which the constants are used
   * 
   * @param funccall function call obtained from dlsym() (dynamic library)
   * 
   * @param ftemplate function template present for the function in the
   * given domain
   * 
   * @numTerms number of terms which the function takes
   * 
   * @currentTerm number of the current term
   * 
   * @currentConstants counters for each term, telling us which constant is
   * currently being inserted
   * 
   */
  void zzinsertPermutationsOfLinkedFunction(const Domain* const & domain,
                                            void* funccall,
                                            const FunctionTemplate* ftemplate,
                                            int numTerms, int currentTerm,
                                            Array<int>* currentConstants)
  {
    const Array<int>* constants =
      domain->getConstantsByType(ftemplate->getTermTypeAsInt(currentTerm));
  
      // Base case: at the last term
    if (currentTerm == numTerms - 1)
    {
      for (int i = 0; i < constants->size(); i++)
      {
        (*currentConstants)[currentTerm] = i;
        zzinsertPermutationOfLinkedFunction(domain, funccall, ftemplate, numTerms,
                                            currentConstants);
      }
      return;
    }
    
      // Not yet at last term
    zzinsertPermutationsOfLinkedFunction(domain, funccall, ftemplate, numTerms,
                                         currentTerm + 1, currentConstants);
    
    if (++(*currentConstants)[currentTerm] < constants->size())
      zzinsertPermutationsOfLinkedFunction(domain, funccall, ftemplate, numTerms,
                                           currentTerm, currentConstants);
  
    (*currentConstants)[currentTerm] = 0;
    return;
  }
  
  /**
   * Generates all valid groundings for a linked-in function.
   * 
   * @param domain the domain from which the function names and constants
   * are used
   * 
   * @param funcname name of function for which the groundings are
   * being produced
   * 
   * @param handle handle obtained from dlopen() on a file name
   * 
   */
  void zzgenerateGroundingsFromLinkedFunction(const Domain* const & domain,
  										    const char* funcname,
  										    void* handle)
  {
    char* error;
    void* funccall;
    
      // Obtain functioncall from dynamic library
    dlerror();    // Clear any existing error
    funccall = dlsym(handle, funcname);
    if ((error = dlerror()) != NULL)
    {
      printf("Error while evaluating function %s\n", funcname);
      fprintf (stderr, "dlerror: %s\n", error);
      return;
    }
  
      // Find number of terms for function
    const FunctionTemplate* ftemplate = domain->getFunctionTemplate(funcname);
    int numTerms = ftemplate->getNumTerms();
  
      // Insert all possible permutations of constants
    const Array<int>* termTypes = ftemplate->getTermTypesAsInt();
    zzassert(numTerms == termTypes->size(),
             "Number of terms and term types in function don't match");
    Array<int>* currentConstants = new Array<int>;
    for (int i = 0; i < numTerms; i++) currentConstants->append(0);
    zzinsertPermutationsOfLinkedFunction(domain, funccall, ftemplate, numTerms, 0,
                                         currentConstants);
  
    return;
  }
  
  /**
   * Generates all valid groundings from all linked in functions based on
   * the constants present in a domain. Looks at each declared function in
   * the domain and if it is a linked-in function, then the groundings are
   * generated.
   * 
   * @param domain The domain from which the function names and constants
   * are used
   * 
   */
  void zzgenerateGroundingsFromLinkedFunctions(const Domain* const & domain)
  {
      // First check if a file with functions exists
    void *handle;
    char* openFileName;
    openFileName = (char *)malloc((strlen("./") +
                                   strlen(ZZ_FUNCTION_SO_FILE) + 1)*sizeof(char));
    strcpy(openFileName, "./");
    strcat(openFileName, ZZ_FUNCTION_SO_FILE);
    handle = dlopen(openFileName, RTLD_LAZY);
    if (!handle)
    {
        // Can not open file, so no linked-in functions
      printf("No file for linked-in functions found.\n");
      fprintf (stderr, "%s\n", dlerror());
      dlclose(handle);
      return;
    }
  
      // Look at each function
    const Array<const char*>* fnames = domain->getFunctionNames();
    for (int i = 0; i < fnames->size(); i++)
    {
        // If it is a linked-in function,
        // then generate groundings for each permutation of the given types
      if (!zzisInternalFunction((*fnames)[i]) &&
          zzisLinkedFunction((*fnames)[i], handle))
      {
        cout << "Found linked-in function: " << (*fnames)[i] << endl;
        zzgenerateGroundingsFromLinkedFunction(domain, (*fnames)[i], handle);
      }
    }
    dlclose(handle);
    return;
  }
  
  
  /**
   * Inserts one permutation of constants for a predicate to take as
   * arguments.
   * 
   * @param domain the domain from which the constants are used
   * 
   * @param funccall function call obtained from dlsym() (dynamic library)
   * 
   * @param ptemplate predicate template present for the predicate in the
   * given domain
   * 
   * @numTerms number of terms which the predicate takes
   * 
   * @currentConstants counters for each term, telling us which constant is
   * currently being inserted
   * 
   */
  void zzinsertPermutationOfLinkedPredicate(const Domain* const & domain,
                                            void* funccall,
                                            const PredicateTemplate* ptemplate,
                                            int numTerms,
                                            Array<int>* currentConstants)
  {
    bool retBool = false;
    string arguments[numTerms];
    string argumentsAsNum[numTerms];
    
      // Find the arguments for the predicate according to currentConstants
    for (int i = 0; i < numTerms; i++)
    {
      const Array<int>* constantsByType =
        domain->getConstantsByType(ptemplate->getTermTypeAsInt(i));
  
      arguments[i] =
        domain->getConstantName((*constantsByType)[((*currentConstants)[i])]);
        // If constant is a number, then we have to cut it out of the string
        // C@Type@Number
      unsigned int at = arguments[i].rfind("@");
      if (at != string::npos)
        argumentsAsNum[i] = arguments[i].substr(at+1, arguments[i].length()-at-1);
      else argumentsAsNum[i] = arguments[i];
    }
    
      // Make the function call (max. 5 arguments)
    switch (numTerms)
    {
      case 0:
        retBool = (*(bool (*)())(funccall))();
        break;
      case 1:
        retBool = (*(bool (*)(string))(funccall))(argumentsAsNum[0]);
        break;
      case 2:
        retBool = (*(bool (*)(string, string))(funccall))
                      (argumentsAsNum[0], argumentsAsNum[1]);
        break;
      case 3:
        retBool = (*(bool (*)(string, string, string))(funccall))
                      (argumentsAsNum[0], argumentsAsNum[1], argumentsAsNum[2]);
        break;
      case 4:
        retBool = (*(bool (*)(string, string, string, string))(funccall))
                      (argumentsAsNum[0], argumentsAsNum[1], argumentsAsNum[2],
                       argumentsAsNum[3]);
        break;
      case 5:
        retBool = (*(bool (*)(string, string, string, string, string))(funccall))
                      (argumentsAsNum[0], argumentsAsNum[1], argumentsAsNum[2],
                       argumentsAsNum[3], argumentsAsNum[4]);
        break;
      default:
        cout << "Linked-in predicates can take max. 5 arguments\n" << endl;
        return;    
    }
    
      // Insert the predicate definition just created  
    const char* predName;
    predName = ptemplate->getName();
    //for (int i = 0; i < currentConstants->size(); i++)
      //printf("%d ", (*currentConstants)[i]);
    zzcreatePred(zzpred, predName);
    if (retBool) zzpred->setTruthValue(TRUE);
    else zzpred->setTruthValue(FALSE);
    
      // Add constant terms to predicate
    for (int i = 0; i < numTerms; i++)
    {
      const char* term = arguments[i].c_str();
      int constId = domain->getConstantId(term);
      zzpredAppendConstant(zzpred, constId, term);
    }
  	
    zzcheckPredNumTerm(zzpred);
    int predId = zzpred->getId();
  
      // Insert mapping of grounding
    hash_map<int,PredicateHashArray*>::iterator it;
    if ((it=zzpredIdToGndPredMap.find(predId)) == zzpredIdToGndPredMap.end())
     	zzpredIdToGndPredMap[predId] = new PredicateHashArray;
    
  //cout << "Mapping " << endl;
  //zzpred->printWithStrVar(cout, zzdomain);
  //cout << " " << zzpred->getTruthValue() << endl;
  
    PredicateHashArray* pha = zzpredIdToGndPredMap[predId];
    if (pha->append(zzpred) < 0)
    {
      int a = pha->find(zzpred);
      zzassert(a >= 0, "expecting ground predicate to be found");
      string origTvStr = (*pha)[a]->getTruthValueAsStr();
      (*pha)[a]->setTruthValue(zzpred->getTruthValue());
      string newTvStr = (*pha)[a]->getTruthValueAsStr();
  
      if (zzwarnDuplicates)
      {
        ostringstream oss;
        oss << "Duplicate ground predicate "; zzpred->print(oss, zzdomain); 
        oss << " found. ";
        if (origTvStr.compare(newTvStr) != 0)
          oss << "Changed its truthValue from " << origTvStr << " to " << newTvStr
              << endl;
        zzwarn(oss.str().c_str());
      }
      delete zzpred;
    }
    zzpred = NULL;
  }
  
  /**
   * Inserts all permutations of constants for a predicate to take as
   * arguments.
   * 
   * @param domain the domain from which the constants are used
   * 
   * @param funccall function call obtained from dlsym() (dynamic library)
   * 
   * @param ptemplate predicate template present for the predicate in the
   * given domain
   * 
   * @numTerms number of terms which the predicate takes
   * 
   * @currentTerm number of the current term
   * 
   * @currentConstants counters for each term, telling us which constant is
   * currently being inserted
   * 
   */
  void zzinsertPermutationsOfLinkedPredicate(const Domain* const & domain,
                                             void* funccall,
                                             const PredicateTemplate* ptemplate,
                                             int numTerms, int currentTerm,
                                             Array<int>* currentConstants)
  {
    const Array<int>* constants =
      domain->getConstantsByType(ptemplate->getTermTypeAsInt(currentTerm));
  
      // Base case: at the last term
    if (currentTerm == numTerms - 1)
    {
      for (int i = 0; i < constants->size(); i++)
      {
        (*currentConstants)[currentTerm] = i;
        zzinsertPermutationOfLinkedPredicate(domain, funccall, ptemplate,
                                             numTerms, currentConstants);
      }
      return;
    }
    
      // Not yet at last term
    zzinsertPermutationsOfLinkedPredicate(domain, funccall, ptemplate, numTerms,
                                          currentTerm + 1, currentConstants);
    
    if (++(*currentConstants)[currentTerm] < constants->size())
      zzinsertPermutationsOfLinkedPredicate(domain, funccall, ptemplate, numTerms,
                                            currentTerm, currentConstants);
  
    (*currentConstants)[currentTerm] = 0;
    return;
  }
  
  /**
   * Generates all valid groundings for a linked-in predicate.
   * 
   * @param domain the domain from which the predicate names and constants
   * are used
   * 
   * @param predicatename name of predicate for which the groundings are
   * being produced
   * 
   * @param handle handle obtained from dlopen() on a file name
   * 
   */
  void zzgenerateGroundingsFromLinkedPredicate(const Domain* const & domain,
  										     const char* predname,
  										     void* handle)
  {
    char* error;
    void* funccall;
    
      // Obtain functioncall from dynamic library
    dlerror();    // Clear any existing error
    funccall = dlsym(handle, predname);
    if ((error = dlerror()) != NULL)
    {
      printf("Error while evaluating predicate %s\n", predname);
      fprintf (stderr, "dlerror: %s\n", error);
      return;
    }
  
      // Find number of terms for predicate
    const PredicateTemplate* ptemplate = domain->getPredicateTemplate(predname);
    int numTerms = ptemplate->getNumTerms();
  
      // Insert all possible permutations of constants
    const Array<int>* termTypes = ptemplate->getTermTypesAsInt();
    zzassert(numTerms == termTypes->size(),
             "Number of terms and term types in function don't match");
    Array<int>* currentConstants = new Array<int>;
    for (int i = 0; i < numTerms; i++) currentConstants->append(0);
    zzinsertPermutationsOfLinkedPredicate(domain, funccall, ptemplate, numTerms,
                                          0, currentConstants);
  
    return;
  }
  
  /**
   * Generates all valid groundings from all linked in predicates based on
   * the constants present in a domain. Looks at each declared predicate in
   * the domain and if it is a linked-in predicate, then the groundings are
   * generated.
   * 
   * @param domain The domain from which the predicate names and constants
   * are used
   * 
   */
  void zzgenerateGroundingsFromLinkedPredicates(const Domain* const & domain)
  {
      // First check if a file with predicates exists
    void *handle;
    char* openFileName;
    openFileName = (char *)malloc((strlen("./") +
                                   strlen(ZZ_FUNCTION_SO_FILE) + 1)*sizeof(char));
    strcpy(openFileName, "./");
    strcat(openFileName, ZZ_FUNCTION_SO_FILE);
    handle = dlopen(openFileName, RTLD_LAZY);
    if (!handle)
    {
        // Can not open file, so no linked-in predicates
      printf("No file for linked-in predicates found.\n");
      fprintf (stderr, "%s\n", dlerror());
      dlclose(handle);
      return;
    }
  
      // Look at each predicate
    const Array<const char*>* pnames = domain->getPredicateNames();
    for (int i = 0; i < pnames->size(); i++)
    {
        // If it is a linked-in predicate,
        // then generate groundings for each permutation of the given types
      if (!zzisInternalPredicate((*pnames)[i]) &&
          zzisLinkedPredicate((*pnames)[i], handle))
      {
        cout << "Found linked-in predicate: " << (*pnames)[i] << endl;
        zzgenerateGroundingsFromLinkedPredicate(domain, (*pnames)[i], handle);
      }
    }
    dlclose(handle);
    return;
  }
  
  /**
   * Declares all internally implemented predicates and functions
   * (see zzinternalPredicates and zzinternalFunctions).
   * (no longer used, internals are declared on-the-fly)
   */
  /*
  void zzdeclareInternalPredicatesAndFunctions()
  {
    // Predicates
    for (int i = 0; i < zzinternalPredicates.size(); i++)
    {
    	const char* predName = zzinternalPredicates[i][0];
  	  //predicate has not been declared a function
    	zzassert(zzdomain->getFunctionId(predName) < 0, 
      	       "not expecting pred name to be declared as a function name");
    	zzassert(zzpredTemplate==NULL,"expecting zzpredTemplate==NULL");
    	zzpredTemplate = new PredicateTemplate();
    	zzpredTemplate->setName(predName);
   	
    	// Add types
    	for (int j = 1; j < zzinternalPredicates[i].size(); j++)
    	{
    	  int id;
    	  const char* ttype = zzinternalPredicates[i][j];
    	  if (!zzdomain->isType(ttype))
    	  {
  		id = zzaddTypeToDomain(zzdomain, ttype);
    		zzassert(id >= 0, "expecting var id >= 0");
    	  }
    	  zzaddType(ttype, zzpredTemplate, NULL, false, zzdomain);
  	  //delete [] ttype;
    	}
    	
    	// Add template to domain
    	zzassert(zzpredTemplate, "not expecting zzpredTemplate==NULL");
  	int id = zzdomain->addPredicateTemplate(zzpredTemplate);
    	zzassert(id >= 0, "expecting pred template id >= 0");
    	zzpredTemplate->setId(id);
    	zzpredTemplate = NULL;
    }
    
    
    // Functions
    for (int i = 0; i < zzinternalFunctions.size(); i++)
    {
  	zzassert(zzfuncTemplate==NULL, "expecting zzfuncTemplate==NULL");
  	zzfuncTemplate = new FunctionTemplate();
  
  	// We are creating a new predicate as well
    	zzassert(zzpredTemplate==NULL,"expecting zzpredTemplate==NULL");
    	zzpredTemplate = new PredicateTemplate();
  
    	const char* funcName = zzinternalFunctions[i][0];
  
  	zzassert(zzdomain->getPredicateId(funcName) < 0, 
      	     "not expecting func name to be declared as pred name");
    	zzassert(zzfuncTemplate,"expecting zzfuncTemplate!=NULL");
  	zzfuncTemplate->setName(funcName);
  
  	// Predicate name is PredicateTemplate::ZZ_RETURN_PREFIX + function name
  	char* predName;
  	predName = (char *)malloc((strlen(PredicateTemplate::ZZ_RETURN_PREFIX) +
    							strlen(funcName) + 1)*sizeof(char));
  	strcpy(predName, PredicateTemplate::ZZ_RETURN_PREFIX);
  	strcat(predName, funcName);
      	
  	// Check that predicate has not been declared a function
  	zzassert(zzdomain->getFunctionId(predName) < 0, 
    		     "not expecting pred name to be declared as a function name");
    	zzassert(zzpredTemplate,"expecting zzpredTemplate!=NULL");
   	zzpredTemplate->setName(predName);
  	delete [] predName;  
    	
    	// Add return type
    	const char* retTypeName = zzinternalFunctions[i][1];
  
  	if (!zzdomain->isType(retTypeName))
    	{
     	  int id = zzaddTypeToDomain(zzdomain, retTypeName);
        zzassert(id >= 0, "expecting retTypeName's id >= 0");
    	}
  
  	zzfuncTemplate->setRetTypeName(retTypeName,zzdomain);
    	// We are creating a new predicate as well
  	zzaddType(retTypeName, zzpredTemplate, NULL, false, zzdomain);
    
    	// Add types
    	for (int j = 2; j < zzinternalFunctions[i].size(); j++)
    	{
    	  int id;
    	  const char* ttype = zzinternalFunctions[i][j];
    	  if (!zzdomain->isType(ttype))
    	  {
  		id = zzaddTypeToDomain(zzdomain, ttype);
    		zzassert(id >= 0, "expecting var id >= 0");
    	  }
    	  zzaddType(ttype, zzpredTemplate, NULL, false, zzdomain);
  	  // Add the type to the function too
  	  zzaddType(ttype, NULL, zzfuncTemplate, false, zzdomain);
    	}
  
    // Add templates to domain
    zzassert(zzfuncTemplate, "expecting zzfuncTemplate != NULL");
    int id = zzdomain->addFunctionTemplate(zzfuncTemplate);
    zzassert(id >= 0, "expecting function template's id >= 0");
    zzfuncTemplate->setId(id);
    zzfuncTemplate = NULL;
  
    zzassert(zzpredTemplate, "not expecting zzpredTemplate==NULL");
    int predId = zzdomain->addPredicateTemplate(zzpredTemplate);
    zzassert(predId >= 0, "expecting pred template id >= 0");
    zzpredTemplate->setId(predId);
    zzpredTemplate = NULL;
    }
    
    return;
  }
  */
  
  /**
   * Inserts one permutation of constants for a predicate to take as
   * arguments. If a new internal predicate is added, then it has to be
   * registered here.
   * 
   * @param index index of the internal predicate
   * 
   * @param ptemplate predicate template present for the predicate in the
   * given domain
   * 
   * @numTerms number of terms which the predicate takes
   * 
   * @currentConstants counters for each term, telling us which constant is
   * currently being inserted 
   */
  void zzinsertPermutationOfInternalPredicate(int index,
                                        const PredicateTemplate* const& ptemplate,
                                              int numTerms,
                                              Array<int>* currentConstants)
  {
    bool retBool = false;
    string arguments[numTerms];
    string argumentsAsNum[numTerms];
    
      // Find the arguments for the predicate according to currentConstants
    for (int i = 0; i < numTerms; i++)
    {
      const Array<int>* constantsByType =
        zzdomain->getConstantsByType(ptemplate->getTermTypeAsInt(i));
  
      arguments[i] =
        zzdomain->getConstantName((*constantsByType)[((*currentConstants)[i])]);
        // If constant is a number, then we have to cut it out of the string
        // C@Type@Number
      unsigned int at = arguments[i].rfind("@");
      if (at != string::npos)
        argumentsAsNum[i] = arguments[i].substr(at+1, arguments[i].length()-at-1);
      else
      {
        argumentsAsNum[i] = arguments[i];
          // Remove " from constants
        string::size_type loc = argumentsAsNum[i].find("\"", 0);
        while (loc != string::npos)
        {
          argumentsAsNum[i].erase(loc, 1);
          loc = argumentsAsNum[i].find("\"", 0);
        }
      }
    }
    
      // Make the function call
    int a, b;
    switch(index)
    {
      case 0:
        Internals::stringToInt(argumentsAsNum[0], a);
        Internals::stringToInt(argumentsAsNum[1], b);
        retBool = Internals::greaterThan(a, b);
        break;
      case 1:
        Internals::stringToInt(argumentsAsNum[0], a);
        Internals::stringToInt(argumentsAsNum[1], b);
        retBool = Internals::lessThan(a, b);
        break;
      case 2:
        Internals::stringToInt(argumentsAsNum[0], a);
        Internals::stringToInt(argumentsAsNum[1], b);
        retBool = Internals::greaterThanEq(a, b);
        break;
      case 3:
        Internals::stringToInt(argumentsAsNum[0], a);
        Internals::stringToInt(argumentsAsNum[1], b);
        retBool = Internals::lessThanEq(a, b);
        break;
      case 4:
        retBool = Internals::substr(argumentsAsNum[0], argumentsAsNum[1]);
        break;
    }
      
      // Insert the predicate definition just created  
    const char* predName;
    predName = ptemplate->getName();
    zzcreatePred(zzpred, predName);
    if (retBool) zzpred->setTruthValue(TRUE);
    else zzpred->setTruthValue(FALSE);
    
      // Add constant terms to predicate
    for (int i = 0; i < numTerms; i++)
    {
      const char* term = arguments[i].c_str();
      int constId = zzdomain->getConstantId(term);
      zzpredAppendConstant(zzpred, constId, term);
    }
  
    zzcheckPredNumTerm(zzpred);
    int predId = zzpred->getId();
  
      // Insert mapping of grounding
    hash_map<int,PredicateHashArray*>::iterator it;
    if ((it=zzpredIdToGndPredMap.find(predId)) == zzpredIdToGndPredMap.end())
      zzpredIdToGndPredMap[predId] = new PredicateHashArray;
    
  //cout << "Mapping " << endl;
  //zzpred->printWithStrVar(cout, zzdomain);
  //cout << " " << zzpred->getTruthValue() << endl;
  
    PredicateHashArray* pha = zzpredIdToGndPredMap[predId];
    if (pha->append(zzpred) < 0)
    {
      int a = pha->find(zzpred);
      zzassert(a >= 0, "expecting ground predicate to be found");
      string origTvStr = (*pha)[a]->getTruthValueAsStr();
      (*pha)[a]->setTruthValue(zzpred->getTruthValue());
      string newTvStr = (*pha)[a]->getTruthValueAsStr();
  
      if (zzwarnDuplicates)
      {
        ostringstream oss;
        oss << "Duplicate ground predicate "; zzpred->print(oss, zzdomain); 
        oss << " found. ";
        if (origTvStr.compare(newTvStr) != 0)
          oss << "Changed its truthValue from " << origTvStr << " to " << newTvStr
              << endl;
        zzwarn(oss.str().c_str());
      }
      delete zzpred;
    }
  
    zzpred = NULL;
  }
  
  /**
   * Inserts one permutation of constants for a function to take as
   * arguments. If a new internal function is added, then it has to
   * be registered here.
   * 
   * @param index index of the internal function
   * 
   * @param ftemplate function template present for the function in the
   * given domain
   * 
   * @numTerms number of terms which the function takes
   * 
   * @currentConstants counters for each term, telling us which constant is
   * currently being inserted
   * 
   */
  void zzinsertPermutationOfInternalFunction(int index,
                                             const FunctionTemplate* ftemplate,
                                             int numTerms,
                                             Array<int>* currentConstants)
  {
    char constName[1000];
    string arguments[numTerms];
    string argumentsAsNum[numTerms];
    
      // Find the arguments for the predicate according to currentConstants
    for (int i = 0; i < numTerms; i++)
    {
      const Array<int>* constantsByType =
        zzdomain->getConstantsByType(ftemplate->getTermTypeAsInt(i));
  
      arguments[i] =
        zzdomain->getConstantName((*constantsByType)[((*currentConstants)[i])]);
        // If constant is a number, then we have to cut it out of the string
        // C@Type@Number
      unsigned int at = arguments[i].rfind("@");
      if (at != string::npos)
        argumentsAsNum[i] = arguments[i].substr(at+1, arguments[i].length()-at-1);
      else argumentsAsNum[i] = arguments[i];
    }
    
      // Make the function call
    int a, b;
    switch(index)
    {
      case 0:
        Internals::stringToInt(argumentsAsNum[0], a);
        zzcreateIntConstant(constName, ftemplate->getRetTypeName(),
                            Internals::succ(a));
        break;
      case 1:
        Internals::stringToInt(argumentsAsNum[0], a);
        Internals::stringToInt(argumentsAsNum[1], b);
        zzcreateIntConstant(constName, ftemplate->getRetTypeName(),
                            Internals::plus(a, b));
        break;
      case 2:
        Internals::stringToInt(argumentsAsNum[0], a);
        Internals::stringToInt(argumentsAsNum[1], b);
        zzcreateIntConstant(constName, ftemplate->getRetTypeName(),
                            Internals::minus(a, b));
        break;
      case 3:
        Internals::stringToInt(argumentsAsNum[0], a);
        Internals::stringToInt(argumentsAsNum[1], b);
        zzcreateIntConstant(constName, ftemplate->getRetTypeName(),
                            Internals::times(a, b));
        break;
      case 4:
        Internals::stringToInt(argumentsAsNum[0], a);
        Internals::stringToInt(argumentsAsNum[1], b);
        zzcreateIntConstant(constName, ftemplate->getRetTypeName(),
                            Internals::dividedBy(a, b));
        break;
      case 5:
        Internals::stringToInt(argumentsAsNum[0], a);
        Internals::stringToInt(argumentsAsNum[1], b);
        zzcreateIntConstant(constName, ftemplate->getRetTypeName(),
                            Internals::mod(a, b));
        break;
      case 6:
        strcpy(constName,
               Internals::concat(argumentsAsNum[0], argumentsAsNum[1]).c_str());
    }
    
      // The return value has to be an existing constant of the return type
    int constantId = zzdomain->getConstantId(constName);
    const Array<int>* returnConstants =
      zzdomain->getConstantsByType(ftemplate->getRetTypeId());
    
    if (returnConstants->contains(constantId))
    {
        // Insert the function definition just created  
        // Predicate name is PredicateTemplate::ZZ_RETURN_PREFIX + function name
      char* predName;
      predName = (char *)malloc((strlen(PredicateTemplate::ZZ_RETURN_PREFIX) +
                                 strlen(ftemplate->getName()) + 1)*sizeof(char));
      strcpy(predName, PredicateTemplate::ZZ_RETURN_PREFIX);
      strcat(predName, ftemplate->getName());
      zzcreatePred(zzpred, predName);
      zzpred->setTruthValue(TRUE);
  
        // Add return constant to predicate
      zzpredAppendConstant(zzpred, constantId, constName);
        // Add constant terms to predicate
      for (int i = 0; i < numTerms; i++)
      {
        const char* term = arguments[i].c_str();
        int constId = zzdomain->getConstantId(term);
        zzpredAppendConstant(zzpred, constId, term);
      }
      
      zzcheckPredNumTerm(zzpred);
      int predId = zzpred->getId();
        // Insert mapping of grounding
      hash_map<int,PredicateHashArray*>::iterator it;
      if ((it=zzpredIdToGndPredMap.find(predId)) == zzpredIdToGndPredMap.end())
        zzpredIdToGndPredMap[predId] = new PredicateHashArray;
  
  //cout << "Mapping " << endl;
  //zzpred->printWithStrVar(cout, zzdomain);
  //cout << " " << zzpred->getTruthValue() << endl;
    
      PredicateHashArray* pha = zzpredIdToGndPredMap[predId];
      if (pha->append(zzpred) < 0)
      {
        int a = pha->find(zzpred);
        zzassert(a >= 0, "expecting ground predicate to be found");
        string origTvStr = (*pha)[a]->getTruthValueAsStr();
        (*pha)[a]->setTruthValue(zzpred->getTruthValue());
        string newTvStr = (*pha)[a]->getTruthValueAsStr();
  
        if (zzwarnDuplicates)
        {
          ostringstream oss;
          oss << "Duplicate ground predicate "; zzpred->print(oss, zzdomain); 
          oss << " found. ";
          if (origTvStr.compare(newTvStr) != 0)
            oss << "Changed its truthValue from " << origTvStr << " to "
                << newTvStr << endl;
          zzwarn(oss.str().c_str());
        }
        delete zzpred;
      }
  
      free(predName);
      zzpred = NULL;
    }
    //delete returnConstants;
  }
  
  /**
   * Inserts all permutations of constants for a predicate to take as
   * arguments.
   * 
   * @param index index of the internal predicate
   * 
   * @param ptemplate predicate template present for the predicate in the
   * given domain
   * 
   * @numTerms number of terms which the predicate takes
   * 
   * @currentTerm number of the current term
   * 
   * @currentConstants counters for each term, telling us which constant is
   * currently being inserted
   * 
   */
  void zzinsertPermutationsOfInternalPredicate(int index,
                                        const PredicateTemplate* const& ptemplate,
                                               int numTerms, int currentTerm,
                                               Array<int>* currentConstants)
  {
    const Array<int>* constants =
      zzdomain->getConstantsByType(ptemplate->getTermTypeAsInt(currentTerm));
  
      // Base case: at the last term
    if (currentTerm == numTerms - 1)
    {
      for (int i = 0; i < constants->size(); i++)
      {
        (*currentConstants)[currentTerm] = i;
        zzinsertPermutationOfInternalPredicate(index, ptemplate, numTerms,
                                               currentConstants);
      }
      return;
    }
    
      // Not yet at last term
    zzinsertPermutationsOfInternalPredicate(index, ptemplate, numTerms,
                                            currentTerm + 1, currentConstants);
    
    if (++(*currentConstants)[currentTerm] < constants->size())
      zzinsertPermutationsOfInternalPredicate(index, ptemplate, numTerms,
                                              currentTerm, currentConstants);
  
    (*currentConstants)[currentTerm] = 0;
    return;
  }
  
  
  /**
   * Inserts all permutations of constants for a function to take as
   * arguments.
   * 
   * @param index index of the internal function
   * 
   * @param ftemplate function template present for the function in the
   * given domain
   * 
   * @numTerms number of terms which the predicate takes
   * 
   * @currentTerm number of the current term
   * 
   * @currentConstants counters for each term, telling us which constant is
   * currently being inserted
   * 
   */
  void zzinsertPermutationsOfInternalFunction(int index,
                                         const FunctionTemplate* const& ftemplate,
                                         int numTerms, int currentTerm,
                                         Array<int>* currentConstants)
  {
    const Array<int>* constants =
      zzdomain->getConstantsByType(ftemplate->getTermTypeAsInt(currentTerm));
  
      // Base case: at the last term
    if (currentTerm == numTerms - 1)
    {
      for (int i = 0; i < constants->size(); i++)
      {
        (*currentConstants)[currentTerm] = i;
        zzinsertPermutationOfInternalFunction(index, ftemplate, numTerms,
                                              currentConstants);
      }
      return;
    }
    
      // Not yet at last term
    zzinsertPermutationsOfInternalFunction(index, ftemplate, numTerms,
                                           currentTerm + 1, currentConstants);
    
    if (++(*currentConstants)[currentTerm] < constants->size())
      zzinsertPermutationsOfInternalFunction(index, ftemplate, numTerms,
                                             currentTerm, currentConstants);
  
    (*currentConstants)[currentTerm] = 0;
    return;
  }
  
  /**
   * Generates all valid groundings for an internal predicate.
   * 
   * @param index Index of the internal predicate
   */
  void zzgenerateGroundingsFromInternalPredicate(int index,
                                        const PredicateTemplate* const& ptemplate)
  {
      // Find number of terms for predicate
    if (ptemplate != NULL)
    {
      int numTerms = ptemplate->getNumTerms();
  
        // Insert all possible permutations of constants
      const Array<int>* termTypes = ptemplate->getTermTypesAsInt();
      zzassert(numTerms == termTypes->size(),
               "Number of terms and term types in predicate don't match");
      Array<int>* currentConstants = new Array<int>;
      for (int i = 0; i < numTerms; i++) currentConstants->append(0);
      zzinsertPermutationsOfInternalPredicate(index, ptemplate, numTerms, 0,
                                              currentConstants);
      delete currentConstants;
    }
    return;
  }
  
  /**
   * Generates all valid groundings for an internal function.
   * 
   * @param index Index of the internal function
   */
  void zzgenerateGroundingsFromInternalFunction(int index,
                                         const FunctionTemplate* const& ftemplate)
  {
    // Find number of terms for function
    if (ftemplate != NULL)
    {
      int numTerms = ftemplate->getNumTerms();
  
        // Insert all possible permutations of constants
      const Array<int>* termTypes = ftemplate->getTermTypesAsInt();
      zzassert(numTerms == termTypes->size(),
               "Number of terms and term types in predicate don't match");
      Array<int>* currentConstants = new Array<int>;
      for (int i = 0; i < numTerms; i++) currentConstants->append(0);
      zzinsertPermutationsOfInternalFunction(index, ftemplate, numTerms, 0,
                                             currentConstants);
      delete currentConstants;
    }
    return;
  }
  
  /**
   * Generates all valid groundings from internally implemented predicates and
   * functions  (see internalPredicates and internalFunctions).
   * 
   * @param domain The domain from which the predicate / function names and
   * constants are used
   * 
   */
  void zzgenerateGroundingsFromInternalPredicatesAndFunctions()
  {
      // Look at each predicate
    for (int i = 0; i < zzdomain->getNumPredicates(); i++)
    {
      const PredicateTemplate* ptemplate = zzdomain->getPredicateTemplate(i);
      if (ptemplate->isInternalPredicateTemplate())
      {
        cout << "Found internal predicate: " << ptemplate->getName() << endl;
        for (int j = 0; j < zzinternalPredicates.size(); j++)
        {
  cout << "h1" << endl;
          if (strncmp(ptemplate->getName(), zzinternalPredicates[j][0],
                      strlen(zzinternalPredicates[j][0])) == 0)
          {
  cout << "h2" << endl;
            zzgenerateGroundingsFromInternalPredicate(j, ptemplate);
  cout << "h3" << endl;
            break;
          }
  cout << "h4" << endl;
        }
      }
    }
  
      // Look at each function
    for (int i = 0; i < zzdomain->getNumFunctions(); i++)
    {
      const FunctionTemplate* ftemplate = zzdomain->getFunctionTemplate(i);
      if (ftemplate->isInternalFunctionTemplate())
      {
        cout << "Found internal function: " << ftemplate->getName() << endl;
        for (int j = 0; j < zzinternalFunctions.size(); j++)
        {
          if (strncmp(ftemplate->getName(), zzinternalFunctions[j][0],
                      strlen(zzinternalFunctions[j][0])) == 0)
          {
            zzgenerateGroundingsFromInternalFunction(j, ftemplate);
            break;
          }
        }
      }
    }
  
    return;
  }
  
  void zzcreateInternalPredTemplate(const string& predName,
                                    const char* const & ttype)
  {
      // If already declared then return
    if (zzdomain->getPredicateId(predName.c_str()) >= 0) return;
    int index;
    string baseName = predName.substr(0, predName.find_last_of("_"));
    
    if ((index = zzfindInternalPredicate(baseName.c_str())) >= 0)
    {
      zzassert(zzdomain->getFunctionId(predName.c_str()) < 0, 
               "not expecting pred name to be declared as a function name");
      PredicateTemplate* ptemplate = new PredicateTemplate();
      ptemplate->setName(predName.c_str());
   	
        // Add types
      for (int j = 1; j < zzinternalPredicates[index].size(); j++)
      {
        int id;
        if (!zzdomain->isType(ttype))
        {
          id = zzaddTypeToDomain(zzdomain, ttype);
          zzassert(id >= 0, "expecting var id >= 0");
        }
        zzaddType(ttype, ptemplate, NULL, false, zzdomain);
      }
  
        // Add template to domain
      zzassert(ptemplate, "not expecting ptemplate==NULL");
      int id = zzdomain->addPredicateTemplate(ptemplate);
      zzassert(id >= 0, "expecting pred template id >= 0");
      ptemplate->setId(id);
    }
    else
      zzexit("Predicate %s is not an internal predicate.", predName.c_str());
  }
  
  void zzsetInternalPredTypeName(const char* const & predName, const int& typeId)
  {
    const char * typeName = zzdomain->getTypeName(typeId);
    string intPredName =
      PredicateTemplate::createInternalPredTypeName(predName, typeName);
    zzcreateInternalPredTemplate(intPredName, typeName);
    const PredicateTemplate* t =
      zzdomain->getPredicateTemplate(intPredName.c_str());
    zzpred->setTemplate((PredicateTemplate*)t);
    zzassert(zzdomain->getPredicateTemplate(intPredName.c_str()) != NULL,
             "expect internal pred template != NULL");
    ListObj* predlo = zzpredFuncListObjs.top();
    predlo->replace(predName, intPredName.c_str());
  }
  
  void zzcreateInternalFuncTemplate(const string & funcName,
  								  const Array<string>& typeNames)
  {
      // If already declared then return
    if (zzdomain->getFunctionId(funcName.c_str()) >= 0) return;
    int index;
    string baseName = funcName.substr(0, funcName.find_first_of("_"));
  
    if ((index = zzfindInternalFunction(baseName.c_str())) >= 0)
    {
      zzassert(zzfuncTemplate==NULL, "expecting zzfuncTemplate==NULL");
      zzfuncTemplate = new FunctionTemplate();
  
        // We are creating a new predicate as well
      zzassert(zzpredTemplate==NULL,"expecting zzpredTemplate==NULL");
      zzpredTemplate = new PredicateTemplate();
  
      zzassert(zzdomain->getPredicateId(funcName.c_str()) < 0, 
               "not expecting func name to be declared as pred name");
      zzassert(zzfuncTemplate,"expecting zzfuncTemplate!=NULL");
      zzfuncTemplate->setName(funcName.c_str());
  
        // Predicate name is PredicateTemplate::ZZ_RETURN_PREFIX + function name
      char* predName;
      predName = (char *)malloc((strlen(PredicateTemplate::ZZ_RETURN_PREFIX) +
                                 strlen(funcName.c_str()) + 1)*sizeof(char));
      strcpy(predName, PredicateTemplate::ZZ_RETURN_PREFIX);
      strcat(predName, funcName.c_str());
  
        // Check that predicate has not been declared a function
      zzassert(zzdomain->getFunctionId(predName) < 0, 
               "not expecting pred name to be declared as a function name");
      zzassert(zzpredTemplate,"expecting zzpredTemplate!=NULL");
      zzpredTemplate->setName(predName);
      free(predName);  
      
        // Add return type
      const char* retTypeName = typeNames[0].c_str();
  
      if (!zzdomain->isType(retTypeName))
      {
        int id = zzaddTypeToDomain(zzdomain, retTypeName);
        zzassert(id >= 0, "expecting retTypeName's id >= 0");
      }
  
      zzfuncTemplate->setRetTypeName(retTypeName, zzdomain);
        // We are creating a new predicate as well
      zzaddType(retTypeName, zzpredTemplate, NULL, false, zzdomain);
    
        // Add types
      for (int j = 1; j < typeNames.size(); j++)
      {
        int id;
        const char* ttype = typeNames[j].c_str();
        if (!zzdomain->isType(ttype))
        {
          id = zzaddTypeToDomain(zzdomain, ttype);
          zzassert(id >= 0, "expecting var id >= 0");
        }
        zzaddType(ttype, zzpredTemplate, NULL, false, zzdomain);
          // Add the type to the function too
        zzaddType(ttype, NULL, zzfuncTemplate, false, zzdomain);
      }
  
        // Add templates to domain
      zzassert(zzfuncTemplate, "expecting zzfuncTemplate != NULL");
      int id = zzdomain->addFunctionTemplate(zzfuncTemplate);
      zzassert(id >= 0, "expecting function template's id >= 0");
      zzfuncTemplate->setId(id);
      zzfuncTemplate = NULL;
  
      zzassert(zzpredTemplate, "not expecting zzpredTemplate==NULL");
      int predId = zzdomain->addPredicateTemplate(zzpredTemplate);
      zzassert(predId >= 0, "expecting pred template id >= 0");
      zzpredTemplate->setId(predId);
      zzpredTemplate = NULL;  	
    }
    else
      zzexit("Function %s is not an internal function.", funcName.c_str());
  }
  
  void zzsetInternalFuncTypeName(const char* const & funcName,
                                 const Array<int>& typeIds)
  {
    Array<string> typeNames(typeIds.size());
    for (int i = 0; i < typeIds.size(); i++)
      typeNames.append(zzdomain->getTypeName(typeIds[i]));
    string intFuncName =
      FunctionTemplate::createInternalFuncTypeName(funcName, typeNames);
    zzcreateInternalFuncTemplate(intFuncName, typeNames);
    
    const FunctionTemplate* t =
      zzdomain->getFunctionTemplate(intFuncName.c_str());
    zzfunc->setTemplate((FunctionTemplate*)t);
    zzassert(zzdomain->getFunctionTemplate(intFuncName.c_str()) != NULL,
             "expect internal func template != NULL");
    ListObj* funclo = zzpredFuncListObjs.top();
    funclo->replace(funcName, intFuncName.c_str());
  }
  
  const FunctionTemplate* zzgetGenericInternalFunctionTemplate(
                                                     const char* const & funcName)
  {
    zzassert(FunctionTemplate::isInternalFunctionTemplateName(funcName),
             "expect internal function name");
    int index = zzfindInternalFunction(funcName);
    FunctionTemplate* funcTemplate = new FunctionTemplate();
    funcTemplate->setName(funcName);
    	
      // Add return type
    funcTemplate->setRetTypeName(PredicateTemplate::ANY_TYPE_NAME, zzdomain);
    
      // Add types
    for (int j = 2; j < zzinternalFunctions[index].size(); j++)
    {
        // Add the type to the function
      zzaddType(PredicateTemplate::ANY_TYPE_NAME, NULL, funcTemplate, false,
                zzdomain);
    }
    return funcTemplate;
  }
  
  /**
   * Moves a term attached to the previous function / predicate to the current infix
   * function. If the parser encounters a term, it is first attached to the current
   * function / predicate. After encountering an infix function sign, the term has to
   * be transferred via this method.
   */
  void moveTermToInfixFunction()
  {
      // top in zzpredFuncListObjs must be infix function, second to top is pred /
      // func in which it is nested
  
    Term* term = NULL;
      // In a function
    if (!zzfuncStack.empty())
    {
      Function* prevFunc = zzfuncStack.top();
      term = prevFunc->removeLastTerm();
    }
      // Not in a function
    else
    {
      zzassert(zzpred, "expecting to be in a predicate");
      term = zzpred->removeLastTerm();
    }
    term->setParent(zzfunc, false);
    zzfunc->appendTerm(term);
    ListObj* lo = zzpredFuncListObjs.top();
    zzpredFuncListObjs.pop();
    lo->append((zzpredFuncListObjs.top())->removeLast());
    zzpredFuncListObjs.push(lo);
  }
  
  #endif
  