path: root/test/spass/flags.c

/**************************************************************/
/* ********************************************************** */
/* *                                                        * */
/* *                 FLAGS OF SPASS                         * */
/* *                                                        * */
/* *  $Module:   FLAGS                                      * */ 
/* *                                                        * */
/* *  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: 35442 $                                        * */
/* $State$                                            * */
/* $Date: 2007-03-28 17:24:40 -0700 (Wed, 28 Mar 2007) $                             * */
/* $Author: jeffc $                                       * */
/* *                                                        * */
/* *             Contact:                                   * */
/* *             Christoph Weidenbach                       * */
/* *             MPI fuer Informatik                        * */
/* *             Stuhlsatzenhausweg 85                      * */
/* *             66123 Saarbruecken                         * */
/* *             Email: weidenb@mpi-sb.mpg.de               * */
/* *             Germany                                    * */
/* *                                                        * */
/* ********************************************************** */
/**************************************************************/


/* $RCSfile$ */

#include <stdio.h>
#include <string.h>

#include "flags.h"
#include "misc.h"
#include "stringsx.h"

/**************************************************************/
/* Global Declarations                                        */
/**************************************************************/

const int flag_CLEAN = -5;


/**************************************************************/
/* File Local Declarations                                    */
/**************************************************************/

/* Define flag properties */
typedef struct {
  int        minimum;
  int        maximum;
  FLAG_TYPE  type;
  const char *name;
} FLAG_PROPERTY;


static FLAGARRAY     flag_DEFAULTSTORE;
static FLAG_PROPERTY flag_PROPERTIES[flag_MAXFLAG];


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

static __inline__ void flag_InitIntern (FLAG_ID Flag, FLAG_TYPE Type,
					const char *Name, int Value,
					int Minimum, int Maximum)
{
  FLAG_PROPERTY *property;

  flag_CheckFlagIdInRange(Flag);

  property = &(flag_PROPERTIES[Flag]);

  /* Set the flag type */
  flag_CheckFlagTypeInRange(Type);
  property->type = Type;

  /* Set flag name */
  property->name = Name;

  /* Set flag minimum and maximum */
  property->minimum = Minimum;
  property->maximum = Maximum;

  /* Set flag value */
#ifdef CHECK
  if (Value > Minimum && Value < Maximum) {
#endif

    flag_DEFAULTSTORE[Flag] = Value;

#ifdef CHECK
  }
  else {
    misc_StartErrorReport();
    misc_ErrorReport("\n In flag_InitIntern: Default value out of range.");
    misc_ErrorReport("\n Flag: %s. Value: %d.", Name, Value);
    misc_FinishErrorReport();
  }
#endif
}

