Parsers.hpp File Reference

Defines classes and functions for parsing CNF formulas and processing clauses. More...

#include "../solvers/SolverInterface.hpp"
#include "containers/ClauseUtils.hpp"
#include "containers/Formula.hpp"
#include <algorithm>
#include <functional>

Include dependency graph for Parsers.hpp:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	Parsers::ClauseProcessor
	Abstract base class for clause processors. More...
class	Parsers::RedundancyFilter
	Filter for removing redundant clauses. More...
class	Parsers::TautologyFilter
	Filter for removing tautological clauses. A tautological clause or simple a tautology is a clause that contains a literal and its complement, thus always satisfied. More...

Namespaces
namespace	Parsers
	A set of helper functions for CNF file parsing.

Functions
bool	Parsers::parseCNF (const char *filename, std::vector< simpleClause > &clauses, unsigned int *varCount, const std::vector< std::unique_ptr< ClauseProcessor > > &processors={})
	Parse a CNF formula from a file into a vector of clauses.
bool	Parsers::parseCNF (const char *filename, Formula &formula, const std::vector< std::unique_ptr< ClauseProcessor > > &processors={})
	Parse a CNF formula from a file into a Formula object.
bool	Parsers::parseCNFParameters (FILE *f, unsigned int &varCount, unsigned int &clauseCount)
	Parse the CNF parameters (variable count and clause count) from a file.

Detailed Description

Defines classes and functions for parsing CNF formulas and processing clauses.