Basic working version bound to Python

runtimeverification · Nov 24, 2023 · e2b3946 · e2b3946
1 parent 4db5e79
commit e2b3946
Show file tree

Hide file tree

Showing 5 changed files with 2,220 additions and 1 deletion.
diff --git a/bindings/core/src/core.cpp b/bindings/core/src/core.cpp
@@ -67,7 +67,15 @@ simplify(std::shared_ptr<KOREPattern> pattern, std::shared_ptr<KORESort> sort) {
 std::shared_ptr<KOREPattern> evaluate_function(
     std::string const &label,
     std::vector<std::shared_ptr<KOREPattern>> const &args) {
-  abort();
+  auto term_args = std::vector<void *>{};
+  for (auto const &arg : args) {
+    term_args.push_back(static_cast<void *>(construct_term(arg)));
+  }
+
+  auto tag = getTagForSymbolName(label.c_str());
+  auto result = evaluateFunctionSymbol(tag, term_args.data());
+
+  return term_to_pattern(static_cast<block *>(result));
 }
 
 bool is_sort_kitem(std::shared_ptr<KORESort> const &sort) {

diff --git a/bindings/python/runtime.cpp b/bindings/python/runtime.cpp
@@ -2,6 +2,7 @@
 #include <kllvm/bindings/core/core.h>
 
 #include <pybind11/pybind11.h>
+#include <pybind11/stl.h>
 
 // This header needs to be included last because it pollutes a number of macro
 // definitions into the global namespace.