Parsers::TautologyFilter Class Reference

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...

#include <Parsers.hpp>

Inheritance diagram for Parsers::TautologyFilter:

Collaboration diagram for Parsers::TautologyFilter:

Public Member Functions
bool	initMembers (unsigned int varCount, unsigned int clauseCount) override
	Initialize the tautology filter.
bool	operator() (simpleClause &clause) override
	Check if a clause is a tautology.
Public Member Functions inherited from Parsers::ClauseProcessor

Detailed Description

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.

TautologyFilter checks for and removes tautological clauses during parsing.

Member Function Documentation

initMembers()

bool Parsers::TautologyFilter::initMembers ( unsigned int varCount, unsigned int clauseCount )

overridevirtual

Initialize the tautology filter.

Parameters

varCount	The number of variables in the problem.
clauseCount	The number of clauses in the problem.

Returns

Always returns true.

Implements Parsers::ClauseProcessor.

operator()()

bool Parsers::TautologyFilter::operator() ( simpleClause & clause )

overridevirtual

Check if a clause is a tautology.

This method checks if the clause contains both a literal and its negation.

Parameters

clause

The clause to check.

Returns

true if the clause is not a tautology, false if it is.

Implements Parsers::ClauseProcessor.

---

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

• /github/workspace/src/utils/Parsers.hpp