void flag_Init(void)
/**************************************************************
  INPUT:   None.
  RETURNS: Nothing.
  EFFECT:  Sets all default values for known flags.
  MEMORY:  Allocates memory for the default store.
***************************************************************/
{
  /* Autonomous mode */
  flag_InitIntern(flag_AUTO, flag_UNIQUE, "Auto", flag_AUTOON,
		  flag_AUTOMIN, flag_AUTOMAX);

  /* Set of Support Mode */
  flag_InitIntern(flag_SOS, flag_UNIQUE, "SOS", flag_SOSOFF,
		  flag_SOSMIN, flag_SOSMAX);

  /* If set input is considered from stdin and printed to stdout */
  flag_InitIntern(flag_STDIN, flag_UNIQUE, "Stdin", flag_STDINOFF,
		  flag_STDINMIN, flag_STDINMAX);

   /* If set interactive queries are possible */
  flag_InitIntern(flag_INTERACTIVE, flag_UNIQUE, "Interactive", flag_INTERACTIVEOFF,
		  flag_INTERACTIVEMIN, flag_INTERACTIVEMAX);

  /* If set only Flotter CNF-translation is performed */
  flag_InitIntern(flag_FLOTTER, flag_UNIQUE, "Flotter", flag_FLOTTEROFF,
		  flag_FLOTTERMIN, flag_FLOTTERMAX);

  /* Allowed number of loops, -1 means no restriction */
  flag_InitIntern(flag_LOOPS, flag_UNIQUE, "Loops", flag_LOOPSUNLIMITED,
		  flag_LOOPSMIN, flag_LOOPSMAX);

  /* Allowed number of splits, -1 means no restriction */
  flag_InitIntern(flag_SPLITS, flag_UNIQUE, "Splits", flag_SPLITSOFF,
		  flag_SPLITSMIN, flag_SPLITSMAX);

  /* Decides the level of sort usage: if 0 then no sort information is processed,
     if 1 all negative monadic literals with a variable as its argument are processed,
     if 2 all negative monadic literals are processed */
  flag_InitIntern(flag_SORTS, flag_UNIQUE, "Sorts", flag_SORTSOFF,
		  flag_SORTSMIN, flag_SORTSMAX);

  /* ForwardSubsumption output not activated */
  flag_InitIntern(flag_PSUB, flag_PRINTING, "PSub", flag_PSUBOFF,
		  flag_PSUBMIN, flag_PSUBMAX);

  /* Maximal memory allocation */
  flag_InitIntern(flag_MEMORY, flag_UNIQUE, "Memory", flag_MEMORYUNLIMITED,
		  flag_MEMORYMIN, flag_MEMORYMAX);

  /* Document static soft typing  */
  flag_InitIntern(flag_DOCSST, flag_PRINTING, "DocSST", flag_DOCSSTOFF,
		  flag_DOCSSTMIN, flag_DOCSSTMAX);

  /* Rewriting output not activated  */
  flag_InitIntern(flag_PREW, flag_PRINTING, "PRew", flag_PREWOFF,
		  flag_PREWMIN, flag_PREWMAX);

  /* Contextual rewriting output not activated  */
  flag_InitIntern(flag_PCRW, flag_PRINTING, "PCRw", flag_PCRWOFF,
		  flag_PCRWMIN, flag_PCRWMAX);

  /* Condensing output not activated  */
  flag_InitIntern(flag_PCON, flag_PRINTING, "PCon", flag_PCONOFF,
		  flag_PCONMIN, flag_PCONMAX);

 /* Assignment Equation Deletion output not activated  */
  flag_InitIntern(flag_PAED, flag_PRINTING, "PAED", flag_PAEDOFF,
		  flag_PAEDMIN, flag_PAEDMAX);

  /* Tautology output not activated  */
  flag_InitIntern(flag_PTAUT, flag_PRINTING, "PTaut", flag_PTAUTOFF,
		  flag_PTAUTMIN, flag_PTAUTMAX);

  /* Output of obvious red. not activated  */
  flag_InitIntern(flag_POBV, flag_PRINTING, "PObv", flag_POBVOFF,
		  flag_POBVMIN, flag_POBVMAX);

  /* SortSimplification output not activated  */
  flag_InitIntern(flag_PSSI, flag_PRINTING, "PSSi", flag_PSSIOFF,
		  flag_PSSIMIN, flag_PSSIMAX);

  /* Static soft typing output not activated  */
  flag_InitIntern(flag_PSST, flag_PRINTING, "PSST", flag_PSSTOFF,
		  flag_PSSTMIN, flag_PSSTMAX);

  /* Proof output not activated  */
  flag_InitIntern(flag_DOCPROOF, flag_UNIQUE, "DocProof", flag_DOCPROOFOFF,
		  flag_DOCPROOFMIN, flag_DOCPROOFMAX);

  /* Matching Replacement Resolution output not activated  */
  flag_InitIntern(flag_PMRR, flag_PRINTING, "PMRR", flag_PMRROFF,
		  flag_PMRRMIN, flag_PMRRMAX);

  /* Unit conflict output not activated  */
  flag_InitIntern(flag_PUNC, flag_PRINTING, "PUnC", flag_PUNCOFF,
		  flag_PUNCMIN, flag_PUNCMAX);

  /* Derived clauses output not activated  */
  flag_InitIntern(flag_PDER, flag_PRINTING, "PDer", flag_PDEROFF,
		  flag_PDERMIN, flag_PDERMAX);

  /* Given clause output activated  */
  flag_InitIntern(flag_PGIVEN, flag_PRINTING, "PGiven", flag_PGIVENON,
		  flag_PGIVENMIN, flag_PGIVENMAX);

  /* If labels are created they are not printed  */
  flag_InitIntern(flag_PLABELS, flag_PRINTING, "PLabels", flag_PLABELSOFF,
		  flag_PLABELSMIN, flag_PLABELSMAX);

  /* Kept clauses output not activated  */
  flag_InitIntern(flag_PKEPT, flag_PRINTING, "PKept", flag_PKEPTOFF,
		  flag_PKEPTMIN, flag_PKEPTMAX);

  /* Split backtrack emphasizing not activated */
  flag_InitIntern(flag_DOCSPLIT, flag_PRINTING, "DocSplit", flag_DOCSPLITOFF,
		  flag_DOCSPLITMIN, flag_DOCSPLITMAX);

  /* Print information about input clauses */
  flag_InitIntern(flag_PPROBLEM, flag_PRINTING, "PProblem", flag_PPROBLEMON,
		  flag_PPROBLEMMIN, flag_PPROBLEMMAX);

  /* Print all derived empty clauses */
  flag_InitIntern(flag_PEMPTYCLAUSE, flag_PRINTING, "PEmptyClause", flag_PEMPTYCLAUSEOFF,
		  flag_PEMPTYCLAUSEMIN, flag_PEMPTYCLAUSEMAX);

  /* Print statistic about memory, clauses */
  flag_InitIntern(flag_PSTATISTIC, flag_PRINTING, "PStatistic", flag_PSTATISTICON,
		  flag_PSTATISTICMIN, flag_PSTATISTICMAX);

  /* Output saturated set of clauses to file, default no */
  flag_InitIntern(flag_FPMODEL, flag_PRINTING, "FPModel", flag_FPMODELOFF,
		  flag_FPMODELMIN, flag_FPMODELMAX);

  /* Output proof in DFG format to file, default no */
  flag_InitIntern(flag_FPDFGPROOF, flag_PRINTING, "FPDFGProof", flag_FPDFGPROOFOFF,
		  flag_FPDFGPROOFMIN, flag_FPDFGPROOFMAX);

  /* Output the actual values of all SPASS flags */
  flag_InitIntern(flag_PFLAGS, flag_PRINTING, "PFlags", flag_PFLAGSOFF,
		  flag_PFLAGSMIN, flag_PFLAGSMAX);

  /* Optimized skolemization output not activated  */
  flag_InitIntern(flag_POPTSKOLEM, flag_PRINTING, "POptSkolem", flag_POPTSKOLEMOFF,
		  flag_POPTSKOLEMMIN, flag_POPTSKOLEMMAX);

  /* Strong skolemization output not activated  */
  flag_InitIntern(flag_PSTRSKOLEM, flag_PRINTING, "PStrSkolem", flag_PSTRSKOLEMOFF,
		  flag_PSTRSKOLEMMIN, flag_PSTRSKOLEMMAX);

  /* Printing of clauses deleted by bound restriction not activated  */
  flag_InitIntern(flag_PBDC, flag_PRINTING, "PBDC", flag_PBDCOFF,
		  flag_PBDCMIN, flag_PBDCMAX);

  /* Printing of bound increase actions  */
  flag_InitIntern(flag_PBINC, flag_PRINTING, "PBInc", flag_PBINCOFF,
		  flag_PBINCMIN, flag_PBINCMAX);

  /* Application of definitions  output activated  */
  flag_InitIntern(flag_PAPPLYDEFS, flag_PRINTING, "PApplyDefs", flag_PAPPLYDEFSOFF,
		  flag_PAPPLYDEFSMIN, flag_PAPPLYDEFSMAX);

  /* Amount of time (seconds) available to SPASS, -1 means arbitrary */
  flag_InitIntern(flag_TIMELIMIT, flag_UNIQUE, "TimeLimit", flag_TIMELIMITUNLIMITED,
		  flag_TIMELIMITMIN, flag_TIMELIMITMAX);
  
  /* Select: 0 -> no selection, 1 -> select if multiple maximal literals, 2 -> always select */
  flag_InitIntern(flag_SELECT, flag_UNIQUE, "Select", flag_SELECTIFSEVERALMAXIMAL,
		  flag_SELECTMIN, flag_SELECTMAX);

  /* Activates the inference rule Empty Sort */
  flag_InitIntern(flag_IEMS, flag_INFERENCE, "IEmS", flag_EMPTYSORTOFF,
		  flag_EMPTYSORTMIN, flag_EMPTYSORTMAX);

  /* Activates the inference rule Sort Resolution */
  flag_InitIntern(flag_ISOR, flag_INFERENCE, "ISoR", flag_SORTRESOLUTIONOFF,
		  flag_SORTRESOLUTIONMIN, flag_SORTRESOLUTIONMAX);

  /* Activates the inference rule Equality Resolution */
  flag_InitIntern(flag_IEQR, flag_INFERENCE, "IEqR", flag_EQUALITYRESOLUTIONOFF,
		  flag_EQUALITYRESOLUTIONMIN, flag_EQUALITYRESOLUTIONMAX);

  /* Activates the inference rule Reflexivity Resolution */
  flag_InitIntern(flag_IERR, flag_INFERENCE, "IERR", flag_REFLEXIVITYRESOLUTIONOFF,
		  flag_REFLEXIVITYRESOLUTIONMIN, flag_REFLEXIVITYRESOLUTIONMAX);

  /* Activates the inference rule Equality Factoring */
  flag_InitIntern(flag_IEQF, flag_INFERENCE, "IEqF", flag_EQUALITYFACTORINGOFF,
		  flag_EQUALITYFACTORINGMIN, flag_EQUALITYFACTORINGMAX);

  /* Activates the inference rule Merging Paramodulation */
  flag_InitIntern(flag_IMPM, flag_INFERENCE, "IMPm", flag_MERGINGPARAMODULATIONOFF,
		  flag_MERGINGPARAMODULATIONMIN, flag_MERGINGPARAMODULATIONMAX);

  /* Activates the inference rule Superposition Right */
  flag_InitIntern(flag_ISPR, flag_INFERENCE, "ISpR", flag_SUPERPOSITIONRIGHTOFF,
		  flag_SUPERPOSITIONRIGHTMIN, flag_SUPERPOSITIONRIGHTMAX);
  
  /* Inference rule Ordered Paramodulation not active */  
  flag_InitIntern(flag_IOPM, flag_INFERENCE, "IOPm", flag_ORDEREDPARAMODULATIONOFF,
		  flag_ORDEREDPARAMODULATIONMIN, flag_ORDEREDPARAMODULATIONMAX);

  /*   Inference rule Paramodulation not active */  
  flag_InitIntern(flag_ISPM, flag_INFERENCE, "ISPm", flag_STANDARDPARAMODULATIONOFF,
		  flag_STANDARDPARAMODULATIONMIN, flag_STANDARDPARAMODULATIONMAX);   

  /* Activates the inference rule Superposition Left */
  flag_InitIntern(flag_ISPL, flag_INFERENCE, "ISpL", flag_SUPERPOSITIONLEFTOFF,
		  flag_SUPERPOSITIONLEFTMIN, flag_SUPERPOSITIONLEFTMAX);
  
  /* Activates the inference rule Ordered Resolution */
  flag_InitIntern(flag_IORE, flag_INFERENCE, "IORe", flag_ORDEREDRESOLUTIONOFF,
		  flag_ORDEREDRESOLUTIONMIN, flag_ORDEREDRESOLUTIONMAX);

  /* Activates the inference rule Standard Resolution */
  flag_InitIntern(flag_ISRE, flag_INFERENCE, "ISRe", flag_STANDARDRESOLUTIONOFF,
		  flag_STANDARDRESOLUTIONMIN, flag_STANDARDRESOLUTIONMAX);

  /* Activates the inference rule Standard Hyperresolution */
  flag_InitIntern(flag_ISHY, flag_INFERENCE, "ISHy", flag_STANDARDHYPERRESOLUTIONOFF,
		  flag_STANDARDHYPERRESOLUTIONMIN, flag_STANDARDHYPERRESOLUTIONMAX);
  
  /* Activates the inference rule Ordered Hyperresolution */
  flag_InitIntern(flag_IOHY, flag_INFERENCE, "IOHy", flag_ORDEREDHYPERRESOLUTIONOFF,
		  flag_ORDEREDHYPERRESOLUTIONMIN, flag_ORDEREDHYPERRESOLUTIONMAX);

  /* Activates the inference rule UR Resolution */
  flag_InitIntern(flag_IURR, flag_INFERENCE, "IURR", flag_UNITRESULTINGRESOLUTIONOFF,
		  flag_UNITRESULTINGRESOLUTIONMIN, flag_UNITRESULTINGRESOLUTIONMAX);

  /* Activates the inference rule Ordered Factoring */
  flag_InitIntern(flag_IOFC, flag_INFERENCE, "IOFc", flag_FACTORINGOFF,
		  flag_FACTORINGMIN, flag_FACTORINGMAX);

    /* Activates the inference rule Standard Factoring */
  flag_InitIntern(flag_ISFC, flag_INFERENCE, "ISFc", flag_STANDARDFACTORINGOFF,
		  flag_STANDARDFACTORINGMIN, flag_STANDARDFACTORINGMAX);

  /* Activates the inference rule Bounded Unit Resolution */
  flag_InitIntern(flag_IBUR, flag_INFERENCE, "IBUR", flag_BOUNDEDDEPTHUNITRESOLUTIONOFF,
		  flag_BOUNDEDDEPTHUNITRESOLUTIONMIN, flag_BOUNDEDDEPTHUNITRESOLUTIONMAX);

  /* Activates the inference rule Definition Application */
  flag_InitIntern(flag_IDEF, flag_INFERENCE, "IDEF", flag_DEFINITIONAPPLICATIONOFF,
		  flag_DEFINITIONAPPLICATIONMIN, flag_DEFINITIONAPPLICATIONMAX);

  /* Activates the inference rule  Unit Resolution */
  flag_InitIntern(flag_IUNR, flag_INFERENCE, "IUnR", flag_UNITRESOLUTIONOFF,
		  flag_UNITRESOLUTIONMIN, flag_UNITRESOLUTIONMAX);
  
  /* Activates Forward Rewriting */
  flag_InitIntern(flag_RFREW, flag_REDUCTION, "RFRew", flag_RFREWOFF,
		  flag_RFREWMIN, flag_RFREWMAX);

  /* Activates Backward Rewriting */
  flag_InitIntern(flag_RBREW, flag_REDUCTION, "RBRew", flag_RBREWOFF,
		  flag_RBREWMIN, flag_RBREWMAX);

  /* Activates Forward Contextual Rewriting */
  flag_InitIntern(flag_RFCRW, flag_REDUCTION, "RFCRw", flag_RFCRWOFF,
		  flag_RFCRWMIN, flag_RFCRWMAX);

  /* Activates Backward Contextual Rewriting */
  flag_InitIntern(flag_RBCRW, flag_REDUCTION, "RBCRw", flag_RBCRWOFF,
		  flag_RBCRWMIN, flag_RBCRWMAX);

  /* Activates Unit Conflict */
  flag_InitIntern(flag_RUNC, flag_REDUCTION, "RUnC", flag_RUNCOFF,
		  flag_RUNCMIN, flag_RUNCMAX);

  /* Activates Terminator */
  flag_InitIntern(flag_RTER, flag_REDUCTION, "RTer", flag_RTEROFF,
		  flag_RTERMIN, flag_RTERMAX);

  /* Activates Forward Subsumption */
  flag_InitIntern(flag_RFSUB, flag_REDUCTION, "RFSub", flag_RFSUBOFF,
		  flag_RFSUBMIN, flag_RFSUBMAX);

  /* Activates Backward Subsumption */
  flag_InitIntern(flag_RBSUB, flag_REDUCTION, "RBSub", flag_RBSUBOFF,
		  flag_RBSUBMIN, flag_RBSUBMAX);

  /* Activates Forward Matching Replacement Resolution */
  flag_InitIntern(flag_RFMRR, flag_REDUCTION, "RFMRR", flag_RFMRROFF,
		  flag_RFMRRMIN, flag_RFMRRMAX);

  /* Activates Backward Matching Replacement Resolution */
  flag_InitIntern(flag_RBMRR, flag_REDUCTION, "RBMRR", flag_RBMRROFF,
		  flag_RBMRRMIN, flag_RBMRRMAX);

  /* Activates the reduction rule Obvious Reduction */
  flag_InitIntern(flag_ROBV, flag_REDUCTION, "RObv", flag_ROBVOFF,
		  flag_ROBVMIN, flag_ROBVMAX);

  /* Activates the reduction rule Tautology */
  flag_InitIntern(flag_RTAUT, flag_REDUCTION, "RTaut", flag_RTAUTOFF,
		  flag_RTAUTMIN, flag_RTAUTMAX);

  /* Activates the reduction rule Sort Simplification */
  flag_InitIntern(flag_RSSI, flag_REDUCTION, "RSSi", flag_RSSIOFF,
		  flag_RSSIMIN, flag_RSSIMAX);

  /* Activates static soft typing */
  flag_InitIntern(flag_RSST, flag_REDUCTION, "RSST", flag_RSSTOFF,
		  flag_RSSTMIN, flag_RSSTMAX);

  /* Activates Assignment Equation Deletion */
  /* If set to 2 it also eliminates equations */
  /* that are redundant only in non-trivial domains */
  flag_InitIntern(flag_RAED, flag_REDUCTION, "RAED", flag_RAEDOFF,
		  flag_RAEDMIN, flag_RAEDMAX);

  /* Activates Condensing */
  flag_InitIntern(flag_RCON, flag_REDUCTION, "RCon", flag_RCONOFF,
		  flag_RCONMIN, flag_RCONMAX);

  /* Activates reduction of input clauses */
  flag_InitIntern(flag_RINPUT, flag_UNIQUE, "RInput", flag_RINPUTON,
		  flag_RINPUTMIN, flag_RINPUTMAX);

  /* Activates application of definitions */
  flag_InitIntern(flag_APPLYDEFS, flag_UNIQUE, "ApplyDefs", flag_APPLYDEFSOFF,
		  flag_APPLYDEFSMIN, flag_APPLYDEFSMAX);

  /* If true usable and worked off are completely interreduced; otherwise only worked off */
  flag_InitIntern(flag_FULLRED, flag_UNIQUE, "FullRed", flag_FULLREDON,
		  flag_FULLREDMIN, flag_FULLREDMAX);

  /* Activates unit saturation of input clauses */
  flag_InitIntern(flag_SATINPUT, flag_UNIQUE, "SatInput", flag_SATINPUTOFF,
		  flag_SATINPUTMIN, flag_SATINPUTMAX);

  /* Ratio between weight and depth selection of clauses from usable */
  flag_InitIntern(flag_WDRATIO, flag_UNIQUE, "WDRatio", 5,
		  flag_WDRATIOMIN, flag_WDRATIOMAX);

  /* Factor to divide the weight of conjecture clauses to prefer them for selection */
  flag_InitIntern(flag_PREFCON, flag_UNIQUE, "PrefCon", flag_PREFCONUNCHANGED, 
		  flag_PREFCONMIN, flag_PREFCONMAX);

  /* Weight of a function symbol; weight of clause is used to select given */
  flag_InitIntern(flag_FUNCWEIGHT, flag_UNIQUE, "FuncWeight", 1,
		  flag_FUNCWEIGHTMIN, flag_FUNCWEIGHTMAX);

  /* Weight of a variable symbol; weight of clause is used to select given */
  flag_InitIntern(flag_VARWEIGHT, flag_UNIQUE, "VarWeight", 1,
		  flag_VARWEIGHTMIN, flag_VARWEIGHTMAX);

  /* Prefer the selection of clauses with many variable occurrences */
  flag_InitIntern(flag_PREFVAR, flag_UNIQUE, "PrefVar", flag_PREFVAROFF,
		  flag_PREFVARMIN, flag_PREFVARMAX);

  /* The type of bound: 0 (no bound) 1 (by clause weight) 2 (by clause term depth) */
  flag_InitIntern(flag_BOUNDMODE, flag_UNIQUE, "BoundMode", flag_BOUNDMODEUNLIMITED,
		  flag_BOUNDMODEMIN, flag_BOUNDMODEMAX);

  /* The initial bound value, where -1 means no restriction */
  flag_InitIntern(flag_BOUNDSTART, flag_UNIQUE, "BoundStart", flag_BOUNDSTARTUNLIMITED,
		  flag_BOUNDSTARTMIN, flag_BOUNDSTARTMAX);

  /* The number of bound saturation loops */
  flag_InitIntern(flag_BOUNDLOOPS, flag_UNIQUE, "BoundLoops", 1,
		  flag_BOUNDLOOPSMIN, flag_BOUNDLOOPSMAX);

  /* Flags for selecting the ordering to use */
  flag_InitIntern(flag_ORD, flag_UNIQUE, "Ordering", flag_ORDKBO,
		  flag_ORDMIN, flag_ORDMAX);

  /* CNF flag, if set optimized skolemization is performed */
  flag_InitIntern(flag_CNFOPTSKOLEM, flag_UNIQUE, "CNFOptSkolem", flag_CNFOPTSKOLEMON,
		  flag_CNFOPTSKOLEMMIN, flag_CNFOPTSKOLEMMAX);

  /* CNF flag, restricts the number of optimized skolemization proof steps */
  flag_InitIntern(flag_CNFPROOFSTEPS, flag_UNIQUE, "CNFProofSteps", 100,
		  flag_CNFPROOFSTEPSMIN, flag_CNFPROOFSTEPSMAX);

  /* CNF flag, if set renaming is performed */
  flag_InitIntern(flag_CNFRENAMING, flag_UNIQUE, "CNFRenaming", flag_CNFRENAMINGON,
		  flag_CNFRENAMINGMIN, flag_CNFRENAMINGMAX);

  /* CNF flag, if set renaming is printed */
  flag_InitIntern(flag_CNFPRENAMING, flag_UNIQUE, "CNFPRenaming", flag_CNFPRENAMINGOFF,
		  flag_CNFPRENAMINGMIN, flag_CNFPRENAMINGMAX);

  /* CNF flag, if set strong skolemization is performed */
  flag_InitIntern(flag_CNFSTRSKOLEM, flag_UNIQUE, "CNFStrSkolem", flag_CNFSTRSKOLEMON,
		  flag_CNFSTRSKOLEMMIN, flag_CNFSTRSKOLEMMAX);

  /* CNF flag, if set reductions on equality literals are performed */
  flag_InitIntern(flag_CNFFEQREDUCTIONS, flag_UNIQUE, "CNFFEqR", flag_CNFFEQREDUCTIONSON,
		  flag_CNFFEQREDUCTIONSMIN, flag_CNFFEQREDUCTIONSMAX);

  /* dfg2otter flag, if set input options for otter are generated */
  flag_InitIntern(flag_TDFG2OTTEROPTIONS, flag_UNIQUE, "TDfg2OtterOptions", flag_TDFG2OTTEROPTIONSOFF,
		  flag_TDFG2OTTEROPTIONSMIN, flag_TDFG2OTTEROPTIONSMAX);
}


