OKlibrary  0.2.1.6
LinInequal Namespace Reference

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::N ( const std::string &  v,
const unsigned int  i 
) [inline]

Creating a negative literal (as string) "vi ".

Definition at line 50 of file LinInequal.hpp.

References StringHandling::toString().

Referenced by AddBin(), AddVar(), compvar_eq(), and compvar_le().

std::string LinInequal::N ( const std::string &  v) [inline]

Creating a negative literal (as string) "v ".

Definition at line 58 of file LinInequal.hpp.

std::string LinInequal::P ( const std::string &  v,
const unsigned int  i 
) [inline]

Creating a positive literal (as string) "vi ".

Definition at line 46 of file LinInequal.hpp.

References StringHandling::toString().

Referenced by AddBin(), AddVar(), Assignment(), compvar_eq(), count_bound(), and main().

std::string LinInequal::P ( const std::string &  v) [inline]

Creating a positive literal (as string) "v ".

Definition at line 54 of file LinInequal.hpp.