carl::io::DIMACSExporter< Pol > Class Template Reference

Write formulas to the DIMAS format. More...

#include <DIMACSExporter.h>

Collaboration diagram for carl::io::DIMACSExporter< Pol >:

Public Member Functions
bool	operator() (const Formula< Pol > &formula)
void	clear ()

Private Member Functions
std::size_t	id (carl::Variable::Arg v)
long long	getLiteral (const Formula< Pol > &f)
bool	addDisjunction (const Formula< Pol > &f)

Private Attributes
std::map< carl::Variable, std::size_t >	mVariables
std::vector< std::vector< long long > >	mClauses

Friends
template<typename P >
std::ostream &	operator<< (std::ostream &os, const DIMACSExporter< P > &de)

Detailed Description

template<typename Pol>
class carl::io::DIMACSExporter< Pol >

Write formulas to the DIMAS format.

Definition at line 19 of file DIMACSExporter.h.

Member Function Documentation

addDisjunction()

template<typename Pol >

bool carl::io::DIMACSExporter< Pol >::addDisjunction ( const Formula< Pol > &  f )

inlineprivate

Definition at line 43 of file DIMACSExporter.h.

Here is the call graph for this function:

Here is the caller graph for this function:

clear()

template<typename Pol >

void carl::io::DIMACSExporter< Pol >::clear ( )

inline

Definition at line 92 of file DIMACSExporter.h.

getLiteral()

template<typename Pol >

long long carl::io::DIMACSExporter< Pol >::getLiteral ( const Formula< Pol > &  f )

inlineprivate

Definition at line 32 of file DIMACSExporter.h.

Here is the call graph for this function:

Here is the caller graph for this function:

id()

template<typename Pol >

std::size_t carl::io::DIMACSExporter< Pol >::id ( carl::Variable::Arg  v )

inlineprivate

Definition at line 24 of file DIMACSExporter.h.

Here is the caller graph for this function:

operator()()

template<typename Pol >

bool carl::io::DIMACSExporter< Pol >::operator() ( const Formula< Pol > &  formula )

inline

Definition at line 70 of file DIMACSExporter.h.

Here is the call graph for this function:

Friends And Related Function Documentation

operator<<

template<typename Pol >

template<typename P >

std::ostream& operator<< ( std::ostream &  os, const DIMACSExporter< P > &  de  )

friend

Definition at line 97 of file DIMACSExporter.h.

Field Documentation

mClauses

template<typename Pol >

std::vector<std::vector<long long> > carl::io::DIMACSExporter< Pol >::mClauses

private

Definition at line 22 of file DIMACSExporter.h.

mVariables

template<typename Pol >

std::map<carl::Variable, std::size_t> carl::io::DIMACSExporter< Pol >::mVariables

private

Definition at line 21 of file DIMACSExporter.h.

---

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

• carl-io/DIMACSExporter.h