SolverInterface.hpp

 
#pragma once
 
#include "containers/ClauseExchange.hpp"
#include "containers/ClauseUtils.hpp"
#include "utils/Logger.hpp"
 
#include <atomic>
#include <memory>
#include <random>
#include <stdio.h>
#include <stdlib.h>
#include <typeindex>
#include <typeinfo>
#include <unordered_map>
#include <vector>
 
 
/* Forward Declaration */
class SolverInterface;
 
using SeedGenerator = std::function<int(SolverInterface*)>;
 
enum class SatResult
{
    SAT = 10,     
    UNSAT = 20,   
    TIMEOUT = 30, 
    UNKNOWN = 0   
};
 
enum class SolverAlgorithmType
{
    CDCL = 0,         
    LOCAL_SEARCH = 1, 
    LOOK_AHEAD = 2,   
    OTHER = 3,        
    UNKNOWN = 255     
};
 
class SolverInterface
{
  public:
    virtual unsigned int getVariablesCount() = 0;
 
    virtual int getDivisionVariable() = 0;
 
    virtual void setSolverInterrupt() = 0;
 
    virtual void unsetSolverInterrupt() = 0;
 
    virtual void printWinningLog();
 
    virtual SatResult solve(const std::vector<int>& cube) = 0;
 
    virtual void addClause(ClauseExchangePtr clause) = 0;
 
    virtual void addClauses(const std::vector<ClauseExchangePtr>& clauses) = 0;
 
    virtual void addInitialClauses(const std::vector<simpleClause>& clauses, unsigned int nbVars) = 0;
 
    virtual void loadFormula(const char* filename) = 0;
 
    virtual void printStatistics();
 
    virtual std::vector<int> getModel() = 0;
 
    virtual void printParameters();
 
    virtual void diversify(const SeedGenerator& getSeed = [](SolverInterface* s) { return s->getSolverId(); }) = 0;
 
    bool isInitialized() { return this->m_initialized; }
 
    void setInitialized(bool value) { this->m_initialized = value; }
 
    SolverAlgorithmType getAlgoType() { return this->m_algoType; }
 
    unsigned int getSolverTypeId() { return this->m_solverTypeId; }
 
    void setSolverTypeId(unsigned int typeId) { this->m_solverTypeId = typeId; }
 
    unsigned int getSolverId() { return this->m_solverId; }
 
    void setSolverId(unsigned int id) { this->m_solverId = id; }
 
    unsigned int getSolverTypeCount() const
    {
        auto it = s_instanceCounts.find(std::type_index(typeid(*this)));
        return (it != s_instanceCounts.end()) ? it->second.load() : 0;
    }
 
    SolverInterface(SolverAlgorithmType algoType, int solverId);
 
    virtual ~SolverInterface();
 
  protected:
    template<typename Derived>
    static unsigned int getAndIncrementTypeCount()
    {
        auto [it, inserted] = s_instanceCounts.try_emplace(std::type_index(typeid(Derived)), 0);
        return it->second.fetch_add(1);
    }
 
    template<typename Derived>
    void initializeTypeId()
    {
        m_solverTypeId = getAndIncrementTypeCount<Derived>();
        LOGDEBUG1("I am solver of type %s: id %d, typeId: %u", typeid(Derived).name(), m_solverId, m_solverTypeId);
    }
 
  protected:
    SolverAlgorithmType m_algoType;  
    std::atomic<bool> m_initialized; 
    unsigned int m_solverTypeId;     
    int m_solverId;                  
    static inline std::unordered_map<std::type_index, std::atomic<unsigned int>> s_instanceCounts;
};