From d33ecef98bd499d721f381e2c213d083bcd105af Mon Sep 17 00:00:00 2001 From: Roberto Rosmaninho Date: Wed, 18 Sep 2024 15:02:35 -0300 Subject: [PATCH] Exposing `llvm_pattern_matching_failure_event` to Python Bindings (#1148) We missed this feature while implementing the new step event; we now need to add it so the Pi2 MPG Team can handle it on the Python side. A subsequent K PR will also be necessary to correctly expose this feature. --- bindings/python/ast.cpp | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/bindings/python/ast.cpp b/bindings/python/ast.cpp index 28d04f9b2..99ee92de9 100644 --- a/bindings/python/ast.cpp +++ b/bindings/python/ast.cpp @@ -418,6 +418,14 @@ void bind_proof_trace(py::module_ &m) { .def_property_readonly( "check_result", &llvm_side_condition_end_event::get_result); + py::class_< + llvm_pattern_matching_failure_event, + std::shared_ptr>( + proof_trace, "llvm_pattern_matching_failure_event", step_event) + .def_property_readonly( + "function_name", + &llvm_pattern_matching_failure_event::get_function_name); + py::class_>( proof_trace, "llvm_function_event", step_event) .def_property_readonly("name", &llvm_function_event::get_name)