Implementations related to variables, literals, and clauses. More...

#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include <limits.h>
#include "OK.h"
#include "Parameter.h"
#include "VarLitKlm.h"

Classes
struct	var
struct	lit
Functions
__inline__ LIT	Literal (const VAR v, const VZ e)
	literals from variables and signs
__inline__ VAR	Var (const LIT l)
	the underlying variable of a literal
__inline__ LIT	Komp (const LIT l)
	the complement of a literal
__inline__ ZWort	VPosition (const VAR v)
	the word-index of a variable
__inline__ Wort	VMaske (const VAR v)
	the mask of a variable w.r.t. its word
bool	belegt (const VAR v)
	is variable assigned?
void	setzenbelegt (const VAR v, const bool T)
	set truth-value for assigned-test
const char *	Symbol (const VAR v)
	the original name (in the input-file, in extended DIMACS-format) of a variable
__inline__ void	loeseV (const VAR v)
	remove a variable from the current list
__inline__ void	bindeV (const VAR v)
	re-insert the variable to the current list
__inline__ VAR	ersteVar (void)
	begin of the variable-list
__inline__ bool	echteVar (const VAR v)
	variable is not after-the-end?
__inline__ VAR	naechsteVar (const VAR v)
	next variable in the list
__inline__ unsigned int	RundeL (const LIT l)
	round of a literal
__inline__ void	setzenRundeL (const LIT l)
	set round of literal to the current round
__inline__ void	NullsetzenRL (void)
	reset round of all literals
__inline__ void	loeseLv (const LITV x)
	remove literal-occurrence from list of all occurrences
__inline__ void	bindeLv (const LITV x)
	re-insert literal-occurrence into list of all occurrences
__inline__ void	loeseLK (const LITV x)
	remove literal-occurrence from clause-list
__inline__ void	bindeLK (const LITV x)
	re-insert literal-occurrence into clause-list
__inline__ LITV	erstesVork (const LIT l)
	begin of list of literal-occurrences for literal l
__inline__ bool	echtesVork (const LITV x, const LIT dummy)
	literal-occurrence is not past-the-end?
__inline__ LITV	naechstesVork (const LITV x)
	next literal-occurrence for literal l
__inline__ LITV	naechstesVorkK (const LITV x)
	next literal-occurrence in clause
__inline__ LIT	LitVk (const LITV x)
	literal of literal-occurrence
__inline__ KLN	KlnVk (const LITV x)
	clause-identifier of literal-occurrence
__inline__ KLL	Laenge (const KLN k)
	current length of clause
__inline__ void	ZuwLaenge (const KLN k, const KLL m)
	set length of clause
__inline__ KLL	LaengeM1 (const KLN k)
	current length, with post-decrement
__inline__ KLL	LaengeP1 (KLN k)
	current length, with post-increment
__inline__ KLL	LaLaenge (const KLN k)
	current look-ahead-length of clause
__inline__ void	ZuwLaLaenge (const KLN k, const KLL m)
	set look-ahead-length of clause
__inline__ KLL	M1LaLaenge (const KLN k)
	current look-ahead-length of clause with pre-decrement
__inline__ unsigned int	RundeK (const KLN k)
	current round-counter-value of clause
__inline__ void	setzenRundeK (const KLN k)
	set round-counter of clause
__inline__ void	NullsetzenRK (void)
	reset all clause-round-counters
__inline__ void	ZuwUrLaenge (const KLN k, const unsigned int m)
__inline__ void	ZuwersteVK (const KLN k, VarMaske *const p)
__inline__ unsigned int	UrLaenge (const KLN k)
	original length of clause
__inline__ VarMaske *	ersteVK (const KLN k)
	variable mask for first variable (others follow)
__inline__ void	Klauselanfangen (void)
	open a new clause (for input)
__inline__ void	Literaleintragen (const int l)
	Adding literal l to the current clause.
__inline__ void	Klauselbeenden (void)
	close a clause (for input)
__inline__ void	Symboleintragen (const unsigned int v, const char *const S)
	set name of variable (for input)
__inline__ void	setzenerstesV (const LIT l, const LITV x)
	set first literal-occurrence for a literal
__inline__ void	setzenLit (const LITV x, const LIT l)
	set literal for a literal-occurrence
__inline__ void	setzenKln (const LITV x, const KLN k)
	set clause for a literal-occurrence
