OKlibrary  0.2.1.6
Einlesen.c File Reference

Implementations of input/output functions. More...

#include <stdio.h>
#include <stddef.h>
#include <stdlib.h>
#include <math.h>
#include <ctype.h>
#include <limits.h>
#include <string.h>
#include <assert.h>
#include "OK.h"
#include "VarLitKlm.h"
#include "anlVar.h"
#include "Parameter.h"
#include "Einlesen.h"
#include "Ausgaben.h"
#include "Speicher.h"
#include "Belegung.h"

Go to the source code of this file.

Typedefs

typedef char * VarSym

Functions

void setzenStandard ()
__inline__ bool Kommzeichen (const char c)
__inline__ bool Sepzeichen (const char c)
__inline__ bool Negzeichen (const char c)
__inline__ bool Variablenanfang (const char c)
__inline__ bool Klauselbeginn (const char c)
__inline__ bool Klauselende (const char c)
__inline__ bool uebernehmenLiteral (const int l)
__inline__ bool uebernehmenKlausel ()
unsigned int Hash (const char *Name)
unsigned int eintragen ()
void Fehlerumgebung (FILE *const fp, char c)
TEIN Einlesen (FILE *const fp, const unsigned int G)
void AufraeumenEinlesen ()
static __inline__ char * Symbol1 (unsigned int v)
void AusgabeBelegung (FILE *const fp)
 Function to output a satisfying assignment.

Variables

bool nurVorreduktion
bool Schranken
static unsigned int maxn
static unsigned int maxl
static unsigned int maxk
static unsigned int maxlk
static bool unsichermaxn
static bool unsichermaxl
static bool unsichermaxk
static unsigned int M
static const unsigned int Lastfaktor = 4
static char * Eingabesymbole
static char * freiSymbole
static char * Eingabesymbole0 = NULL
static unsigned int * Hashtabelle = NULL
static int * LitTab = NULL
static int * aktKlauselAnfang
static int * aktfreies
static bool leereKlausel
static bool Tautologie
static bool globalTautologie
static bool EinerKlausel
static unsigned int aktp
static unsigned int aktp0
static void * Z0 = NULL
static void * Basis0 = NULL
static VarSymVarTab = NULL
static unsigned int * VarTab1 = NULL
static unsigned * VarTab2 = NULL
static int * Pfad0 = NULL
bool Beginn [CHAR_MAX]
bool Ende [CHAR_MAX]
bool Trenner [CHAR_MAX]
bool Negator [CHAR_MAX]
bool Kommentar [CHAR_MAX]

Detailed Description

Implementations of input/output functions.

Definition in file Einlesen.c.


Typedef Documentation

typedef char* VarSym

Definition at line 91 of file Einlesen.c.


Function Documentation

void AufraeumenEinlesen ( void  )

Definition at line 1403 of file Einlesen.c.

References Basis0, Eingabesymbole0, Hashtabelle, LitTab, Pfad0, VarTab, VarTab1, VarTab2, and Z0.

Referenced by main().

void AusgabeBelegung ( FILE *const  fp)

Function to output a satisfying assignment.

Definition at line 1424 of file Einlesen.c.

References Dateiausgabe, Dimacs_Format, EinerKlausel, Format, InitEinerRed, LGAES::Literal(), Neg, Pfad, Pfad0, PfadLit(), Pos, Symbol(), Symbol1(), Tiefe, Literals::Var(), and XML_Format.

Referenced by main(), and SATEntscheidung().

unsigned int eintragen ( )

Definition at line 242 of file Einlesen.c.

References Eingabesymbole, freiSymbole, Hash(), Hashtabelle, M, maxn, N0, unsichermaxn, and VarTab.

Referenced by Einlesen().

void Fehlerumgebung ( FILE *const  fp,
char  c 
)

Definition at line 269 of file Einlesen.c.

References Meldung().

Referenced by Einlesen().

unsigned int Hash ( const char *  Name)

Definition at line 236 of file Einlesen.c.

References M.

Referenced by eintragen().

__inline__ bool Klauselbeginn ( const char  c)

Definition at line 176 of file Einlesen.c.

References Beginn.

Referenced by Einlesen().

__inline__ bool Klauselende ( const char  c)
__inline__ bool Kommzeichen ( const char  c)

Definition at line 161 of file Einlesen.c.

References Kommentar.

Referenced by Einlesen().

__inline__ bool Negzeichen ( const char  c)

Definition at line 167 of file Einlesen.c.

References Negator.

Referenced by Einlesen().

__inline__ bool Sepzeichen ( const char  c)

Definition at line 164 of file Einlesen.c.

References Trenner.

Referenced by Einlesen().

void setzenStandard ( void  )

Definition at line 124 of file Einlesen.c.

References Beginn, Ende, Kommentar, Negator, Standard, and Trenner.

Referenced by main().

static __inline__ char* Symbol1 ( unsigned int  v) [static]

Definition at line 1418 of file Einlesen.c.

References VarTab, and VarTab1.

Referenced by AusgabeBelegung().

Definition at line 213 of file Einlesen.c.

References aktfreies, aktKlauselAnfang, aktp, aktp0, EinerKlausel, K, K0, maxk, P, P0, Tautologie, and unsichermaxk.

Referenced by Einlesen().

__inline__ bool uebernehmenLiteral ( const int  l)

