From 0fe98c6d18fbd9b4b817ae6c34ca6e5457dcde06 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Wed, 2 Jul 2003 14:28:06 +0000 Subject: [PATCH] * src/tgba/tgbabddcoredata.hh (tgba_bdd_core_data::translate): New function. * src/tgba/tgbabddcoredata.cc (tgba_bdd_core_data::translate): Likewise. * src/tgba/tgbabddtranslatefactory.cc (tgba_bdd_translate_factory::tgba_bdd_translate_factory): Use tgba_bdd_core_data::translate. --- ChangeLog | 8 ++++++++ src/tgba/tgbabddcoredata.cc | 18 ++++++++++++++++++ src/tgba/tgbabddcoredata.hh | 6 ++++++ src/tgba/tgbabddtranslatefactory.cc | 21 ++------------------- 4 files changed, 34 insertions(+), 19 deletions(-) diff --git a/ChangeLog b/ChangeLog index c215e2739..fb57ab877 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,5 +1,13 @@ 2003-07-02 Alexandre Duret-Lutz + * src/tgba/tgbabddcoredata.hh (tgba_bdd_core_data::translate): New + function. + * src/tgba/tgbabddcoredata.cc (tgba_bdd_core_data::translate): + Likewise. + * src/tgba/tgbabddtranslatefactory.cc + (tgba_bdd_translate_factory::tgba_bdd_translate_factory): Use + tgba_bdd_core_data::translate. + * src/tgba/tgbabddcoredata.hh (tgba_bdd_core_data::nownext_set): New attribute. * tgba/tgbabddcoredata.cc, tgba/tgbabddtranslatefactory.cc: diff --git a/src/tgba/tgbabddcoredata.cc b/src/tgba/tgbabddcoredata.cc index 9fdf1ae4e..04fa29e90 100644 --- a/src/tgba/tgbabddcoredata.cc +++ b/src/tgba/tgbabddcoredata.cc @@ -108,4 +108,22 @@ namespace spot acc_set &= acc; negacc_set &= !acc; } + + void + tgba_bdd_core_data::translate(bddPair* rewrite) + { + relation = bdd_replace(relation, rewrite); + accepting_conditions = bdd_replace(accepting_conditions, rewrite); + now_set = bdd_replace(now_set, rewrite); + next_set = bdd_replace(next_set, rewrite); + nownext_set = bdd_replace(nownext_set, rewrite); + notnow_set = bdd_replace(notnow_set, rewrite); + notnext_set = bdd_replace(notnext_set, rewrite); + notvar_set = bdd_replace(notvar_set, rewrite); + var_set = bdd_replace(var_set, rewrite); + varandnext_set = bdd_replace(varandnext_set, rewrite); + acc_set = bdd_replace(acc_set, rewrite); + notacc_set = bdd_replace(notacc_set, rewrite); + negacc_set = bdd_replace(negacc_set, rewrite); + } } diff --git a/src/tgba/tgbabddcoredata.hh b/src/tgba/tgbabddcoredata.hh index 344e62b77..e2eea8d42 100644 --- a/src/tgba/tgbabddcoredata.hh +++ b/src/tgba/tgbabddcoredata.hh @@ -122,6 +122,12 @@ namespace spot /// \brief Update the variable sets to take a new accepting condition /// into account. void declare_accepting_condition(bdd prom); + + /// \brief Translate BDD variables. + /// + /// Rewrite the variables according to \a rewrite. + /// This used by spot::tgba_bdd_translate_factory. + void translate(bddPair* rewrite); }; } diff --git a/src/tgba/tgbabddtranslatefactory.cc b/src/tgba/tgbabddtranslatefactory.cc index a10fb3b6e..506c0e39f 100644 --- a/src/tgba/tgbabddtranslatefactory.cc +++ b/src/tgba/tgbabddtranslatefactory.cc @@ -6,28 +6,11 @@ namespace spot { tgba_bdd_translate_factory::tgba_bdd_translate_factory (const tgba_bdd_concrete& from, const tgba_bdd_dict& to) - : dict_(to) + : data_(from.get_core_data()), dict_(to) { bddPair* rewrite = compute_pairs(from.get_dict()); - - const tgba_bdd_core_data& in = from.get_core_data(); - - data_.relation = bdd_replace(in.relation, rewrite); - data_.accepting_conditions = bdd_replace(in.accepting_conditions, rewrite); - data_.now_set = bdd_replace(in.now_set, rewrite); - data_.next_set = bdd_replace(in.next_set, rewrite); - data_.nownext_set = bdd_replace(in.nownext_set, rewrite); - data_.notnow_set = bdd_replace(in.notnow_set, rewrite); - data_.notnext_set = bdd_replace(in.notnext_set, rewrite); - data_.notvar_set = bdd_replace(in.notvar_set, rewrite); - data_.var_set = bdd_replace(in.var_set, rewrite); - data_.varandnext_set = bdd_replace(in.varandnext_set, rewrite); - data_.acc_set = bdd_replace(in.acc_set, rewrite); - data_.notacc_set = bdd_replace(in.notacc_set, rewrite); - data_.negacc_set = bdd_replace(in.negacc_set, rewrite); - + data_.translate(rewrite); init_ = bdd_replace(from.get_init_bdd(), rewrite); - bdd_freepair(rewrite); }