folhelper.h

/*
 * All of the documentation and software included in the
 * Alchemy Software is copyrighted by Stanley Kok, Parag
 * Singla, Matthew Richardson, Pedro Domingos, Marc
 * Sumner and Hoifung Poon.
 * 
 * Copyright [2004-07] Stanley Kok, Parag Singla, Matthew
 * Richardson, Pedro Domingos, Marc Sumner and Hoifung
 * Poon. 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 and Hoifung
 * Poon 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;

  //Each clause derived from a unit formula with mutually exclusive and 
  //exhaustive variables is given a weight that is 1.5 times
  //that of the maximum soft clause weight. You can change this value by setting
  //EXIST_UNIQUE_WEIGHT_MULTIPLIER below. If you wish to set the clause weight 
  //to a specific value, you can set EXIST_UNIQUE_WEIGHT to that value below. 
  //If EXIST_UNIQUE_WEIGHT is DBL_MIN, EXIST_UNIQUE_WEIGHT_MULTIPLIER is used 
  //instead of EXIST_UNIQUE_WEIGHT; otherwise the latter is used.
const double EXIST_UNIQUE_WEIGHT_MULTIPLIER = 1.5;
const double EXIST_UNIQUE_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;
Array<int> zzuniqueVarIndexes; // index of unique variable in unit clause
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;

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_; 
};

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_; 
};

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;

  

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; 


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;


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 Array<int>& uuniqueVarIndexes, 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;

    uniqueVarIndexes.append(uuniqueVarIndexes);
  }

  ~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;
  Array<int> uniqueVarIndexes;
  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);
}



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_;
  }
}




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

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

bool zzisLinkedFunction(const char* funcname, void* handle)
{
  string (*funccall)(string);
  char *error;

  dlerror();    // Clear any existing error
  *(void **) (&funccall) = dlsym(handle, funcname);
  if ((error = dlerror()) != NULL) return false;

  return true;
}

bool zzisLinkedPredicate(const char* predname, void* handle)
{
  bool (*funccall)(string);
  char *error;

  dlerror();    // Clear any existing error
  *(void **) (&funccall) = 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));
}



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



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 ((clauselo[0]->getStr())[0] == 'v')
  {
    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;
}


  //create clauses from an existentially and uniquely quantified variables
int zzcreateExistUniqueClauses(Array<Clause*>& clauses, 
                               const Array<int>& uniqueVarIndexes,
                               const Domain* const & domain)
{
  if (clauses.size() != 1 || uniqueVarIndexes.size() <= 0)
    zzexit("ERROR: in zzcreateExistUniqueClauses. "
           "clauses.size() != 1 || uniqueVarIndexes.size() <= 0");

    //c has been canonicalized
  Clause* c = clauses[0];
  clauses.clear();
  Predicate* pred = (Predicate*) c->getPredicate(0); 
 
  Array<int> nonUniqVarIndexes, nonUniqVarIds;
  for (int i = 0; i < pred->getNumTerms(); i++)
  {
    if (uniqueVarIndexes.contains(i)) continue;
    nonUniqVarIndexes.append(i);
    nonUniqVarIds.append(pred->getTerm(i)->getId());
  }

  for (int i = 0; i < nonUniqVarIndexes.size(); i++)
    ((Term*)pred->getTerm(nonUniqVarIndexes[i]))->setId(1);
 
  Array<Predicate*> predArr;
  pred->createAllGroundings(domain, &predArr, NULL);
  int numPreds = predArr.size();

  for (int i = 0; i < numPreds; i++)
  {
    Predicate* newPred = predArr[i];
    for (int j = 0; j < nonUniqVarIndexes.size(); j++)
    {
      Term* t = (Term*)newPred->getTerm(nonUniqVarIndexes[j]);
      t->setId(nonUniqVarIds[j]);
    }
  }

    // Commented out: Mut. excl. and exh. variables are handled
    // internally by the learning and inference algorithms
/*      
    // At-least-one (ALO) clause
  Clause* cc = new Clause;
  for (int i = 0; i < numPreds; i++)
  {
    Predicate* newPred = new Predicate(*(predArr[i]));
    newPred->setParent(cc);
    cc->appendPredicate(newPred);
  }
  clauses.append(cc);

    // At-most-one (AMO) clauses
  for (int i = 0; i < numPreds; i++)
    for (int j = i+1; j < numPreds; j++)
    {
      Clause* cc = new Clause;
      Predicate* newPred = new Predicate(*(predArr[i]));
      newPred->setParent(cc);
      newPred->setSense(false);
      cc->appendPredicate(newPred);

      Predicate* newPred2 = new Predicate(*(predArr[j]));
      newPred2->setParent(cc);
      newPred2->setSense(false);
      cc->appendPredicate(newPred2);
      clauses.append(cc);
    }
*/
    // Add predicates to blocks
  Array<Array<Predicate*>*>* predBlocks = new Array<Array<Predicate*>*>;
  
    // # blocks = (# const. of nonUniqVar 1) * (# const. of nonUniqVar 2) ...
  int numBlocks = 1;
  for (int i = 0; i < nonUniqVarIndexes.size(); i++)
  {
    int typeId = pred->getTermTypeAsInt(nonUniqVarIndexes[i]);
    numBlocks *= domain->getNumConstantsByType(typeId);
  }
  predBlocks->growToSize(numBlocks);

  for (int i = 0; i < numBlocks; i++)
  {
    Array<Predicate*>* predBlock = new Array<Predicate*>;
    (*predBlocks)[i] = predBlock;
  }
  
  for (int i = 0; i < numPreds; i++)
  {
    Predicate* newPred = new Predicate(*(predArr[i]));
    Array<Predicate*> predGndings;
    newPred->createAllGroundings(domain, &predGndings, NULL);

    for (int j = 0; j < predGndings.size(); j++)
    {
      Predicate* predGnding = new Predicate(*(predGndings[j]));
      (*predBlocks)[j]->append(predGnding);
    }
    predGndings.deleteItemsAndClear();
    delete newPred;
  }

  for (int i = 0; i < numBlocks; i++)
  {
    Array<Predicate*>* predBlock = (*predBlocks)[i];
    int blockIdx = domain->addPredBlock(predBlock);
    
    for (int j = 0; j < predBlock->size(); j++)
    {
      Predicate* p = (*predBlock)[j];

        // If groundings of this pred occur
      if ((zzpredIdToGndPredMap.find(pred->getId())) != 
           zzpredIdToGndPredMap.end())
      {
        PredicateHashArray* pha = zzpredIdToGndPredMap[pred->getId()];
        int a = pha->find(p);
      
          // Only one atom in a block can be true
        if (a >= 0 && (*pha)[a]->getTruthValue() == TRUE)
        {
          zzassert(!domain->getBlockEvidence(blockIdx),
                   "More than one true atom found for mutually "
                   "exclusive and exhaustive variables");
          domain->setBlockEvidence(blockIdx, true);
        }
      }
    }
  }
  delete predBlocks;

  predArr.deleteItemsAndClear();
  delete c;  
  return numPreds;
}