__inline__ void	setzennLv (const LITV x, const LITV y)
	set next literal occurrence for literal-occurrence x
__inline__ void	setzenlLv (const LITV x, const LITV y)
	set previous literal occurrence for literal-occurrence x
__inline__ void	setzennLK (const LITV x, const LITV y)
	set next literal-occurrence in clause
__inline__ void	setzenlLK (const LITV x, const LITV y)
	set previous literal-occurrence in clause
size_t	BedarfVarLitKlmV (void)
void *	VarLitKlmV (void *Z)
	Initialisation of the datastructure representing variables, literals and clauses-nodes.
void	InitVarLitKlm (void)
	initialisation of variable-sets for original clause in case of not LITTAB
Variables
const LIT	NullLiteral = NULL
	the null-literal
static VAR	AnkerVar
static LIT	erstesLiteral
static LITV	F
static KLN	FK
unsigned int *	aktAnzK
	the current number of clauses
unsigned int *	InitAnzK
	initial number of clauses (in case of xml-output)
static VarMaske *	MaskenKl
static LITV	aktLitV
static LITV	aktLitV0
static KLN	aktKln
static VarMaske *	aktMaske
static unsigned int	aktKlLaenge

Detailed Description

Implementations related to variables, literals, and clauses.

Implementations of the types and functions representing the abstract data type for variables, literals, literal occurrences and clause-information-nodes; also initialisation functions.

Definition in file VarLitKlm.c.

Function Documentation

size_t BedarfVarLitKlmV ( void )

Definition at line 533 of file VarLitKlm.c.

References BAUMRES, Format, GroesseVarMenge, L, LITTAB, N, and XML_Format.

Referenced by Einlesen().

bool belegt ( const VAR v )

is variable assigned?

Definition at line 110 of file VarLitKlm.c.

References belegt().

Referenced by belegt(), Einlesen(), Reduktion1(), setzenbelegt(), and VarLitKlmV().

__inline__ void bindeLK ( const LITV x )

re-insert literal-occurrence into clause-list

Definition at line 254 of file VarLitKlm.c.

Referenced by rebelege(), and rebelege_Verz().

__inline__ void bindeLv ( const LITV x )

re-insert literal-occurrence into list of all occurrences

Definition at line 233 of file VarLitKlm.c.

Referenced by rebelege(), and rebelege_Verz().

__inline__ void bindeV ( const VAR v )

re-insert the variable to the current list

Definition at line 135 of file VarLitKlm.c.

References var::nae, and var::vor.

Referenced by rebelege(), and rebelege_Verz().

__inline__ bool echtesVork	(	const LITV	x,
		const LIT	dummy
	)

literal-occurrence is not past-the-end?

Definition at line 269 of file VarLitKlm.c.

Referenced by belege(), belege_VK(), belege_VKRed(), belegeRed(), berechne_Huelle(), La_belege(), La_belegeFil(), rebelege(), rebelege_Verz(), and Reduktion2().

__inline__ bool echteVar ( const VAR v )

variable is not after-the-end?

Definition at line 149 of file VarLitKlm.c.

Referenced by Reduktion1(), Reduktion2(), and SATEntscheidung().

__inline__ LITV erstesVork ( const LIT l )

begin of list of literal-occurrences for literal l

Definition at line 263 of file VarLitKlm.c.

Referenced by belege(), belege_VK(), belege_VKRed(), belegeRed(), berechne_Huelle(), La_belege(), La_belegeFil(), rebelege(), rebelege_Verz(), and Reduktion2().

__inline__ VAR ersteVar ( void )

begin of the variable-list

Definition at line 144 of file VarLitKlm.c.

References var::nae.

Referenced by Reduktion1(), Reduktion2(), and SATEntscheidung().

__inline__ VarMaske* ersteVK ( const KLN k )

variable mask for first variable (others follow)

Definition at line 395 of file VarLitKlm.c.

Referenced by hinzufuegenKl().

void InitVarLitKlm ( void )

initialisation of variable-sets for original clause in case of not LITTAB

Definition at line 640 of file VarLitKlm.c.

References aktrelV, F, KlnVk(), L, LitVk(), M, Literals::Var(), VMaske(), and VPosition().

Referenced by main().

__inline__ void Klauselanfangen ( void )

open a new clause (for input)

Definition at line 416 of file VarLitKlm.c.

