GlucoseSyrup.hpp

#pragma once
 
#include "SolverCdclInterface.hpp"
#include "containers/ClauseBuffer.hpp"
#include "containers/ClauseDatabase.hpp"
#include "containers/ClauseUtils.hpp"
#include "utils/Threading.hpp"
 
#define GLUCOSE_
 
// Some forward declatarations for Glucose
namespace Glucose {
class ParallelSolver;
class Lit;
template<class T>
class vec;
class Clause;
}
 
class GlucoseSyrup : public SolverCdclInterface
{
  public:
    void loadFormula(const char* filename);
 
    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;
 
    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) override;
 
    void getHeuristicData(std::vector<int>** flipActivity,
                          std::vector<int>** nbPropagations,
                          std::vector<int>** nbDecisionVar);
 
    void setHeuristicData(std::vector<int>* flipActivity,
                          std::vector<int>* nbPropagations,
                          std::vector<int>* nbDecisionVar);
 
    std::vector<int> getFinalAnalysis();
 
    std::vector<int> getSatAssumptions();
 
    GlucoseSyrup(int id,
                 const std::shared_ptr<ClauseDatabase>& clauseDB);
 
    GlucoseSyrup(const GlucoseSyrup& other,
                 int id,
                 const std::shared_ptr<ClauseDatabase>& clauseDB);
 
    virtual ~GlucoseSyrup();
 
  protected:
    Glucose::ParallelSolver* solver;
 
    std::unique_ptr<ClauseDatabase> unitsToImport;  
 
    ClauseBuffer clausesToAdd;
 
    friend void glucoseExportUnary(void*, Glucose::Lit&);
 
    friend void glucoseExportClause(void*, Glucose::Clause&);
 
    friend Glucose::Lit glucoseImportUnary(void*);
 
    friend bool glucoseImportClause(void*, int*, Glucose::vec<Glucose::Lit>&);
 
  public:
    ;
};