From 5bc2d77e6081560ea85cae90c3f9e68d04d15a09 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 25 Jul 2003 14:32:50 +0000 Subject: [PATCH] * src/tgbaalgos/lbtt.cc (bdd_less_than): Move ... * src/misc/bddlt.hh: ... in this new file. * src/misc/Makefile.am (misc_HEADERS): Add bddlt.hh. --- ChangeLog | 4 ++++ src/misc/Makefile.am | 1 + src/misc/bddlt.hh | 19 +++++++++++++++++++ src/tgbaalgos/lbtt.cc | 10 +--------- 4 files changed, 25 insertions(+), 9 deletions(-) create mode 100644 src/misc/bddlt.hh diff --git a/ChangeLog b/ChangeLog index 4fb21cbae..52101a242 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,9 @@ 2003-07-25 Alexandre Duret-Lutz + * src/tgbaalgos/lbtt.cc (bdd_less_than): Move ... + * src/misc/bddlt.hh: ... in this new file. + * src/misc/Makefile.am (misc_HEADERS): Add bddlt.hh. + * iface/gspn/dcswave.test: Comment state space sizes. * src/tgbaalgos/Makefile.am (tgbaalgos_HEADERS): Add reachiters.hh. diff --git a/src/misc/Makefile.am b/src/misc/Makefile.am index 56b4be474..7a81aa43b 100644 --- a/src/misc/Makefile.am +++ b/src/misc/Makefile.am @@ -5,6 +5,7 @@ miscdir = $(pkgincludedir)/misc misc_HEADERS = \ bddalloc.hh \ + bddlt.hh \ const_sel.hh noinst_LTLIBRARIES = libmisc.la diff --git a/src/misc/bddlt.hh b/src/misc/bddlt.hh new file mode 100644 index 000000000..2ca90a9c6 --- /dev/null +++ b/src/misc/bddlt.hh @@ -0,0 +1,19 @@ +#ifndef SPOT_MISC_BDDLT_HH +# define SPOT_MISC_BDDLT_HH + +# include + +namespace spot +{ + /// Comparison functor for BDDs. + struct bdd_less_than + { + bool + operator()(const bdd& left, const bdd& right) const + { + return left.id() < right.id(); + } + }; +} + +#endif // SPOT_MISC_BDDLT_HH diff --git a/src/tgbaalgos/lbtt.cc b/src/tgbaalgos/lbtt.cc index 9712af113..6f8a48afe 100644 --- a/src/tgbaalgos/lbtt.cc +++ b/src/tgbaalgos/lbtt.cc @@ -7,18 +7,10 @@ #include "tgba/bddprint.hh" #include "ltlvisit/tostring.hh" #include "tgba/bddprint.hh" +#include "misc/bddlt.hh" namespace spot { - struct bdd_less_than - { - bool - operator()(const bdd& left, const bdd& right) const - { - return left.id() < right.id(); - } - }; - // At some point we'll need to print an accepting set into LBTT's // forma. LBTT expect numbered accepting sets, so first we'll // number each accepting condition, and latter when we have to print