Parsing

Functions
bool	vallst_closeInTheoryFile (VallstInstance *vi)
FILE *	vallst_getInTheoryFile (VallstInstance *vi)
char *	vallst_getInTheoryFileName (VallstInstance *vi)
unsigned char	vallst_getProblemType (VallstInstance *vi)
VallstResult	vallst_parseCommandLineOptions (VallstInstance *vi, int argC, char **argV)
VallstResult	vallst_readInTheoryBody (VallstInstance *vi, VallstLiteralN pNrOfVars, VallstFormulaName *(*newNamePtrFunc)(void *newNamePtrFuncArg, VallstInstance *vi, bool *errorFlag), void *newNamePtrFuncArg)
VallstLiteralN	vallst_readInTheoryHead (VallstInstance *vi)
void	vallst_setIgnorePrologue (VallstInstance *vi, bool b)
void	vallst_setInTheoryFile (VallstInstance *vi, FILE *f)
void	vallst_setInTheoryFileName (VallstInstance *vi, char *fileName)
void	vallst_setPBVarPrefixChar (VallstInstance *vi, bool b)
void	vallst_setProblemType (VallstInstance *vi, unsigned char type)
void	vallst_setVarMapFile (VallstInstance *vi, FILE *f)
void	vallst_setVarMapFileName (VallstInstance *vi, char *fileName)

---

Function Documentation

bool vallst_closeInTheoryFile (  VallstInstance *  vi  )

Closes the in-theory file, if it isn't stdin. Will however *not* reset the in-theory file *name*. Returns true iff fclose returned an error (EOF). Also sets the in-theory file to NULL. Examples: vallst.c.

FILE* vallst_getInTheoryFile (  VallstInstance *  vi  )

Returns the in-theory file.

char* vallst_getInTheoryFileName (  VallstInstance *  vi  )

Returns the in-theory file name.

unsigned char vallst_getProblemType (  VallstInstance *  vi  )

Returns the problem type (see Problem types description above).

VallstResult vallst_parseCommandLineOptions (  VallstInstance *  vi, int  argC, char **  argV )

Parses command line options. vi will be updated according to the options. argC and argV work like C's 'main' function arguments. VallstResult_other is returned if a help or version flag is encountered. VallstResult_other + 1 is returned iff no other VallstResult value is applicable, which is usually the case. You are free to free the argV memory after the call; vallst won't store and use any argV pointer. Examples: vallst.c.

VallstResult vallst_readInTheoryBody (  VallstInstance *  vi, VallstLiteralN  pNrOfVars, VallstFormulaName *(*)(void *newNamePtrFuncArg, VallstInstance *vi, bool *errorFlag)  newNamePtrFunc, void *  newNamePtrFuncArg )

Reads the body of an in-theory. At invocation it's assumed that the in-theory file pointer is between the head and the body. VallstLiteralN_parseError is returned on parse error. VallstResult_notEnoughMemory might also be returned. VallstResult_other+1 is returned if the newNamePtrFunc returned an error. VallstResult_other is returned if no other value is applicable. A name of each min/max formula will be saved to a name pointer provided by newNamePtrFunc. What is stated for vallst_addNamedAxiom() relating to names also holds here. A difference though is that here, the name will be assigned NULL if it doesn't point to a vallst axiom (confer *namePtr being NULL or pointing to the provided 'axiom' array parameter in the vallst_addNamedAxiom() case). If nothing else applies, the name will be set to NULL. newNamePtrFunc should return a name pointer when called. newNamePtrFunc will be called when a name pointer is needed for giving a name to a min/max formula. The name pointer returned by newNamePtrFunc will be used to store the name of the formula to be named. newNamePtrFuncArg is a fixed pointer argument that will be supplied to newNamePtrFunc each call. If newNamePtrFunc returns NULL, the formula wont be given a name. You may set newNamePtrFunc to NULL in which case no formulas will be given names. If newNamePtrFunc sets *errorFlag to true, the parsing will be aborted and VallstResult_other+1 will be returned. *errorFlag is false by default so you don't need to set *errorFlag to false in newNamePtrFunc each time. The pNrOfVars argument is supposed to be the value returned from the preceding vallst_readInTheoryHead() call. (It's currently used only for tsp problems.) See vallst.c for an example. Examples: vallst.c.

VallstLiteralN vallst_readInTheoryHead (  VallstInstance *  vi  )

Reads the head (i.e. any optional prologue) of the in-theory file, placing the file pointer just after any optional prologue but before any character in the body (i.e. before any character in any formula definition) --- no matter what is returned except for file error i.e. when VallstLiteralN_fileError is returned. Returns the prologue's nrOfVars. If no such prologue nrOfVars can be found or vi's ignorePrologue flag is true, the maximal variable occurring in the file is returned provided that the file can be reread. If there is no prologue nrOfVars and the file can't be reread, VallstLiteralN_noPrologueNrOfVars is returned. The nrOf3Clauses and nrOfLitOccs values from the vallst prologue, see Vallst prologue description above, will, if present, be read and saved in vi. If the whole file is read twice (because of reasons related to nrOfVars; see above) *and* no vallst prologue nrOf3Clauses was found and it hasn't been set before in some other way, an estimate of the number of ternary clauses will be saved in vi; and similar for nrOfLitOccs. VallstLiteralN_parseError is returned on parse error. VallstLiteralN_fileError is returned on file error. Examples: vallst.c.

void vallst_setIgnorePrologue (  VallstInstance *  vi, bool  b )

Sets the ignore-prologue flag. The prologue nrOfVars, in any in-theory file read, will be ignored, if possible, iff the ignore-prologue flag is true.

void vallst_setInTheoryFile (  VallstInstance *  vi, FILE *  f )

Sets the in-theory file.

void vallst_setInTheoryFileName (  VallstInstance *  vi, char *  fileName )

Sets the in-theory file name. There is no need really to supply a name for the in-theory file, if there even is one, since it is only used for error messages. NULL is the default. The string will *not* be copied and the pointer (fileName) will be saved.

void vallst_setPBVarPrefixChar (  VallstInstance *  vi, bool  b )

Sets flag. If true, it is assumed that pb variables are on the form <char><positive_integer>. Otherwise the variables can be any string of characters.

void vallst_setProblemType (  VallstInstance *  vi, unsigned char  type )

Sets the problem type (see Problem types description above).

void vallst_setVarMapFile (  VallstInstance *  vi, FILE *  f )

Sets the pb variable map file. The file will be used for any variable mapping. Used for pb problems where variables can be arbitrary character strings. The file will contain a list of string variable names. The first variable in the file is mapped to the first internal variable name (1 or 2), and so on. May also be used for holding the prefix character for pb problems if the single prefix character mode is used. See vallst_setPBVarPrefixChar().

void vallst_setVarMapFileName (  VallstInstance *  vi, char *  fileName )

Sets the pb variable map file name. The string will *not* be copied and the pointer (fileName) will be saved.

---