References aktLitV, and aktMaske.

Referenced by Einlesen().

__inline__ void Klauselbeenden ( void )

close a clause (for input)

Definition at line 468 of file VarLitKlm.c.

References aktAnzK, aktKlLaenge, aktKln, Laenge(), and UrLaenge().

Referenced by Einlesen().

__inline__ KLN KlnVk ( const LITV x )

clause-identifier of literal-occurrence

Definition at line 293 of file VarLitKlm.c.

Referenced by belege(), belege_VK(), belege_VKRed(), belegeRed(), berechne_Huelle(), InitVarLitKlm(), La_belege(), La_belegeFil(), rebelege(), and rebelege_Verz().

__inline__ LIT Komp ( const LIT l )

the complement of a literal

Definition at line 93 of file VarLitKlm.c.

References Komp().

Referenced by belege(), belege_VK(), belege_VKRed(), belegeRed(), berechne_Huelle(), Komp(), La_belege(), La_belegeFil(), rebelege(), rebelege_Verz(), and VarLitKlmV().

__inline__ KLL Laenge ( const KLN k )

current length of clause

Definition at line 300 of file VarLitKlm.c.

References Laenge().

Referenced by belege_VKRed(), belegeRed(), berechne_Huelle(), Klauselbeenden(), La_belege(), La_belegeFil(), Laenge(), LaengeM1(), LaengeP1(), and ZuwLaenge().

__inline__ KLL LaengeM1 ( const KLN k )

current length, with post-decrement

Definition at line 310 of file VarLitKlm.c.

References Laenge().

Referenced by belege(), belege_VK(), belege_VKRed(), and belegeRed().

__inline__ KLL LaengeP1 ( KLN k )

current length, with post-increment

Definition at line 315 of file VarLitKlm.c.

References Laenge().

Referenced by rebelege(), and rebelege_Verz().

__inline__ KLL LaLaenge ( const KLN k )

current look-ahead-length of clause

Definition at line 320 of file VarLitKlm.c.

References LaLaenge().

Referenced by berechne_Huelle(), La_belege(), La_belegeFil(), LaLaenge(), M1LaLaenge(), and ZuwLaLaenge().

__inline__ LIT Literal	(	const VAR	v,
		const VZ	e
	)

literals from variables and signs

Definition at line 78 of file VarLitKlm.c.

References BoolVarLit::neg, Neg, BoolVarLit::pos, and Pos.

__inline__ void Literaleintragen ( const int l )

Adding literal l to the current clause.

enter literal into a clause (for input)

Definition at line 431 of file VarLitKlm.c.

References aktKlLaenge, aktKln, aktLitV, aktLitV0, aktMaske, LGAES::Literal(), var::Maske, Neg, Pos, var::Position, VMaske(), and VPosition().

Referenced by Einlesen().

__inline__ LIT LitVk ( const LITV x )

literal of literal-occurrence

Definition at line 288 of file VarLitKlm.c.

Referenced by berechne_Huelle(), InitVarLitKlm(), La_belege(), and La_belegeFil().

__inline__ void loeseLK ( const LITV x )

remove literal-occurrence from clause-list

Definition at line 247 of file VarLitKlm.c.

Referenced by belege(), belege_VK(), belege_VKRed(), and belegeRed().

__inline__ void loeseLv ( const LITV x )

remove literal-occurrence from list of all occurrences

Definition at line 219 of file VarLitKlm.c.

Referenced by belege(), belege_VK(), belege_VKRed(), and belegeRed().

__inline__ void loeseV ( const VAR v )

remove a variable from the current list

Definition at line 128 of file VarLitKlm.c.

References var::nae, and var::vor.

Referenced by belege(), belege_VK(), belege_VKRed(), and belegeRed().

__inline__ KLL M1LaLaenge ( const KLN k )

current look-ahead-length of clause with pre-decrement

Definition at line 330 of file VarLitKlm.c.

References LaLaenge().

Referenced by berechne_Huelle(), La_belege(), and La_belegeFil().

__inline__ LITV naechstesVork ( const LITV x )

next literal-occurrence for literal l

Definition at line 274 of file VarLitKlm.c.

Referenced by belege(), belege_VK(), belege_VKRed(), belegeRed(), berechne_Huelle(), La_belege(), La_belegeFil(), rebelege(), and rebelege_Verz().

