test minterms_of enumerator

* tests/core/minterm.cc, tests/core/minterm.test: New files.
* tests/core/.gitignore, tests/Makefile.am: Add them.

tests/Makefile.am

@@ -1,5 +1,5 @@
 ## -*- coding: utf-8 -*-
-## Copyright (C) 2009-2020 Laboratoire de Recherche et Développement
+## Copyright (C) 2009-2021 Laboratoire de Recherche et Développement
 ## de l'Epita (LRDE).
 ## Copyright (C) 2003-2006 Laboratoire d'Informatique de Paris 6
 ## (LIP6), département Systèmes Répartis Coopératifs (SRC), Université
@@ -85,6 +85,7 @@ check_PROGRAMS = \
   core/ltlrel \
   core/lunabbrev \
   core/mempool \
+  core/minterm \
   core/nequals \
   core/nenoform \
   core/ngraph \
@@ -134,6 +135,7 @@ core_ltl2text_SOURCES = core/readltl.cc
 core_ltlrel_SOURCES = core/ltlrel.cc
 core_lunabbrev_SOURCES = core/equalsf.cc
 core_lunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DUNABBREV='"^ie"'
+core_minterm_SOURCES = core/minterm.cc
 core_nenoform_SOURCES = core/equalsf.cc
 core_nenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM
 core_nequals_SOURCES = core/equalsf.cc
@@ -211,6 +213,7 @@ TESTS_misc = \
   core/bitvect.test \
   core/bricks.test \
   core/intvcomp.test \
+  core/minterm.test \
   core/minusx.test \
   core/full.test \
   core/trival.test

tests/core/.gitignore

@@ -43,6 +43,7 @@ Makefile
 Makefile.in
 maskacc
 mempool
+minterm
 mixprod
 nequals
 nenoform

tests/core/minterm.cc

@@ -0,0 +1,173 @@
+// -*- coding: utf-8 -*-
+// Copyright (C) 2021 Laboratoire de Recherche et Développement
+// de l'Epita.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 3 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+#undef NDEBUG
+
+#include "config.h"
+
+#include <bddx.h>
+#include <cassert>
+
+int main()
+{
+  bdd_init(10000, 10000);
+  bdd_setvarnum(5);
+
+  bdd a = bdd_ithvar(0);
+  bdd b = bdd_ithvar(1);
+  bdd c = bdd_ithvar(2);
+  bdd d = bdd_ithvar(3);
+  bdd e = bdd_ithvar(4);
+
+  bdd fun = a | (b & d);
+  bdd var = a & b & c & d & e;
+  std::cout << fun << '\n';
+  std::cout << var << "\n\n";
+  bdd sum = bddfalse;
+  int count = 0;
+  for (auto minterm: minterms_of(fun, var))
+    {
+      ++count;
+      sum |= minterm;
+    }
+  assert(count == 20);
+  assert(fun == sum);
+
+  var = a & b & d;
+  std::cout << fun << '\n';
+  std::cout << var << "\n\n";
+  sum = bddfalse;
+  count = 0;
+  for (auto minterm: minterms_of(fun, var))
+    {
+      ++count;
+      sum |= minterm;
+    }
+  assert(count == 5);
+  assert(fun == sum);
+
+  fun = bddtrue;
+  std::cout << fun << '\n';
+  std::cout << var << "\n\n";
+  sum = bddfalse;
+  count = 0;
+  for (auto minterm: minterms_of(fun, var))
+    {
+      ++count;
+      sum |= minterm;
+    }
+  assert(count == 8);
+  assert(fun == sum);
+
+  fun = var;
+  std::cout << fun << '\n';
+  std::cout << var << "\n\n";
+  sum = bddfalse;
+  count = 0;
+  for (auto minterm: minterms_of(fun, var))
+    {
+      ++count;
+      sum |= minterm;
+    }
+  assert(count == 1);
+  assert(fun == sum);
+
+  fun = var = bddtrue;
+  std::cout << fun << '\n';
+  std::cout << var << "\n\n";
+  sum = bddfalse;
+  count = 0;
+  for (auto minterm: minterms_of(fun, var))
+    {
+      ++count;
+      sum |= minterm;
+    }
+  assert(count == 1);
+  assert(fun == sum);
+
+  fun = bddfalse;
+  std::cout << fun << '\n';
+  std::cout << var << "\n\n";
+  sum = bddfalse;
+  count = 0;
+  for (auto minterm: minterms_of(fun, var))
+    {
+      ++count;
+      sum |= minterm;
+    }
+  assert(count == 0);
+  assert(fun == sum);
+
+  fun = (!a) | b;
+  var = a & b;
+  std::cout << fun << '\n';
+  std::cout << var << "\n\n";
+  sum = bddfalse;
+  count = 0;
+  for (auto minterm: minterms_of(fun, var))
+    {
+      ++count;
+      sum |= minterm;
+    }
+  assert(count == 3);
+  assert(fun == sum);
+
+  fun = b;
+  var = a & b;
+  std::cout << fun << '\n';
+  std::cout << var << "\n\n";
+  sum = bddfalse;
+  count = 0;
+  for (auto minterm: minterms_of(fun, var))
+    {
+      ++count;
+      sum |= minterm;
+    }
+  assert(count == 2);
+  assert(fun == sum);
+
+  fun = a;
+  std::cout << fun << '\n';
+  std::cout << var << "\n\n";
+  sum = bddfalse;
+  count = 0;
+  for (auto minterm: minterms_of(fun, var))
+    {
+      ++count;
+      sum |= minterm;
+    }
+  assert(count == 2);
+  assert(fun == sum);
+
+  fun = ((!a)&d) | (b&c&d);
+  var = a & b & c & d;
+  std::cout << fun << '\n';
+  std::cout << var << "\n\n";
+  sum = bddfalse;
+  count = 0;
+  for (auto minterm: minterms_of(fun, var))
+    {
+      ++count;
+      sum |= minterm;
+    }
+  assert(count == 5);
+  assert(fun == sum);
+
+
+}

tests/core/minterm.test

@@ -0,0 +1,23 @@
+#!/bin/sh
+# -*- coding: utf-8 -*-
+# Copyright (C) 2021 Laboratoire de Recherche et Développement de l'Epita.
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 3 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with this program.  If not, see <http://www.gnu.org/licenses/>.
+
+. ./defs
+
+set -e
+../minterm