SolverCdclInterface.hpp

#pragma once
 
#include "containers/ClauseDatabase.hpp"
#include "sharing/SharingEntity.hpp"
#include "solvers/SolverInterface.hpp"
 
enum class SolverCdclType
{
    GLUCOSE = 0,
    LINGELING = 1,
    CADICAL = 2,
    MINISAT = 3,
    KISSAT = 4,
    MAPLECOMSPS = 5,
    KISSATMAB = 6,
    KISSATINC = 7
};
 
struct SolvingCdclStatistics
{
    SolvingCdclStatistics()
    {
        propagations = 0;
        decisions = 0;
        conflicts = 0;
        restarts = 0;
        memPeak = 0;
    }
 
    unsigned long propagations; 
    unsigned long decisions;    
    unsigned long conflicts;    
    unsigned long restarts;     
    double memPeak;             
};
 
class SolverCdclInterface
    : public SolverInterface
    , public SharingEntity
{
  public:
    virtual void setPhase(const unsigned int var, const bool phase) = 0;
 
    virtual void bumpVariableActivity(const int var, const int times) = 0;
 
    virtual std::vector<int> getFinalAnalysis() = 0;
 
    virtual std::vector<int> getSatAssumptions() = 0;
 
    void printWinningLog() { this->SolverInterface::printWinningLog(); }
 
    SolverCdclType getSolverType() { return this->m_cdclType; }
 
    SolverCdclInterface(int solverId, const std::shared_ptr<ClauseDatabase>& clauseDB, SolverCdclType solverCdclType)
        : SolverInterface(SolverAlgorithmType::CDCL, solverId)
        , m_clausesToImport(clauseDB)
        , m_cdclType(solverCdclType)
        , SharingEntity()
    {
    }
 
    virtual ~SolverCdclInterface() { LOGDEBUG2("Destroying solver %d", this->getSolverId()); }
 
    SolverCdclType m_cdclType;
 
  protected:
    std::shared_ptr<ClauseDatabase> m_clausesToImport;
};