__inline__ LITV naechstesVorkK ( const LITV x )

next literal-occurrence in clause

Definition at line 281 of file VarLitKlm.c.

Referenced by belege(), belege_VK(), belege_VKRed(), belegeRed(), berechne_Huelle(), La_belege(), La_belegeFil(), rebelege(), and rebelege_Verz().

__inline__ VAR naechsteVar ( const VAR v )

next variable in the list

Definition at line 154 of file VarLitKlm.c.

References var::nae.

Referenced by Reduktion1(), Reduktion2(), and SATEntscheidung().

__inline__ void NullsetzenRK ( void )

reset all clause-round-counters

Definition at line 348 of file VarLitKlm.c.

References FK, K, and RundeK().

Referenced by berechne_Huelle(), La_Huelle(), and La_HuelleFil().

__inline__ void NullsetzenRL ( void )

reset round of all literals

Definition at line 172 of file VarLitKlm.c.

References N, and Runde.

Referenced by berechne_Huelle(), La_Huelle(), and La_HuelleFil().

__inline__ unsigned int RundeK ( const KLN k )

current round-counter-value of clause

Definition at line 337 of file VarLitKlm.c.

References RundeK().

Referenced by berechne_Huelle(), La_belege(), La_belegeFil(), NullsetzenRK(), RundeK(), setzenRundeK(), and VarLitKlmV().

__inline__ unsigned int RundeL ( const LIT l )

round of a literal

Definition at line 161 of file VarLitKlm.c.

References Runde.

Referenced by berechne_Huelle(), La_belege(), La_belegeFil(), neue1Klausel(), and Reduktion1().

void setzenbelegt	(	const VAR	v,
		const bool	T
	)

set truth-value for assigned-test

Definition at line 115 of file VarLitKlm.c.

References belegt(), and T.

Referenced by belege(), belege_VK(), belege_VKRed(), belegeRed(), rebelege(), and rebelege_Verz().

__inline__ void setzenerstesV	(	const LIT	l,
		const LITV	x
	)

set first literal-occurrence for a literal

Definition at line 489 of file VarLitKlm.c.

__inline__ void setzenKln	(	const LITV	x,
		const KLN	k
	)

set clause for a literal-occurrence

Definition at line 501 of file VarLitKlm.c.

__inline__ void setzenLit	(	const LITV	x,
		const LIT	l
	)

set literal for a literal-occurrence

Definition at line 495 of file VarLitKlm.c.

__inline__ void setzenlLK	(	const LITV	x,
		const LITV	y
	)

set previous literal-occurrence in clause

Definition at line 525 of file VarLitKlm.c.

__inline__ void setzenlLv	(	const LITV	x,
		const LITV	y
	)

set previous literal occurrence for literal-occurrence x

Definition at line 513 of file VarLitKlm.c.

__inline__ void setzennLK	(	const LITV	x,
		const LITV	y
	)

set next literal-occurrence in clause

Definition at line 519 of file VarLitKlm.c.

__inline__ void setzennLv	(	const LITV	x,
		const LITV	y
	)

set next literal occurrence for literal-occurrence x

Definition at line 507 of file VarLitKlm.c.

__inline__ void setzenRundeK ( const KLN k )

set round-counter of clause

Definition at line 342 of file VarLitKlm.c.

References Runde, and RundeK().

Referenced by berechne_Huelle(), La_belege(), and La_belegeFil().

__inline__ void setzenRundeL ( const LIT l )

set round of literal to the current round

Definition at line 166 of file VarLitKlm.c.

References Runde.

Referenced by berechne_Huelle(), La_belegeFil(), La_Huelle(), La_HuelleFil(), and neue1Klausel().

const char* Symbol ( const VAR v )

the original name (in the input-file, in extended DIMACS-format) of a variable

Definition at line 120 of file VarLitKlm.c.

References Symbol().

Referenced by AusgabeBelegung(), Symbol(), Symboleintragen(), and Verzweigungsliteralausgabe().

__inline__ void Symboleintragen	(	const unsigned int	v,
		const char *const	S
	)

set name of variable (for input)

Definition at line 481 of file VarLitKlm.c.

References Symbol().

Referenced by Einlesen().

__inline__ unsigned int UrLaenge ( const KLN k )

original length of clause

Definition at line 390 of file VarLitKlm.c.

