OKlibrary  0.2.1.6
OKlib::InputOutput::CLSAdaptorDIMACSOutput< Int, String, AdaptorStatistics > Class Template Reference

Adaptor for clause-sets for output in DIMACS format. More...

#include <ClauseSetAdaptors.hpp>

List of all members.

Public Types

typedef Int int_type
typedef String string_type
typedef
adaptor_statistics_type::statistics_type 
statistics_type

Public Member Functions

 CLSAdaptorDIMACSOutput (std::ostream &out)
void comment (const string_type &s)
void n (const int_type pn)
void c (const int_type pc)
void finish ()
void tautological_clause (const int_type t)
template<class ForwardRange >
void clause (const ForwardRange &r, const int_type t)
const adaptor_statistics_type & stat () const

Detailed Description

template<typename Int = int, class String = std::string, class AdaptorStatistics = CLSAdaptorStatistics<Int, String>>
class OKlib::InputOutput::CLSAdaptorDIMACSOutput< Int, String, AdaptorStatistics >

Adaptor for clause-sets for output in DIMACS format.

Parameter n is considered as maximal possible variable index, while parameter c is considered as upper bound on the number of clauses.

The role of the template parameters are as follows:

  1. Int is the integral type for the Dimacs literals.
  2. String is the string type for comments.
  3. AdaptorStatistics is a CLSAdaptor which handles statistics.
Todo:
For the output-jobs message-classes should be employed.
Todo:
Handling of extended Dimacs-format (with real variable-names) is needed:
  • Instead of using the indices, the output might use the names via a supplied map from indices to strings.
  • Or the mapping from indices to names is added to the comment section.

Definition at line 490 of file ClauseSetAdaptors.hpp.


Member Typedef Documentation

template<typename Int = int, class String = std::string, class AdaptorStatistics = CLSAdaptorStatistics<Int, String>>
typedef Int OKlib::InputOutput::CLSAdaptorDIMACSOutput< Int, String, AdaptorStatistics >::int_type

Definition at line 497 of file ClauseSetAdaptors.hpp.

template<typename Int = int, class String = std::string, class AdaptorStatistics = CLSAdaptorStatistics<Int, String>>
typedef adaptor_statistics_type::statistics_type OKlib::InputOutput::CLSAdaptorDIMACSOutput< Int, String, AdaptorStatistics >::statistics_type

Definition at line 499 of file ClauseSetAdaptors.hpp.

template<typename Int = int, class String = std::string, class AdaptorStatistics = CLSAdaptorStatistics<Int, String>>
typedef String OKlib::InputOutput::CLSAdaptorDIMACSOutput< Int, String, AdaptorStatistics >::string_type

Definition at line 498 of file ClauseSetAdaptors.hpp.


Constructor & Destructor Documentation

template<typename Int = int, class String = std::string, class AdaptorStatistics = CLSAdaptorStatistics<Int, String>>
OKlib::InputOutput::CLSAdaptorDIMACSOutput< Int, String, AdaptorStatistics >::CLSAdaptorDIMACSOutput ( std::ostream &  out) [inline]

Definition at line 501 of file ClauseSetAdaptors.hpp.


Member Function Documentation

template<typename Int = int, class String = std::string, class AdaptorStatistics = CLSAdaptorStatistics<Int, String>>
void OKlib::InputOutput::CLSAdaptorDIMACSOutput< Int, String, AdaptorStatistics >::c ( const int_type  pc) [inline]

Definition at line 519 of file ClauseSetAdaptors.hpp.

template<typename Int = int, class String = std::string, class AdaptorStatistics = CLSAdaptorStatistics<Int, String>>
template<class ForwardRange >
void OKlib::InputOutput::CLSAdaptorDIMACSOutput< Int, String, AdaptorStatistics >::clause ( const ForwardRange &  r,
const int_type  t 
) [inline]

Definition at line 530 of file ClauseSetAdaptors.hpp.

References Latex_Handler::begin(), and end.

template<typename Int = int, class String = std::string, class AdaptorStatistics = CLSAdaptorStatistics<Int, String>>
void OKlib::InputOutput::CLSAdaptorDIMACSOutput< Int, String, AdaptorStatistics >::comment ( const string_type s) [inline]

Definition at line 506 of file ClauseSetAdaptors.hpp.

References s.

template<typename Int = int, class String = std::string, class AdaptorStatistics = CLSAdaptorStatistics<Int, String>>
void OKlib::InputOutput::CLSAdaptorDIMACSOutput< Int, String, AdaptorStatistics >::finish ( ) [inline]

Definition at line 525 of file ClauseSetAdaptors.hpp.

template<typename Int = int, class String = std::string, class AdaptorStatistics = CLSAdaptorStatistics<Int, String>>
void OKlib::InputOutput::CLSAdaptorDIMACSOutput< Int, String, AdaptorStatistics >::n ( const int_type  pn) [inline]

Definition at line 514 of file ClauseSetAdaptors.hpp.

template<typename Int = int, class String = std::string, class AdaptorStatistics = CLSAdaptorStatistics<Int, String>>
const adaptor_statistics_type& OKlib::InputOutput::CLSAdaptorDIMACSOutput< Int, String, AdaptorStatistics >::stat ( ) const [inline]

Definition at line 546 of file ClauseSetAdaptors.hpp.

template<typename Int = int, class String = std::string, class AdaptorStatistics = CLSAdaptorStatistics<Int, String>>
void OKlib::InputOutput::CLSAdaptorDIMACSOutput< Int, String, AdaptorStatistics >::tautological_clause ( const int_type  t) [inline]

Definition at line 526 of file ClauseSetAdaptors.hpp.


The documentation for this class was generated from the following file: