analyze.hh

#pragma once
 
#include <clingo/input/statement.hh>
 
#include <clingo/core/logger.hh>
 
#include <cstring>
 
namespace CppClingo::Input {
 
 
enum class TermCheckType : uint8_t {
    atom,              
    sig,               
    identifier,        
    signed_identifier, 
    pos_number         
};
 
struct CheckTypeResult {
    bool has_sign = false;
    Number const *pos_number = nullptr;
    String identifier;
};
 
[[nodiscard]] auto check_type(Term const &term, TermCheckType type, CheckTypeResult *res = nullptr) -> bool;
 
class LinearTerm {
  public:
    [[nodiscard]] auto m() const -> Number const & { return std::get<TermSymbol>(term_m()).value().num(); }
    [[nodiscard]] auto n() const -> Number const & { return std::get<TermSymbol>(term_n()).value().num(); }
    [[nodiscard]] auto x() const -> String { return std::get<TermVariable>(term_x()).name(); }
    [[nodiscard]] auto term_m() const -> Term const & { return *std::get<TermBinary>(term_mx()).lhs(); }
    [[nodiscard]] auto term_n() const -> Term const & { return mxn_->rhs(); }
    [[nodiscard]] auto term_x() const -> Term const & { return *std::get<TermBinary>(term_mx()).rhs(); }
    [[nodiscard]] auto term_mx() const -> Term const & { return mxn_->lhs(); }
    [[nodiscard]] auto term_mxn() const -> TermBinary const & { return *mxn_; }
 
    friend auto check_linear(TermBinary const &term) -> std::optional<LinearTerm>;
 
  private:
    LinearTerm(TermBinary const &mxn) : mxn_{&mxn} {}
 
    TermBinary const *mxn_;
};
 
[[nodiscard]] auto is_linear(Term const &term) -> bool;
 
[[nodiscard]] auto is_linear(TermBinary const &term) -> bool;
 
auto check_linear(TermBinary const &term) -> std::optional<LinearTerm>;
 
auto check_linear(Term const &term) -> std::optional<LinearTerm>;
 
[[nodiscard]] auto is_interval(Term const &term) -> bool;
 
[[nodiscard]] auto is_external(Term const &term) -> bool;
 
[[nodiscard]] auto is_interval(TermBinary const &term) -> bool;
 
[[nodiscard]] auto always_numeric(Term const &term) -> bool;
 
[[nodiscard]] auto never_numeric(Term const &term) -> bool;
 
[[nodiscard]] inline auto is_symbol(Term const &term) -> bool {
    return std::holds_alternative<TermSymbol>(term);
}
 
[[nodiscard]] inline auto is_variable(Term const &term) -> bool {
    return std::holds_alternative<TermVariable>(term);
}
 
[[nodiscard]] inline auto is_fixed(Lit const &lit) -> std::optional<bool> {
    if (auto const *blit = std::get_if<LitBool>(&lit); blit != nullptr) {
        return blit->value() == (blit->sign() != Sign::once);
    }
    return std::nullopt;
}
 
[[nodiscard]] auto is_atom(Term const &term) -> bool;
 
[[nodiscard]] auto is_atom(Lit const &lit) -> bool;
 
[[nodiscard]] auto is_atom(HdLit const &lit) -> bool;
 
[[nodiscard]] auto is_atom(BdLit const &lit) -> bool;
 
[[nodiscard]] inline auto is_boolean(Lit const &lit) -> std::optional<bool> {
    if (auto const *lb = std::get_if<LitBool>(&lit); lb != nullptr) {
        return lb->value() == (lb->sign() != Sign::once);
    }
    return std::nullopt;
}
 
[[nodiscard]] auto is_test(BdLit const &lit) -> bool;
 
[[nodiscard]] auto is_classical(HdLit const &lit) -> bool;
 
[[nodiscard]] auto is_fact(SymbolStore &store, StmRule const &rule) -> std::optional<Symbol>;
 
[[nodiscard]] auto is_fact(SymbolStore &store, Stm const &stm) -> std::optional<Symbol>;
 
[[nodiscard]] auto check_global(Logger &log, VariableSet const &global, Stm const &stm) -> bool;
 
[[nodiscard]] inline auto is_theory_operator(std::string_view name) -> bool {
    return (!name.empty() && std::strchr("/!<=>+-*\\?&@|:;~^.", name.front()) != nullptr) || (name == "not");
}
 
[[nodiscard]] auto signature(Term const &term) -> std::optional<std::tuple<String, size_t, bool>>;
 
[[nodiscard]] auto is_matchable(Term const &term) -> bool;
 
void extract_can_fail(Term const &term, std::vector<Term> &result);
 
 
} // namespace CppClingo::Input