From b48815795733650e837f66d72462bd1aea536480 Mon Sep 17 00:00:00 2001
From: Alexandre Duret-Lutz <adl@lrde.epita.fr>
Date: Thu, 26 Mar 2015 19:39:47 +0100
Subject: [PATCH] sat-minimize: omit impossible histories

When the reference acceptance condition is complex enough, some
accepting SCCs may not use all acceptance sets.  In that case
we don't have to encode all possible histories for this SCC.

* src/twaalgos/dtgbasat.cc: Improve the encoding by omitting
histories involving sets that are not used in a reference SCC.
---
 src/twaalgos/dtgbasat.cc | 36 ++++++++++++++++++++++++++++++++----
 1 file changed, 32 insertions(+), 4 deletions(-)

diff --git a/src/twaalgos/dtgbasat.cc b/src/twaalgos/dtgbasat.cc
index 65ad89dca..32b37b6ba 100644
--- a/src/twaalgos/dtgbasat.cc
+++ b/src/twaalgos/dtgbasat.cc
@@ -281,6 +281,7 @@ namespace spot
       std::vector<acc_cond::mark_t> all_ref_acc;
 
       std::vector<bool> is_weak_scc;
+      std::vector<acc_cond::mark_t> scc_marks;
 
       acc_cond cacc;
 
@@ -294,6 +295,20 @@ namespace spot
     unsigned declare_vars(const const_twa_graph_ptr& aut,
 			  dict& d, bdd ap, bool state_based, scc_info& sm)
     {
+      d.is_weak_scc = sm.weak_sccs();
+      unsigned scccount = sm.scc_count();
+      {
+	auto tmp = sm.used_acc();
+	d.scc_marks.reserve(scccount);
+	for (auto& v: tmp)
+	  {
+	    acc_cond::mark_t m = 0U;
+	    for (auto i: v)
+	      m |= i;
+	    d.scc_marks.emplace_back(m);
+	  }
+      }
+
       bdd_dict_ptr bd = aut->get_dict();
       d.cacc.add_sets(d.cand_nacc);
       d.all_cand_acc.push_back(0U);
@@ -343,14 +358,20 @@ namespace spot
 		  for (unsigned l = 0; l < d.cand_size; ++l)
 		    {
 		      size_t sfp = is_weak ? 1 : d.all_ref_acc.size();
+		      acc_cond::mark_t sccmarks =
+			is_weak ? d.all_ref_acc.back() : d.scc_marks[i_scc];
 		      for (size_t fp = 0; fp < sfp; ++fp)
 			{
+			  auto refhist = d.all_ref_acc[fp];
+			  // refhist cannot have more sets than used in the SCC
+			  if ((sccmarks & refhist) != refhist)
+			    continue;
+
 			  size_t sf = d.all_cand_acc.size();
 			  for (size_t f = 0; f < sf; ++f)
 			    {
 			      path p(j, i, l, k,
-				     d.all_cand_acc[f],
-				     d.all_ref_acc[fp]);
+				     d.all_cand_acc[f], refhist);
 			      d.pathid[p] = ++d.nvars;
 			    }
 
@@ -455,7 +476,6 @@ namespace spot
 
       scc_info sm(ref);
       sm.determine_unknown_acceptance();
-      d.is_weak_scc = sm.weak_sccs();
 
       // Number all the SAT variables we may need.
       unsigned ref_size = declare_vars(ref, d, ap, state_based, sm);
@@ -600,11 +620,19 @@ namespace spot
 		  {
 		    size_t sf = d.all_cand_acc.size();
 		    size_t sfp = is_weak ? 1 : d.all_ref_acc.size();
+		    acc_cond::mark_t sccmarks =
+		      is_weak ? d.all_ref_acc.back() : d.scc_marks[q1p_scc];
+
 		    for (size_t f = 0; f < sf; ++f)
 		      for (size_t fp = 0; fp < sfp; ++fp)
 			{
+			  auto refhist = d.all_ref_acc[fp];
+			  // refhist cannot have more sets than used in the SCC
+			  if ((sccmarks & refhist) != refhist)
+			    continue;
+
 			  path p(q1, q1p, q2, q2p,
-				 d.all_cand_acc[f], d.all_ref_acc[fp]);
+				 d.all_cand_acc[f], refhist);
 
 			  dout << "(11&12&13) paths from " << p << '\n';