ClauseUtils.hpp

#pragma once
 
#include "containers/ClauseExchange.hpp"
#include <cstdint>
#include <memory>
#include <vector>
 
namespace ClauseUtils {
 
#define _jenkins_rot(x, k) (((x) << (k)) | ((x) >> (32 - (k))))
 
inline size_t
lookup3_hash(size_t key)
{
    size_t s1, s2;
    s1 = s2 = 0xdeadbeef;
    s2 ^= s1;
    s2 -= _jenkins_rot(s1, 14);
    key ^= s2;
    key -= _jenkins_rot(s2, 11);
    s1 ^= key;
    s1 -= _jenkins_rot(key, 25);
    s2 ^= s1;
    s2 -= _jenkins_rot(s1, 16);
    key ^= s2;
    key -= _jenkins_rot(s2, 4);
    s1 ^= key;
    s1 -= _jenkins_rot(key, 14);
    s2 ^= s1;
    s2 -= _jenkins_rot(s1, 24);
 
    return s2;
}
 
inline size_t
lookup3_hash_clause(const int* clause, unsigned int size)
{
    if (size == 0)
        return 0;
    size_t hash = lookup3_hash(clause[0]);
    for (unsigned int i = 1; i < size; i++) {
        hash ^= lookup3_hash(clause[i]);
    }
    return hash;
}
 
std::size_t
hashClause(const simpleClause& clause);
 
bool
operator==(const simpleClause& lhs, const simpleClause& rhs);
 
int
getLiteralsCount(const std::vector<ClauseExchangePtr>& clauses);
 
struct ClauseHash
{
    std::size_t operator()(const simpleClause& clause) const { return hashClause(clause); }
};
 
struct ClauseExchangeHash
{
    std::size_t operator()(const ClauseExchange& clause) const { return lookup3_hash_clause(clause.lits, clause.size); }
};
 
struct ClauseExchangeEqual
{
    bool operator()(const ClauseExchange& left, const ClauseExchange& right) const
    {
        if (left.size != right.size)
            return false;
 
        // Same size: check if all literals in left are in right
        uint ri = 0; // right index
 
        for (int lit : left) {
 
            // Same elements (if sorted and equal will only continue => linear complexity)
            if (lit == right[ri]) {
                ri++;
                continue;
            }
 
            // A different element: check if it is present in remaining element of right
            if (std::find(right.begin() + ri + 1, right.end(), lit) == right.end())
                return false;
        }
 
        // Same size and all literals match
        return true;
    }
};
 
struct ClauseExchangePtrHash
{
    std::size_t operator()(const ClauseExchangePtr& clause) const { return ClauseExchangeHash()(*clause); }
};
 
struct ClauseExchangePtrEqual
{
    bool operator()(const ClauseExchangePtr& left, const ClauseExchangePtr& right) const
    {
        return ClauseExchangeEqual()(*left, *right);
    }
};
 
} // namespace ClauseUtils