FLAGSTORE flag_DefaultStore(void)
/**************************************************************
  INPUT:   None.
  RETURNS: Default flag store.
***************************************************************/
{
  return flag_DEFAULTSTORE;
}


void flag_Print(FLAGSTORE Store)
/**************************************************************
  INPUT:   A FlagStore.
  RETURNS: Nothing.
  EFFECT:  Prints the values of all flags to stdout.
***************************************************************/
{
  flag_FPrint(stdout, Store);
}


void flag_FPrint(FILE* File, FLAGSTORE Store)
/**************************************************************
  INPUT:   A File to print to, and a FlagStore.
  RETURNS: Nothing.
  EFFECT:  Prints the values of all flags to File.
***************************************************************/
{
  FLAG_ID  i;
  char name[30];
  
  fputs("list_of_settings(SPASS).{*", File);

  for (i = (FLAG_ID) 0; i < flag_MAXFLAG; i+= (FLAG_ID) 3) {
    sprintf(name,"set_flag(%s,%d).", flag_Name(i), flag_GetFlagValue(Store, i));
    fprintf(File,"\n %-30s",name);
    if (i+1 < flag_MAXFLAG) {
      sprintf(name,"set_flag(%s,%d).", flag_Name(i+ (FLAG_ID) 1), flag_GetFlagValue(Store, i+ (FLAG_ID) 1));
      fprintf(File," %-30s",name);
      if (i+2 < flag_MAXFLAG) {
	sprintf(name," set_flag(%s,%d).", flag_Name(i+ (FLAG_ID) 2), flag_GetFlagValue(Store, i+ (FLAG_ID) 2));
	fprintf(File," %-30s",name);
      }
    }
  }
  fputs("*}\nend_of_list.\n", File);
}


