| /**************************************************************/ |
| /* ********************************************************** */ |
| /* * * */ |
| /* * 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 <limits.h> |
| #include <stdio.h> |
| |
| #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 |
| |
| |
| |
| |
| |
| |
