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

zlktree: add a cheap unit-propagation

Browse source 
If the top-level has top unit-Inf, propagate it.  This was suggested
by Jan Strejček yesterday.

* spot/twaalgos/zlktree.cc (max_models): Here.
This commit is contained in:
Alexandre Duret-Lutz 2021-09-08 17:12:14 +02:00
parent cb1f6b1239
commit 850608a5fd
1 changed files with 15 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

16
spot/twaalgos/zlktree.cc
View file

@ -80,11 +80,25 @@ namespace spot
[&](auto& mod) {
return mod.model.subset(colors);
}), out.end());
return;
}
else if (acc_cond::mark_t fu = cond.fin_unit())
// If the condition has some Inf(x) forced at the top-level, we
// may simply replace Inf(x) by t and Fin(x) by f in condition
// to simplify it. This is a kind of cheap unit-propagation.
if (acc_cond::mark_t fu = cond.inf_unit())
cond = cond.remove(fu, false);
// Now if we have some Fin(x) forced at the top-level,
// we know the corresponding color need to me removed from
// the set.
if (acc_cond::mark_t fu = cond.fin_unit())
{
max_models(cond.remove(fu, true), colors - fu, out);
}
// Otherwise, we simply have to pick a random Fin(x) and see if
// we can satisfy the condition when x is present or absent. In
// this case, we do not know whether the generated models will
// be maximal, so this justifies the inclusion checks between
// models at the top of this function.
else if (int fo = cond.fin_one(); fo >= 0)
{
acc_cond::mark_t fo_m = {(unsigned) fo};