BOOL flag_Lookup(const char* String)
/**************************************************************
  INPUT:   A string <String>.
  RETURNS: TRUE iff <String> is the string of a known flag.
***************************************************************/
{
  return (flag_Id(String) != -1);
}


FLAG_ID flag_Id(const char* String)
/**************************************************************
  INPUT:   A string <String>.
  RETURNS: The identification of the flag <String> if it exists
           -1 otherwise.
***************************************************************/
{
  FLAG_ID i;

  for (i = (FLAG_ID) 0; i < flag_MAXFLAG; i++)
    if (string_Equal(flag_Name(i), String))
      return i;

  return (FLAG_ID) -1;
}


const char* flag_Name(FLAG_ID Flag)
/**************************************************************
  INPUT:   A FlagId.
  RETURNS: The name of the flag <Flag>.
  EFFECT:  Looks up the name of the flag <Flag> and returns it,
           if it exists.
***************************************************************/
{
  flag_CheckFlagIdInRange(Flag);
 
  return(flag_PROPERTIES[Flag].name);
}


int flag_Minimum(FLAG_ID Flag)
/**************************************************************
  INPUT:   A FlagId.
  RETURNS: The first integer below the minimal legal value 
           of the flag.
***************************************************************/
{
  flag_CheckFlagIdInRange(Flag);
 
  return flag_PROPERTIES[Flag].minimum;
}


