rewrite_context.hh

#pragma once
 
#include <clingo/input/program.hh>
 
#include <clingo/util/ordered_set.hh>
#include <clingo/util/unordered_map.hh>
 
namespace CppClingo::Input {
 
 
enum class Arity : uint8_t {
    unary = 0,  
    binary = 1, 
};
 
enum class Associativity : uint8_t {
    left = 0,      
    right = 1,     
    non_assoc = 2, 
};
 
class TheoryTermParser {
  public:
    void add(Logger &log, TheoryOpDefinition const &def);
 
    void check_operator(Logger &log, String op, Arity arity, Location const &loc) const;
 
    auto parse(Logger &log, TheoryTermUnparsed const &term) const -> TheoryTerm;
 
    [[nodiscard]] auto has_error() const { return has_error_; }
 
  private:
    using Table = Util::unordered_map<std::pair<SharedString, Arity>, std::pair<int, Associativity>>;
    using Stack = std::vector<std::pair<SharedString, Arity>>;
    using Terms = std::vector<TheoryTerm>;
 
    auto priority_and_associativity_(String op) const -> std::pair<int, Associativity>;
 
    auto priority_(String op, Arity arity) const -> int;
 
    auto check_(String op) const -> bool;
 
    void reduce_() const;
 
    Table table_;
    mutable Terms terms_;
    mutable Stack stack_;
    mutable bool has_error_ = false;
};
 
class TheoryAtomParser {
  public:
    void add_theory(Logger &log, StmTheory const &stm);
 
    template <bool has_sign>
    auto parse(Logger &log, TheoryAtom<has_sign> const &atom, bool fact) const -> std::optional<TheoryAtom<has_sign>>;
 
    [[nodiscard]] auto has_error() const -> bool;
 
  private:
    using ParserIndex = size_t;
    using GuardTable = std::pair<SharedStringSet, ParserIndex>;
    using AtomTable = Util::unordered_map<std::pair<SharedString, size_t>,
                                          std::tuple<TheoryAtomType, ParserIndex, std::optional<GuardTable>>>;
 
    std::vector<TheoryTermParser> term_parsers_;
    AtomTable atom_table_;
    mutable bool has_error_ = false;
};
 
using AuxTermVec = std::vector<std::pair<Term, Term>>;
 
using ParamMap = Util::ordered_set<SharedString>;
 
class RewriteContext {
  public:
    struct pop_ {
        void operator()(RewriteContext *ctx) const {
            if (ctx != nullptr) {
                ctx->pop();
                ctx = nullptr;
            }
        }
    };
    using Guard = std::unique_ptr<RewriteContext, pop_>;
    RewriteContext(Logger &log, SymbolStore &store, RewriteOptions const &opts, TheoryAtomParser const &parser,
                   ParamMap const &param_map, ConstMap const &const_map)
        : log_{log}, opts_{opts}, parser_{parser}, const_map_{const_map}, param_map_{param_map}, gen_{store, {}, "_A"} {
    }
    RewriteContext(RewriteContext &&) noexcept = delete;
    void init(StringSet names, char const *prefix) {
        aux_.clear();
        gen_.init(std::move(names), prefix);
    }
    [[nodiscard]] auto logger() const -> Logger & { return log_; }
    [[nodiscard]] auto options() const -> RewriteOptions const & { return opts_; }
    [[nodiscard]] auto parser() const -> TheoryAtomParser const & { return parser_; }
    [[nodiscard]] auto store() const -> SymbolStore & { return gen_.store(); }
    [[nodiscard]] auto gen() -> NameGen & { return gen_; }
    [[nodiscard]] auto is_param(String name) const -> std::optional<size_t> {
        if (auto it = param_map_.find(name); it != param_map_.end()) {
            return std::distance(param_map_.begin(), it);
        }
        return std::nullopt;
    }
    [[nodiscard]] auto is_const(String name) const -> std::optional<Symbol> {
        if (auto it = const_map_.find(name); it != const_map_.end()) {
            assert(!is_param(name));
            return *it->second.second;
        }
        return std::nullopt;
    }
    [[nodiscard]] auto has_params() const -> bool { return !const_map_.empty() || !param_map_.empty(); }
    [[nodiscard]] auto aux() -> AuxTermVec & {
        assert(!aux_.empty());
        return aux_.back();
    }
    void pop() {
        assert(!aux_.empty());
        aux_.pop_back();
    }
    [[nodiscard]] auto push() -> Guard {
        aux_.emplace_back();
        return Guard{this};
    }
 
    void set_error() { has_error_ = true; }
 
    [[nodiscard]] auto has_error() const -> bool { return has_error_; }
 
  private:
    Logger &log_;                    
    RewriteOptions const &opts_;     
    TheoryAtomParser const &parser_; 
    ConstMap const &const_map_;      
    ParamMap const &param_map_;      
    NameGen gen_;                    
    std::vector<AuxTermVec> aux_;    
    bool has_error_ = false;         
};
 
 
} // namespace CppClingo::Input