diff --git a/spot/twaalgos/cobuchi.cc b/spot/twaalgos/cobuchi.cc index 9fab6b64d..783cd0903 100644 --- a/spot/twaalgos/cobuchi.cc +++ b/spot/twaalgos/cobuchi.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2017-2018 Laboratoire de Recherche et Développement +// Copyright (C) 2017-2018, 2021 Laboratoire de Recherche et Développement // de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -426,13 +426,11 @@ namespace spot ap_(aut->ap_vars()) { // Get all bdds. - bdd all = bddtrue; - for (unsigned i = 0; all != bddfalse; ++i) + unsigned i = 0; + for (bdd one: minterms_of(bddtrue, ap_)) { - bdd one = bdd_satoneset(all, ap_, bddfalse); num2bdd_.push_back(one); - bdd2num_[one] = i; - all -= one; + bdd2num_[one] = i++; } } @@ -455,15 +453,8 @@ namespace spot { size_t base = src * nc; for (auto& t: aut_->out(src)) - { - bdd all = t.cond; - while (all != bddfalse) - { - bdd one = bdd_satoneset(all, ap_, bddfalse); - all -= one; - bv_aut_trans_->at(base + bdd2num_[one]).set(t.dst); - } - } + for (bdd one: minterms_of(t.cond, ap_)) + bv_aut_trans_->at(base + bdd2num_[one]).set(t.dst); } trace << "All_states:\n" << *bv_aut_trans_ << '\n'; diff --git a/spot/twaalgos/complement.cc b/spot/twaalgos/complement.cc index 9cbe7d138..20be9c3eb 100644 --- a/spot/twaalgos/complement.cc +++ b/spot/twaalgos/complement.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2015, 2017-2020 Laboratoire de Recherche et +// Copyright (C) 2013-2015, 2017-2021 Laboratoire de Recherche et // Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -484,15 +484,10 @@ namespace spot {0}); } } - while (all != bddfalse) - { - bdd one = bdd_satoneset(all, msupport, bddfalse); - all -= one; - - // Compute all new states available from the generated - // letter. - ncsb_successors(std::move(ms), top.second, one); - } + for (bdd one: minterms_of(all, msupport)) + // Compute all new states available from the generated + // letter. + ncsb_successors(std::move(ms), top.second, one); } res_->merge_edges(); diff --git a/spot/twaalgos/determinize.cc b/spot/twaalgos/determinize.cc index c3a981353..00fe04ee2 100644 --- a/spot/twaalgos/determinize.cc +++ b/spot/twaalgos/determinize.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2015-2020 Laboratoire de Recherche et +// Copyright (C) 2015-2021 Laboratoire de Recherche et // Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -548,21 +548,6 @@ namespace spot return res; } - // Compute a vector of letters from a given support - std::vector - letters(const bdd& allap) - { - std::vector res; - bdd all = bddtrue; - while (all != bddfalse) - { - bdd one = bdd_satoneset(all, allap, bddfalse); - all -= one; - res.emplace_back(one); - } - return res; - } - class safra_support { const std::vector& state_supports; @@ -579,7 +564,11 @@ namespace spot supp &= state_supports[n.first]; auto i = cache.emplace(supp, std::vector()); if (i.second) // insertion took place - i.first->second = letters(supp); + { + std::vector& res = i.first->second; + for (bdd one: minterms_of(bddtrue, supp)) + res.emplace_back(one); + } return i.first->second; } }; diff --git a/spot/twaalgos/dtbasat.cc b/spot/twaalgos/dtbasat.cc index 045970f5f..eb39a69b6 100644 --- a/spot/twaalgos/dtbasat.cc +++ b/spot/twaalgos/dtbasat.cc @@ -1,6 +1,6 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2018 Laboratoire de Recherche -// et Développement de l'Epita. +// Copyright (C) 2013-2018, 2021 Laboratoire de Recherche et +// Développement de l'Epita. // // This file is part of Spot, a model checking library. // @@ -272,17 +272,16 @@ namespace spot } // Fill dict's bdd vetor (alpha_vect) and save each bdd and it's - // corresponding index in alpha_map. This is necessary beacause some - // loops start from a precise bdd. Therefore, it's useful to know - // it's corresponding index to deal with vars_helper. - bdd all = bddtrue; - for (unsigned j = 0; all != bddfalse; ++j) - { - bdd one = bdd_satoneset(all, ap, bddfalse); - d.alpha_vect.push_back(one); - d.alpha_map[d.alpha_vect[j]] = j; - all -= one; - } + // corresponding index in alpha_map. This is necessary beacause + // some loops start from a precise bdd. Therefore, it's useful + // to know its corresponding index to deal with vars_helper. + unsigned j = 0; + for (bdd one: minterms_of(bddtrue, ap)) + { + d.alpha_vect.push_back(one); + d.alpha_map[d.alpha_vect[j]] = j; + ++j; + } // Initialize vars_helper by giving it all the necessary information. // 1: nacc_size is 1 (with Büchi) | true: means dtbasat, i-e, not dtwasat. @@ -389,24 +388,18 @@ namespace spot for (auto& tr: ref->out(q1p)) { unsigned dp = tr.dst; - bdd all = tr.cond; - while (all != bddfalse) - { - bdd s = bdd_satoneset(all, ap, bddfalse); - all -= s; + for (bdd s: minterms_of(tr.cond, ap)) + for (unsigned q2 = 0; q2 < d.cand_size; q2++) + { + int prev = d.pathid_ref(q1, q1p, q1, q1p); + int succ = d.pathid_ref(q2, dp, q2, dp); + if (prev == succ) + continue; - for (unsigned q2 = 0; q2 < d.cand_size; q2++) - { - int prev = d.pathid_ref(q1, q1p, q1, q1p); - int succ = d.pathid_ref(q2, dp, q2, dp); - if (prev == succ) - continue; - - cnf_comment(prev, "∧", d.fmt_t(q1, s, q2), "δ →", - d.fmt_p(q2, dp, q2, dp), '\n'); - solver.add({-prev, -d.transid(q1, s, q2), succ, 0}); - } - } + cnf_comment(prev, "∧", d.fmt_t(q1, s, q2), "δ →", + d.fmt_p(q2, dp, q2, dp), '\n'); + solver.add({-prev, -d.transid(q1, s, q2), succ, 0}); + } } } } @@ -452,11 +445,8 @@ namespace spot { if (dp == q1p && q3 == q1) // (4) looping { - bdd all = tr.cond; - while (all != bddfalse) + for (bdd s: minterms_of(tr.cond, ap)) { - bdd s = bdd_satoneset(all, ap, bddfalse); - all -= s; #if TRACE std::string f_t = d.fmt_t(q2, s, q1); cnf_comment(f_p, "R ∧", f_t, "δ → ¬", f_t, @@ -474,12 +464,8 @@ namespace spot if (pid1 == pid2) continue; - bdd all = tr.cond; - while (all != bddfalse) + for (bdd s: minterms_of(tr.cond, ap)) { - bdd s = bdd_satoneset(all, ap, bddfalse); - all -= s; - cnf_comment(f_p, "R ∧", d.fmt_t(q2, s, q3), "δ →", d.fmt_p(q1, q1p, q3, dp), "R\n"); @@ -539,11 +525,8 @@ namespace spot // it is accepting in the reference. if (!ra.accepting(tr.acc)) continue; - bdd all = tr.cond; - while (all != bddfalse) + for (bdd s: minterms_of(tr.cond, ap)) { - bdd s = bdd_satoneset(all, ap, bddfalse); - all -= s; #if TRACE std::string f_t = d.fmt_t(q2, s, q1); cnf_comment(f_p, "C ∧", f_t, "δ →", f_t, @@ -561,11 +544,8 @@ namespace spot if (pid1 == pid2) continue; - bdd all = tr.cond; - while (all != bddfalse) + for (bdd s: minterms_of(tr.cond, ap)) { - bdd s = bdd_satoneset(all, ap, bddfalse); - all -= s; #if TRACE std::string f_t = d.fmt_t(q2, s, q3); cnf_comment(f_p, "C ∧", f_t, "δ ∧ ¬", f_t, diff --git a/spot/twaalgos/dtwasat.cc b/spot/twaalgos/dtwasat.cc index 23b666517..e3c625ba4 100644 --- a/spot/twaalgos/dtwasat.cc +++ b/spot/twaalgos/dtwasat.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2013-2020 Laboratoire de Recherche +// Copyright (C) 2013-2021 Laboratoire de Recherche // et Développement de l'Epita. // // This file is part of Spot, a model checking library. @@ -501,16 +501,15 @@ namespace spot } // Fill dict's bdd vetor (alpha_vect) and save each bdd and it's - // corresponding index in alpha_map. This is necessary beacause some - // loops start from a precise bdd. Therefore, it's useful to know - // it's corresponding index to deal with vars_helper. - bdd all = bddtrue; - for (unsigned j = 0; all != bddfalse; ++j) + // corresponding index in alpha_map. This is necessary beacause + // some loops start from a precise bdd. Therefore, it's useful + // to know its corresponding index to deal with vars_helper. + unsigned j = 0; + for (bdd one: minterms_of(bddtrue, ap)) { - bdd one = bdd_satoneset(all, ap, bddfalse); d.alpha_vect.push_back(one); d.alpha_map[d.alpha_vect[j]] = j; - all -= one; + ++j; } // Initialize vars_helper by giving it all the necessary information. @@ -670,24 +669,17 @@ namespace spot for (auto& tr: ref->out(q1p)) { unsigned dp = tr.dst; - bdd all = tr.cond; - while (all != bddfalse) - { - bdd s = bdd_satoneset(all, ap, bddfalse); - all -= s; - - for (unsigned q2 = 0; q2 < d.cand_size; ++q2) - { - int succ = d.pathid(q2, dp, q2, dp); - if (p1id == succ) - continue; - - cnf_comment(d.fmt_p(q1, q1p, q1, q1p), " ∧ ", - d.fmt_t(q1, s, q2), "δ → ", - d.fmt_p(q2, dp, q2, dp), '\n'); - solver.add({-p1id, -d.transid(q1, s, q2), succ, 0}); - } - } + for (bdd s: minterms_of(tr.cond, ap)) + for (unsigned q2 = 0; q2 < d.cand_size; ++q2) + { + int succ = d.pathid(q2, dp, q2, dp); + if (p1id == succ) + continue; + cnf_comment(d.fmt_p(q1, q1p, q1, q1p), " ∧ ", + d.fmt_t(q1, s, q2), "δ → ", + d.fmt_p(q2, dp, q2, dp), '\n'); + solver.add({-p1id, -d.transid(q1, s, q2), succ, 0}); + } } } @@ -738,13 +730,9 @@ namespace spot for (unsigned q3 = 0; q3 < d.cand_size; ++q3) { - bdd all = tr.cond; acc_cond::mark_t curacc = tr.acc; - while (all != bddfalse) + for (bdd l: minterms_of(tr.cond, ap)) { - bdd l = bdd_satoneset(all, ap, bddfalse); - all -= l; - int ti = d.transid(q2, l, q3); if (dp == q1p && q3 == q1) // (11,12) loop { diff --git a/spot/twaalgos/hoa.cc b/spot/twaalgos/hoa.cc index fe72896ea..6c474fb2a 100644 --- a/spot/twaalgos/hoa.cc +++ b/spot/twaalgos/hoa.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2014-2020 Laboratoire de Recherche et +// Copyright (C) 2014-2021 Laboratoire de Recherche et // Developpement de l'Epita (LRDE). // // This file is part of Spot, a model checking library. @@ -710,33 +710,28 @@ namespace spot else { for (auto& t: aut->out(i)) - { - bdd cond = t.cond; - while (cond != bddfalse) - { - bdd one = bdd_satoneset(cond, md.all_ap, bddfalse); - cond -= one; - unsigned level = 1; - unsigned pos = 0U; - while (one != bddtrue) - { - bdd h = bdd_high(one); - if (h == bddfalse) - { - one = bdd_low(one); - } - else - { - pos |= level; - one = h; - } - level <<= 1; - } - out[pos] = t.dst; - if (this_acc != Hoa_Acceptance_States) - outm[pos] = t.acc; - } - } + for (bdd one: minterms_of(t.cond, md.all_ap)) + { + unsigned level = 1; + unsigned pos = 0U; + while (one != bddtrue) + { + bdd h = bdd_high(one); + if (h == bddfalse) + { + one = bdd_low(one); + } + else + { + pos |= level; + one = h; + } + level <<= 1; + } + out[pos] = t.dst; + if (this_acc != Hoa_Acceptance_States) + outm[pos] = t.acc; + } unsigned n = out.size(); for (unsigned i = 0; i < n;) { diff --git a/spot/twaalgos/powerset.cc b/spot/twaalgos/powerset.cc index 5093d885a..c5fc07f94 100644 --- a/spot/twaalgos/powerset.cc +++ b/spot/twaalgos/powerset.cc @@ -1,5 +1,5 @@ // -*- coding: utf-8 -*- -// Copyright (C) 2009-2011, 2013-2019 Laboratoire de Recherche et +// Copyright (C) 2009-2011, 2013-2019, 2021 Laboratoire de Recherche et // Développement de l'Epita (LRDE). // Copyright (C) 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // département Systèmes Répartis Coopératifs (SRC), Université Pierre @@ -96,12 +96,9 @@ namespace spot std::vector num2bdd; num2bdd.reserve(1UL << nap); std::map bdd2num; - bdd all = bddtrue; bdd allap = aut->ap_vars(); - while (all != bddfalse) + for (bdd one: minterms_of(bddtrue, allap)) { - bdd one = bdd_satoneset(all, allap, bddfalse); - all -= one; bdd2num.emplace(one, num2bdd.size()); num2bdd.emplace_back(one); } @@ -183,16 +180,11 @@ namespace spot for (unsigned i = 0; i < nc; ++i) bv->at(base + i).clear_all(); for (auto& t: aut->out(src)) - { - bdd all = t.cond; - while (all != bddfalse) - { - bdd one = bdd_satoneset(all, allap, bddfalse); - all -= one; - unsigned num = bdd2num[one]; - bv->at(base + num).set(t.dst); - } - } + for (bdd one: minterms_of(t.cond, allap)) + { + unsigned num = bdd2num[one]; + bv->at(base + num).set(t.dst); + } assert(idx == lru.begin()->first); return idx;