/**************************************************************/ /* ********************************************************** */ /* * * */ /* * 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$ * */ /* $State$ * */ /* $Date$ * */ /* $Author$ * */ /* * * */ /* * Contact: * */ /* * Christoph Weidenbach * */ /* * MPI fuer Informatik * */ /* * Stuhlsatzenhausweg 85 * */ /* * 66123 Saarbruecken * */ /* * Email: weidenb@mpi-sb.mpg.de * */ /* * Germany * */ /* * * */ /* ********************************************************** */ /**************************************************************/ /* $RCSfile$ */ #ifndef _FLAGS_ #define _FLAGS_ #include #include #include "memory.h" #include "misc.h" /**************************************************************/ /* Data Structures and Constants */ /**************************************************************/ extern const int flag_CLEAN; /* Define the legal values for all flags as data types. All flags have a minimum and a maximum. Legal values are within that range, *excluding* the minimum, maximum value. By using flag_XXXMIN and flag_XXXMAX we have a simple test for a flag's correctness: if flag value <= flag minimum or flag value >= flag maximum then the flag has an illegal state. Boolean flags have two legal values: * flag_XXXOFF ( = 0) * flag_XXXON ( = 1) */ /* State definitions for boolean flags */ typedef enum { flag_OFF = 0, flag_ON = 1 } FLAG_BOOLEAN; /* State definitions for flag_APPLYDEFS */ typedef enum { flag_APPLYDEFSMIN = -1, flag_APPLYDEFSOFF = flag_OFF, flag_APPLYDEFSMAX = INT_MAX } FLAG_APPLYDEFSTYPE; /* State definitions for flag_AUTO */ typedef enum { flag_AUTOMIN = -1, flag_AUTOOFF = flag_OFF, flag_AUTOON = flag_ON, flag_AUTOMAX } FLAG_AUTOTYPE; /* State definitions for flag_BOUNDLOOPS */ typedef enum { flag_BOUNDLOOPSMIN = 0, flag_BOUNDLOOPSMAX = INT_MAX } FLAG_BOUNDLOOPSTYPE; /* State definitions for flag_BOUNDMODE */ typedef enum { flag_BOUNDMODEMIN = -1, flag_BOUNDMODEUNLIMITED, flag_BOUNDMODERESTRICTEDBYWEIGHT, flag_BOUNDMODERESTRICTEDBYDEPTH, flag_BOUNDMODEMAX } FLAG_BOUNDMODETYPE; /* State definitions for flag_BOUNDSTART */ typedef enum { flag_BOUNDSTARTMIN = -2, flag_BOUNDSTARTUNLIMITED, flag_BOUNDSTARTMAX = INT_MAX } FLAG_BOUNDSTARTTYPE; /* State definitions for flag_CNFFEQREDUCTIONS */ typedef enum { flag_CNFFEQREDUCTIONSMIN = -1, flag_CNFFEQREDUCTIONSOFF = flag_OFF, flag_CNFFEQREDUCTIONSON = flag_ON, flag_CNFFEQREDUCTIONSMAX } FLAG_CNFFEQREDUCTIONSTYPE; /* State definitions for flag_CNFOPTSKOLEM */ typedef enum { flag_CNFOPTSKOLEMMIN = -1, flag_CNFOPTSKOLEMOFF = flag_OFF, flag_CNFOPTSKOLEMON = flag_ON, flag_CNFOPTSKOLEMMAX } flag_CNFOPTSKOLEMTYPE; /* State definitions for flag_CNFPRENAMING */ typedef enum { flag_CNFPRENAMINGMIN = -1, flag_CNFPRENAMINGOFF = flag_OFF, flag_CNFPRENAMINGON = flag_ON, flag_CNFPRENAMINGMAX } FLAG_CNFPRENAMINGTYPE; /* State definitions for flag_CNFPROOFSTEPS */ typedef enum { flag_CNFPROOFSTEPSMIN = 0, flag_CNFPROOFSTEPSMAX = INT_MAX } FLAG_CNFPROOFSTEPSTYPE; /* State definitions for flag_CNFRENAMING */ typedef enum { flag_CNFRENAMINGMIN = -1, flag_CNFRENAMINGOFF = flag_OFF, flag_CNFRENAMINGON = flag_ON, flag_CNFRENAMINGMAX } FLAG_CNFRENAMINGTYPE; /* State definitions for flag_CNFSTRSKOLEM */ typedef enum { flag_CNFSTRSKOLEMMIN = -1, flag_CNFSTRSKOLEMOFF = flag_OFF, flag_CNFSTRSKOLEMON = flag_ON, flag_CNFSTRSKOLEMMAX } FLAG_CNFSTRSKOLEMTYPE; /* State definitions for flag_DOCPROOF */ typedef enum { flag_DOCPROOFMIN = -1, flag_DOCPROOFOFF = flag_OFF, flag_DOCPROOFON = flag_ON, flag_DOCPROOFMAX } FLAG_DOCPROOFTYPE; /* State definitions for flag_DOCSPLIT */ typedef enum { flag_DOCSPLITMIN = -1, flag_DOCSPLITOFF = flag_OFF, flag_DOCSPLITON = flag_ON, flag_DOCSPLITMAX } FLAG_DOCSPLITTYPE; /* State definitions for flag_DOCSST */ typedef enum { flag_DOCSSTMIN = -1, flag_DOCSSTOFF = flag_OFF, flag_DOCSSTON = flag_ON, flag_DOCSSTMAX } FLAG_DOCSSTTYPE; /* State definitions for flag_FLOTTER */ typedef enum { flag_FLOTTERMIN = -1, flag_FLOTTEROFF = flag_OFF, flag_FLOTTERON = flag_ON, flag_FLOTTERMAX } FLAG_FLOTTERTYPE; /* State definitions for flag_FPDFGPROOF */ typedef enum { flag_FPDFGPROOFMIN = -1, flag_FPDFGPROOFOFF = flag_OFF, flag_FPDFGPROOFON = flag_ON, flag_FPDFGPROOFMAX } FLAG_FPDFGPROOFTYPE; /* State definitions for flag_FPMODEL */ typedef enum { flag_FPMODELMIN = -1, flag_FPMODELOFF = flag_OFF, flag_FPMODELALLCLAUSES, flag_FPMODELPOTENTIALLYPRODUCTIVECLAUSES, flag_FPMODELMAX } FLAG_FPMODELTYPE; /* State definitions for flag_FULLRED */ typedef enum { flag_FULLREDMIN = -1, flag_FULLREDOFF = flag_OFF, flag_FULLREDON = flag_ON, flag_FULLREDMAX } FLAG_FULLREDTYPE; /* State definitions for flag_FUNCWEIGHT */ typedef enum { flag_FUNCWEIGHTMIN = 0, flag_FUNCWEIGHTMAX = INT_MAX } FLAG_FUNCWEIGHTTYPE; /* State definitions for flag_IBUR */ typedef enum { flag_BOUNDEDDEPTHUNITRESOLUTIONMIN = -1, flag_BOUNDEDDEPTHUNITRESOLUTIONOFF = flag_OFF, flag_BOUNDEDDEPTHUNITRESOLUTIONON = flag_ON, flag_BOUNDEDDEPTHUNITRESOLUTIONMAX } FLAG_IBURTYPE; /* State definitions for flag_IDEF */ typedef enum { flag_DEFINITIONAPPLICATIONMIN = -1, flag_DEFINITIONAPPLICATIONOFF = flag_OFF, flag_DEFINITIONAPPLICATIONON = flag_ON, flag_DEFINITIONAPPLICATIONMAX } FLAG_IDEFTYPE; /* State definitions for flag_IEMS */ typedef enum { flag_EMPTYSORTMIN = -1, flag_EMPTYSORTOFF = flag_OFF, flag_EMPTYSORTON = flag_ON, flag_EMPTYSORTMAX } FLAG_IEMSTYPE; /* State definitions for flag_IEQF */ typedef enum { flag_EQUALITYFACTORINGMIN = -1, flag_EQUALITYFACTORINGOFF = flag_OFF, flag_EQUALITYFACTORINGON = flag_ON, flag_EQUALITYFACTORINGMAX } FLAG_IEQFTYPE; /* State definitions for flag_IEQR */ typedef enum { flag_EQUALITYRESOLUTIONMIN = -1, flag_EQUALITYRESOLUTIONOFF = flag_OFF, flag_EQUALITYRESOLUTIONON = flag_ON, flag_EQUALITYRESOLUTIONMAX } FLAG_IEQRTYPE; /* State definitions for flag_IERR */ typedef enum { flag_REFLEXIVITYRESOLUTIONMIN = -1, flag_REFLEXIVITYRESOLUTIONOFF = flag_OFF, flag_REFLEXIVITYRESOLUTIONON = flag_ON, flag_REFLEXIVITYRESOLUTIONMAX } FLAG_IERRTYPE; /* State definitions for flag_IMPM */ typedef enum { flag_MERGINGPARAMODULATIONMIN = -1, flag_MERGINGPARAMODULATIONOFF = flag_OFF, flag_MERGINGPARAMODULATIONON = flag_ON, flag_MERGINGPARAMODULATIONMAX } FLAG_IMPMTYPE; /* State definitions for flag_INTERACTIVE */ typedef enum { flag_INTERACTIVEMIN = -1, flag_INTERACTIVEOFF = flag_OFF, flag_INTERACTIVEON = flag_ON, flag_INTERACTIVEMAX } FLAG_INTERACTIVETYPE; /* State definitions for flag_IOFC */ typedef enum { flag_FACTORINGMIN = -1, flag_FACTORINGOFF = flag_OFF, flag_FACTORINGONLYRIGHT, flag_FACTORINGRIGHTANDLEFT, flag_FACTORINGMAX } FLAG_IOFCTYPE; /* State definitions for flag_IOHY */ typedef enum { flag_ORDEREDHYPERRESOLUTIONMIN = -1, flag_ORDEREDHYPERRESOLUTIONOFF = flag_OFF, flag_ORDEREDHYPERRESOLUTIONON = flag_ON, flag_ORDEREDHYPERRESOLUTIONMAX } FLAG_IOHYTYPE; /* State definitions for flag_IOPM */ typedef enum { flag_ORDEREDPARAMODULATIONMIN = -1, flag_ORDEREDPARAMODULATIONOFF = flag_OFF, flag_ORDEREDPARAMODULATIONON = flag_ON, flag_ORDEREDPARAMODULATIONMAX } FLAG_IOPMTYPE; /* State definitions for flag_IORE */ typedef enum { flag_ORDEREDRESOLUTIONMIN = -1, flag_ORDEREDRESOLUTIONOFF = flag_OFF, flag_ORDEREDRESOLUTIONNOEQUATIONS, flag_ORDEREDRESOLUTIONWITHEQUATIONS, flag_ORDEREDRESOLUTIONMAX } FLAG_IORETYPE; /* State definitions for flag_ISFC */ typedef enum { flag_STANDARDFACTORINGMIN = -1, flag_STANDARDFACTORINGOFF = flag_OFF, flag_STANDARDFACTORINGON = flag_ON, flag_STANDARDFACTORINGMAX } FLAG_ISFCTYPE; /* State definitions for flag_ISHY */ typedef enum { flag_STANDARDHYPERRESOLUTIONMIN = -1, flag_STANDARDHYPERRESOLUTIONOFF = flag_OFF, flag_STANDARDHYPERRESOLUTIONON = flag_ON, flag_STANDARDHYPERRESOLUTIONMAX } FLAG_ISHYTYPE; /* State definitions for flag_ISOR */ typedef enum { flag_SORTRESOLUTIONMIN = -1, flag_SORTRESOLUTIONOFF = flag_OFF, flag_SORTRESOLUTIONON = flag_ON, flag_SORTRESOLUTIONMAX } FLAG_ISORTYPE; /* State definitions for flag_ISPL */ typedef enum { flag_SUPERPOSITIONLEFTMIN = -1, flag_SUPERPOSITIONLEFTOFF = flag_OFF, flag_SUPERPOSITIONLEFTON = flag_ON, flag_SUPERPOSITIONLEFTMAX } FLAG_ISPLTYPE; /* State definitions for flag_ISPM */ typedef enum { flag_STANDARDPARAMODULATIONMIN = -1, flag_STANDARDPARAMODULATIONOFF = flag_OFF, flag_STANDARDPARAMODULATIONON = flag_ON, flag_STANDARDPARAMODULATIONMAX } FLAG_ISPMTYPE; /* State definitions for flag_ISPR */ typedef enum { flag_SUPERPOSITIONRIGHTMIN = -1, flag_SUPERPOSITIONRIGHTOFF = flag_OFF, flag_SUPERPOSITIONRIGHTON = flag_ON, flag_SUPERPOSITIONRIGHTMAX } FLAG_ISPRTYPE; /* State definitions for flag_ISRE */ typedef enum { flag_STANDARDRESOLUTIONMIN = -1, flag_STANDARDRESOLUTIONOFF = flag_OFF, flag_STANDARDRESOLUTIONNOEQUATIONS, flag_STANDARDRESOLUTIONWITHEQUATIONS, flag_STANDARDRESOLUTIONMAX } FLAG_ISRETYPE; /* State definitions for flag_IUNR */ typedef enum { flag_UNITRESOLUTIONMIN = -1, flag_UNITRESOLUTIONOFF = flag_OFF, flag_UNITRESOLUTIONON = flag_ON, flag_UNITRESOLUTIONMAX } FLAG_IUNRTYPE; /* State definitions for flag_IURR */ typedef enum { flag_UNITRESULTINGRESOLUTIONMIN = -1, flag_UNITRESULTINGRESOLUTIONOFF = flag_OFF, flag_UNITRESULTINGRESOLUTIONON = flag_ON, flag_UNITRESULTINGRESOLUTIONMAX } FLAG_IURRTYPE; /* State definitions for flag_LOOPS */ typedef enum { flag_LOOPSMIN = -2, flag_LOOPSUNLIMITED, flag_LOOPSMAX = INT_MAX } FLAG_LOOPSTYPE; /* State definitions for flag_MEMORY */ typedef enum { flag_MEMORYMIN = -2, flag_MEMORYUNLIMITED, flag_MEMORYMAX = INT_MAX } FLAG_MEMORYTYPE; /* State definitions for flag_ORD */ typedef enum { flag_ORDMIN = -1, flag_ORDKBO, flag_ORDRPOS, flag_ORDMAX } FLAG_ORDTYPE; /* State definitions for flag_PAPPLYDEFS */ typedef enum { flag_PAPPLYDEFSMIN = -1, flag_PAPPLYDEFSOFF = flag_OFF, flag_PAPPLYDEFSON = flag_ON, flag_PAPPLYDEFSMAX } FLAG_PAPPLYDEFSTYPE; /* State definitions for flag_PBDC */ typedef enum { flag_PBDCMIN = -1, flag_PBDCOFF = flag_OFF, flag_PBDCON = flag_ON, flag_PBDCMAX } FLAG_PBDCTYPE; /* State definitions for flag_PBINC */ typedef enum { flag_PBINCMIN = -1, flag_PBINCOFF = flag_OFF, flag_PBINCON = flag_ON, flag_PBINCMAX } FLAG_PBINCTYPE; /* State definitions for flag_PMRR */ typedef enum { flag_PMRRMIN = -1, flag_PMRROFF = flag_OFF, flag_PMRRON = flag_ON, flag_PMRRMAX } FLAG_PMRRTYPE; /* State definitions for flag_PCON */ typedef enum { flag_PCONMIN = -1, flag_PCONOFF = flag_OFF, flag_PCONON = flag_ON, flag_PCONMAX } FLAG_PCONTYPE; /* State definitions for flag_PDER */ typedef enum { flag_PDERMIN = -1, flag_PDEROFF = flag_OFF, flag_PDERON = flag_ON, flag_PDERMAX } FLAG_PDERTYPE; /* State definitions for flag_PEMPTYCLAUSE */ typedef enum { flag_PEMPTYCLAUSEMIN = -1, flag_PEMPTYCLAUSEOFF = flag_OFF, flag_PEMPTYCLAUSEON = flag_ON, flag_PEMPTYCLAUSEMAX } FLAG_PEMPTYCLAUSETYPE; /* State definitions for flag_PFLAGS */ typedef enum { flag_PFLAGSMIN = -1, flag_PFLAGSOFF = flag_OFF, flag_PFLAGSON = flag_ON, flag_PFLAGSMAX } FLAG_PFLAGSTYPE; /* State definitions for flag_PGIVEN */ typedef enum { flag_PGIVENMIN = -1, flag_PGIVENOFF = flag_OFF, flag_PGIVENON = flag_ON, flag_PGIVENMAX } FLAG_PGIVENTYPE; /* State definitions for flag_PKEPT */ typedef enum { flag_PKEPTMIN = -1, flag_PKEPTOFF = flag_OFF, flag_PKEPTON = flag_ON, flag_PKEPTMAX } FLAG_PKEPTTYPE; /* State definitions for flag_PLABELS */ typedef enum { flag_PLABELSMIN = -1, flag_PLABELSOFF = flag_OFF, flag_PLABELSON = flag_ON, flag_PLABELSMAX } FLAG_PLABELSTYPE; /* State definitions for flag_POBV */ typedef enum { flag_POBVMIN = -1, flag_POBVOFF = flag_OFF, flag_POBVON = flag_ON, flag_POBVMAX } FLAG_POBVTYPE; /* State definitions for flag_POPTSKOLEM */ typedef enum { flag_POPTSKOLEMMIN = -1, flag_POPTSKOLEMOFF = flag_OFF, flag_POPTSKOLEMON = flag_ON, flag_POPTSKOLEMMAX } FLAG_POPTSKOLEMTYPE; /* State definitions for flag_PPROBLEM */ typedef enum { flag_PPROBLEMMIN = -1, flag_PPROBLEMOFF = flag_OFF, flag_PPROBLEMON = flag_ON, flag_PPROBLEMMAX } FLAG_PPROBLEMTYPE; /* State definitions for flag_PREFCON */ typedef enum { flag_PREFCONMIN = 0, flag_PREFCONUNCHANGED, flag_PREFCONMAX = INT_MAX } FLAG_PREFCONTYPE; /* State definitions for flag_PREFVAR */ typedef enum { flag_PREFVARMIN = -1, flag_PREFVAROFF = flag_OFF, flag_PREFVARON = flag_ON, flag_PREFVARMAX } FLAG_PREFVARTYPE; /* State definitions for flag_PREW */ typedef enum { flag_PREWMIN = -1, flag_PREWOFF = flag_OFF, flag_PREWON = flag_ON, flag_PREWMAX } FLAG_PREWTYPE; /* State definitions for flag_PCRW */ typedef enum { flag_PCRWMIN = -1, flag_PCRWOFF = flag_OFF, flag_PCRWON = flag_ON, flag_PCRWMAX } FLAG_PCRWTYPE; /* State definitions for flag_PAED */ typedef enum { flag_PAEDMIN = -1, flag_PAEDOFF = flag_OFF, flag_PAEDON = flag_ON, flag_PAEDMAX } FLAG_PAEDTYPE; /* State definitions for flag_PSSI */ typedef enum { flag_PSSIMIN = -1, flag_PSSIOFF = flag_OFF, flag_PSSION = flag_ON, flag_PSSIMAX } FLAG_PSSITYPE; /* State definitions for flag_PSST */ typedef enum { flag_PSSTMIN = -1, flag_PSSTOFF = flag_OFF, flag_PSSTON = flag_ON, flag_PSSTMAX } FLAG_PSSTTYPE; /* State definitions for flag_PSTATISTIC */ typedef enum { flag_PSTATISTICMIN = -1, flag_PSTATISTICOFF = flag_OFF, flag_PSTATISTICON = flag_ON, flag_PSTATISTICMAX } FLAG_PSTATISTICTYPE; /* State definitions for flag_PSTRSKOLEM */ typedef enum { flag_PSTRSKOLEMMIN = -1, flag_PSTRSKOLEMOFF = flag_OFF, flag_PSTRSKOLEMON = flag_ON, flag_PSTRSKOLEMMAX } FLAG_PSTRSKOLEMTYPE; /* State definitions for flag_PSUB */ typedef enum { flag_PSUBMIN = -1, flag_PSUBOFF = flag_OFF, flag_PSUBON = flag_ON, flag_PSUBMAX } FLAG_PSUBTYPE; /* State definitions for flag_PTAUT */ typedef enum { flag_PTAUTMIN = -1, flag_PTAUTOFF = flag_OFF, flag_PTAUTON = flag_ON, flag_PTAUTMAX } FLAG_PTAUTTYPE; /* State definitions for flag_PUNC */ typedef enum { flag_PUNCMIN = -1, flag_PUNCOFF = flag_OFF, flag_PUNCON = flag_ON, flag_PUNCMAX } FLAG_PUNCTYPE; /* State definitions for flag_RBMRR */ typedef enum { flag_RBMRRMIN = -1, flag_RBMRROFF = flag_OFF, flag_RBMRRON = flag_ON, flag_RBMRRMAX } FLAG_RBMRRTYPE; /* State definitions for flag_RBREW */ typedef enum { flag_RBREWMIN = -1, flag_RBREWOFF = flag_OFF, flag_RBREWON = flag_ON, flag_RBREWMAX } FLAG_RBREWTYPE; /* State definitions for flag_RBCRW */ typedef enum { flag_RBCRWMIN = -1, flag_RBCRWOFF = flag_OFF, flag_RBCRWON = flag_ON, flag_RBCRWMAX } FLAG_RBCRWTYPE; /* State definitions for flag_RBSUB */ typedef enum { flag_RBSUBMIN = -1, flag_RBSUBOFF = flag_OFF, flag_RBSUBON = flag_ON, flag_RBSUBMAX } FLAG_RBSUBTYPE; /* State definitions for flag_RCON */ typedef enum { flag_RCONMIN = -1, flag_RCONOFF = flag_OFF, flag_RCONON = flag_ON, flag_RCONMAX } FLAG_RCONTYPE; /* State definitions for flag_RFMRR */ typedef enum { flag_RFMRRMIN = -1, flag_RFMRROFF = flag_OFF, flag_RFMRRON = flag_ON, flag_RFMRRMAX } FLAG_RFMRRTYPE; /* State definitions for flag_RFREW */ typedef enum { flag_RFREWMIN = -1, flag_RFREWOFF = flag_OFF, flag_RFREWON = flag_ON, flag_RFREWMAX } FLAG_RFREWTYPE; /* State definitions for flag_RFCRW */ typedef enum { flag_RFCRWMIN = -1, flag_RFCRWOFF = flag_OFF, flag_RFCRWON = flag_ON, flag_RFCRWMAX } FLAG_RFCRWTYPE; /* State definitions for flag_RFSUB */ typedef enum { flag_RFSUBMIN = -1, flag_RFSUBOFF = flag_OFF, flag_RFSUBON = flag_ON, flag_RFSUBMAX } FLAG_RFSUBTYPE; /* State definitions for flag_RINPUT */ typedef enum { flag_RINPUTMIN = -1, flag_RINPUTOFF = flag_OFF, flag_RINPUTON = flag_ON, flag_RINPUTMAX } FLAG_RINPUTTYPE; /* State definitions for flag_ROBV */ typedef enum { flag_ROBVMIN = -1, flag_ROBVOFF = flag_OFF, flag_ROBVON = flag_ON, flag_ROBVMAX } FLAG_ROBVTYPE; /* State definitions for flag_RAED */ typedef enum { flag_RAEDMIN = -1, flag_RAEDOFF = flag_OFF, flag_RAEDSOUND, flag_RAEDPOTUNSOUND, flag_RAEDMAX } FLAG_RAEDTYPE; /* State definitions for flag_RSSI */ typedef enum { flag_RSSIMIN = -1, flag_RSSIOFF = flag_OFF, flag_RSSION = flag_ON, flag_RSSIMAX } FLAG_RSSITYPE; /* State definitions for flag_RSST */ typedef enum { flag_RSSTMIN = -1, flag_RSSTOFF = flag_OFF, flag_RSSTON = flag_ON, flag_RSSTMAX } FLAG_RSSTTYPE; /* State definitions for flag_RTAUT */ typedef enum { flag_RTAUTMIN = -1, flag_RTAUTOFF = flag_OFF, flag_RTAUTSYNTACTIC, flag_RTAUTSEMANTIC, flag_RTAUTMAX } FLAG_RTAUTTYPE; /* State definitions for flag_RTER */ typedef enum { flag_RTERMIN = -1, flag_RTEROFF = flag_OFF, flag_RTERMAX = INT_MAX } FLAG_RTERTYPE; /* State definitions for flag_RUNC */ typedef enum { flag_RUNCMIN = -1, flag_RUNCOFF = flag_OFF, flag_RUNCON = flag_ON, flag_RUNCMAX } FLAG_RUNCTYPE; /* State definitions for flag_SATINPUT */ typedef enum { flag_SATINPUTMIN = -1, flag_SATINPUTOFF = flag_OFF, flag_SATINPUTON = flag_ON, flag_SATINPUTMAX } FLAG_SATINPUTTYPE; /* State definitions for flag_SELECT */ typedef enum { flag_SELECTMIN = -1, flag_SELECTOFF = flag_OFF, flag_SELECTIFSEVERALMAXIMAL, flag_SELECTALWAYS, flag_SELECTMAX } FLAG_SELECTTYPE; /* State definitions for flag_SORTS */ typedef enum { flag_SORTSMIN = -1, flag_SORTSOFF = flag_OFF, flag_SORTSMONADICWITHVARIABLE, flag_SORTSMONADICALL, flag_SORTSMAX } FLAG_SORTSTYPE; /* State definitions for flag_SOS */ typedef enum { flag_SOSMIN = -1, flag_SOSOFF = flag_OFF, flag_SOSON = flag_ON, flag_SOSMAX } FLAG_SOSTYPE; /* State definitions for flag_SPLITS */ typedef enum { flag_SPLITSMIN = -2, flag_SPLITSUNLIMITED, flag_SPLITSOFF = flag_OFF, flag_SPLITSMAX = INT_MAX } FLAG_SPLITSTYPE; /* State definitions for flag_STDIN */ typedef enum { flag_STDINMIN = -1, flag_STDINOFF = flag_OFF, flag_STDINON = flag_ON, flag_STDINMAX } FLAG_STDINTYPE; /* State definitions for flag_TDFG2OTTEROPTIONS */ typedef enum { flag_TDFG2OTTEROPTIONSMIN = -1, flag_TDFG2OTTEROPTIONSOFF = flag_OFF, flag_TDFG2OTTEROPTIONSPROOFCHECK, flag_TDFG2OTTEROPTIONSAUTO, flag_TDFG2OTTEROPTIONSAUTO2, flag_TDFG2OTTEROPTIONSMAX } FLAG_TDFG2OTTEROPTIONSTYPE; /* State definitions for flag_TIMELIMIT */ typedef enum { flag_TIMELIMITMIN = -2, flag_TIMELIMITUNLIMITED, flag_TIMELIMITMAX = INT_MAX } FLAG_TIMELIMITTYPE; /* State definitions for flag_VARWEIGHT */ typedef enum { flag_VARWEIGHTMIN = 0, flag_VARWEIGHTMAX = INT_MAX } FLAG_VARWEIGHTTYPE; /* State definitions for flag_WDRATIO */ typedef enum { flag_WDRATIOMIN = 0, flag_WDRATIOMAX = INT_MAX } FLAG_WDRATIOTYPE; /* Define all flags */ typedef enum { flag_AUTO, flag_STDIN, flag_INTERACTIVE, flag_FLOTTER, flag_SOS, flag_SPLITS, flag_MEMORY, flag_TIMELIMIT, flag_DOCSST, flag_DOCPROOF, flag_DOCSPLIT, flag_LOOPS, flag_PSUB, flag_PREW, flag_PCRW, flag_PCON, flag_PTAUT, flag_POBV, flag_PSSI, flag_PSST, flag_PMRR, flag_PUNC, flag_PAED, flag_PDER, flag_PGIVEN, flag_PLABELS, flag_PKEPT, flag_PPROBLEM, flag_PEMPTYCLAUSE, flag_PSTATISTIC, flag_FPMODEL, flag_FPDFGPROOF, flag_PFLAGS, flag_POPTSKOLEM, flag_PSTRSKOLEM, flag_PBDC, flag_PBINC, flag_PAPPLYDEFS, flag_SELECT, flag_RINPUT, flag_SORTS, flag_SATINPUT, flag_WDRATIO, flag_PREFCON, flag_FULLRED, flag_FUNCWEIGHT, flag_VARWEIGHT, flag_PREFVAR, flag_BOUNDMODE, flag_BOUNDSTART, flag_BOUNDLOOPS, flag_APPLYDEFS, flag_ORD, flag_CNFOPTSKOLEM, flag_CNFSTRSKOLEM, flag_CNFPROOFSTEPS, flag_CNFRENAMING, flag_CNFPRENAMING, flag_CNFFEQREDUCTIONS, flag_IEMS, flag_ISOR, flag_IEQR, flag_IERR, flag_IEQF, flag_IMPM, flag_ISPR, flag_IOPM, flag_ISPM, flag_ISPL, flag_IORE, flag_ISRE, flag_ISHY, flag_IOHY, flag_IURR, flag_IOFC, flag_ISFC, flag_IUNR, flag_IBUR, flag_IDEF, flag_RFREW, flag_RBREW, flag_RFCRW, flag_RBCRW, flag_RFMRR, flag_RBMRR, flag_ROBV, flag_RUNC, flag_RTER, flag_RTAUT, flag_RSST, flag_RSSI, flag_RFSUB, flag_RBSUB, flag_RAED, flag_RCON, flag_TDFG2OTTEROPTIONS, flag_MAXFLAG } FLAG_ID; /* flag_MAXFLAG is a final Dummy */ /* Define different flag types */ typedef enum { flag_INFERENCE, flag_PRINTING, flag_REDUCTION, flag_UNIQUE, /* miscellaneous flags */ flag_MAXTYPE } FLAG_TYPE; /* Define the flag data type */ typedef int FLAG; /* Define the internal representation of a flag store */ typedef FLAG FLAGARRAY[flag_MAXFLAG]; /* Define the flag store */ typedef FLAG *FLAGSTORE; /**************************************************************/ /* Functions */ /**************************************************************/ void flag_Init(void); void flag_InitFlotterFlags(FLAGSTORE, FLAGSTORE); void flag_InitFlotterSubproofFlags(FLAGSTORE, FLAGSTORE); FLAGSTORE flag_DefaultStore(void); void flag_Print(FLAGSTORE); void flag_FPrint(FILE*, FLAGSTORE); BOOL flag_Lookup(const char*); FLAG_ID flag_Id(const char*); const char* flag_Name(FLAG_ID); int flag_Minimum(FLAG_ID); int flag_Maximum(FLAG_ID); FLAG_TYPE flag_Type(FLAG_ID Flag); void flag_ClearInferenceRules(FLAGSTORE Store); void flag_ClearReductionRules(FLAGSTORE Store); void flag_ClearPrinting(FLAGSTORE Store); void flag_SetReductionsToDefaults(FLAGSTORE Store); void flag_CheckStore(FLAGSTORE Store); /**************************************************************/ /* Macros */ /**************************************************************/ static __inline__ void flag_CheckFlagIdInRange(FLAG_ID FlagId) /* prints an error report if a FLAG_ID is not valid */ { #ifdef CHECK if (FlagId >= flag_MAXFLAG) { misc_StartErrorReport(); misc_ErrorReport("\n In flag_CheckFlagIdInRange: Range of flags exceeded."); misc_FinishErrorReport(); } #endif } static __inline__ void flag_CheckFlagValueInRange(FLAG_ID FlagId, int Value) /* prints an error report if a flag's value is out of range */ { flag_CheckFlagIdInRange(FlagId); if (Value <= flag_Minimum(FlagId)) { misc_StartUserErrorReport(); misc_UserErrorReport("\n Error: Flag value %d is too small for flag %s.\n", Value, flag_Name(FlagId)); misc_FinishUserErrorReport(); } else if (Value >= flag_Maximum(FlagId)) { misc_StartUserErrorReport(); misc_UserErrorReport("\n Error: Flag value %d is too large for flag %s.\n", Value, flag_Name(FlagId)); misc_FinishUserErrorReport(); } } static __inline__ void flag_CheckFlagTypeInRange(FLAG_TYPE Type) /* prints an error report if a flag's type is out of range */ { #ifdef CHECK if (Type >= flag_MAXTYPE) { misc_StartErrorReport(); misc_ErrorReport("\n In flag_CheckFlagTypeInRange: Range of types exceeded."); misc_FinishErrorReport(); } #endif } static __inline__ BOOL flag_StoreIsDefaultStore(FLAGSTORE Store) /* returns TRUE if a flag store is the default store, FALSE otherwise */ { return (BOOL) (Store == flag_DefaultStore()); } static __inline__ int flag_GetFlagValue(FLAGSTORE Store, FLAG_ID FlagId) { int Value; flag_CheckFlagIdInRange(FlagId); Value = Store[FlagId]; #ifdef CHECK if (Value == flag_CLEAN) { misc_StartErrorReport(); misc_ErrorReport("\n In flag_GetFlagValue:"); misc_ErrorReport(" Attempt to read undefined flag value."); misc_FinishErrorReport(); } #endif return Value; } static __inline__ void flag_SetFlagValue(FLAGSTORE Store, FLAG_ID FlagId, int Value) { #ifdef CHECK if (flag_StoreIsDefaultStore(Store)) { misc_StartErrorReport(); misc_ErrorReport("\n In flag_SetFlagValue:"); misc_ErrorReport(" Attempt to modify default flag value."); misc_FinishErrorReport(); } #endif flag_CheckFlagIdInRange(FlagId); flag_CheckFlagValueInRange (FlagId, Value); Store[FlagId] = Value; } static __inline__ BOOL flag_ValueIsClean(FLAGSTORE Store, FLAG_ID FlagId) { #ifdef CHECK flag_CheckFlagIdInRange(FlagId); return (BOOL) (Store[FlagId] == flag_CLEAN); #else return (BOOL) (flag_GetFlagValue(Store, FlagId) == flag_CLEAN); #endif } static __inline__ void flag_CleanStore(FLAGSTORE Store) { int i; for (i = 0; i < flag_MAXFLAG; i++) Store[i] = flag_CLEAN; } static __inline__ FLAGSTORE flag_CreateStore(void) /* creates a fresh, clean FLAGSTORE */ { FLAGSTORE store; store = (FLAGSTORE) memory_Malloc(sizeof(FLAGARRAY)); flag_CleanStore(store); return store; } static __inline__ void flag_DeleteStore(FLAGSTORE Store) { #ifdef CHECK /* Check if the flag store is a valid state */ flag_CheckStore(Store); #endif memory_Free(Store,sizeof(FLAGARRAY)); } static __inline__ void flag_InitStoreByDefaults(FLAGSTORE Store) { FLAG_ID i; for (i = (FLAG_ID) 0; i < flag_MAXFLAG; i++) flag_SetFlagValue(Store, i, flag_GetFlagValue(flag_DefaultStore(),i)); } static __inline__ void flag_SetFlagToDefault(FLAGSTORE Store, FLAG_ID Flag) { flag_SetFlagValue(Store, Flag, flag_GetFlagValue(flag_DefaultStore(), Flag)); } static __inline__ void flag_TransferFlag(FLAGSTORE Source, FLAGSTORE Destination, FLAG_ID FlagId) { flag_SetFlagValue(Destination, FlagId, flag_GetFlagValue(Source, FlagId)); } static __inline__ void flag_TransferAllFlags(FLAGSTORE Source, FLAGSTORE Destination) { FLAG_ID i; for (i = (FLAG_ID) 0; i < flag_MAXFLAG; i++) Destination[i] = Source[i]; } static __inline__ void flag_TransferSetFlags(FLAGSTORE Source, FLAGSTORE Destination) { FLAG_ID i; for (i = (FLAG_ID) 0; i < flag_MAXFLAG; i++) if (!flag_ValueIsClean(Source,i)) flag_TransferFlag(Source, Destination, i); } static __inline__ BOOL flag_IsOfType(FLAG_ID Flag, FLAG_TYPE Type) /************************************************************** INPUT: A FlagId and a flag type. RETURNS: TRUE is the flag is of given type, FALSE otherwise. ***************************************************************/ { flag_CheckFlagIdInRange(Flag); flag_CheckFlagTypeInRange(Type); return (BOOL) (flag_Type(Flag) == Type); } static __inline__ BOOL flag_IsInference(FLAG_ID Flag) /************************************************************** INPUT: A FlagId. RETURNS: TRUE is the flag is an inference flag, FALSE otherwise. ***************************************************************/ { flag_CheckFlagIdInRange(Flag); return flag_IsOfType(Flag, flag_INFERENCE); } static __inline__ BOOL flag_IsReduction(FLAG_ID Flag) /************************************************************** INPUT: A FlagId. RETURNS: TRUE is the flag is a reduction flag, FALSE otherwise. ***************************************************************/ { flag_CheckFlagIdInRange(Flag); return flag_IsOfType(Flag, flag_REDUCTION); } static __inline__ BOOL flag_IsPrinting(FLAG_ID Flag) /************************************************************** INPUT: A FlagId. RETURNS: TRUE is the flag is a printing flag, FALSE otherwise. ***************************************************************/ { flag_CheckFlagIdInRange(Flag); return flag_IsOfType(Flag, flag_PRINTING); } static __inline__ BOOL flag_IsUnique(FLAG_ID Flag) /************************************************************** INPUT: A FlagId. RETURNS: TRUE is the flag is an unique flag, FALSE otherwise. ***************************************************************/ { flag_CheckFlagIdInRange(Flag); return flag_IsOfType(Flag, flag_UNIQUE); } static __inline__ void flag_PrintReductionRules(FLAGSTORE Store) /************************************************************** INPUT: A FlagStore. RETURNS: Nothing. EFFECT: Prints the values of all reduction flags to stdout. ***************************************************************/ { FLAG_ID i; fputs("\n Reductions: ", stdout); for (i = (FLAG_ID) 0; i < flag_MAXFLAG; i++) { if (flag_IsReduction(i) && flag_GetFlagValue(Store, i)) printf("%s=%d ",flag_Name(i), flag_GetFlagValue(Store, i)); } } static __inline__ void flag_PrintInferenceRules(FLAGSTORE Store) /************************************************************** INPUT: A FlagStore. RETURNS: Nothing. EFFECT: Prints the values of all inference flags to stdout. ***************************************************************/ { FLAG_ID i; fputs("\n Inferences: ", stdout); for (i = (FLAG_ID) 0; i < flag_MAXFLAG; i++) { if (flag_IsInference(i) && flag_GetFlagValue(Store, i)) printf("%s=%d ",flag_Name(i), flag_GetFlagValue(Store,i)); } } #endif