/**************************************************************/
/* ********************************************************** */
/* *                                                        * */
/* *              FIRST ORDER LOGIC SYMBOLS                 * */
/* *                                                        * */
/* *  $Module:   FOL      DFG                               * */ 
/* *                                                        * */
/* *  Copyright (C) 1996, 1997, 1998, 1999, 2000, 2001      * */
/* *  MPI fuer Informatik                                   * */
/* *                                                        * */
/* *  This program is free software; you can redistribute   * */
/* *  it and/or modify it under the terms of the GNU        * */
/* *  General Public License as published by the Free       * */
/* *  Software Foundation; either version 2 of the License, * */
/* *  or (at your option) any later version.                * */
/* *                                                        * */
/* *  This program is distributed in the hope that it will  * */
/* *  be useful, but WITHOUT ANY WARRANTY; without even     * */
/* *  the implied warranty of MERCHANTABILITY or FITNESS    * */
/* *  FOR A PARTICULAR PURPOSE.  See the GNU General Public * */
/* *  License for more details.                             * */
/* *                                                        * */
/* *  You should have received a copy of the GNU General    * */
/* *  Public License along with this program; if not, write * */
/* *  to the Free Software Foundation, Inc., 59 Temple      * */
/* *  Place, Suite 330, Boston, MA  02111-1307  USA         * */
/* *                                                        * */
/* *                                                        * */
/* $Revision$                                        * */
/* $State$                                            * */
/* $Date$                             * */
/* $Author$                                       * */
/* *                                                        * */
/* *             Contact:                                   * */
/* *             Christoph Weidenbach                       * */
/* *             MPI fuer Informatik                        * */
/* *             Stuhlsatzenhausweg 85                      * */
/* *             66123 Saarbruecken                         * */
/* *             Email: weidenb@mpi-sb.mpg.de               * */
/* *             Germany                                    * */
/* *                                                        * */
/* ********************************************************** */
/**************************************************************/


/* $RCSfile$ */

#ifndef _FOLDFG_
#define _FOLDFG_

/**************************************************************/
/* Includes                                                   */
/**************************************************************/

#include "flags.h"
#include "unify.h"
#include "context.h"
#include "term.h"

/**************************************************************/
/* Global Variables and Constants (Only seen by macros)       */
/**************************************************************/

extern SYMBOL  fol_ALL;
extern SYMBOL  fol_EXIST;
extern SYMBOL  fol_AND;
extern SYMBOL  fol_OR;
extern SYMBOL  fol_NOT;
extern SYMBOL  fol_IMPLIES;
extern SYMBOL  fol_IMPLIED;
extern SYMBOL  fol_EQUIV;
extern SYMBOL  fol_VARLIST;
extern SYMBOL  fol_EQUALITY;
extern SYMBOL  fol_TRUE;
extern SYMBOL  fol_FALSE;

/**************************************************************/
/* Access to the first-order symbols.                         */
/**************************************************************/

static __inline__ SYMBOL fol_All(void)
{
  return fol_ALL;
}

static __inline__ SYMBOL fol_Exist(void)
{
  return fol_EXIST;
}

static __inline__ SYMBOL fol_And(void)
{
  return fol_AND;
}

static __inline__ SYMBOL fol_Or(void)
{
  return fol_OR;
}

static __inline__ SYMBOL fol_Not(void)
{
  return fol_NOT;
}

static __inline__ SYMBOL fol_Implies(void)
{
  return fol_IMPLIES;
}

static __inline__ SYMBOL fol_Implied(void)
{
  return fol_IMPLIED;
}

static __inline__ SYMBOL fol_Equiv(void)
{
  return fol_EQUIV;
}

static __inline__ SYMBOL fol_Varlist(void)
{
  return fol_VARLIST;
}

static __inline__ SYMBOL fol_Equality(void)
{
  return fol_EQUALITY;
}

static __inline__ SYMBOL fol_True(void)
{
  return fol_TRUE;
}

static __inline__ SYMBOL fol_False(void)
{
  return fol_FALSE;
}

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

static __inline__ BOOL fol_IsQuantifier(SYMBOL S)
{
  return symbol_Equal(fol_ALL,S) || symbol_Equal(fol_EXIST,S);
}

static __inline__ BOOL fol_IsTrue(TERM S)
{
  return symbol_Equal(fol_TRUE,term_TopSymbol(S));
}

static __inline__ BOOL fol_IsFalse(TERM S)
{
  return symbol_Equal(fol_FALSE,term_TopSymbol(S));
}

static  __inline__ LIST fol_QuantifierVariables(TERM T)
  /* T's top symbol must be a quantifier ! */
{
  return term_ArgumentList(term_FirstArgument(T));
}

static __inline__ BOOL fol_IsLiteral(TERM T)
{
  return symbol_IsPredicate(term_TopSymbol(T)) ||
    (symbol_Equal(term_TopSymbol(T),fol_Not()) && 
     symbol_IsPredicate(term_TopSymbol(term_FirstArgument(T))));
}

static __inline__ BOOL fol_IsNegativeLiteral(TERM T)
{
  return (symbol_Equal(term_TopSymbol(T),fol_Not()) && 
	  symbol_IsPredicate(term_TopSymbol(term_FirstArgument(T))));
}


static __inline__ BOOL fol_IsJunctor(SYMBOL S)
{
  return fol_IsQuantifier(S) || symbol_Equal(S, fol_AND) || 
    symbol_Equal(S, fol_OR) || symbol_Equal(S, fol_NOT) ||
    symbol_Equal(S, fol_IMPLIED) ||  symbol_Equal(S, fol_VARLIST) ||
    symbol_Equal(S, fol_IMPLIES) || symbol_Equal(S, fol_EQUIV);
}

