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

lazy eval for sat mealy minimization

Browse source 
Evaluate incomp of player conditions only if necessary

* spot/twaalgos/mealy_machine.cc: Here
This commit is contained in:
Philipp Schlehuber-Caissier 2022-10-06 22:03:28 +02:00
parent 6e2e7c942e
commit 427f667f9f
1 changed files with 19 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

33
spot/twaalgos/mealy_machine.cc
View file

@ -1312,7 +1312,9 @@ namespace
// Associated condition and id of each player state // Associated condition and id of each player state
std::vector<std::pair<bdd, unsigned>> ps2c; std::vector<std::pair<bdd, unsigned>> ps2c;
ps2c.reserve(n_tot - n_env); ps2c.reserve(n_tot - n_env);
// bdd id -> internal index
std::unordered_map<unsigned, unsigned> all_out_cond; std::unordered_map<unsigned, unsigned> all_out_cond;
for (unsigned s1 = n_env; s1 < n_tot; ++s1) for (unsigned s1 = n_env; s1 < n_tot; ++s1)
{ {
const bdd &c1 = get_cond(s1); const bdd &c1 = get_cond(s1);
@ -1327,24 +1329,26 @@ namespace
#endif #endif
} }
// Are two player condition ids states incompatible // Are two player condition ids states incompatible
// Matrix for incompatibility
square_matrix<bool, true> inc_player(all_out_cond.size(), false); square_matrix<bool, true> inc_player(all_out_cond.size(), false);
// Matrix whether computed or not
square_matrix<bool, true> inc_player_comp(all_out_cond.size(), false);
// Compute. First is id of bdd // Compute. First is id of bdd
for (const auto& p1 : all_out_cond) // Lazy eval: Compute incompatibility between out conditions
for (const auto& p2 : all_out_cond) // only if demanded
{
if (p1.second > p2.second)
continue;
inc_player.set(p1.second, p2.second,
!bdd_have_common_assignment(
bdd_from_int((int) p1.first),
bdd_from_int((int) p2.first)));
assert(inc_player.get(p1.second, p2.second)
== ((bdd_from_int((int) p1.first)
& bdd_from_int((int) p2.first)) == bddfalse));
}
auto is_p_incomp = [&](unsigned s1, unsigned s2) auto is_p_incomp = [&](unsigned s1, unsigned s2)
{ {
return inc_player.get(ps2c[s1].second, ps2c[s2].second); const auto& [s1bdd, s1idx] = ps2c[s1];
const auto& [s2bdd, s2idx] = ps2c[s2];
if (!inc_player_comp.get(s1idx, s2idx))
{
inc_player_comp.set(s1idx, s2idx, true);
inc_player.set(s1idx, s2idx,
!bdd_have_common_assignment(s1bdd, s2bdd));
}
return inc_player.get(s1idx, s2idx);
}; };
si.player_incomp_time = si.restart(); si.player_incomp_time = si.restart();
@ -3948,6 +3952,7 @@ namespace
si.task = "presat"; si.task = "presat";
stopwatch sglob; stopwatch sglob;
sglob.start(); sglob.start();
si.start();
if ((premin < -1) || (premin > 1)) if ((premin < -1) || (premin > 1))
throw std::runtime_error("premin has to be -1, 0 or 1"); throw std::runtime_error("premin has to be -1, 0 or 1");