Stub out sort contains relation

Author: Baltoli

include/kllvm/ast/AST.h

@@ -938,6 +938,7 @@ class KOREDefinition {
   SubsortMap subsorts;
   SubsortMap supersorts;
   SymbolMap overloads;
+  SubsortMap sortContains;
 
   std::vector<sptr<KOREModule>> modules;
   std::unordered_map<std::string, sptr<KORECompositePattern>> attributes;
@@ -961,6 +962,7 @@ class KOREDefinition {
 
   void buildSubsortRelation();
   void buildOverloadRelation();
+  void buildSortContainsRelation();
 
 public:
   /*
@@ -1029,6 +1031,23 @@ class KOREDefinition {
    */
   SymbolMap getOverloads() const { return overloads; }
 
+  /*
+   * Return a relation specifying the set of sorts that may syntactically occur
+   * as children of another sort. For example, given symbols:
+   *
+   *   c(S_1, ..., S_N) : S_R
+   *   c(T_1, ..., T_N) : S_R
+   *
+   * The relation will contain an entry:
+   *
+   *   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
+   * `c` is of sort S_1, a term whose sort is a subsort of S_1 may also occur in
+   * the first argument position).
+   */
+  SubsortMap getSortContains() const { return sortContains; }
+
   std::vector<sptr<KOREModule>> const &getModules() const { return modules; }
   KORECompositeSortDeclarationMapType const &getSortDeclarations() const {
     return sortDeclarations;

lib/ast/definition.cpp

@@ -17,6 +17,7 @@ ptr<KOREDefinition> KOREDefinition::load(std::string const &filename) {
 void KOREDefinition::precompute() {
   buildSubsortRelation();
   buildOverloadRelation();
+  buildSortContainsRelation();
 }
 
 std::unordered_set<std::string>
@@ -103,6 +104,8 @@ void KOREDefinition::buildOverloadRelation() {
   overloads = transitive_closure(overloads);
 }
 
+void KOREDefinition::buildSortContainsRelation() { }
+
 // NOLINTNEXTLINE(*-function-cognitive-complexity)
 void KOREDefinition::preprocess() {
   insertReservedSymbols();