bdd_to_formula: add CNF variant

* spot/twa/formula2bdd.hh,
spot/twa/formula2bdd.cc (bdd_to_cnf_formula): New function.
* python/spot/__init__.py: Add a default dictionary for convenience.
* tests/python/bdditer.py: Add test cases.
* NEWS: Mention it.

NEWS

@@ -14,6 +14,9 @@ New in spot 2.11.4.dev  (not yet released)
     supports only one): it now reuse the edges leaving initial states
     without incoming transitions.
 
+  - spot::bdd_to_cnf_formula() is a new variant of spot::bdd_to_formula()
+    that converts a BDD into a CNF instead of a DNF.
+
   Python:
 
   - spot.acd() no longer depends on jQuery for interactivity.

python/spot/__init__.py

@@ -1,6 +1,6 @@
 # -*- coding: utf-8 -*-
-# Copyright (C) 2014-2022  Laboratoire de
+# Copyright (C) 2014-2023 Laboratoire de Recherche et Développement de
-# Recherche et Développement de l'Epita (LRDE).
+# l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
 #
@@ -1347,6 +1347,10 @@ def bdd_to_formula(b, dic=_bdd_dict):
     from spot.impl import bdd_to_formula as bf
     return bf(b, dic)
 
+def bdd_to_cnf_formula(b, dic=_bdd_dict):
+    from spot.impl import bdd_to_cnf_formula as bf
+    return bf(b, dic)
+
 
 def language_containment_checker(dic=_bdd_dict):
     from spot.impl import language_containment_checker as c

spot/twa/formula2bdd.cc

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2009-2019 Laboratoire de Recherche et Développement
+// Copyright (C) 2009-2019, 2023 Laboratoire de Recherche et Développement
 // de l'Epita (LRDE).
 // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris
 // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
@@ -30,11 +30,14 @@ namespace spot
   namespace
   {
     // Convert a BDD which is known to be a conjonction into a formula.
+    // If dual is true, dualize the result, i.e., negate literals, and
+    // exchange ∧ and ∨.
+    template<bool dual>
     static formula
     conj_to_formula(bdd b, const bdd_dict_ptr d)
     {
       if (b == bddfalse)
-        return formula::ff();
+        return dual ? formula::tt() : formula::ff();
       std::vector<formula> v;
       while (b != bddtrue)
         {
@@ -49,11 +52,14 @@ namespace spot
           bdd high = bdd_high(b);
           if (high == bddfalse)
             {
+              if (!dual)
                 res = formula::Not(res);
               b = bdd_low(b);
             }
           else
             {
+              if (dual)
+                res = formula::Not(res);
               // If bdd_low is not false, then b was not a conjunction.
               assert(bdd_low(b) == bddfalse);
               b = high;
@@ -61,7 +67,7 @@ namespace spot
           assert(b != bddfalse);
           v.emplace_back(res);
         }
-      return formula::And(v);
+      return dual ? formula::Or(v) : formula::And(v);
     }
   } // anonymous
 
@@ -143,7 +149,23 @@ namespace spot
     minato_isop isop(f);
     bdd cube;
     while ((cube = isop.next()) != bddfalse)
-      v.emplace_back(conj_to_formula(cube, d));
+      v.emplace_back(conj_to_formula<false>(cube, d));
     return formula::Or(std::move(v));
   }
+
+  formula
+  bdd_to_cnf_formula(bdd f, const bdd_dict_ptr d)
+  {
+    if (f == bddtrue)
+      return formula::tt();
+
+    std::vector<formula> v;
+
+    minato_isop isop(!f);
+    bdd cube;
+    while ((cube = isop.next()) != bddfalse)
+      v.emplace_back(conj_to_formula<true>(cube, d));
+    return formula::And(std::move(v));
+  }
+
 }

spot/twa/formula2bdd.hh

@@ -1,5 +1,5 @@
 // -*- coding: utf-8 -*-
-// Copyright (C) 2012, 2013, 2014, 2015 Laboratoire de Recherche et
+// Copyright (C) 2012-2015, 2023 Laboratoire de Recherche et
 // Développement de l'Epita (LRDE).
 // Copyright (C) 2003  Laboratoire d'Informatique de Paris 6 (LIP6),
 // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@@ -52,12 +52,21 @@ namespace spot
 
   /// \brief Convert a BDD into a formula.
   ///