bool zzcheckPlusTypes(const char* const & typeName,
                      const Domain* const & dom, const Domain* const & domain0)
{
  if (domain0 == NULL) return true;

  const Array<int>* c = dom->getConstantsByType(typeName);
  assert(c);
  
  const Array<int>* cc = domain0->getConstantsByType(typeName);
  
  if (cc == NULL || (c->size() != cc->size())) 
  {
    zzerr("the type (\"%s\") of variables to which '+' is applied must have "
          "the same constants across all databases.", typeName);
    return false;
  }
  
  for (int k = 0; k < c->size(); k++)
  {
    const char* constName = dom->getConstantName((*c)[k]);      
    int cconstId = domain0->getConstantId(constName);
    const char* ttypeName = domain0->getConstantTypeName(cconstId);
    
    if (cconstId < 0 || strcmp(typeName,ttypeName) != 0)
    {
      zzerr("the type (\"%s\") of variables to which '+' is applied must have"
            " the same constants across all databases.", typeName);
      zzerr("constant %s not found or is of the wrong type", constName);
      return false;
    }
  }
  return true;
}


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

    const char* typeName = domain->getTypeName(typeId);
    if (domain0 && !zzcheckPlusTypes(typeName, domain, domain0)) return;

    Array<int>* constArr;
    if (domain0) 
    {
      constArr = new Array<int>;
      cleanUp.append(constArr);
      const Array<int>* carr = domain0->getConstantsByType(typeName);
      constArr->growToSize(carr->size());
      for (int i = 0; i < carr->size(); i++)
      {
        const char* constName = domain0->getConstantName((*carr)[i]);
        int constId = domain->getConstantId(constName);
        zzassert(constId >= 0, "failed to find constant in zzgroundPlusVar");
        (*constArr)[i] = constId;
      }
    }
    else         
      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);

    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);
    }
    formulas.append(gndFormula);

    string s = formulaStr;
    for (int i = 0; i < constIds.size(); i++)
    {
      unsigned int a = s.find("+");
      assert(a != string::npos);
      unsigned int b = a+1;
      while(s.at(b) != ',' && s.at(b) != ')') b++;
      string front = s.substr(0, a);
      string back = s.substr(b, s.length()-b);
      s = front; 
      s.append(domain->getConstantName(constIds[i]));
      s.append(back);
    }

    formulaStrs.append(s);
  }

  if (domain0) cleanUp.deleteItemsAndClear();
}



