Typedefs
typedef std::vector< unsigned int >	ui_vec
	Type of vectors of unsigned integers.
Functions
unsigned int	bin_length (const unsigned int x)
	Length of binary representation.
std::string	P (const std::string &v, const unsigned int i)
	Creating a positive literal (as string) "vi ".
std::string	N (const std::string &v, const unsigned int i)
	Creating a negative literal (as string) "vi ".
std::string	P (const std::string &v)
	Creating a positive literal (as string) "v ".
std::string	N (const std::string &v)
	Creating a negative literal (as string) "v ".
std::string	E ()
	The end-of-clause marker (Dimacs format)
void	AddBin (const std::string &A, const unsigned int length_A, const std::string &B, const unsigned int length_B, const std::string out, const std::string aux, std::ostream &os)
	Given boolean variables Ai, Bi, the binary representations of natural numbers, output clauses to os which represent via variables "out i" the result of (binary) addition.
template<typename It >
void	AddVar (const It V_b, const It V_e, const std::string &out, const std::string aux, std::ostream &os)
	Given a range of boolean variables, output clauses to os representing their addition via variables "out i".
template<typename It >
void	compvar_le (const It V_b, const It V_e, unsigned int bound, std::ostream &os)
	Output the clauses to os which express that a range of boolean variables expressing a binary number (least-significant first) is at most "bound".
template<typename It >
void	compvar_eq (const It V_b, const It V_e, unsigned int bound, std::ostream &os)
	Output the clauses to os which express that a range of boolean variables expressing a binary number is equal to "bound"; if this is impossible (the clause-set is unsatisfiable, throw an exception of type std::
template<typename It >
void	count_bound (const It V_b, const It V_e, unsigned int bound, std::ostream &os, const std::string &prefix)
	Output clauses to os expressing that the sum of a range of boolean variables is at most bound, using "S"-variables for the sum and "H"-variables for the auxiliary results.
std::string	AV (const std::string &ident, const unsigned int choice)
	Construction of identifiers of the form: "ident" string "choice" int.
void	Assignment (const ui_vec &C, std::istream &in, const unsigned int level, std::ostream &out)
	???

Typedef Documentation

typedef std::vector<unsigned int> LinInequal::ui_vec

Type of vectors of unsigned integers.

Definition at line 310 of file LinInequal.hpp.

Function Documentation

void LinInequal::AddBin	(	const std::string &	A,
		const unsigned int	length_A,
		const std::string &	B,
		const unsigned int	length_B,
		const std::string	out,
		const std::string	aux,
		std::ostream &	os
	)		`[inline]`

Given boolean variables Ai, Bi, the binary representations of natural numbers, output clauses to os which represent via variables "out i" the result of (binary) addition.

Variables "aux i" represent auxiliary results. Position 1 is least-significant.

Definition at line 74 of file LinInequal.hpp.

References E(), N(), and P().

Referenced by AddVar().

template<typename It >

void LinInequal::AddVar	(	const It	V_b,
		const It	V_e,
		const std::string &	out,
		const std::string	aux,
		std::ostream &	os
	)		`[inline]`

Given a range of boolean variables, output clauses to os representing their addition via variables "out i".

The auxiliary variables use prefix aux.

Definition at line 149 of file LinInequal.hpp.

References AddBin(), bin_length(), E(), N(), and P().

Referenced by count_bound(), and main().

void LinInequal::Assignment	(	const ui_vec &	C,
		std::istream &	in,
		const unsigned int	level,
		std::ostream &	out
	)

???

Definition at line 320 of file LinInequal.hpp.

References AV(), Latex_Handler::begin(), count_bound(), E(), end, P(), and StringHandling::toString().

std::string LinInequal::AV	(	const std::string &	ident,
		const unsigned int	choice
	)		`[inline]`

Construction of identifiers of the form: "ident" string "choice" int.

Definition at line 313 of file LinInequal.hpp.

References StringHandling::toString().

Referenced by Assignment().

unsigned int LinInequal::bin_length ( const unsigned int x ) [inline]

Length of binary representation.

Definition at line 38 of file LinInequal.hpp.

Referenced by AddVar(), compvar_eq(), compvar_le(), count_bound(), and main().

template<typename It >

void LinInequal::compvar_eq	(	const It	V_b,
		const It	V_e,
		unsigned int	bound,
		std::ostream &	os
	)		`[inline]`

Output the clauses to os which express that a range of boolean variables expressing a binary number is equal to "bound"; if this is impossible (the clause-set is unsatisfiable, throw an exception of type std::

Definition at line 255 of file LinInequal.hpp.

References bin_length(), E(), N(), and P().

Referenced by main().

template<typename It >

void LinInequal::compvar_le	(	const It	V_b,
		const It	V_e,
		unsigned int	bound,
		std::ostream &	os
	)		`[inline]`

Output the clauses to os which express that a range of boolean variables expressing a binary number (least-significant first) is at most "bound".

Definition at line 211 of file LinInequal.hpp.

References bin_length(), E(), and N().

Referenced by count_bound(), and main().

template<typename It >

void LinInequal::count_bound	(	const It	V_b,
		const It	V_e,
		unsigned int	bound,
		std::ostream &	os,
		const std::string &	prefix
	)

Output clauses to os expressing that the sum of a range of boolean variables is at most bound, using "S"-variables for the sum and "H"-variables for the auxiliary results.

String prefix is prepended to all variable names.

Definition at line 293 of file LinInequal.hpp.

References AddVar(), bin_length(), compvar_le(), P(), and S.

Referenced by Assignment().

std::string LinInequal::E ( ) [inline]

The end-of-clause marker (Dimacs format)

Definition at line 62 of file LinInequal.hpp.

Referenced by AddBin(), AddVar(), Assignment(), compvar_eq(), compvar_le(), OKlib::Combinatorics::Hypergraphs::Transversals::Bounded::Minimum_transversals_mongen< SetSystem, Generator, Output >::operator()(), and XercesTools::x2s().