ClauseDatabaseMallob.hpp

#pragma once
 
#include "containers/ClauseBuffer.hpp"
#include "containers/ClauseDatabase.hpp"
#include <atomic>
#include <shared_mutex>
#include <unordered_map>
#include <vector>
 
#define MIN_LBD 2
#define UNIT_SIZE 1
 
class ClauseDatabaseMallob : public ClauseDatabase
{
  public:
    ClauseDatabaseMallob() = delete;
 
    explicit ClauseDatabaseMallob(int maxClauseSize, int maxPartitioningLbd, size_t maxCapacity, int maxFreeSize);
 
    ~ClauseDatabaseMallob() override;
 
    bool addClause(ClauseExchangePtr clause) override;
 
    size_t giveSelection(std::vector<ClauseExchangePtr>& selectedCls, unsigned int literalCountLimit) override;
 
    void getClauses(std::vector<ClauseExchangePtr>& v_cls) override;
 
    bool getOneClause(ClauseExchangePtr& cls) override;
 
    size_t getSize() const override;
 
    size_t shrinkDatabase() override;
 
    void clearDatabase() override;
 
  protected:
    inline unsigned getIndex(int size, int lbd) const
    {
        if (size < UNIT_SIZE || lbd < MIN_LBD)
            throw std::invalid_argument("size is less than 1 or lbd is less than 2");
        return (size - 1) * m_maxPartitioningLbd + std::min(lbd - MIN_LBD, m_maxPartitioningLbd - 1);
    }
 
    inline int getSizeFromIndex(unsigned index) const { return (index == 0) ? 1 : (index / m_maxPartitioningLbd) + 1; }
 
    inline int getLbdPartitionFromIndex(unsigned index) const { return (index % m_maxPartitioningLbd) + MIN_LBD; }
 
    const size_t m_totalLiteralCapacity; 
    const int m_maxPartitioningLbd;      
    const int m_maxClauseSize;           
    const int m_freeMaxSize; 
 
    std::vector<std::unique_ptr<ClauseBuffer>> m_clauses; 
    std::atomic<long> m_currentLiteralSize;  
    std::atomic<int> m_currentWorstIndex;    
    mutable std::shared_mutex m_shrinkMutex; 
    ClauseBuffer m_missedAdditionsBfr;
};