CNF.hpp

Go to the documentation of this file.

#pragma once
 
#include <cstdint>
#include <iostream>
#include <mutable/mutable-config.hpp>
#include <mutable/parse/AST.hpp>
#include <vector>
 
 
namespace m {
 
namespace cnf {
 
struct M_EXPORT Predicate
{
    private:
    uintptr_t literal_; 
 
    explicit Predicate(uintptr_t l) : literal_(l) { }
 
    public:
    static Predicate Positive(const ast::Expr *e) { return Predicate(reinterpret_cast<uintptr_t>(e) | 0x0UL); }
    static Predicate Negative(const ast::Expr *e) { return Predicate(reinterpret_cast<uintptr_t>(e) | 0x1UL); }
    static Predicate Create(const ast::Expr *e, bool is_negative) { return is_negative ? Negative(e) : Positive(e); }
 
    bool negative() const { return literal_ & 0x1UL; }
 
    ast::Expr & expr() { return *reinterpret_cast<ast::Expr*>(literal_ & ~0b11UL); }
    const ast::Expr & expr() const { return *reinterpret_cast<const ast::Expr*>(literal_ & ~0b11UL); }
    const ast::Expr & operator*() const { return expr(); }
    const ast::Expr * operator->() const { return &expr(); }
 
    bool is_equi() const {
        auto binary = cast<const ast::BinaryExpr>(&expr());
        if (not binary) return false;
        if (not negative() and binary->tok != TK_EQUAL) return false;   // `=` is ok
        if (negative() and binary->tok != TK_BANG_EQUAL) return false;  // negated `!=` is ok
        return is<const ast::Designator>(binary->lhs) and is<const ast::Designator>(binary->rhs);
    }
    bool can_be_null() const { return expr().can_be_null(); }
 
    Predicate operator!() const { return Predicate(literal_ ^ 0x1UL); }
 
    bool operator==(Predicate other) const {
        return this->negative() == other.negative() and this->expr() == other.expr();
    }
    bool operator!=(Predicate other) const { return not operator==(other); }
 
    bool operator<(Predicate other) const { return this->literal_ < other.literal_; }
 
    void to_sql(std::ostream &out) const;
 
    friend std::ostream & M_EXPORT operator<<(std::ostream &out, const Predicate &pred);
    friend M_EXPORT std::string to_string(const Predicate &pred) {
        std::ostringstream oss;
        oss << pred;
        return oss.str();
    }
 
    void dump(std::ostream &out) const;
    void dump() const;
};
 
struct M_EXPORT Clause : public std::vector<Predicate>
{
    using std::vector<Predicate>::vector; // c'tor
 
    bool operator<=(const Clause &other) const;
    bool operator>=(const Clause &other) const { return other <= *this; }
    bool operator==(const Clause &other) const { return *this >= other and *this <= other; }
    bool operator!=(const Clause &other) const { return not operator==(other); }
 
    Schema get_required() const {
        Schema required;
        for (auto &P : *this)
            required |= P->get_required();
        return required;
    }
 
    bool is_equi() const {
        if (size() != 1) return false;
        auto &literal = operator[](0);
        return literal.is_equi();
    }
    bool can_be_null() const {
        for (auto &P : *this)
            if (P.can_be_null()) return true;
        return false;
    }
 
    void to_sql(std::ostream &out) const;
 
    friend std::ostream & M_EXPORT operator<<(std::ostream &out, const Clause &clause);
    friend M_EXPORT std::string to_string(const Clause &clause) {
        std::ostringstream oss;
        oss << clause;
        return oss.str();
    }
 
    void dump(std::ostream &out) const;
    void dump() const;
};
 
struct M_EXPORT CNF : public std::vector<Clause>
{
    using std::vector<Clause>::vector; // c'tor
 
    Schema get_required() const {
        Schema required;
        for (auto &clause : *this)
            required |= clause.get_required();
        return required;
    }
 
    bool is_equi() const {
        if (size() == 0)
            return false;
        for (auto &clause : *this)
            if (not clause.is_equi()) return false;
        return true;
    }
    bool can_be_null() const {
        for (auto &clause : *this)
            if (clause.can_be_null()) return true;
        return false;
    }
 
    bool operator<=(const CNF &other) const;
    bool operator>=(const CNF &other) const { return other <= *this; }
    bool operator==(const CNF &other) const { return *this >= other and *this <= other; }
    bool operator!=(const CNF &other) const { return not operator==(other); }
 
    void to_sql(std::ostream &out) const;
 
    friend M_EXPORT std::ostream & operator<<(std::ostream &out, const CNF &cnf);
    friend M_EXPORT std::string to_string(const CNF &cnf) {
        std::ostringstream oss;
        oss << cnf;
        return oss.str();
    }
 
    void dump(std::ostream &out) const;
    void dump() const;
};
 
Clause M_EXPORT operator||(const Clause &lhs, const Clause &rhs);
 
CNF M_EXPORT operator&&(const Clause &lhs, const Clause &rhs);
 
CNF M_EXPORT operator&&(const CNF &lhs, const CNF &rhs);
 
CNF M_EXPORT operator||(const CNF &lhs, const CNF &rhs);
 
CNF M_EXPORT operator!(const Clause &clause);
 
CNF M_EXPORT operator!(const CNF &cnf);
 
CNF M_EXPORT to_CNF(const ast::Expr &e);
CNF M_EXPORT get_CNF(const ast::Clause &c);
 
}
 
}
 
namespace std {
 
template<>
struct hash<m::cnf::Predicate>
{
    std::size_t operator()(m::cnf::Predicate P) const {
        return P.expr().hash() ^ (-P.negative());
    }
};
 
}