HordeSatSharing.hpp

#pragma once
 
#include "sharing/Filters/BloomFilter.hpp"
#include "sharing/SharingStrategy.hpp"
 
#include <atomic>
#include <unordered_map>
#include <vector>
 
class HordeSatSharing : public SharingStrategy
{
  public:
    HordeSatSharing(const std::shared_ptr<ClauseDatabase>& clauseDB,
                    unsigned long literalsPerProducerPerRound,
                    unsigned int  initialLbdLimit,
                    unsigned int  roundsBeforeLbdIncrease,
                    const std::vector<std::shared_ptr<SharingEntity>>& producers = {},
                    const std::vector<std::shared_ptr<SharingEntity>>& consumers = {});
 
    ~HordeSatSharing();
 
    // SharingEntity Interface
    // =======================
    bool importClause(const ClauseExchangePtr& clause) override;
 
    void importClauses(const std::vector<ClauseExchangePtr>& v_clauses) override
    {
        for (auto clause : v_clauses)
            importClause(clause);
    }
 
    // SharingStrategy Interface
    // =========================
 
    bool doSharing() override;
 
  protected:
    void addProducer(std::shared_ptr<SharingEntity> producer) override
    {
        SharingStrategy::addProducer(producer);
        /* lock m_producerMutex is released */
 
        this->lbdLimitPerProducer.emplace(producer->getSharingId(), initialLbdLimit);
        this->literalsPerProducer.emplace(producer->getSharingId(), 0);
    }
 
    void removeProducer(std::shared_ptr<SharingEntity> producer) override
    {
        SharingStrategy::removeProducer(producer);
        /* lock m_producer is released */
        this->lbdLimitPerProducer.erase(producer->getSharingId());
        this->literalsPerProducer.erase(producer->getSharingId());
    }
 
  protected:
    unsigned long literalPerRound;
 
    unsigned int initialLbdLimit;
 
    unsigned int roundBeforeIncrease;
 
    int round;
 
    std::vector<ClauseExchangePtr> selection;
 
    // Static Constants
    // ----------------
 
    static constexpr int UNDER_UTILIZATION_THRESHOLD = 75;
    static constexpr int OVER_UTILIZATION_THRESHOLD = 98;
 
    // Data accessible from other threads via importClause
    // ---------------------------------------------------
 
    std::unordered_map<unsigned int, std::atomic<unsigned int>> lbdLimitPerProducer;
 
    std::unordered_map<unsigned int, std::atomic<unsigned long>> literalsPerProducer;
};