Definition at line 186 of file Einlesen.c.

References aktfreies, aktKlauselAnfang, aktp, aktp0, globalTautologie, L, L0, maxl, Tautologie, and unsichermaxl.

Referenced by Einlesen().

__inline__ bool Variablenanfang ( const char  c)

Definition at line 170 of file Einlesen.c.

References Kommentar, and Standard.

Referenced by Einlesen().


Variable Documentation

int* aktfreies [static]

Definition at line 74 of file Einlesen.c.

Referenced by Einlesen(), uebernehmenKlausel(), and uebernehmenLiteral().

int* aktKlauselAnfang [static]

Definition at line 73 of file Einlesen.c.

Referenced by Einlesen(), uebernehmenKlausel(), and uebernehmenLiteral().

unsigned int aktp [static]

Definition at line 81 of file Einlesen.c.

Referenced by Einlesen(), uebernehmenKlausel(), and uebernehmenLiteral().

unsigned int aktp0 [static]

Definition at line 81 of file Einlesen.c.

Referenced by Einlesen(), uebernehmenKlausel(), and uebernehmenLiteral().

void* Basis0 = NULL [static]

Definition at line 85 of file Einlesen.c.

Referenced by AufraeumenEinlesen(), and Einlesen().

bool Beginn[CHAR_MAX]

Definition at line 118 of file Einlesen.c.

Referenced by Klauselbeginn(), and setzenStandard().

bool EinerKlausel [static]

Definition at line 79 of file Einlesen.c.

Referenced by AusgabeBelegung(), Einlesen(), and uebernehmenKlausel().

char* Eingabesymbole [static]

Definition at line 60 of file Einlesen.c.

Referenced by Einlesen(), and eintragen().

char* Eingabesymbole0 = NULL [static]

Definition at line 62 of file Einlesen.c.

Referenced by AufraeumenEinlesen(), and Einlesen().

char* freiSymbole [static]

Definition at line 61 of file Einlesen.c.

Referenced by Einlesen(), and eintragen().

bool globalTautologie [static]

Definition at line 78 of file Einlesen.c.

Referenced by Einlesen(), and uebernehmenLiteral().

unsigned int* Hashtabelle = NULL [static]

Definition at line 67 of file Einlesen.c.

Referenced by AufraeumenEinlesen(), Einlesen(), and eintragen().

bool Kommentar[CHAR_MAX]

Definition at line 122 of file Einlesen.c.

Referenced by Kommzeichen(), setzenStandard(), and Variablenanfang().

const unsigned int Lastfaktor = 4 [static]

Definition at line 57 of file Einlesen.c.

Referenced by Einlesen().

bool leereKlausel [static]

Definition at line 76 of file Einlesen.c.

Referenced by Einlesen().

int* LitTab = NULL [static]

Definition at line 69 of file Einlesen.c.

Referenced by AufraeumenEinlesen(), and Einlesen().

unsigned int maxk [static]

Definition at line 49 of file Einlesen.c.

Referenced by Einlesen(), main(), and uebernehmenKlausel().

unsigned int maxl [static]

Definition at line 49 of file Einlesen.c.

Referenced by Einlesen(), main(), Clausesets::Cls::pmax(), and uebernehmenLiteral().

unsigned int maxlk [static]

Definition at line 49 of file Einlesen.c.

Referenced by Einlesen().

unsigned int maxn [static]

Definition at line 49 of file Einlesen.c.

Referenced by Einlesen(), eintragen(), and main().

bool Negator[CHAR_MAX]

Definition at line 121 of file Einlesen.c.

Referenced by Negzeichen(), and setzenStandard().

Definition at line 130 of file OKsolver_2002_lnk.c.

Referenced by Einlesen(), InitSat(), and main().

int* Pfad0 = NULL [static]

Definition at line 109 of file Einlesen.c.

Referenced by AufraeumenEinlesen(), AusgabeBelegung(), and Einlesen().

bool Schranken

Definition at line 131 of file OKsolver_2002_lnk.c.

Referenced by Einlesen(), and main().

bool Tautologie [static]

Definition at line 77 of file Einlesen.c.

Referenced by Einlesen(), uebernehmenKlausel(), and uebernehmenLiteral().

bool unsichermaxk [static]

Definition at line 54 of file Einlesen.c.

Referenced by Einlesen(), and uebernehmenKlausel().

bool unsichermaxl [static]

Definition at line 53 of file Einlesen.c.

Referenced by Einlesen(), and uebernehmenLiteral().

bool unsichermaxn [static]

Definition at line 52 of file Einlesen.c.

Referenced by Einlesen(), and eintragen().

VarSym* VarTab = NULL [static]

Definition at line 104 of file Einlesen.c.

Referenced by AufraeumenEinlesen(), Einlesen(), eintragen(), and Symbol1().

unsigned int* VarTab1 = NULL [static]

Definition at line 106 of file Einlesen.c.

Referenced by AufraeumenEinlesen(), Einlesen(), and Symbol1().

unsigned* VarTab2 = NULL [static]

Definition at line 107 of file Einlesen.c.

Referenced by AufraeumenEinlesen(), and Einlesen().

void* Z0 = NULL [static]

Definition at line 83 of file Einlesen.c.

Referenced by AufraeumenEinlesen(), AufraeumenSat(), and Einlesen().