Formula.hpp

 
#include "vector2D.hpp"
#include <unordered_set>
 
using namespace painless;
 
// Macros for literal representation conversion
#define PLIT_IDX(LIT) (LIT * 2 - 2)
#define NLIT_IDX(LIT) (-LIT * 2 - 1)
#define LIT_IDX(LIT) (LIT > 0 ? PLIT_IDX(LIT) : NLIT_IDX(LIT))
#define IDX_LIT(IDX) (((IDX)&1) ? -(((IDX) + 1) >> 1) : (((IDX) >> 1) + 1))
 
class Formula
{
  public:
    bool push_clause(const std::vector<int>& clause);
 
    bool emplace_clause(std::initializer_list<int> clause);
 
    bool insert_unit(int lit);
 
    void delete_nonUnit(unsigned int index);
 
    bool delete_lit_nonUnit(unsigned int index, int lit);
 
    bool delete_nonUnit_occurence(int lit, unsigned int index);
 
    void delete_unit(int lit) { units.erase(lit); }
 
    void setVarCount(unsigned int varCount) { this->varCount = varCount; }
 
    unsigned int getVarCount() { return this->varCount; }
 
    skipzero_span<const int> getNonUnit(unsigned int i) const { return nonUnits[i]; }
 
    unsigned int getNonUnitEfficientSize(unsigned int i) const { return nonUnits.getRowSize(i); }
 
    const std::unordered_set<int>& getUnits() const { return this->units; }
 
    std::unordered_set<int>& getUnits() { return this->units; }
 
    skipzero_span<unsigned int> getOccurenceList(int lit)
    {
        return skipzero_span<unsigned int>(this->occurenceLists.at(LIT_IDX(lit)));
    }
 
    unsigned int getUnitCount() { return this->units.size(); }
 
    unsigned int getNonUnitsCount() { return this->nonUnits.getRowsCount() - this->deletedClausesCount; }
 
    unsigned int getAllClauseCount() { return this->getUnitCount() + this->getNonUnitsCount(); }
 
    void shrink_structures();
 
  private:
    std::unordered_set<int> units;  
    vector2D<int> nonUnits;  
    std::vector<std::vector<unsigned int>> occurenceLists;  
    unsigned int varCount = 0;  
    unsigned int deletedClausesCount = 0;  
};