From 9bbcf85b3acae7d1011165e528d5e50b66dc061f Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Wed, 9 Dec 2015 11:21:41 +0100
Subject: [PATCH] acc: move unsat_mark in acc_cond

so that we can optimize it when no Fin are used

* spot/twa/acc.cc, spot/twa/acc.hh: Do it.
* spot/twaalgos/complete.cc, spot/twaalgos/strength.cc: Adjust.
---
 spot/twa/acc.cc           | 10 ++++++----
 spot/twa/acc.hh           |  9 +++++----
 spot/twaalgos/complete.cc |  2 +-
 spot/twaalgos/strength.cc | 21 +++++----------------
 4 files changed, 17 insertions(+), 25 deletions(-)

diff --git a/spot/twa/acc.cc b/spot/twa/acc.cc
index 1d5211311..5e5ac1e83 100644
--- a/spot/twa/acc.cc
+++ b/spot/twa/acc.cc
@@ -857,12 +857,14 @@ namespace spot
   }
 
   std::pair<bool, acc_cond::mark_t>
-  acc_cond::acc_code::unsat_mark() const
+  acc_cond::unsat_mark() const
   {
-    if (empty())
+    if (is_tt())
       return {false, 0U};
+    if (!uses_fin_acceptance())
+      return {true, 0U};
 
-    auto used = acc_cond::acc_code::used_sets();
+    auto used = code_.used_sets();
     unsigned c = used.count();
     unsigned max = used.max_set();
 
@@ -884,7 +886,7 @@ namespace spot
 	  }
       }
 
-    bdd res = to_bdd_rec(&back(), &r[0]);
+    bdd res = to_bdd_rec(&code_.back(), &r[0]);
 
     if (res == bddtrue)
       return {false, 0U};
diff --git a/spot/twa/acc.hh b/spot/twa/acc.hh
index 059462180..f3ccf5e09 100644
--- a/spot/twa/acc.hh
+++ b/spot/twa/acc.hh
@@ -832,10 +832,6 @@ namespace spot
       // Return the set of sets appearing in the condition.
       acc_cond::mark_t used_sets() const;
 
-      // Return (true, m) if there exist some m that does not satisfy
-      // the acceptance condition.  Return (false, 0U) otherwise.
-      std::pair<bool, acc_cond::mark_t> unsat_mark() const;
-
       // Return the sets used as Inf or Fin in the acceptance condition
       std::pair<acc_cond::mark_t, acc_cond::mark_t> used_inf_fin_sets() const;
 
@@ -958,6 +954,11 @@ namespace spot
       return acc_code::inf(m);
     }
 
+    // Return (true, m) if there exist some acceptance mark m that
+    // does not satisfy the acceptance condition.  Return (false, 0U)
+    // otherwise.
+    std::pair<bool, acc_cond::mark_t> unsat_mark() const;
+
   protected:
     bool check_fin_acceptance() const;
 
diff --git a/spot/twaalgos/complete.cc b/spot/twaalgos/complete.cc
index 07fb1751f..796273e9e 100644
--- a/spot/twaalgos/complete.cc
+++ b/spot/twaalgos/complete.cc
@@ -34,7 +34,7 @@ namespace spot
     // UM is a pair (bool, mark).  If the Boolean is false, the
     // acceptance is always satisfiable.  Otherwise, MARK is an
     // example of unsatisfiable mark.
-    auto um = aut->get_acceptance().unsat_mark();
+    auto um = aut->acc().unsat_mark();
     if (!um.first)
       {
 	// We cannot safely complete an automaton if its
diff --git a/spot/twaalgos/strength.cc b/spot/twaalgos/strength.cc
index 6367ef016..39fbc0166 100644
--- a/spot/twaalgos/strength.cc
+++ b/spot/twaalgos/strength.cc
@@ -171,26 +171,15 @@ namespace spot
 	    (std::string("unknown option for decompose_strength(): ") + c);
 	}
 
+    auto p = aut->acc().unsat_mark();
+    bool all_accepting = !p.first;
     acc_cond::mark_t wacc = 0U;	// Acceptance for weak SCCs
-    acc_cond::mark_t uacc = 0U;	// Acceptance for "needed" SCCs, that
-				// we only want to traverse.
+    acc_cond::mark_t uacc = p.second; // Acceptance for "needed" SCCs, that
+                                      // we only want to traverse.
 
     // If the acceptance condition is always satisfiable, we will
-    // consider the automaton has weak (even if that is not the
+    // consider the automaton as weak (even if that is not the
     // case syntactically) and not output any strong part.
-    bool all_accepting = false;
-    if (aut->acc().is_tt())
-      {
-	all_accepting = true;
-      }
-    else if (aut->acc().uses_fin_acceptance())
-      {
-	auto p = aut->get_acceptance().unsat_mark();
-	if (p.first)
-	  uacc = p.second;
-	else
-	  all_accepting = true;
-      }
     if (all_accepting)
       {
 	keep &= ~Strong;
-- 
GitLab