OKlibrary  0.2.1.6
OK.h File Reference

Main header file for the old OKsolver. More...

#include <stdbool.h>

Go to the source code of this file.

Defines

#define VERSIONSNUMMER1   "1"
#define VERSIONSNUMMER2   "51"
#define DATUM   "18.12.2011"
#define __inline__   inline
#define BAUMRES
 Option for performing tree resolution cutting (intelligent backtracking)
#define LITTAB
 Option for more space efficient tree pruning.
#define OPTIONENKENNUNG1   "TT"
#define OPTIONENKENNUNG2   ""
#define OPTIONENKENNUNG3   ""
#define OPTIONENKENNUNG4   ""
#define OPTIONENKENNUNG5   ""
#define OPTIONENKENNUNG6   "I"
#define OPTIONENKENNUNG7   ""
#define ANZSPRACHEN   2
#define ANZSTANDARDS   4
#define DIMACSAUS

Typedefs

typedef unsigned int KLL
typedef unsigned long int StatisticsCount
 Unsigned integral type for counting for example nodes and reductions.
typedef unsigned int StatisticsCount_short
 Unsigned integral type for example the maximal search-tree depth.

Enumerations

enum  VZ { Pos = 0, Neg = 1 }
enum  Ausgabeformat { Dimacs_Format, XML_Format }

Variables

const bool internal
unsigned int Sprache
unsigned int Standard
bool Belegung
unsigned int P0
unsigned int P
unsigned int N0
 number of variables in input (a constant)
unsigned int N
 number of variables after initial reduction (a constant)
unsigned int L0
unsigned int L
unsigned int K0
unsigned int K
unsigned int aktN
 current number of unassigned variables (<= N)
unsigned int aktP
unsigned int MAXN
unsigned int MAXL
unsigned int MAXK
StatisticsCount Knoten
StatisticsCount SingleKnoten
StatisticsCount VerSingleKnoten
StatisticsCount QuasiSingleKnoten
StatisticsCount PureL
StatisticsCount Autarkien
StatisticsCount V1KlRed
StatisticsCount FastAutarkien
StatisticsCount InitEinerRed
StatisticsCount neue2Klauseln
StatisticsCount maxneue2K
StatisticsCount_short Suchbaumtiefe
StatisticsCount_short Ueberschreitung2
StatisticsCount_short init2Klauseln

Detailed Description

Main header file for the old OKsolver.

Definition in file OK.h.


Define Documentation

#define __inline__   inline

Definition at line 152 of file OK.h.

#define ANZSPRACHEN   2

Definition at line 311 of file OK.h.

Referenced by Konstantenfehler(), and main().

#define ANZSTANDARDS   4

Definition at line 320 of file OK.h.

Referenced by Konstantenfehler(), and main().

#define BAUMRES

Option for performing tree resolution cutting (intelligent backtracking)

If option NBAUMRES is defined then BAUMRES is not defined (i.e., no pruning), while otherwise BAUMRES is defined.

Definition at line 191 of file OK.h.

Referenced by BedarfVarLitKlmV(), Einlesen(), and La_belege().

#define DATUM   "18.12.2011"

Definition at line 129 of file OK.h.

Referenced by main().

#define DIMACSAUS

Definition at line 333 of file OK.h.

#define LITTAB

Option for more space efficient tree pruning.

If option NLITTAB is defined then LITTAB is not defined (i.e., more space is needed), while otherwise LITTAB is defined.

Definition at line 208 of file OK.h.

Referenced by BedarfVarLitKlmV().

#define OPTIONENKENNUNG1   "TT"

Definition at line 235 of file OK.h.

Referenced by main().

#define OPTIONENKENNUNG2   ""

Definition at line 256 of file OK.h.

Referenced by main().

#define OPTIONENKENNUNG3   ""

Definition at line 257 of file OK.h.

Referenced by main().

#define OPTIONENKENNUNG4   ""

Definition at line 258 of file OK.h.

Referenced by main().

#define OPTIONENKENNUNG5   ""

Definition at line 264 of file OK.h.

Referenced by main().

#define OPTIONENKENNUNG6   "I"

Definition at line 268 of file OK.h.

Referenced by main().

#define OPTIONENKENNUNG7   ""

Definition at line 276 of file OK.h.

Referenced by main().

#define VERSIONSNUMMER1   "1"

Definition at line 125 of file OK.h.

Referenced by main().

#define VERSIONSNUMMER2   "51"

Definition at line 126 of file OK.h.

Referenced by main().


Typedef Documentation

typedef unsigned int KLL

Definition at line 305 of file OK.h.

Unsigned integral type for counting for example nodes and reductions.

Definition at line 399 of file OK.h.

Unsigned integral type for example the maximal search-tree depth.

Definition at line 418 of file OK.h.


Enumeration Type Documentation

Enumerator:
Dimacs_Format 
XML_Format 

Definition at line 387 of file OK.h.

enum VZ
Enumerator:
Pos 
Neg 

Definition at line 302 of file OK.h.


Variable Documentation

unsigned int aktN

current number of unassigned variables (<= N)

Definition at line 190 of file OKsolver_2002_lnk.c.

Referenced by belege_Huelle(), Einlesen(), InitAbstand2(), Reduktion2(), and SATEntscheidung().

unsigned int aktP
const bool internal

Definition at line 115 of file OKsolver_2002_lnk.c.

unsigned int K0

Definition at line 190 of file OKsolver_2002_lnk.c.

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

unsigned int L0

Definition at line 190 of file OKsolver_2002_lnk.c.

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

unsigned int MAXK

Definition at line 168 of file OKsolver_2002_lnk.c.

Referenced by Einlesen(), and main().

unsigned int MAXL

Definition at line 167 of file OKsolver_2002_lnk.c.

Referenced by Einlesen(), and main().

unsigned int MAXN

Definition at line 166 of file OKsolver_2002_lnk.c.

Referenced by Einlesen(), and main().

Definition at line 200 of file OKsolver_2002_lnk.c.

Referenced by AufraeumenSat(), and Statistikzeile().

unsigned int N0

number of variables in input (a constant)

Definition at line 190 of file OKsolver_2002_lnk.c.

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

Definition at line 200 of file OKsolver_2002_lnk.c.

Referenced by AufraeumenSat(), and Statistikzeile().

unsigned int P0

Definition at line 190 of file OKsolver_2002_lnk.c.

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

Definition at line 200 of file OKsolver_2002_lnk.c.

Referenced by AufraeumenSat(), Reduktion2(), and Statistikzeile().

unsigned int Standard