PreprocessorInterface.hpp

#pragma once
 
#include "solvers/SolverInterface.hpp"
 
struct PreprocessorStats
{
    unsigned int newFormulaSize;
    unsigned int deletedClauses;
    unsigned int shrinkedClauses;
    unsigned int addedVariables;
    unsigned int eliminatedVariables;
};
 
enum PreprocessorAlgorithm
{
    MIX = 0,
    BVA = 1,
    BVE = 2,
    GAUSS = 3
    /* To fill */
};
 
class PreprocessorInterface : public SolverInterface
{
  public:
    PreprocessorInterface(PreprocessorAlgorithm algo, int id)
        : SolverInterface(SolverAlgorithmType::OTHER, id)
        , preProcType(algo)
    {
    }
 
    virtual std::vector<simpleClause> getSimplifiedFormula() = 0;
 
    virtual void restoreModel(std::vector<int>& model) = 0;
 
    virtual PreprocessorStats getPreprocessorStatistics() = 0;
 
    virtual void releaseMemory() = 0;
 
  private:
    PreprocessorAlgorithm preProcType; 
};