acc: implement to_dnf() using BDDs

This way we have for instance
  (Inf(1) | Fin(2)) & (Fin(1) | Inf(3)) & Inf(0)
converted into just
  (Fin(1) & Fin(2) & Inf(0)) | (Inf(0)&Inf(1)&Inf(3))
while previously we would produce 4 terms:
  (Fin(2) & Fin(1) & Inf(0)) | (Fin(2) & (Inf(0)&Inf(3)))
  | (Fin(1) & (Inf(0)&Inf(1))) | (Inf(0)&Inf(1)&Inf(3))

* src/tgba/acc.cc (to_dnf): Recode it.
* src/tgbatest/acc2.test: Adjust.

src/tgba/acc.cc

@@ -21,6 +21,8 @@
 #include <iostream>
 #include <set>
 #include "acc.hh"
+#include "priv/bddalloc.hh"
+#include "misc/minato.hh"
 
 namespace spot
 {
@@ -334,7 +336,7 @@ namespace spot
 
   namespace
   {
-    std::set<acc_cond::acc_code> to_dnf_rec(const acc_cond::acc_word* c)
+    bdd to_bdd_rec(const acc_cond::acc_word* c, const bdd* map)
     {
       auto sz = c->size;
       auto start = c - sz - 1;
@@ -345,10 +347,10 @@ namespace spot
 	case acc_cond::acc_op::Or:
 	  {
 	    --c;
+	    bdd res = bddfalse;
 	    do
 	      {
-		for (auto& i: to_dnf_rec(c))
+		res |= to_bdd_rec(c, map);
-		  res.emplace(std::move(i));
 		c -= c->size + 1;
 	      }
 	    while (c > start);
@@ -356,22 +358,11 @@ namespace spot
 	  }
 	case acc_cond::acc_op::And:
 	  {
-	    std::set<acc_cond::acc_code> old;
-	    // Add true to the set.
-	    res.emplace(acc_cond::acc_code());
 	    --c;
+	    bdd res = bddtrue;
 	    do
 	      {
-		old.clear();
+		res &= to_bdd_rec(c, map);
-		std::swap(res, old);
-		// AND any element in the set with the DNF of c.
-		for (auto& i: to_dnf_rec(c))
-		  for (auto& j: old)
-		    {
-		      auto ac = i;
-		      ac.append_and(j);
-		      res.insert(ac);
-		    }
 		c -= c->size + 1;
 	      }
 	    while (c > start);
@@ -379,33 +370,25 @@ namespace spot
 	  }
 	case acc_cond::acc_op::Fin:
 	  {
-	    acc_cond::acc_code w;
+	    bdd res = bddfalse;
-	    w.resize(2);
-	    w[1].op = acc_cond::acc_op::Fin;
-	    w[1].size = 1;
 	    for (auto i: c[-1].mark.sets())
-	      {
+	      res |= !map[i];
-		w[0].mark = 0U;
+	    return res;
-		w[0].mark.set(i);
-		res.insert(w);
-	      }
-	    if (!res.empty())
-	      return res;
-	    /* fall through to handle false */;
 	  }
 	case acc_cond::acc_op::Inf:
 	  {
-	    acc_cond::acc_code w;
+	    bdd res = bddtrue;
-	    w.insert(w.begin(), c - 1, c + 1);
+	    for (auto i: c[-1].mark.sets())
-	    return { w };
+	      res &= map[i];
+	    return res;
 	  }
 	case acc_cond::acc_op::InfNeg:
 	case acc_cond::acc_op::FinNeg:
 	  SPOT_UNREACHABLE();
-	  return std::set<acc_cond::acc_code>{};
+	  return bddfalse;
 	}
       SPOT_UNREACHABLE();
-      return std::set<acc_cond::acc_code>{};
+      return bddfalse;
     }
   }
 
@@ -413,20 +396,70 @@ namespace spot
   {
     if (empty())
       return *this;
-    acc_cond::acc_code res;
+
-    unsigned count = 0;
+    auto used = acc_cond::acc_code::used_sets();
-    for (auto&i : to_dnf_rec(&back()))
+    unsigned c = used.count();
+
+    bdd_allocator ba;
+    int base = ba.allocate_variables(c);
+    std::vector<bdd> r;
+    std::vector<unsigned> sets(c);
+    for (unsigned i = 0; r.size() < c; ++i)
       {
-	res.insert(res.end(), i.begin(), i.end());
+	if (used.has(i))
-	++count;
+	  {
+	    sets[base] = i;
+	    r.push_back(bdd_ithvar(base++));
+	  }
+	else
+	  {
+	    r.push_back(bddfalse);
+	  }
       }
-    if (count <= 1)
+
-      return res;
+    bdd res = to_bdd_rec(&back(), &r[0]);
-    acc_cond::acc_word w;
+
-    w.op = acc_op::Or;
+    if (res == bddtrue)
-    w.size = res.size();
+      return t();
-    res.push_back(w);
+    if (res == bddfalse)
-    return res;
+      return f();
+
+    minato_isop isop(res);
+    bdd cube;
+    acc_code rescode = f();
+    while ((cube = isop.next()) != bddfalse)
+      {
+	mark_t i = 0U;
+	acc_code c;
+	while (cube != bddtrue)
+	  {
+	    // The acceptance set associated to this BDD variable
+	    mark_t s = 0U;
+	    s.set(sets[bdd_var(cube)]);
+
+	    bdd h = bdd_high(cube);
+	    if (h == bddfalse)	// Negative variable? -> Fin
+	      {
+		cube = bdd_low(cube);
+		// The strange order here make sure we can smaller set
+		// numbers at the end of the acceptance code, i.e., at
+		// the front of the output.
+		auto a = fin(s);
+		a.append_and(std::move(c));
+		std::swap(a, c);
+	      }
+	    else		// Positive variable? -> Inf
+	      {
+		i |= s;
+		cube = h;
+	      }
+	  }
+	c.append_and(inf(i));
+	// See comment above for the order.
+	c.append_or(std::move(rescode));
+	std::swap(c, rescode);
+      }
+    return rescode;
   }
 
   bool acc_cond::acc_code::is_dnf() const

src/tgbatest/acc2.test

@@ -48,17 +48,16 @@ State: 0
 EOF
 
 
-res="(Fin(2) & Fin(1) & Inf(0)) | (Fin(2) & (Inf(0)&Inf(3)))"
+res="(Fin(1) & Fin(2) & Inf(0)) | (Inf(0)&Inf(1)&Inf(3))"
-res="$res | (Fin(1) & (Inf(0)&Inf(1))) | (Inf(0)&Inf(1)&Inf(3))"
 cat >acceptances<<EOF
 2 Inf(0)&Inf(1), 2 Inf(0)&Inf(1)
 2 Fin(0) & Inf(1), 2 Fin(0) & Inf(1)
 2 t, 2 t
 2 f, 2 f
-3 (Inf(1) | Fin(2)) & Inf(0), 3 (Fin(2) & Inf(0)) | (Inf(0)&Inf(1))
+3 (Inf(1) | Fin(2)) & Inf(0), 3 (Inf(0)&Inf(1)) | (Fin(2) & Inf(0))
 4 (Inf(1) | Fin(2)) & (Fin(1) | Inf(3)) & Inf(0), 4 $res
 4 $res, 4 $res
-3 (Fin(0)|Fin(1)) & Fin(2), 3 (Fin(1) & Fin(2)) | (Fin(0) & Fin(2))
+3 (Fin(0)|Fin(1)) & Fin(2), 3 (Fin(0) & Fin(2)) | (Fin(1) & Fin(2))
 EOF
 
 while IFS=, read a b