References UrLaenge().

Referenced by hinzufuegenKl(), Klauselbeenden(), UrLaenge(), and ZuwUrLaenge().

__inline__ VAR Var ( const LIT l )

the underlying variable of a literal

Definition at line 88 of file VarLitKlm.c.

References Literals::Var().

void* VarLitKlmV ( void * Z )

Initialisation of the datastructure representing variables, literals and clauses-nodes.

Definition at line 554 of file VarLitKlm.c.

References aktAnzK, aktrelV, AnkerVar, ANZWORTE, belegt(), BITS, erstesLiteral, FK, Format, GroesseVarMenge, InitAnzK, K, Komp(), L, M, N, BoolVarLit::neg, P, BoolVarLit::pos, q, Runde, RundeK(), and XML_Format.

Referenced by Einlesen().

__inline__ Wort VMaske ( const VAR v )

the mask of a variable w.r.t. its word

Definition at line 104 of file VarLitKlm.c.

References var::Maske.

Referenced by enthalten(), InitVarLitKlm(), and Literaleintragen().

__inline__ ZWort VPosition ( const VAR v )

the word-index of a variable

Definition at line 99 of file VarLitKlm.c.

References var::Position.

Referenced by enthalten(), InitVarLitKlm(), and Literaleintragen().

__inline__ void ZuwersteVK	(	const KLN	k,
		VarMaske *const	p
	)

Definition at line 384 of file VarLitKlm.c.

__inline__ void ZuwLaenge	(	const KLN	k,
		const KLL	m
	)

set length of clause

Definition at line 305 of file VarLitKlm.c.

References Laenge().

__inline__ void ZuwLaLaenge	(	const KLN	k,
		const KLL	m
	)

set look-ahead-length of clause

Definition at line 325 of file VarLitKlm.c.

References LaLaenge().

Referenced by berechne_Huelle(), La_belege(), and La_belegeFil().

__inline__ void ZuwUrLaenge	(	const KLN	k,
		const unsigned int	m
	)

Definition at line 379 of file VarLitKlm.c.

References UrLaenge().

Variable Documentation

unsigned int* aktAnzK

the current number of clauses

Definition at line 63 of file VarLitKlm.c.

Referenced by auswerten(), belege_Huelle(), Einlesen(), InitAbstand2(), Klauselbeenden(), Reduktion1(), Reduktion2(), SATEntscheidung(), and VarLitKlmV().

unsigned int aktKlLaenge [static]

Definition at line 414 of file VarLitKlm.c.

Referenced by Klauselbeenden(), and Literaleintragen().

KLN aktKln [static]

Definition at line 408 of file VarLitKlm.c.

Referenced by Klauselbeenden(), and Literaleintragen().

LITV aktLitV [static]

Definition at line 406 of file VarLitKlm.c.

Referenced by Klauselanfangen(), and Literaleintragen().

LITV aktLitV0 [static]

Definition at line 407 of file VarLitKlm.c.

Referenced by Literaleintragen().

VarMaske* aktMaske [static]

Definition at line 411 of file VarLitKlm.c.

Referenced by Klauselanfangen(), and Literaleintragen().

VAR AnkerVar [static]

Definition at line 58 of file VarLitKlm.c.

Referenced by VarLitKlmV().

LIT erstesLiteral [static]

Definition at line 59 of file VarLitKlm.c.

Referenced by VarLitKlmV().

LITV F [static]

Definition at line 60 of file VarLitKlm.c.

Referenced by InputCls::Construct_Cls_dynamic< Clauseset >::finish(), OKlib::Combinatorics::Hypergraphs::Generators::GreenTao< UInt >::hyperedge_set(), InitVarLitKlm(), main(), InputCls::Construct_Cls_dynamic< Clauseset >::new_clause(), and test_InputCls().

KLN FK [static]

Definition at line 61 of file VarLitKlm.c.

Referenced by NullsetzenRK(), and VarLitKlmV().

unsigned int* InitAnzK

initial number of clauses (in case of xml-output)

Definition at line 64 of file VarLitKlm.c.

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

VarMaske* MaskenKl [static]

Definition at line 70 of file VarLitKlm.c.

const LIT NullLiteral = NULL

the null-literal

Definition at line 56 of file VarLitKlm.c.

Classes

Functions

Variables

Detailed Description

Function Documentation

Variable Documentation