YalSat.hpp

#pragma once
 
#define YALSAT_
 
#include "LocalSearchInterface.hpp"
 
/* Includes not having any ifdef macro */
extern "C"
{
#include "yalsat/yals.h"
}
 
class YalSat : public LocalSearchInterface
{
  public:
    YalSat(int _id, unsigned long flipsLimit, unsigned long maxNoise);
 
    ~YalSat();
 
    unsigned int getVariablesCount();
 
    int getDivisionVariable();
 
    void setSolverInterrupt();
 
    void unsetSolverInterrupt();
 
    void setPhase(const unsigned int var, const bool phase);
 
    SatResult solve(const std::vector<int>& cube);
 
    void addClause(ClauseExchangePtr clause);
 
    void addClauses(const std::vector<ClauseExchangePtr>& clauses);
 
    void addInitialClauses(const std::vector<simpleClause>& clauses, unsigned int nbVars);
 
    void loadFormula(const char* filename);
 
    std::vector<int> getModel();
 
    void printStatistics();
 
    void printParameters();
 
    void diversify(const SeedGenerator& getSeed);
 
    friend int yalsat_terminate(void* p_YalSat);
 
  private:
    Yals* solver;
 
    std::atomic<bool> terminateSolver;
 
    unsigned long clausesCount;
 
    unsigned long m_flipsLimit;
 
    unsigned long m_maxNoise;
};