int flag_Maximum(FLAG_ID Flag)
/**************************************************************
  INPUT:   A FlagId.
  RETURNS: The first integer above the maximal legal value 
           of the flag.
***************************************************************/
{
  flag_CheckFlagIdInRange(Flag);
 
  return flag_PROPERTIES[Flag].maximum;
}


FLAG_TYPE flag_Type(FLAG_ID Flag)
/**************************************************************
  INPUT:   A FlagId.
  RETURNS: The flag type.
***************************************************************/
{
  flag_CheckFlagIdInRange(Flag);

  return flag_PROPERTIES[Flag].type;  
}


void flag_ClearInferenceRules(FLAGSTORE Store)
/**************************************************************
  INPUT:   A FlagStore.
  RETURNS: Nothing.
  EFFECT:  Turns all inference rules off.
***************************************************************/
{
  FLAG_ID i;

  for (i = (FLAG_ID) 0; i < flag_MAXFLAG; i++) {
    if (flag_IsInference(i))
      flag_SetFlagValue(Store, i, flag_OFF);
  }
}


void flag_ClearReductionRules(FLAGSTORE Store)
/**************************************************************
  INPUT:   A FlagStore.
  RETURNS: Nothing.
  EFFECT:  Turns all reduction rules off.
***************************************************************/
{
  FLAG_ID i;

  for (i = (FLAG_ID) 0; i < flag_MAXFLAG; i++) {
    if (flag_IsReduction(i)) {
        flag_SetFlagValue(Store, i, flag_OFF);
    }
  }
}


