acc: fix is_dnf()

A Fin() terms with multiple sets should not appear under an And.

* src/tgba/acc.cc (is_dnf): Fix it.
* src/tgbatest/acc.cc, src/tgbatest/acc.test: Augment test case.

src/tgba/acc.cc

@@ -464,10 +464,11 @@ namespace spot
 
   bool acc_cond::acc_code::is_dnf() const
   {
-    if (empty())
+    if (empty() || size() == 2)
       return true;
     auto pos = &back();
     auto start = &front();
+    auto and_scope = pos + 1;
     if (pos->op == acc_cond::acc_op::Or)
       --pos;
     while (pos > start)
@@ -477,12 +478,16 @@ namespace spot
 	  case acc_cond::acc_op::Or:
 	    return false;
 	  case acc_cond::acc_op::And:
+	    and_scope = std::min(and_scope, pos - pos->size);
 	    --pos;
 	    break;
-	  case acc_cond::acc_op::Inf:
-	  case acc_cond::acc_op::InfNeg:
 	  case acc_cond::acc_op::Fin:
 	  case acc_cond::acc_op::FinNeg:
+	    if (pos[-1].mark.count() > 1 && pos > and_scope)
+	      return false;
+	    /* fall through */
+	  case acc_cond::acc_op::Inf:
+	  case acc_cond::acc_op::InfNeg:
 	    pos -= 2;
 	    break;
 	  }

src/tgbatest/acc.cc

@@ -108,15 +108,23 @@ int main()
 
 
   auto code1 = ac.inf({0, 1, 3});
-  std::cout << code1.size() << ' ' << code1 << '\n';
+  std::cout << code1.size() << ' ' << code1 << ' ' << code1.is_dnf() << '\n';
   code1.append_or(ac.fin({2}));
-  std::cout << code1.size() << ' ' << code1 << '\n';
+  std::cout << code1.size() << ' ' << code1 << ' ' << code1.is_dnf() << '\n';
   code1.append_or(ac.fin({0}));
-  std::cout << code1.size() << ' ' << code1 << '\n';
+  std::cout << code1.size() << ' ' << code1 << ' ' << code1.is_dnf() << '\n';
   code1.append_or(ac.fin({}));
-  std::cout << code1.size() << ' ' << code1 << '\n';
+  std::cout << code1.size() << ' ' << code1 << ' ' << code1.is_dnf() << '\n';
   code1.append_and(ac.inf({}));
-  std::cout << code1.size() << ' ' << code1 << '\n';
+  std::cout << code1.size() << ' ' << code1 << ' ' << code1.is_dnf() << '\n';
+  auto code2 = code1;
+  code1.append_and(ac.fin({0, 1}));
+  std::cout << code1.size() << ' ' << code1 << ' ' << code1.is_dnf() << '\n';
   code1.append_and(ac.fin({}));
-  std::cout << code1.size() << ' ' << code1 << '\n';
+  std::cout << code1.size() << ' ' << code1 << ' ' << code1.is_dnf() << '\n';
+  code2.append_or(ac.fin({0, 1}));
+  std::cout << code2.size() << ' ' << code2 << ' ' << code2.is_dnf() << '\n';
+  auto code3 = ac.inf({0, 1});
+  code3.append_and(ac.fin({2, 3}));
+  std::cout << code3.size() << ' ' << code3 << ' ' << code3.is_dnf() << '\n';
 }

src/tgbatest/acc.test

@@ -59,12 +59,15 @@ stripping
 #1: {0}
 #1: {4}
 #1: {2}
-2 Inf(0)&Inf(1)&Inf(3)
-5 Fin(2) | (Inf(0)&Inf(1)&Inf(3))
-7 Fin(0) | Fin(2) | (Inf(0)&Inf(1)&Inf(3))
-7 Fin(0) | Fin(2) | (Inf(0)&Inf(1)&Inf(3))
-7 Fin(0) | Fin(2) | (Inf(0)&Inf(1)&Inf(3))
-2 f
+2 Inf(0)&Inf(1)&Inf(3) 1
+5 Fin(2) | (Inf(0)&Inf(1)&Inf(3)) 1
+7 Fin(0) | Fin(2) | (Inf(0)&Inf(1)&Inf(3)) 1
+7 Fin(0) | Fin(2) | (Inf(0)&Inf(1)&Inf(3)) 1
+7 Fin(0) | Fin(2) | (Inf(0)&Inf(1)&Inf(3)) 1
+10 (Fin(0)|Fin(1)) & (Fin(0) | Fin(2) | (Inf(0)&Inf(1)&Inf(3))) 0
+2 f 1
+9 (Fin(0)|Fin(1)) | Fin(0) | Fin(2) | (Inf(0)&Inf(1)&Inf(3)) 1
+5 (Fin(2)|Fin(3)) & (Inf(0)&Inf(1)) 0
 EOF
 
 run 0 ../acc | tee stdout