void zzcreateListObjFromTop(stack<ListObj*>& stack, const char* const & op)
{
  zzassert(zzformulaListObjs.size()>=1, "expect zzformulaListObjs.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");  
  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");  
  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)
{
  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 (db->storeGroundPreds()) db->addAllGroundings();

  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)
{  
  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);
    zzformulaStr.append(constName);
  }
  else 
    zzexit("No function or predicate to hold constant %s", constName);
}


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 (isupper(varName[0])) 
  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); 
    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();
  zzuniqueVarIndexes.clear();
  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");
  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");
  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");
  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");
  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");
  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");
  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;
  zzuniqueVarIndexes.clear();
  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 & 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);
      }
    }
  }
  

  if (allPredsExceptQueriesAreClosedWorld)
  {
    isClosedWorldArr.growToSize(zzdomain->getNumPredicates(), true);
    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;
      }
    }
  }
  else
  {   // some or all predicates are open world
    isClosedWorldArr.growToSize(zzdomain->getNumPredicates(), true);
 
    // '=' predicates are always closed world

    Array<string> owPredNames;
      // if no open world predicates are specified then all are open world
    if (openWorldPredNames == NULL || openWorldPredNames->empty())
      zzdomain->getNonEqualPredicateNames(owPredNames);
    else
      for (int i = 0; i < openWorldPredNames->size(); i++) 
        owPredNames.append((*openWorldPredNames)[i]);

    for (int i = 0; i < owPredNames.size(); i++) 
    {
      const char* predName = owPredNames[i].c_str();
      int predId = zzdomain->getPredicateId(predName);
      if (predId < 0)
      {
        zzerr("predicate %s is not declared. Please declare it.", predName);
        continue;
      }
      
      isClosedWorldArr[predId] = false;
    }

    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 Array<int>& uniqueVarIndexes,
                                 const bool& hasFullStop,
                                 const bool& readHardClauseWts,
                                 const bool& mustHaveWtOrFullStop,
                                 Array<int>& hardClauseIdxs,
                                 Array<string>& hardFormulas,
                                 Array<int>& existUniqueClauseIdxs,
                                 Array<string>& existUniqueFormulas,
                                 Clause*& flippedClause,
                                 const Domain* const & domain0)
{
  //cout << "orig formula = " << endl << "\t: " << formulaStr << endl;    
  //cout << "formula      = " << endl << "\t: " << *formula << endl;

  bool isExistUnique = (uniqueVarIndexes.size() > 0);

  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;

        //if the '!' operator is used
      if (isExistUnique)
      {
        assert(formulas.size() == 1); // no '+' is used
        assert(formulas2.size() == 1); //no '*' is used
      }
      Array<Clause*> clauses;
      zzcreateClauses(cnf, clauses, flippedClause);
      int numEPreds = 0;
      if (isExistUnique) 
        numEPreds=zzcreateExistUniqueClauses(clauses,uniqueVarIndexes,zzdomain);

      cout << "\tCNF has  " << clauses.size() << " clause"
           << ((clauses.size()>1)?"s":"") << endl;
      delete cnf; delete vars;

      double perClauseWt = 0;
      double formulaWt = 0;
      bool setHardWtLater = false;
      bool setExistUniqueWtLater = 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;
        }
        if (isExistUnique) numEPreds = 0;
      }
      else
      if (wt)
      { perClauseWt = (*wt)/clauses.size(); formulaWt = *wt; }
      else
      {
        if (mustHaveWtOrFullStop && !isExistUnique)
          zzerr("a weight or full stop must be specified for:\n%s",
                formStr.c_str());
        perClauseWt = defaultWt/clauses.size();
        formulaWt = defaultWt;

        if (isExistUnique) 
        { 
          perClauseWt = 0; formulaWt = 0; 
          existUniqueFormulas.append(formStr);
          setExistUniqueWtLater = true;
          numEPreds = 0;
        }
      }

      
      for (int i = 0; i < clauses.size(); i++)
      {
          //if this clause belongs to the CNF of  an exist. & unique. quant. 
          //formula and a prior mean was explicitly specified
        if (isExistUnique && numEPreds > 0) 
        { 
          double n = numEPreds;
          if (i == 0) perClauseWt = (n > 1) ? formulaWt/(n+1) : formulaWt;
          else        perClauseWt = 2*formulaWt/(n*n-1);
        }

        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);
        else if (setExistUniqueWtLater) existUniqueClauseIdxs.append(prevIdx);
      }

      mln->setFormulaNumPreds(formStr, numPreds);
      mln->setFormulaPriorMean(formStr, formulaWt);
      mln->setFormulaWt(formStr, formulaWt);
      mln->setFormulaIsExistUnique(formStr, isExistUnique);
      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, existUniqueClauseIdxs;
  Array<string> hardFormulas, existUniqueFormulas;
  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->uniqueVarIndexes,
                                epfi->hasFullStop, epfi->readHardClauseWts,
                                epfi->mustHaveWtOrFullStop, 
                                hardClauseIdxs, hardFormulas, 
                                existUniqueClauseIdxs, existUniqueFormulas,
                                flippedClause, domain0);
    delete epfi;
    cout<<"CNF conversion took ";Timer::printTime(cout,zztimer.time()-startSec);
    cout<<endl;
  }
  formulaInfos.clear();

  //set the weights of hard clauses and those derived from 
  //existentially & uniquely quant formulas

  double maxSoftWt = mln->getMaxAbsSoftWt();
  if (maxSoftWt == 0) maxSoftWt = 1;

  double hardWt = (HARD_WEIGHT==DBL_MIN) ?  HARD_WEIGHT_MULTIPLIER * maxSoftWt 
                                          : HARD_WEIGHT;
  double existUniqueWt = (EXIST_UNIQUE_WEIGHT==DBL_MIN) ? 
                         EXIST_UNIQUE_WEIGHT_MULTIPLIER *maxSoftWt 
                       : EXIST_UNIQUE_WEIGHT; 

  for (int i = 0; i < existUniqueClauseIdxs.size(); i++)
    ((Clause*)mln->getClause(existUniqueClauseIdxs[i]))->setWt(existUniqueWt);

  for (int i = 0; i < existUniqueFormulas.size(); i++)
  {
    mln->setFormulaWt(existUniqueFormulas[i], existUniqueWt);
    mln->setFormulaPriorMean(existUniqueFormulas[i], existUniqueWt);
  }

  for (int i = 0; i < hardClauseIdxs.size(); i++)
  {
    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);
}

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


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

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

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

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


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

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

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

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

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

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

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

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


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

