ClauseExchange.hpp

#pragma once
 
#include <algorithm>
#include <atomic>
#include <boost/intrusive_ptr.hpp>
#include <cstdlib>
#include <cstring>
#include <sstream>
#include <stdexcept>
#include <vector>
 
using simpleClause = std::vector<int>;
 
// Forward declaration of ClauseExchange
class ClauseExchange;
 
using ClauseExchangePtr = boost::intrusive_ptr<ClauseExchange>;
 
class ClauseExchange
{
  public:
    unsigned int lbd;                     
    int from;                             
    unsigned int size;                    
    std::atomic<unsigned int> refCounter; 
    int lits[0];                          
 
    static ClauseExchangePtr create(const unsigned int size, const unsigned int lbd = 0, const int from = -1);
 
    static ClauseExchangePtr create(const int* begin, const int* end, const unsigned int lbd = 0, const int from = -1);
 
    static ClauseExchangePtr create(const std::vector<int>& v_cls, const unsigned int lbd = 0, const int from = -1);
 
    ~ClauseExchange() = default;
 
    int& operator[](unsigned int index)
    {
        assert(index < size && "Index out of bounds");
        return lits[index];
    }
 
    const int& operator[](unsigned int index) const
    {
        assert(index < size && "Index out of bounds");
        return lits[index];
    }
 
    int* begin() { return lits; }
 
    int* end() { return lits + size; }
 
    const int* begin() const { return lits; }
 
    const int* end() const { return lits + size; }
 
    void sortLiterals() { std::sort(begin(), end()); }
 
    void sortLiteralsDescending() { std::sort(begin(), end(), std::greater<int>()); }
 
    std::string toString() const;
 
    ClauseExchange* toRawPtr()
    {
        refCounter.fetch_add(1, std::memory_order_relaxed);
        return this;
    }
 
    static ClauseExchangePtr fromRawPtr(ClauseExchange* ptr) { return ClauseExchangePtr(ptr, false); }
 
  private:
    ClauseExchange(unsigned int size, unsigned int lbd, int from);
};
 
inline void
intrusive_ptr_add_ref(ClauseExchange* ce)
{
    ce->refCounter.fetch_add(1, std::memory_order_relaxed);
}
 
inline void
intrusive_ptr_release(ClauseExchange* ce)
{
    if (ce->refCounter.fetch_sub(1, std::memory_order_acq_rel) == 1) {
        ce->~ClauseExchange();
        std::free(ce);
    }
}