add axiom filtering property to python bindings (#1061)

This adds a boolean property to kore_axiom_declaration objects which will be `True` if the axiom is used by the LLVM backend and `False` if the LLVM backend filters it out.
runtimeverification · May 17, 2024 · e27ae13 · e27ae13
1 parent 73e5208
commit e27ae13
Show file tree

Hide file tree

Showing 3 changed files with 1,426 additions and 0 deletions.
diff --git a/bindings/python/ast.cpp b/bindings/python/ast.cpp
@@ -178,6 +178,8 @@ void bind_ast(py::module_ &m) {
           py::init(&kore_axiom_declaration::create),
           py::arg("is_claim") = false)
       .def_property_readonly("is_claim", &kore_axiom_declaration::is_claim)
+      .def_property_readonly(
+          "is_required", &kore_axiom_declaration::is_required)
       .def("add_pattern", &kore_axiom_declaration::add_pattern)
       .def_property_readonly("pattern", &kore_axiom_declaration::get_pattern)
       .def_property_readonly("requires", &kore_axiom_declaration::get_requires);