From 75e552fdac8dff6d24b71117de0ff63cc5a6ad01 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Mon, 11 Mar 2024 17:38:52 +0100
Subject: [PATCH] python: add bindings for BuDDy's minterms_of

minterms_of was introduced in BuDDy with Spot 2.10, but
wasn't properly binded in Python.

* python/buddy.i: Add bindings.
* tests/python/bdditer.py: Test them.
---
 python/buddy.i          | 101 ++++++++++++++++++++++++++++++++++++++++
 tests/python/bdditer.py |   6 +++
 2 files changed, 107 insertions(+)

diff --git a/python/buddy.i b/python/buddy.i
index 99eb1cbb1..63156aa3d 100644
--- a/python/buddy.i
+++ b/python/buddy.i
@@ -57,14 +57,82 @@
 %module buddy
 
 %include "std_string.i"
+%include "std_container.i"
 
 %{
 #include <sstream>
+#include <iterator>
 #include "bddx.h"
 #include "fddx.h"
 #include "bvecx.h"
+
 %}
 
+
+// Swig come with iterators that implement a decrement method.  This
+// is not supported in our "successor" iterators.
+%fragment("ForwardNullTerminatedIterator_T","header",fragment="SwigPyIterator_T") {
+namespace swig
+{
+  template<typename OutIterator,
+	   typename ValueType =
+	   typename std::iterator_traits<OutIterator>::value_type,
+	   typename FromOper = from_oper<ValueType> >
+  class ForwardNullTerminatedIterator_T :  public SwigPyIterator
+  {
+  public:
+    FromOper from;
+    typedef OutIterator out_iterator;
+    typedef ValueType value_type;
+    typedef SwigPyIterator  base;
+
+    ForwardNullTerminatedIterator_T(out_iterator curr, PyObject *seq)
+    : SwigPyIterator(seq), current(curr)
+    {
+    }
+
+    PyObject *value() const {
+      if (current == nullptr) {
+	throw stop_iteration();
+      } else {
+	return from(static_cast<value_type>(*(current)));
+      }
+    }
+
+    SwigPyIterator *copy() const
+    {
+      return new ForwardNullTerminatedIterator_T(*this);
+    }
+
+    SwigPyIterator *incr(size_t n = 1)
+    {
+      while (n--) {
+	if (current == nullptr) {
+	  throw stop_iteration();
+	} else {
+	  ++current;
+	}
+      }
+      return this;
+    }
+
+  protected:
+    out_iterator current;
+  };
+
+
+  template<typename OutIter>
+  inline SwigPyIterator*
+  make_forward_null_terminated_iterator(const OutIter& begin, PyObject *seq = 0)
+  {
+    return new ForwardNullTerminatedIterator_T<OutIter>(begin, seq);
+  }
+}}
+%fragment("ForwardNullTerminatedIterator_T");
+
+%traits_swigtype(bdd);
+%fragment(SWIG_Traits_frag(bdd));
+
 %typemap(in) (int* input_buf, int input_buf_size) {
   if (!PySequence_Check($input))
     {
@@ -362,3 +430,36 @@ class bvec
     return (*self)[i];
   }
 }
+
+
+class minterms_of
+{
+public:
+  class minterm_iterator
+  {
+  public:
+    minterm_iterator(minterms_of* me);
+    minterm_iterator& operator++();
+    void operator++(int);
+    bool operator==(std::nullptr_t) const;
+    bool operator!=(std::nullptr_t) const;
+    bdd operator*() const;
+  };
+
+  minterms_of(bdd fun, bdd vars);
+  ~minterms_of();
+  minterm_iterator begin();
+  std::nullptr_t end() const;
+  bool done() const;
+  bdd operator*() const;
+  void operator++();
+};
+
+%extend minterms_of {
+  %newobject __iter__(PyObject **PYTHON_SELF);
+  swig::SwigPyIterator* __iter__(PyObject **PYTHON_SELF)
+   {
+      return swig::make_forward_null_terminated_iterator(self->begin(),
+                                                         *PYTHON_SELF);
+   }
+}
diff --git a/tests/python/bdditer.py b/tests/python/bdditer.py
index 2cee87a4e..a49ab8dde 100644
--- a/tests/python/bdditer.py
+++ b/tests/python/bdditer.py
@@ -65,6 +65,12 @@ del res2
 del c
 gcollect()
 
+res3 = []
+for i in buddy.minterms_of(buddy.bddtrue, run.aut.ap_vars()):
+    res3.append(str(spot.bdd_to_formula(i)))
+tc.assertEqual(res3, ['!a & !b', '!a & b', 'a & !b', 'a & b'])
+gcollect()
+
 f = spot.bdd_to_formula(b)
 tc.assertTrue(f._is(spot.op_And))
 tc.assertTrue(f[0]._is(spot.op_ap))