MallobSharing.hpp

#pragma once
 
#include "GlobalSharingStrategy.hpp"
#include "containers/Bitset.hpp"
#include "containers/ClauseUtils.hpp"
#include <vector>
 
struct ClauseMeta
{
    int32_t productionEpoch; /* last epoch clause was produced */
    int32_t sharedEpoch;     /* last epoch where clause was shared and imported! */
    uint64_t sources;        /* acts like a bitset */
};
 
class MallobSharing : public GlobalSharingStrategy
{
  public:
    MallobSharing(const std::shared_ptr<ClauseDatabase>& clauseDB,
                  unsigned long baseBufferSize,
                  unsigned long maxBufferSize,
                  unsigned int  lbdLimitAtImport,
                  unsigned int  sizeLimitAtImport,
                  unsigned int  roundsPerSecond,
                  float         maxCompensation,
                  /*Filter Options*/
                  unsigned int resharePeriodMicroSec);
 
    ~MallobSharing();
 
    bool initMpiVariables() override;
 
    bool doSharing() override;
 
    void joinProcess(int winnerRank, SatResult res, const std::vector<int>& model) override;
 
    bool importClause(const ClauseExchangePtr& cls) override;
 
    std::chrono::microseconds getSleepingTime() override;
 
  protected:
    bool exportClauseToClient(const ClauseExchangePtr& clause, std::shared_ptr<SharingEntity> client) override;
 
    void deserializeClauses(const std::vector<int>& serialized_v_cls);
 
    int mergeSerializedBuffersWithMine(std::vector<std::reference_wrapper<std::vector<int>>>& buffers,
                                       std::vector<int>& result,
                                       size_t& nonFreeLiteralsCount);
 
    void computeBufferSize(unsigned int aggregationsCount);
 
    bool getOneClauseWrapper(ClauseExchangePtr& cls)
    {
        if (this->m_clauseDB->getOneClause(cls)) {
            return insertClause(cls);
        }
        return false;
    }
 
    void computeCompensation();
 
    unsigned int defaultBufferSize; 
    const unsigned int baseSize;    
    const unsigned int maxSize;     
 
    std::vector<std::reference_wrapper<std::vector<int>>> buffers; 
 
    std::vector<int> clausesToSendSerialized; 
    std::vector<int> receivedClausesLeft;     
    std::vector<int> receivedClausesRight;    
    std::vector<int> receivedClausesFather;   
 
    std::vector<ClauseExchangePtr> deserializedClauses; 
 
    Bitset myBitVector; 
 
    int father;      
    int left_child;  
    int right_child; 
    int nb_children; 
 
    size_t sleepTime; 
 
    bool addChildClauses; 
 
    const int lbdLimitAtImport;  
    const int sizeLimitAtImport; 
    unsigned m_freeSize;         
 
    float accumulatedAdmittedLiterals; 
    float accumulatedDesiredLiterals;  
    size_t lastEpochAdmittedLits;      
    size_t lastEpochReceivedLits;      
    float compensationFactor;          
    float maxCompensationFactor;    
    float estimatedIncomingLits;       
    float estimatedSharedLits;         
 
    // Filter (To be moved when Filter Interface is established)
    // ======
  public:
    void initializeFilter(unsigned int resharingPeriod,
                          unsigned int sharingsPerSecond,
                          unsigned int maxProducerId = 63);
 
    bool doesClauseExist(const ClauseExchangePtr& cls) const;
 
    void updateClause(const ClauseExchangePtr& cls);
 
    bool insertClause(const ClauseExchangePtr& cls);
 
    bool isClauseShared(const ClauseExchangePtr& cls) const;
 
    bool canConsumerImportClause(const ClauseExchangePtr& cls, unsigned consumerId);
 
    void incrementEpoch();
 
    void markClauseAsShared(ClauseExchangePtr& cls);
 
    size_t shrinkFilter();
 
  private:
    unsigned m_sharingPerSecond;   
    unsigned m_maxProducerId;      
    int m_currentEpoch;            
    int m_resharingPeriodInEpochs; 
    std::unordered_map<ClauseExchangePtr,
                       ClauseMeta,
                       ClauseUtils::ClauseExchangePtrHash,
                       ClauseUtils::ClauseExchangePtrEqual>
        m_clauseMetaMap;
};