Refactor subsort table code (#951)

The backend had duplicated logic in a couple of places to build the
subsort[^1] relation for a definition; this PR refactors that code to
live with `KOREDefinition` so that it can be more easily reused. I have
also taken the opportunity to pull some code out of the `AST.cpp`
monolith into a separate translation unit to make it easier to read.

No actual functionality is introduced here; it's just a refactoring to
move identical code inside a common method.

[^1]: Analogously for overloads as well

Author: Baltoli

include/kllvm/ast/AST.h

@@ -934,6 +934,26 @@ class KOREDefinition {
   void addAttribute(sptr<KORECompositePattern> Attribute);
   void print(std::ostream &Out, unsigned indent = 0) const;
 
+  /*
+   * Build this definition's subsort relation from axioms that have the
+   * `subsort` attribute.
+   *
+   * The returned map is as follows:
+   *
+   *   S |-> {T . S is a subsort of T}
+   */
+  SubsortMap getSubsorts() const;
+
+  /*
+   * Build this definition's overload relation from axioms that have the
+   * `overload` attribute.
+   *
+   * The returned map is as follows:
+   *
+   *  P |-> {Q . P is a more specific overload of Q}
+   */
+  SymbolMap getOverloads() const;
+
   const std::vector<sptr<KOREModule>> &getModules() const { return modules; }
   const KORECompositeSortDeclarationMapType &getSortDeclarations() const {
     return sortDeclarations;
@@ -969,27 +989,6 @@ void readMultimap(
 
 sptr<KOREPattern> stripRawTerm(sptr<KOREPattern> const &term);
 
-template <typename Elem, typename Hash, typename Equal>
-std::unordered_map<Elem *, std::unordered_set<Elem *, Hash, Equal>, Hash, Equal>
-transitiveClosure(std::unordered_map<
-                  Elem *, std::unordered_set<Elem *, Hash, Equal>, Hash, Equal>
-                      relations) {
-  bool dirty;
-  do {
-    dirty = false;
-    for (auto &entry : relations) {
-      SortSet newSucc;
-      for (auto &elem : entry.second) {
-        auto &relation = relations[elem];
-        for (auto elem2 : relation) {
-          dirty |= relations[entry.first].insert(elem2).second;
-        }
-      }
-    }
-  } while (dirty);
-  return relations;
-}
-
 namespace detail {
 
 template <typename T>

lib/ast/AST.cpp

@@ -1362,149 +1362,6 @@ void KOREModule::addDeclaration(sptr<KOREDeclaration> Declaration) {
   declarations.push_back(std::move(Declaration));
 }
 
-void KOREDefinition::addModule(sptr<KOREModule> Module) {
-  for (const auto &decl : Module->getDeclarations()) {
-    if (auto *sortDecl
-        = dynamic_cast<KORECompositeSortDeclaration *>(decl.get())) {
-      sortDeclarations.insert({sortDecl->getName(), sortDecl});
-      auto sort = KORECompositeSort::Create(sortDecl->getName());
-    } else if (
-        auto *symbolDecl = dynamic_cast<KORESymbolDeclaration *>(decl.get())) {
-      symbolDeclarations.insert(
-          {symbolDecl->getSymbol()->getName(), symbolDecl});
-    } else if (
-        auto *aliasDecl = dynamic_cast<KOREAliasDeclaration *>(decl.get())) {
-      aliasDeclarations.insert({aliasDecl->getSymbol()->getName(), aliasDecl});
-    } else if (auto *axiom = dynamic_cast<KOREAxiomDeclaration *>(decl.get())) {
-      axioms.push_back(axiom);
-    }
-  }
-  modules.push_back(std::move(Module));
-}
-
-void KOREDefinition::addAttribute(sptr<KORECompositePattern> Attribute) {
-  std::string name = Attribute->getConstructor()->getName();
-  attributes.insert({name, std::move(Attribute)});
-}
-
-void KOREDefinition::insertReservedSymbols() {
-  auto mod = KOREModule::Create("K-RAW-TERM");
-  auto decl = KORESymbolDeclaration::Create("rawTerm", true);
-  auto sort = KORECompositeSort::Create("SortKItem");
-
-  decl->getSymbol()->addSort(sort);
-  decl->getSymbol()->addArgument(sort);
-  mod->addDeclaration(std::move(decl));
-
-  addModule(std::move(mod));
-}
-
-// NOLINTNEXTLINE(*-cognitive-complexity)
-void KOREDefinition::preprocess() {
-  insertReservedSymbols();
-
-  for (auto *axiom : axioms) {
-    axiom->pattern = axiom->pattern->expandAliases(this);
-  }
-  auto symbols = std::map<std::string, std::vector<KORESymbol *>>{};
-  unsigned nextOrdinal = 0;
-  for (const auto &decl : symbolDeclarations) {
-    if (decl.second->getAttributes().count("freshGenerator")) {
-      auto sort = decl.second->getSymbol()->getSort();
-      if (sort->isConcrete()) {
-        freshFunctions[dynamic_cast<KORECompositeSort *>(sort.get())->getName()]
-            = decl.second->getSymbol();
-      }
-    }
-  }
-  for (auto iter = axioms.begin(); iter != axioms.end();) {
-    auto *axiom = *iter;
-    axiom->ordinal = nextOrdinal;
-    ordinals[nextOrdinal++] = axiom;
-    axiom->pattern->markSymbols(symbols);
-    if (!axiom->isRequired()) {
-      iter = axioms.erase(iter);
-    } else {
-      ++iter;
-    }
-  }
-  for (auto &module : modules) {
-    const auto &declarations = module->getDeclarations();
-    for (const auto &declaration : declarations) {
-      auto *decl = dynamic_cast<KORESymbolDeclaration *>(declaration.get());
-      if (decl == nullptr) {
-        continue;
-      }
-      if (decl->isHooked() && decl->getObjectSortVariables().empty()) {
-        KORESymbol *symbol = decl->getSymbol();
-        symbols.emplace(symbol->getName(), std::vector<KORESymbol *>{symbol});
-      }
-    }
-  }
-  for (const auto &entry : symbols) {
-    for (auto *symbol : entry.second) {
-      auto *decl = symbolDeclarations.at(symbol->getName());
-      symbol->instantiateSymbol(decl);
-    }
-  }
-  uint32_t nextSymbol = 0;
-  uint16_t nextLayout = 1;
-  auto instantiations = std::unordered_map<KORESymbol, uint32_t, HashSymbol>{};
-  auto layouts = std::unordered_map<std::string, uint16_t>{};
-  auto variables
-      = std::unordered_map<std::string, std::pair<uint32_t, uint32_t>>{};
-  for (const auto &entry : symbols) {
-    uint32_t firstTag = nextSymbol;
-    for (auto *symbol : entry.second) {
-      if (symbol->isConcrete()) {
-        if (!instantiations.count(*symbol)) {
-          instantiations.emplace(*symbol, nextSymbol++);
-        }
-        std::string layoutStr = symbol->layoutString(this);
-        if (!layouts.count(layoutStr)) {
-          layouts.emplace(layoutStr, nextLayout++);
-        }
-        symbol->firstTag = symbol->lastTag = instantiations.at(*symbol);
-        symbol->layout = layouts.at(layoutStr);
-        objectSymbols[symbol->firstTag] = symbol;
-        allObjectSymbols[ast_to_string(*symbol)] = symbol;
-      }
-    }
-    uint32_t lastTag = nextSymbol - 1;
-    if (!entry.second.empty()) {
-      variables.emplace(
-          entry.first, std::pair<uint32_t, uint32_t>{firstTag, lastTag});
-    }
-  }
-  for (const auto &entry : symbols) {
-    auto range = variables.at(entry.first);
-    for (auto *symbol : entry.second) {
-      for (const auto &sort : symbol->getArguments()) {
-        if (sort->isConcrete()) {
-          hookedSorts[dynamic_cast<KORECompositeSort *>(sort.get())
-                          ->getCategory(this)]
-              = std::dynamic_pointer_cast<KORECompositeSort>(sort);
-        }
-      }
-      if (symbol->getSort()->isConcrete()) {
-        hookedSorts[dynamic_cast<KORECompositeSort *>(symbol->getSort().get())
-                        ->getCategory(this)]
-            = std::dynamic_pointer_cast<KORECompositeSort>(symbol->getSort());
-      }
-      if (!symbol->isConcrete()) {
-        if (symbol->isPolymorphic()) {
-          symbol->firstTag = range.first;
-          symbol->lastTag = range.second;
-          auto *decl = symbolDeclarations.at(symbol->getName());
-          if (decl->getAttributes().count("sortInjection")) {
-            injSymbol = symbol;
-          }
-        }
-      }
-    }
-  }
-}
-
 // Pretty printer
 void KORESortVariable::print(std::ostream &Out, unsigned indent) const {
   std::string Indent(indent, ' ');

lib/ast/CMakeLists.txt

@@ -1,6 +1,7 @@
 add_library(AST
   AST.cpp
   pattern_matching.cpp
+  definition.cpp
 )
 
 target_link_libraries(AST