alarsyo/spot
1
0
Fork 0
Code Issues Pull requests Projects Releases Wiki Activity

acc: make the to_bdd() method public

Browse source 
* spot/twa/acc.cc, spot/twa/acc.hh (acc_code::to_bdd): New method
that calls the private to_bdd_rec() function.
This commit is contained in:
Alexandre Duret-Lutz 2021-07-29 16:17:49 +02:00
parent 31d6dc33e7
commit 803f647dde
2 changed files with 20 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

19
spot/twa/acc.cc
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2015-2020 Laboratoire de Recherche et Développement // Copyright (C) 2015-2021 Laboratoire de Recherche et Développement
// de l'Epita. // de l'Epita.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -1012,6 +1012,13 @@ namespace spot
} }
} }
bdd acc_cond::acc_code::to_bdd(const bdd* map) const
{
if (empty())
return bddtrue;
return to_bdd_rec(&back(), map);
}
std::vector<unsigned> std::vector<unsigned>
acc_cond::acc_code::symmetries() const acc_cond::acc_code::symmetries() const
{ {
@ -1024,7 +1031,7 @@ namespace spot
std::vector<bdd> r; std::vector<bdd> r;
for (unsigned i = 0; r.size() < umax; ++i) for (unsigned i = 0; r.size() < umax; ++i)
r.emplace_back(bdd_ithvar(base++)); r.emplace_back(bdd_ithvar(base++));
bdd bddcode = to_bdd_rec(&back(), &r[0]); bdd bddcode = to_bdd(&r[0]);
bdd tmp; bdd tmp;
std::vector<unsigned> res(umax); std::vector<unsigned> res(umax);
@ -1216,7 +1223,7 @@ namespace spot
} }
} }
bdd res = to_bdd_rec(&back(), &r[0]); bdd res = to_bdd(&r[0]);
if (res == bddtrue) if (res == bddtrue)
return t(); return t();
@ -1285,7 +1292,7 @@ namespace spot
} }
} }
bdd res = to_bdd_rec(&back(), &r[0]); bdd res = to_bdd(&r[0]);
if (res == bddtrue) if (res == bddtrue)
return t(); return t();
@ -1638,7 +1645,7 @@ namespace spot
} }
} }
bdd res = to_bdd_rec(&code_.back(), &r[0]); bdd res = code_.to_bdd(&r[0]);
if (res == bddtrue) if (res == bddtrue)
return {sat, mark_t({})}; return {sat, mark_t({})};
@ -1704,7 +1711,7 @@ namespace spot
} }
} }
bdd res = to_bdd_rec(&back(), &r[0]); bdd res = to_bdd(&r[0]);
res = bdd_restrict(res, known); res = bdd_restrict(res, known);

9
spot/twa/acc.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2014-2020 Laboratoire de Recherche et Développement // Copyright (C) 2014-2021 Laboratoire de Recherche et Développement
// de l'Epita. // de l'Epita.
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
@ -25,7 +25,7 @@
#include <iostream> #include <iostream>
#include <algorithm> #include <algorithm>
#include <numeric> #include <numeric>
#include <bddx.h>
#include <spot/misc/_config.h> #include <spot/misc/_config.h>
#include <spot/misc/bitset.hh> #include <spot/misc/bitset.hh>
#include <spot/misc/trival.hh> #include <spot/misc/trival.hh>
@ -1200,6 +1200,11 @@ namespace spot
/// This implementation is the dual of `to_dnf()`. /// This implementation is the dual of `to_dnf()`.
acc_code to_cnf() const; acc_code to_cnf() const;
/// \brief Convert the acceptance formula into a BDD
///
/// \a map should be a vector indiced by colors, that
/// maps each color to the desired BDD representation.
bdd to_bdd(const bdd* map) const;
/// \brief Return the top-level disjuncts. /// \brief Return the top-level disjuncts.
/// ///