KissatMABSolver.hpp

#pragma once
 
#include "containers/ClauseBuffer.hpp"
#include "containers/ClauseDatabase.hpp"
#include "containers/ClauseUtils.hpp"
#include "utils/Threading.hpp"
#include <fstream>
#include <iostream>
#include <unordered_map>
 
#include "KissatFamily.hpp"
#include "SolverCdclInterface.hpp"
 
#define KISSAT_MAB_
 
// KissatMABSolver includes
extern "C"
{
#include "kissat_mab/src/kissat.h"
}
 
// Wrapping struct
typedef struct kissat kissat_mab;
 
class KissatMABSolver : public SolverCdclInterface
{
  public:
    void setBumpVar(int v);
 
    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) override;
 
    void importClauses(const std::vector<ClauseExchangePtr>& clauses) override;
 
    void printStatistics();
 
    void printWinningLog() override;
 
    void setFamily(KissatFamily family) { this->family = family; };
 
    void computeFamily();
 
    std::vector<int> getModel();
 
    void diversify(const SeedGenerator& getSeed) override;
 
    void initkissatMABOptions();
 
    KissatMABSolver(int id, const std::shared_ptr<ClauseDatabase>& clauseDB);
 
    virtual ~KissatMABSolver();
 
    std::vector<int> getFinalAnalysis();
 
    std::vector<int> getSatAssumptions();
 
    std::unordered_map<std::string, int> kissatMABOptions;
 
  protected:
    int bump_var;
 
    kissat_mab* solver;
 
 
    ClauseBuffer clausesToAdd;
 
    std::atomic<bool> stopSolver;
 
    KissatFamily family;
 
    /* Decided to not use pointers to move because of c++ stl (cannot move an array into a vector,
     * sharedPtr destruction) */
    friend char KissatMabImportUnit(void*, kissat*);
    /* With KissatMabImportClause(void *painless_interface, int *kclause, unsigned int *size): need to not
     * use sharedPtr*/
    friend char KissatMabImportClause(void*, kissat*);
    friend char KissatMabExportClause(void*, kissat*);
};