void flag_ClearPrinting(FLAGSTORE Store)
/**************************************************************
  INPUT:   A FlagStore.
  RETURNS: Nothing.
  EFFECT:  Turns all printing off.
***************************************************************/
{

  FLAG_ID i;

  for (i = (FLAG_ID) 0; i < flag_MAXFLAG; i++) {
    if (flag_IsPrinting(i))
      flag_SetFlagValue(Store, i, flag_OFF);
  }
}


void flag_SetReductionsToDefaults(FLAGSTORE Store)
/**************************************************************
  INPUT:   A FlagStore.
  RETURNS: Nothing.
  EFFECT:  Sets all reduction rules to defaults.
***************************************************************/
{

  FLAG_ID i;

  for (i = (FLAG_ID) 0; i < flag_MAXFLAG; i++) {
    if (flag_IsReduction(i))
      flag_SetFlagToDefault(Store, i);
  }
}


void flag_InitFlotterSubproofFlags(FLAGSTORE Source, FLAGSTORE Target)
/**************************************************************
  INPUT:   Two flag stores.
  RETURNS: Nothing.
  EFFECT:  Initializes the flag store <Target> to the values required by a
           Flotter subproof. The other flag store is needed to take over
           some flags, e.g. DOCPROOF.
***************************************************************/
{
  /* Deactivate printing */
  flag_ClearPrinting(Target);

  /* Deactivate inference rules */
  flag_ClearInferenceRules(Target);

  /* Set reductions to default values */
  flag_SetReductionsToDefaults(Target);

  flag_SetFlagToDefault(Target, flag_CNFFEQREDUCTIONS);
  flag_SetFlagToDefault(Target, flag_RINPUT);
 
  /* Copy flag_DOCPROOF and flag_CNFPROOFSTEPS */
  flag_TransferFlag(Source, Target, flag_DOCPROOF);  
  flag_TransferFlag(Source, Target, flag_CNFPROOFSTEPS);

  /* Activate BoundedDepthUnitResolution */
  flag_SetFlagValue(Target, flag_IBUR, flag_BOUNDEDDEPTHUNITRESOLUTIONON);

  /* Activate KBO */
  flag_SetFlagValue(Target, flag_ORD, flag_ORDKBO);

  /* Transfer Weights for Terms */
  flag_TransferFlag(Source, Target, flag_FUNCWEIGHT);  
  flag_TransferFlag(Source, Target, flag_VARWEIGHT);

  /* Transfer Selection Strategy, not needed for depth bounded */
  /* unit resolution (see above) but for other potentially useful inference rules */
  flag_TransferFlag(Source, Target, flag_SELECT);  
}


