acc: add a to_cnf() function

* src/tgba/acc.cc, src/tgba/acc.hh (to_cnf, is_cnf): New functions.
* src/bin/autfilt.cc: Add a --cnf-acceptance option.
* src/tgbatest/acc2.test: Test it.

src/bin/autfilt.cc

@@ -65,6 +65,7 @@ enum {
   OPT_ACC_SETS = 256,
   OPT_ARE_ISOMORPHIC,
   OPT_CLEAN_ACC,
+  OPT_CNF_ACC,
   OPT_COMPLEMENT_ACC,
   OPT_COUNT,
   OPT_DESTUT,
@@ -128,6 +129,8 @@ static const argp_option options[] =
       "initial state", 0 },
     { "dnf-acceptance", OPT_DNF_ACC, 0, 0,
       "put the acceptance condition in Disjunctive Normal Form", 0 },
+    { "cnf-acceptance", OPT_CNF_ACC, 0, 0,
+      "put the acceptance condition in Conjunctive Normal Form", 0 },
     { "remove-fin", OPT_REM_FIN, 0, 0,
       "rewrite the automaton without using Fin acceptance", 0 },
     { "cleanup-acceptance", OPT_CLEAN_ACC, 0, 0,
@@ -215,6 +218,7 @@ static bool opt_is_empty = false;
 static bool opt_sbacc = false;
 static bool opt_stripacc = false;
 static bool opt_dnf_acc = false;
+static bool opt_cnf_acc = false;
 static bool opt_rem_fin = false;
 static bool opt_clean_acc = false;
 static bool opt_complement_acc = false;
@@ -266,6 +270,10 @@ parse_opt(int key, char* arg, struct argp_state*)
     case OPT_CLEAN_ACC:
       opt_clean_acc = true;
       break;
+    case OPT_CNF_ACC:
+      opt_dnf_acc = false;
+      opt_cnf_acc = true;
+      break;
     case OPT_COMPLEMENT_ACC:
       opt_complement_acc = true;
       break;
@@ -274,6 +282,7 @@ parse_opt(int key, char* arg, struct argp_state*)
       break;
     case OPT_DNF_ACC:
       opt_dnf_acc = true;
+      opt_cnf_acc = false;
       break;
     case OPT_EDGES:
       opt_edges = parse_range(arg, 0, std::numeric_limits<int>::max());
@@ -446,6 +455,9 @@ namespace
       if (opt_dnf_acc)
 	aut->set_acceptance(aut->acc().num_sets(),
 			    aut->get_acceptance().to_dnf());
+      if (opt_cnf_acc)
+	aut->set_acceptance(aut->acc().num_sets(),
+			    aut->get_acceptance().to_cnf());
 
       // Filters.
 

src/tgba/acc.cc

@@ -394,7 +394,7 @@ namespace spot
 
   acc_cond::acc_code acc_cond::acc_code::to_dnf() const
   {
-    if (empty())
+    if (empty() || size() == 2)
       return *this;
 
     auto used = acc_cond::acc_code::used_sets();
@@ -462,6 +462,76 @@ namespace spot
     return rescode;
   }
 
+  acc_cond::acc_code acc_cond::acc_code::to_cnf() const
+  {
+    if (empty() || size() == 2)
+      return *this;
+
+    auto used = acc_cond::acc_code::used_sets();
+    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)
+      {
+	if (used.has(i))
+	  {
+	    sets[base] = i;
+	    r.push_back(bdd_ithvar(base++));
+	  }
+	else
+	  {
+	    r.push_back(bddfalse);
+	  }
+      }
+
+    bdd res = to_bdd_rec(&back(), &r[0]);
+
+    if (res == bddtrue)
+      return t();
+    if (res == bddfalse)
+      return f();
+
+    minato_isop isop(!res);
+    bdd cube;
+    acc_code rescode;
+    while ((cube = isop.next()) != bddfalse)
+      {
+	mark_t m = 0U;
+	acc_code c = f();
+	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? -> Inf
+	      {
+		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 = inf(s);
+		a.append_or(std::move(c));
+		std::swap(a, c);
+	      }
+	    else		// Positive variable? -> Fin
+	      {
+		m |= s;
+		cube = h;
+	      }
+	  }
+	c.append_or(fin(m));
+	// See comment above for the order.
+	c.append_and(std::move(rescode));
+	std::swap(c, rescode);
+      }
+    return rescode;
+  }
+
   bool acc_cond::acc_code::is_dnf() const
   {
     if (empty() || size() == 2)
@@ -495,6 +565,39 @@ namespace spot
     return true;
   }
 
+  bool acc_cond::acc_code::is_cnf() const
+  {
+    if (empty() || size() == 2)
+      return true;
+    auto pos = &back();
+    auto start = &front();
+    auto or_scope = pos + 1;
+    if (pos->op == acc_cond::acc_op::And)
+      --pos;
+    while (pos > start)
+      {
+	switch (pos->op)
+	  {
+	  case acc_cond::acc_op::And:
+	    return false;
+	  case acc_cond::acc_op::Or:
+	    or_scope = std::min(or_scope, pos - pos->size);
+	    --pos;
+	    break;
+	  case acc_cond::acc_op::Inf:
+	  case acc_cond::acc_op::InfNeg:
+	    if (pos[-1].mark.count() > 1 && pos > or_scope)
+	      return false;
+	    /* fall through */
+	  case acc_cond::acc_op::Fin:
+	  case acc_cond::acc_op::FinNeg:
+	    pos -= 2;
+	    break;
+	  }
+      }
+    return true;
+  }
+
   namespace
   {
     acc_cond::acc_code complement_rec(const acc_cond::acc_word* pos)

src/tgba/acc.hh

@@ -635,8 +635,10 @@ namespace spot
       }
 
       bool is_dnf() const;
+      bool is_cnf() const;
 
       acc_code to_dnf() const;
+      acc_code to_cnf() const;
 
       acc_code complement() const;
 

src/tgbatest/acc2.test

@@ -47,6 +47,7 @@ State: 0
 --END--
 EOF
 
+#------------- DNF -------------
 
 res="(Fin(1) & Fin(2) & Inf(0)) | (Inf(0)&Inf(1)&Inf(3))"
 cat >acceptances<<EOF
@@ -68,6 +69,30 @@ done < acceptances > output
 
 diff acceptances output
 
+#------------- CNF -------------
+
+res="(Fin(2) | Inf(1)) & (Fin(1) | Inf(3)) & Inf(0)"
+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(1)) & Inf(0)
+4 (Fin(1) & Fin(2) & Inf(0)) | (Inf(0)&Inf(1)&Inf(3)), 4 $res
+4 $res, 4 $res
+3 (Fin(0) & Fin(2)) | (Fin(1) & Fin(2)), 3 (Fin(0)|Fin(1)) & Fin(2)
+EOF
+
+while IFS=, read a b
+do
+    (cat header; echo 'Acceptance:' $a; cat body) |
+	../../bin/autfilt -H --cnf-acc --stats '%A %G, %a %g'
+done < acceptances > output
+
+diff acceptances output
+
+#------------- COMP -------------
+
 a="(Inf(1) | Fin(2)) & (Fin(1) | Inf(3)) & Inf(0)"
 b="(Fin(1) & Inf(2)) | (Fin(3) & Inf(1)) | Fin(0)"
 cat >acceptances<<EOF