void zzgenerateGroundingsFromInternalPredicate(int index,
                                                                                           const PredicateTemplate* const& ptemplate)
{
  // Find number of terms for predicate
  //const PredicateTemplate* ptemplate =
  //    zzdomain->getPredicateTemplate(zzinternalPredicates[index][0]);

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

void zzgenerateGroundingsFromInternalFunction(int index,
                                                                                          const FunctionTemplate* const& ftemplate)
{
  // Find number of terms for function
  //const FunctionTemplate* ftemplate =
        //zzdomain->getFunctionTemplate(zzinternalFunctions[index][0]);
        
  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;
}

void zzgenerateGroundingsFromInternalPredicatesAndFunctions()
{
  // Look at each predicate
  //for (int i = 0; i < zzinternalPredicates.size(); i++)
  //{
        //const char* predName = zzinternalPredicates[i][0];
        //if (zzdomain->getPredicateId(predName) >= 0)
        //{
          //cout << "Found internal predicate: " << zzinternalPredicates[i][0] << endl;
          //zzgenerateGroundingsFromInternalPredicate(i);
        //}
  //}

  // 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++)
          {
                if (strncmp(ptemplate->getName(), zzinternalPredicates[j][0],
                                        strlen(zzinternalPredicates[j][0])) == 0)
                {
                  zzgenerateGroundingsFromInternalPredicate(j, ptemplate);
                  break;
                }
          }
        }
  }

  // Look at each function
  //for (int i = 0; i < zzinternalFunctions.size(); i++)
  //{
        //const char* funcName = zzinternalFunctions[i][0];
        //if (zzdomain->getFunctionId(funcName) >= 0)
        //{
          //cout << "Found internal function: " << zzinternalFunctions[i][0] << endl;
          //zzgenerateGroundingsFromInternalFunction(i);
        //}
  //}

  // 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;
          //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);
  }
  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 = zzinternalFunctions[index][1];
        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 = 2; j < zzinternalFunctions[index].size(); j++)
        for (int j = 1; j < typeNames.size(); j++)
        {
          int id;
          //const char* ttype = zzinternalFunctions[index][j];
          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;
}

#endif

---