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

* spot/misc/bddlt.hh: Use bdd_stable_cmp, just added to BuDDy.

Browse source
This commit is contained in:
Alexandre Duret-Lutz 2021-06-10 18:01:01 +02:00
parent 9ed2682f67
commit 4965aad0c2
1 changed files with 2 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

24
spot/misc/bddlt.hh
View file

@ -1,5 +1,5 @@
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2011, 2014, 2017 Laboratoire de Recherche et // Copyright (C) 2011, 2014, 2017, 2021 Laboratoire de Recherche et
// Developpement de l'Epita (LRDE). // Developpement de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
@ -56,27 +56,7 @@ namespace spot
bool bool
operator()(const bdd& left, const bdd& right) const operator()(const bdd& left, const bdd& right) const
{ {
int li = left.id(); return bdd_stable_cmp(left, right) < 0;
int ri = right.id();
if (li == ri)
return false;
if (li <= 1 || ri <= 1)
return li < ri;
{
int vl = bdd_var(left);
int vr = bdd_var(right);
if (vl != vr)
return vl < vr;
}
// We check the high side before low, this way
// !a&b comes before a&!b and a&b
{
bdd hl = bdd_high(left);
bdd hr = bdd_high(right);
if (hl != hr)
return operator()(hl, hr);
return operator()(bdd_low(left), bdd_low(right));
}
} }
}; };