static __inline__ BOOL fol_IsPredefinedPred(SYMBOL S)
{
  return symbol_Equal(S, fol_EQUALITY) || symbol_Equal(S, fol_TRUE) ||
    symbol_Equal(S, fol_FALSE);
}

static __inline__ TERM fol_Atom(TERM Lit)
{
  if (term_TopSymbol(Lit) == fol_NOT)
    return term_FirstArgument(Lit);
  else
    return Lit;
}

static __inline__ BOOL fol_IsEquality(TERM Term)
{
  return term_TopSymbol(Term) == fol_EQUALITY;
}


static __inline__ BOOL fol_IsAssignment(TERM Term)
{
  return (term_TopSymbol(Term) == fol_EQUALITY &&
	  ((term_IsVariable(term_FirstArgument(Term)) &&
	    !term_ContainsVariable(term_SecondArgument(Term),
				   term_TopSymbol(term_FirstArgument(Term)))) ||
	   (term_IsVariable(term_SecondArgument(Term)) &&
	    !term_ContainsVariable(term_FirstArgument(Term),
				   term_TopSymbol(term_SecondArgument(Term))))));
}


static __inline__ LIST fol_DeleteFalseTermFromList(LIST List)
/**************************************************************
  INPUT:   A list of terms.
  RETURNS: The list where all terms equal to the 'False' term are removed.
  EFFECTS:  'False' is a special predicate from the fol module.
           Terms are compared with respect to the term_Equal function.
           The terms are deleted, too.
***************************************************************/
{
  return list_DeleteElementIfFree(List, (BOOL (*)(POINTER))fol_IsFalse,
				  (void (*)(POINTER))term_Delete);
}


static __inline__ LIST fol_DeleteTrueTermFromList(LIST List)
/**************************************************************
  INPUT:   A list of terms.
  RETURNS: The list where all terms equal to the 'True' term are removed.
  EFFECTS:  'True' is a special predicate from the fol module.
           Terms are compared with respect to the term_Equal function.
           The terms are deleted, too.
***************************************************************/
{
  return list_DeleteElementIfFree(List, (BOOL (*)(POINTER))fol_IsTrue,
				  (void (*)(POINTER))term_Delete);
}


/**************************************************************/
/* Functions                                                  */
/**************************************************************/

void   fol_Init(BOOL, PRECEDENCE);
SYMBOL fol_IsStringPredefined(const char*);
TERM   fol_CreateQuantifier(SYMBOL, LIST, LIST);
TERM   fol_CreateQuantifierAddFather(SYMBOL, LIST, LIST);
LIST   fol_GetNonFOLPredicates(void);
TERM   fol_ComplementaryTerm(TERM);
LIST   fol_GetAssignments(TERM);
void   fol_Free(void);
void   fol_CheckFatherLinks(TERM);
BOOL   fol_FormulaIsClause(TERM);
void   fol_FPrintOtterOptions(FILE*, BOOL, FLAG_TDFG2OTTEROPTIONSTYPE);
void   fol_FPrintOtter(FILE*, LIST, FLAG_TDFG2OTTEROPTIONSTYPE);
void   fol_FPrintDFGSignature(FILE*);
void   fol_PrettyPrintDFG(TERM);
void   fol_PrintDFG(TERM);
void   fol_FPrintDFG(FILE*, TERM);
void   fol_FPrintDFGProblem(FILE*, const char*, const char*, const char*, const char*, LIST, LIST);
void   fol_PrintPrecedence(PRECEDENCE);
void   fol_FPrintPrecedence(FILE*, PRECEDENCE);
LIST   fol_Instances(TERM, TERM);
LIST   fol_Generalizations(TERM, TERM);
TERM   fol_MostGeneralFormula(LIST);
void   fol_NormalizeVars(TERM);
void   fol_NormalizeVarsStartingAt(TERM, SYMBOL);
LIST   fol_FreeVariables(TERM);
LIST   fol_BoundVariables(TERM);
BOOL   fol_VarOccursFreely(TERM,TERM);
BOOL   fol_AssocEquation(TERM, SYMBOL *);
BOOL   fol_DistributiveEquation(TERM, SYMBOL*, SYMBOL*);
void   fol_ReplaceVariable(TERM, SYMBOL, TERM);
void   fol_PrettyPrint(TERM);
LIST   fol_GetSubstEquations(TERM);
TERM   fol_GetBindingQuantifier(TERM, SYMBOL);
int    fol_TermPolarity(TERM, TERM);
BOOL   fol_PolarCheck(TERM, TERM);
void   fol_PopQuantifier(TERM);
void   fol_DeleteQuantifierVariable(TERM,SYMBOL);
void   fol_SetTrue(TERM);
void   fol_SetFalse(TERM);
void   fol_RemoveImplied(TERM);
BOOL   fol_PropagateFreeness(TERM);
BOOL   fol_PropagateWitness(TERM);
BOOL   fol_PropagateTautologies(TERM);
BOOL   fol_AlphaEqual(TERM, TERM);
BOOL   fol_VarBoundTwice(TERM);
NAT    fol_Depth(TERM);
BOOL   fol_ApplyContextToTerm(CONTEXT, TERM);
BOOL   fol_CheckFormula(TERM);
BOOL   fol_SignatureMatchFormula(TERM, TERM, BOOL);
BOOL   fol_SignatureMatch(TERM, TERM, LIST*, BOOL);

#endif