Parsers.hpp

Go to the documentation of this file.

 
#pragma once
 
#include "../solvers/SolverInterface.hpp"
#include "containers/ClauseUtils.hpp"
#include "containers/Formula.hpp"
#include <algorithm>
#include <functional>
 
namespace Parsers {
 
class ClauseProcessor
{
  public:
    ClauseProcessor() = default;
 
    virtual bool initMembers(unsigned int varCount, unsigned int clauseCount) = 0;
 
    virtual bool operator()(simpleClause& clause) = 0;
 
    virtual ~ClauseProcessor() = default;
};
 
class RedundancyFilter : public ClauseProcessor
{
  public:
    bool initMembers(unsigned int varCount, unsigned int clauseCount) override;
 
    bool operator()(simpleClause& clause) override;
 
  private:
    mutable std::unordered_set<simpleClause, ClauseUtils::ClauseHash> clauseCache;
};
 
class TautologyFilter : public ClauseProcessor
{
  public:
    bool initMembers(unsigned int varCount, unsigned int clauseCount) override;
 
    bool operator()(simpleClause& clause) override;
};
 
bool
parseCNF(const char* filename,
         std::vector<simpleClause>& clauses,
         unsigned int* varCount,
         const std::vector<std::unique_ptr<ClauseProcessor>>& processors = {});
 
bool
parseCNF(const char* filename, Formula& formula, const std::vector<std::unique_ptr<ClauseProcessor>>& processors = {});
 
bool
parseCNFParameters(FILE* f, unsigned int& varCount, unsigned int& clauseCount);
 
} // namespace Parsers