-  /// Format the BDD as an irredundant sum of product (see the
+  /// Format the BDD as a Boolean spot::formula object. This works only
-  /// minato_isop class for details) and map the BDD variables back
+  /// for Boolean formulas, and all the BDD variables used in \a f
-  /// into their atomic propositions.  This works only for Boolean
+  /// should have been registered in \a d.  Although the result has
-  /// formulas, and all the BDD variables used in \a f should have
+  /// type formula, it obviously does not use any temporal operator.
-  /// been registered in \a d.  Although the result has type
+  ///
-  /// formula, it obviously does not use any temporal operator.
+  /// The bdd_to_formula() version produces an irredundant sum of
+  /// product (see the minato_isop class for details) and map the BDD
+  /// variables back into their atomic propositions.
+  ///
+  /// The bdd_to_cnf_formula() version produces an irredundant product of
+  /// sum, using the dual construction.
+  /// @{
   SPOT_API
   formula bdd_to_formula(bdd f, const bdd_dict_ptr d);
+  SPOT_API
+  formula bdd_to_cnf_formula(bdd f, const bdd_dict_ptr d);
+  /// @}
 }

tests/python/bdditer.py

@@ -1,5 +1,5 @@
 # -*- mode: python; coding: utf-8 -*-
-# Copyright (C) 2017, 2018, 2021, 2022 Laboratoire de Recherche et
+# Copyright (C) 2017, 2018, 2021, 2022, 2023 Laboratoire de Recherche et
 # Développement de l'Epita (LRDE).
 #
 # This file is part of Spot, a model checking library.
@@ -27,6 +27,19 @@ import sys
 from unittest import TestCase
 tc = TestCase()
 
+# CPython use reference counting, so that automata are destructed
+# when we expect them to be.   However other implementations like
+# PyPy may call destructors latter, causing different output.
+from platform import python_implementation
+if python_implementation() == 'CPython':
+    def gcollect():
+        pass
+else:
+    import gc
+    def gcollect():
+        gc.collect()
+
+
 run = spot.translate('a & !b').accepting_run()
 b = run.prefix[0].label
 c = buddy.bdd_satone(b)
@@ -43,12 +56,15 @@ while c != buddy.bddtrue:
         c = h
 
 tc.assertEqual(res, [0, -1])
+del res
 
 res2 = []
 for i in run.aut.ap():
     res2.append((str(i), run.aut.register_ap(i)))
 tc.assertEqual(str(res2), "[('a', 0), ('b', 1)]")
-
+del res2
+del c
+gcollect()
 
 f = spot.bdd_to_formula(b)
 tc.assertTrue(f._is(spot.op_And))
@@ -56,9 +72,50 @@ tc.assertTrue(f[0]._is(spot.op_ap))
 tc.assertTrue(f[1]._is(spot.op_Not))
 tc.assertTrue(f[1][0]._is(spot.op_ap))
 tc.assertEqual(str(f), 'a & !b')
+del f
+gcollect()
 
 try:
     f = spot.bdd_to_formula(b, spot.make_bdd_dict())
     sys.exit(2)
 except RuntimeError as e:
     tc.assertIn("not in the dictionary", str(e))
+
+f = spot.bdd_to_cnf_formula(b)
+tc.assertEqual(str(f), 'a & !b')
+
+del run
+del f
+
+gcollect()
+
+f = spot.bdd_to_cnf_formula(buddy.bddtrue)
+tc.assertEqual(str(f), '1')
+del f
+gcollect()
+
+f = spot.bdd_to_cnf_formula(buddy.bddfalse)
+tc.assertEqual(str(f), '0')
+del f
+gcollect()
+
+aut = spot.translate('(a & b) <-> c')
+# With pypy, running GC here will destroy the translator object used
+# by translate().  That object has temporary automata that reference
+# the BDDs variables and those affect the order in which the
+# bdd_to_formula() result is object is presented.  The different order
+# is not wrong, but it makes it diffuclt to write tests.
+gcollect()
+
+for e in aut.out(aut.get_init_state_number()):
+    b = e.cond
+    break
+
+f1 = spot.bdd_to_formula(b)
+tc.assertEqual(str(f1), '(!a & !c) | (a & b & c) | (!b & !c)')
+f2 = spot.bdd_to_cnf_formula(b)
+tc.assertEqual(str(f2), '(a | !c) & (!a | !b | c) & (b | !c)')
+
+b1 = spot.formula_to_bdd(f1, spot._bdd_dict, aut)
+b2 = spot.formula_to_bdd(f2, spot._bdd_dict, aut)
+tc.assertEqual(b1, b2)