Lingeling.hpp

#pragma once
 
#include "containers/ClauseBuffer.hpp"
#include "containers/ClauseDatabase.hpp"
#include "solvers/CDCL/SolverCdclInterface.hpp"
#include "utils/Parsers.hpp"
#include "utils/Threading.hpp"
 
#include <atomic>
 
#define LINGELING_
 
struct LGL;
 
class Lingeling : 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;
 
    std::vector<int> getFinalAnalysis();
 
    std::vector<int> getSatAssumptions();
 
    Lingeling(int id, const std::shared_ptr<ClauseDatabase>& clauseDB);
 
    Lingeling(const Lingeling& other, int id, const std::shared_ptr<ClauseDatabase>& clauseDB);
 
    ~Lingeling();
 
  private:
    // Common Initialization in Constructors
    void initialize();
 
  protected:
    LGL* solver;
 
    std::atomic<bool> stopSolver;
 
    ClauseBuffer clausesToAdd;
 
    boost::lockfree::queue<int, boost::lockfree::fixed_sized<false>> unitsToImport;
 
    size_t unitsBufferSize;
 
    size_t clsBufferSize;
 
    int* unitsBuffer;
 
    int* clsBuffer;
 
    friend int termCallback(void* solverPtr);
 
    friend void produceUnit(void* sp, int lit);
 
    friend void produce(void* sp, int* cls, int glue);
 
    friend void consumeUnits(void* sp, int** start, int** end);
 
    friend void consumeCls(void* sp, int** clause, int* glue);
};