diff --git a/tests/Makefile.am b/tests/Makefile.am
index b033d75de..9ff7351fc 100644
--- a/tests/Makefile.am
+++ b/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
diff --git a/tests/core/.gitignore b/tests/core/.gitignore
index ecd5f0560..d4ebfae45 100644
--- a/tests/core/.gitignore
+++ b/tests/core/.gitignore
@@ -43,6 +43,7 @@ Makefile
Makefile.in
maskacc
mempool
+minterm
mixprod
nequals
nenoform
diff --git a/tests/core/minterm.cc b/tests/core/minterm.cc
new file mode 100644
index 000000000..fe849aa61
--- /dev/null
+++ b/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 .
+
+#undef NDEBUG
+
+#include "config.h"
+
+#include
+#include
+
+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);
+
+
+}
diff --git a/tests/core/minterm.test b/tests/core/minterm.test
new file mode 100644
index 000000000..893813b6e
--- /dev/null
+++ b/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 .
+
+. ./defs
+
+set -e
+../minterm