ad8d24222a
* buddy/src/bdd.h, buddy/src/bvec.h, buddy/src/fdd.h: Rename as... * buddy/src/bddx.h, buddy/src/bvecx.h, buddy/src/fddx.h: ... these. * buddy/src/Makefile.am: Build libbddx.la instead of libbdd.la. * buddy/examples/Makefile.def: Use it. * Makefile.am, buddy/src/bddtest.cxx, buddy/src/bvec.c, buddy/src/cppext.cxx, buddy/src/fdd.c, buddy/src/imatrix.h, buddy/src/kernel.h, buddy/examples/adder/adder.cxx, buddy/examples/bddcalc/parser_.h, buddy/examples/bddtest/bddtest.cxx, buddy/examples/cmilner/cmilner.c, buddy/examples/fdd/fdd.cxx, buddy/examples/milner/milner.cxx, buddy/examples/money/money.cxx, buddy/examples/queen/queen.cxx, buddy/examples/solitare/solitare.cxx, m4/buddy.m4, src/ltlvisit/apcollect.hh, src/ltlvisit/simplify.hh, src/misc/bddlt.hh, src/misc/bddop.hh, src/misc/minato.hh, src/priv/acccompl.hh, src/priv/accconv.hh, src/priv/accmap.hh, src/priv/bddalloc.cc, src/tgba/bdddict.hh, src/tgba/bddprint.hh, src/tgba/tgbamask.hh, src/tgba/tgbasafracomplement.cc, src/tgbaalgos/emptiness.hh, src/tgbaalgos/gtec/sccstack.hh, src/tgbaalgos/neverclaim.cc, src/tgbaalgos/powerset.cc, src/tgbaalgos/sccfilter.hh, src/tgbaalgos/sccinfo.hh, src/tgbaalgos/weight.hh, wrap/python/buddy.i: Adjust. * NEWS, README: Document it.
52 lines
1.4 KiB
C++
52 lines
1.4 KiB
C++
// -*- coding: utf-8 -*-
|
|
// Copyright (C) 2011, 2013, 2014 Laboratoire de Recherche et
|
|
// Developpement de l'Epita (LRDE)
|
|
//
|
|
// This file is part of Spot, a model checking library.
|
|
//
|
|
// Spot is free software; you can redistribute it and/or modify it
|
|
// under the terms of the GNU General Public License as published by
|
|
// the Free Software Foundation; either version 3 of the License, or
|
|
// (at your option) any later version.
|
|
//
|
|
// Spot is distributed in the hope that it will be useful, but WITHOUT
|
|
// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
|
|
// or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public
|
|
// License for more details.
|
|
//
|
|
// You should have received a copy of the GNU General Public License
|
|
// along with this program. If not, see <http://www.gnu.org/licenses/>.
|
|
|
|
#ifndef SPOT_PRIV_ACCCONV_HH
|
|
# define SPOT_PRIV_ACCCONV_HH
|
|
|
|
#include <bddx.h>
|
|
#include "misc/hash.hh"
|
|
#include "misc/bddlt.hh"
|
|
|
|
namespace spot
|
|
{
|
|
/// \brief Help class to convert between acceptance conditions to
|
|
/// other BDD formats.
|
|
class acceptance_convertor
|
|
{
|
|
public:
|
|
acceptance_convertor(bdd allneg)
|
|
: allneg_(allneg)
|
|
{
|
|
}
|
|
|
|
bdd as_positive_product(bdd acc);
|
|
|
|
bdd as_full_product(bdd acc);
|
|
|
|
protected:
|
|
bdd allneg_;
|
|
typedef std::unordered_map<bdd, bdd, bdd_hash> bdd_cache_t;
|
|
bdd_cache_t pos_prod_cache_;
|
|
bdd_cache_t full_prod_cache_;
|
|
};
|
|
|
|
}
|
|
|
|
#endif // SPOT_PRIV_ACCCONV_HH
|