Merge remote-tracking branch 'origin/develop'

runtimeverification · Jun 6, 2024 · 6aa3ed2 · 6aa3ed2
2 parents 744a615 + 30495f7
commit 6aa3ed2
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 6 deletions.
diff --git a/bindings/python/ast.cpp b/bindings/python/ast.cpp
@@ -460,7 +460,7 @@ void bind_proof_trace(py::module_ &m) {
       proof_trace, "kore_header")
       .def(py::init(&kore_header::create), py::arg("path"));
 
-  py::enum_<llvm_event_type>(proof_trace, "LLVMEventType")
+  py::enum_<llvm_event_type>(proof_trace, "EventType")
       .value("PreTrace", llvm_event_type::PreTrace)
       .value("InitialConfig", llvm_event_type::InitialConfig)
       .value("Trace", llvm_event_type::Trace);
@@ -473,6 +473,7 @@ void bind_proof_trace(py::module_ &m) {
       llvm_rewrite_trace_iterator,
       std::shared_ptr<llvm_rewrite_trace_iterator>>(
       proof_trace, "llvm_rewrite_trace_iterator")
+      .def("__repr__", print_repr_adapter<llvm_rewrite_trace_iterator>(true))
       .def_static(
           "from_file",
           [](std::string const &filename, kore_header const &header) {

diff --git a/test/python/test_proof_trace.py b/test/python/test_proof_trace.py
@@ -72,30 +72,30 @@ def test_file(self):
 
         while True:
             event0 = it.get_next_event()
-            if event0.type != kllvm.prooftrace.LLVMEventType.PreTrace:
+            if event0.type != kllvm.prooftrace.EventType.PreTrace:
                 break
 
-        self.assertEqual(event0.type, kllvm.prooftrace.LLVMEventType.InitialConfig)
+        self.assertEqual(event0.type, kllvm.prooftrace.EventType.InitialConfig)
         self.assertTrue(event0.event.is_kore_pattern())
 
         event1 = it.get_next_event()
-        self.assertEqual(event1.type, kllvm.prooftrace.LLVMEventType.Trace)
+        self.assertEqual(event1.type, kllvm.prooftrace.EventType.Trace)
         self.assertTrue(event1.event.is_step_event())
         rule_ordinal = event1.event.step_event.rule_ordinal
         axiom = repr(definition.get_axiom_by_ordinal(rule_ordinal))
         axiom_expected = self.get_pattern_from_ordinal(definition_text, rule_ordinal)
         self.assertEqual(axiom, axiom_expected)
 
         event2 = it.get_next_event()
-        self.assertEqual(event2.type, kllvm.prooftrace.LLVMEventType.Trace)
+        self.assertEqual(event2.type, kllvm.prooftrace.EventType.Trace)
         self.assertTrue(event2.event.is_step_event())
         rule_ordinal = event2.event.step_event.rule_ordinal
         axiom = repr(definition.get_axiom_by_ordinal(rule_ordinal))
         axiom_expected = self.get_pattern_from_ordinal(definition_text, rule_ordinal)
         self.assertEqual(axiom, axiom_expected)
 
         event3 = it.get_next_event()
-        self.assertEqual(event3.type, kllvm.prooftrace.LLVMEventType.Trace)
+        self.assertEqual(event3.type, kllvm.prooftrace.EventType.Trace)
         self.assertTrue(event3.event.is_kore_pattern())
 
         self.assertEqual(it.get_next_event(), None)