MapleCOMSPSSolver.hpp

#pragma once
 
#include "containers/ClauseBuffer.hpp"
#include "containers/ClauseDatabase.hpp"
#include "utils/Threading.hpp"
 
#include "SolverCdclInterface.hpp"
 
#define MAPLECOMSPS_
 
#define ID_SYM 0
#define ID_XOR 1
 
struct parameter
{
    int tier1;
    int chrono;
    int stable;
    int walkinitially;
    int target;
    int phase;
    int heuristic;
    int margin;
    int ccanr;
    int targetinc;
};
 
// Some forward declatarations for MapleCOMSPS
namespace MapleCOMSPS {
class SimpSolver;
class Lit;
template<class T>
class vec;
}
 
class MapleCOMSPSSolver : public SolverCdclInterface
{
  public:
    unsigned int getVariablesCount();
 
    int getDivisionVariable();
 
    void setPhase(const unsigned int var, const bool phase);
 
    void bumpVariableActivity(const int var, const int times);
 
    void setSolverInterrupt();
 
    void unsetSolverInterrupt();
 
    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) override;
 
    void loadFormula(const char* filename) override;
 
    bool importClause(const ClauseExchangePtr& clause);
 
    void importClauses(const std::vector<ClauseExchangePtr>& clauses);
 
    void printStatistics();
 
    void printWinningLog() override;
 
    std::vector<int> getModel();
 
    void diversify(const SeedGenerator& getSeed);
 
    MapleCOMSPSSolver(int id, const std::shared_ptr<ClauseDatabase>& clauseDB);
 
    MapleCOMSPSSolver(const MapleCOMSPSSolver& other, int id, const std::shared_ptr<ClauseDatabase>& clauseDB);
    virtual ~MapleCOMSPSSolver();
 
    std::vector<int> getFinalAnalysis();
 
    std::vector<int> getSatAssumptions();
 
    void setStrengthening(bool b);
 
    void setParameter(parameter p) {};
 
    void initshuffle(int id) {};
 
  protected:
    MapleCOMSPS::SimpSolver* solver;
 
 
    std::unique_ptr<ClauseDatabase> unitsToImport;
 
    ClauseBuffer clausesToAdd;
 
    std::atomic<bool> stopSolver;
 
    friend MapleCOMSPS::Lit cbkMapleCOMSPSImportUnit(void*);
    friend bool cbkMapleCOMSPSImportClause(void*, unsigned int*, MapleCOMSPS::vec<MapleCOMSPS::Lit>&);
    friend void cbkMapleCOMSPSExportClause(void*, unsigned int, MapleCOMSPS::vec<MapleCOMSPS::Lit>&);
 
  public:
    ;
};