Parsers Namespace Reference

A set of helper functions for CNF file parsing. More...

Classes
class	ClauseProcessor
	Abstract base class for clause processors. More...
class	RedundancyFilter
	Filter for removing redundant clauses. More...
class	SBVAInit
	A filter for Structured BVA (Binary Variable Addition) More...
class	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...

Functions
bool	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	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	parseCNFParameters (FILE *f, unsigned int &varCount, unsigned int &clauseCount)
	Parse the CNF parameters (variable count and clause count) from a file.

Detailed Description

A set of helper functions for CNF file parsing.

Function Documentation

parseCNF() [1/2]

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.

Parameters

filename	The path to the file to parse.
formula	Formula object to store the parsed formula.
processors	Vector of clause processors to apply during parsing.

Returns

true if parsing was successful, false otherwise.

parseCNF() [2/2]

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.

Parameters

filename	The path to the file to parse.
clauses	Vector to store the parsed clauses.
varCount	Pointer to store the number of variables.
processors	Vector of clause processors to apply during parsing.

Returns

true if parsing was successful, false otherwise.

parseCNFParameters()

bool Parsers::parseCNFParameters	(	FILE *	f,
		unsigned int &	varCount,
		unsigned int &	clauseCount )

Parse the CNF parameters (variable count and clause count) from a file.

Parameters

f	File pointer to parse from.
varCount	Reference to store the number of variables.
clauseCount	Reference to store the number of clauses.

Returns

true if parsing was successful, false otherwise.