Cadical.hpp

#pragma once
 
#include "containers/ClauseBuffer.hpp"
#include "containers/ClauseUtils.hpp"
 
#include "utils/Threading.hpp"
 
#include <fstream>
#include <iostream>
#include <unordered_map>
 
#include "SolverCdclInterface.hpp"
 
#define CADICAL_
 
// Cadical includes
#include "cadical/src/cadical.hpp"
 
/*---------------------Main Class----------------------*/
 
class Cadical
    : public SolverCdclInterface
    , public CaDiCaL::Learner
    , public CaDiCaL::Terminator
{
  public:
    Cadical(int id, const std::shared_ptr<ClauseDatabase>& clauseDB);
 
    virtual ~Cadical();
 
    /* Execution */
 
    SatResult solve(const std::vector<int>& cube) override;
 
    void setSolverInterrupt() override;
 
    void unsetSolverInterrupt() override;
 
    void initCadicalOptions();
 
    void diversify(const SeedGenerator& getSeed) override;
 
    /* Clause Management */
 
    void loadFormula(const char* filename) override;
 
    void addInitialClauses(const std::vector<simpleClause>& clauses, unsigned int nbVars) override;
 
    void addClause(ClauseExchangePtr clause) override;
 
    void addClauses(const std::vector<ClauseExchangePtr>& clauses) override;
 
    // /// Set clauseToImport Database
    // void setClausesToImportDatabase(std::unique_ptr<ClauseDatabase>&& db) { this->clausesToImport = std::move(db); }
 
    /* Sharing */
 
    bool importClause(const ClauseExchangePtr& clause) override;
 
    void importClauses(const std::vector<ClauseExchangePtr>& clauses) override;
 
    /* Variable Management */
 
    unsigned int getVariablesCount() override;
 
    int getDivisionVariable() override;
 
    void setPhase(const unsigned int var, const bool phase) override;
 
    void bumpVariableActivity(const int var, const int times) override;
 
    /* Statistics And More */
 
    void printStatistics() override;
 
    void printWinningLog() override;
 
    std::vector<int> getFinalAnalysis() override;
 
    std::vector<int> getSatAssumptions() override;
 
    std::vector<int> getModel() override;
 
    std::unordered_map<std::string, int> cadicalOptions;
 
  protected:
    std::unique_ptr<CaDiCaL::Solver> solver;
 
    ClauseBuffer clausesToAdd;
 
    std::atomic<bool> stopSolver;
 
    /*----------------------Learner------------------------*/
  public:
    /* Export */
    bool learning(int size, int glue) override;
 
    void learn(int lit) override;
 
    /* Import */
    bool hasClauseToImport() override;
 
    void getClauseToImport(std::vector<int>& clause, int& glue) override;
 
  private:
    simpleClause tempClause;
    
    int lbd;
    
    ClauseExchangePtr tempClauseToImport;
 
    /*-----------------------Terminator----------------------*/
    bool terminate() { return this->stopSolver; }
};