Initial version of sort-contains

Author: Baltoli

include/kllvm/ast/AST.h

@@ -1040,9 +1040,9 @@ class KOREDefinition {
    *
    * The relation will contain an entry:
    *
-   *   S_R |-> { S_1, S'_1, ..., S_N, T_1, ..., T_N }
+   *   S_R |-> { S_R, S'_R, S_1, S'_1, ..., S_N, T_1, ..., T_N }
    *
-   * where S'_1 is a _subsort_ of S_1 (that is, given that the first argument of
+   * where S'_X is a _subsort_ of S_X (that is, given that the first argument of
    * `c` is of sort S_1, a term whose sort is a subsort of S_1 may also occur in
    * the first argument position).
    */

include/kllvm/util/transitive_closure.h

@@ -29,6 +29,15 @@ Map transitive_closure(Map relations) {
   return relations;
 }
 
+template <typename Map>
+Map reflexive_closure(Map relations) {
+  for (auto &[from, to_set] : relations) {
+    to_set.insert(from);
+  }
+
+  return relations;
+}
+
 } // namespace kllvm
 
 #endif

lib/ast/definition.cpp

@@ -3,6 +3,7 @@
 #include <kllvm/parser/KOREParser.h>
 #include <kllvm/util/transitive_closure.h>
 
+#include <iostream>
 #include <string>
 #include <unordered_set>
 
@@ -104,7 +105,53 @@ void KOREDefinition::buildOverloadRelation() {
   overloads = transitive_closure(overloads);
 }
 
-void KOREDefinition::buildSortContainsRelation() { }
+void KOREDefinition::buildSortContainsRelation() {
+  auto const &supersorts = getSupersorts();
+
+  for (auto const &[name, decl] : getSymbolDeclarations()) {
+    auto const &atts = decl->getAttributes();
+    if (atts.find("function") != atts.end()) {
+      // TODO: exclude collection sorts
+      continue;
+    }
+
+    auto *symbol = decl->getSymbol();
+    auto const &return_sort
+        = std::dynamic_pointer_cast<KORECompositeSort>(symbol->getSort());
+    if (!return_sort) {
+      continue;
+    }
+
+    auto &children = sortContains[return_sort.get()];
+    children.insert(return_sort.get());
+
+    for (auto const &arg : symbol->getArguments()) {
+      children.insert(arg.get());
+    }
+
+    auto subsorts = std::vector<KORESort *>{};
+    for (auto const &child_sort : children) {
+      if (supersorts.find(child_sort) != supersorts.end()) {
+        for (auto const &child_subsort : supersorts.at(child_sort)) {
+          subsorts.push_back(child_subsort);
+        }
+      }
+    }
+
+    std::copy(
+        subsorts.begin(), subsorts.end(),
+        std::inserter(children, children.begin()));
+  }
+
+  sortContains = transitive_closure(sortContains);
+
+  // Hooked sorts produce empty relations in the transitive closure because they
+  // cannot occur as the return sort of a constructor symbol, and cannot be
+  // subsorted. However, we want the relation to encode that a term of hooked
+  // sort H _can_ contain a term of hooked sort H, and so we take the reflexive
+  // closure of the transitive closure to ensure this.
+  sortContains = reflexive_closure(sortContains);
+}
 
 // NOLINTNEXTLINE(*-function-cognitive-complexity)
 void KOREDefinition::preprocess() {