Implement sorted term -> pattern

runtimeverification · Dec 4, 2023 · 063b1f0 · 063b1f0
1 parent 452cecf
commit 063b1f0
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 4 deletions.
diff --git a/bindings/core/src/core.cpp b/bindings/core/src/core.cpp
@@ -78,9 +78,10 @@ std::shared_ptr<KOREPattern> evaluate_function(
   }
 
   auto tag = getTagForSymbolName(label.c_str());
+  auto return_sort = getReturnSortForTag(tag);
   auto result = evaluateFunctionSymbol(tag, term_args.data());
 
-  return term_to_pattern(static_cast<block *>(result));
+  return sortedTermToKorePattern(static_cast<block *>(result), return_sort);
 }
 
 bool is_sort_kitem(std::shared_ptr<KORESort> const &sort) {

diff --git a/include/runtime/header.h b/include/runtime/header.h
@@ -310,6 +310,8 @@ void printConfigurationInternal(
 // you can use the C bindings, which wrap the return value of this method in
 // a POD struct.
 std::shared_ptr<kllvm::KOREPattern> termToKorePattern(block *);
+std::shared_ptr<kllvm::KOREPattern>
+sortedTermToKorePattern(block *, const char *);
 
 // This function injects its argument into KItem before printing, using the sort
 // argument as the source sort. Doing so allows the term to be pretty-printed

diff --git a/runtime/util/ConfigurationSerializer.cpp b/runtime/util/ConfigurationSerializer.cpp
@@ -452,10 +452,18 @@ void serializeRawTermToFile(
   fclose(file);
 }
 
-std::shared_ptr<kllvm::KOREPattern> termToKorePattern(block *subject) {
+std::shared_ptr<kllvm::KOREPattern>
+sortedTermToKorePattern(block *subject, const char *sort) {
+  auto is_kitem = (std::string(sort) == "SortKItem{}");
+  block *term = is_kitem ? subject : constructRawTerm(subject, sort);
+
   char *data_out;
   size_t size_out;
 
-  serializeConfiguration(subject, "SortKItem{}", &data_out, &size_out, true);
-  return deserialize_pattern(data_out, data_out + size_out);
+  serializeConfiguration(term, "SortKItem{}", &data_out, &size_out, true);
+  return deserialize_pattern(data_out, data_out + size_out, true);
+}
+
+std::shared_ptr<kllvm::KOREPattern> termToKorePattern(block *subject) {
+  return sortedTermToKorePattern(subject, "SortKItem{}");
 }