ClauseDatabaseSingleBuffer.hpp

#pragma once
 
#include "containers/ClauseBuffer.hpp"
#include "containers/ClauseDatabase.hpp"
#include <algorithm>
#include <random>
 
class ClauseDatabaseSingleBuffer : public ClauseDatabase
{
  private:
    ClauseBuffer buffer;
 
  public:
    ClauseDatabaseSingleBuffer() = delete;
 
    ClauseDatabaseSingleBuffer(size_t bufferSize)
        : buffer(bufferSize)
    {
    }
 
    ~ClauseDatabaseSingleBuffer() override = default;
 
    bool addClause(ClauseExchangePtr clause) override { return buffer.addClause(std::move(clause)); }
 
    size_t giveSelection(std::vector<ClauseExchangePtr>& selectedCls, unsigned int literalCountLimit) override
    {
        size_t selectedLiterals = 0;
        ClauseExchangePtr clause;
 
        while (buffer.getClause(clause)) {
            if (selectedLiterals + clause->size <= literalCountLimit) {
                selectedCls.push_back(clause);
                selectedLiterals += clause->size;
            } else {
                // If this clause would exceed the limit, put it back and stop
                buffer.addClause(clause);
                break;
            }
        }
 
        return selectedLiterals;
    }
 
    void getClauses(std::vector<ClauseExchangePtr>& v_cls) override { buffer.getClauses(v_cls); }
 
    bool getOneClause(ClauseExchangePtr& cls) override { return buffer.getClause(cls); }
 
    size_t getSize() const override { return buffer.size(); }
 
    size_t shrinkDatabase() override
    {
        LOGDEBUG3("This does nothing!");
        return (size_t)-1;
    };
 
    void clearDatabase() override { buffer.clear(); }
};