void flag_InitFlotterFlags(FLAGSTORE Source, FLAGSTORE Target)
/**************************************************************
  INPUT:   Two flag stores.
  RETURNS: Nothing.
  EFFECT:  Initalizes the flag store <Target> to the values required by
           Flotter. The other flag store is needed to set
           some flags, e.g. DOCPROOF.
***************************************************************/
{
  flag_InitFlotterSubproofFlags(Source, Target);

  /* Set ordering to default value */
  flag_SetFlagToDefault(Target, flag_ORD);

  /* Set weighting flags to default values */
  flag_SetFlagToDefault(Target, flag_FUNCWEIGHT);
  flag_SetFlagToDefault(Target, flag_VARWEIGHT);

  /* Copy given values to diverse flags */
  flag_TransferFlag(Source, Target, flag_CNFRENAMING);
  flag_TransferFlag(Source, Target, flag_CNFOPTSKOLEM);
  flag_TransferFlag(Source, Target, flag_CNFSTRSKOLEM);
  flag_TransferFlag(Source, Target, flag_PAPPLYDEFS);
  flag_TransferFlag(Source, Target, flag_PBDC);
  flag_TransferFlag(Source, Target, flag_PBINC);
  flag_TransferFlag(Source, Target, flag_CNFPRENAMING);
  flag_TransferFlag(Source, Target, flag_POPTSKOLEM);
  flag_TransferFlag(Source, Target, flag_PSTRSKOLEM);
  flag_TransferFlag(Source, Target, flag_INTERACTIVE);
}


void flag_CheckStore(FLAGSTORE Store) 
/**************************************************************
  INPUT:   A flag store.
  RETURNS: TRUE is the flag store is in a valid state,
           FALSE otherwise.
***************************************************************/
{
  FLAG_ID i;
  FLAG value;

  /* check all flags */
  for (i = (FLAG_ID) 0; i < flag_MAXFLAG; i ++) {
    /* Get flag value first. We can't use flag_GetFlagValue() since it
       prints an error message and exits, if a flag is clean. A flag can
       be clean, only reading it is an error (for most functions).
    */

    value = Store[i];
    if (value != flag_CLEAN) {
      flag_CheckFlagValueInRange(i,value);
    }
  }
}