core.hh

#pragma once
 
#include <clingo/core/symbol.hh>
 
#include <clingo/util/algorithm.hh>
 
#include <cstdint>
#include <ostream>
 
namespace CppClingo {
 
 
enum class Sign : uint8_t {
    none,  
    once,  
    twice, 
};
 
auto operator-(Sign a) -> Sign;
auto operator+(Sign a, Sign b) -> Sign;
auto operator+=(Sign &a, Sign b) -> Sign &;
 
auto operator<<(std::ostream &out, Sign sign) -> std::ostream &;
auto operator<<(Util::OutputBuffer &out, Sign sign) -> Util::OutputBuffer &;
 
enum class Relation : uint8_t {
    equal,         
    not_equal,     
    less,          
    less_equal,    
    greater,       
    greater_equal, 
};
 
[[nodiscard]] auto flip(Relation rel) -> Relation;
[[nodiscard]] auto complement(Relation rel) -> Relation;
 
auto evaluate(auto const &lhs, Relation rel, auto const &rhs) -> bool {
    switch (rel) {
        case Relation::equal: {
            return lhs == rhs;
        }
        case Relation::not_equal: {
            return lhs != rhs;
        }
        case Relation::less: {
            return lhs < rhs;
        }
        case Relation::less_equal: {
            return lhs <= rhs;
        }
        case Relation::greater: {
            return lhs > rhs;
        }
        case Relation::greater_equal: {
            return lhs >= rhs;
        }
    }
    Util::unreachable();
}
 
auto operator<<(std::ostream &out, Relation rel) -> std::ostream &;
auto operator<<(Util::OutputBuffer &out, Relation rel) -> Util::OutputBuffer &;
 
enum class TruthValue : uint8_t {
    top,     
    bot,     
    unknown, 
};
 
enum class AggregateFunction : uint8_t {
    count, 
    sum,   
    sump,  
    min,   
    max,   
};
 
auto operator<<(std::ostream &out, AggregateFunction fun) -> std::ostream &;
auto operator<<(Util::OutputBuffer &out, AggregateFunction fun) -> Util::OutputBuffer &;
 
inline auto neutral_val(AggregateFunction fun) -> Symbol {
    switch (fun) {
        case AggregateFunction::sum:
        case AggregateFunction::sump: {
            return SymbolStore::num_ref(0);
        }
        case AggregateFunction::min: {
            return SymbolStore::sup();
        }
        case AggregateFunction::max: {
            return SymbolStore::inf();
        }
        case AggregateFunction::count: {
            throw std::invalid_argument("count function has no neutral value");
        }
    }
    Util::unreachable();
}
 
inline auto neutral_num(AggregateFunction fun) -> std::variant<Number, Symbol> {
    switch (fun) {
        case AggregateFunction::sum:
        case AggregateFunction::sump: {
            return Number(0);
        }
        case AggregateFunction::min: {
            return SymbolStore::sup();
        }
        case AggregateFunction::max: {
            return SymbolStore::inf();
        }
        case AggregateFunction::count: {
            throw std::invalid_argument("count function has no neutral value");
        }
    }
    Util::unreachable();
}
 
inline auto relevant_val(AggregateFunction fun, Symbol sym) -> bool {
    switch (fun) {
        case AggregateFunction::min: {
            return sym.type() != SymbolType::sup;
        }
        case AggregateFunction::max: {
            return sym.type() != SymbolType::inf;
        }
        case AggregateFunction::sum: {
            return sym.type() == SymbolType::number && sym.num() != 0;
        }
        case AggregateFunction::sump: {
            return sym.type() == SymbolType::number && sym.num() > 0;
        }
        case AggregateFunction::count: {
            return true;
        }
    }
    Util::unreachable();
}
 
enum class TheoryTermTupleType : uint8_t {
    tuple, 
    set,   
    list   
};
 
enum class HeuristicType : uint8_t { level = 0, sign = 1, factor = 2, init = 3, true_ = 4, false_ = 5 };
auto operator<<(Util::OutputBuffer &out, HeuristicType type) -> Util::OutputBuffer &;
 
enum class ExternalType : uint8_t { free = 0, true_ = 1, false_ = 2, release = 3 };
auto operator<<(Util::OutputBuffer &out, ExternalType type) -> Util::OutputBuffer &;
 
using TheorySig = std::tuple<String, size_t>;
using TheorySigVec = std::vector<TheorySig>;
 
 
} // namespace CppClingo