From 304f2496eaab3201a40ede87e9f700ac1b6bc200 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 14 Aug 2015 15:16:26 +0200 Subject: [PATCH] bdddict: remove register_clone_acc * src/twa/bdddict.cc, src/twa/bdddict.hh: Here. --- src/twa/bdddict.cc | 18 ------------------ src/twa/bdddict.hh | 15 --------------- 2 files changed, 33 deletions(-) diff --git a/src/twa/bdddict.cc b/src/twa/bdddict.cc index 9a4d57651..6e4751738 100644 --- a/src/twa/bdddict.cc +++ b/src/twa/bdddict.cc @@ -189,24 +189,6 @@ namespace spot register_acceptance_variables(bdd_low(f), for_me); } - int - bdd_dict::register_clone_acc(int v, const void* for_me) - { - assert(unsigned(v) < bdd_map.size()); - bdd_info& i = bdd_map[v]; - assert(i.type == acc); - - std::ostringstream s; - // FIXME: We could be smarter and reuse unused "$n" numbers. - ltl::print_psl(s, i.f) << '$' << ++i.clone_counts; - const ltl::formula* f = - ltl::atomic_prop::instance(s.str(), - ltl::default_environment::instance()); - int res = register_acceptance_variable(f, for_me); - f->destroy(); - return res; - } - const ltl::formula* bdd_dict::oneacc_to_formula(int var) const { diff --git a/src/twa/bdddict.hh b/src/twa/bdddict.hh index 61f28d817..284891f09 100644 --- a/src/twa/bdddict.hh +++ b/src/twa/bdddict.hh @@ -163,21 +163,6 @@ namespace spot } /// @} - /// \brief Clone an acceptance variable VAR for FOR_ME. - /// - /// This is used in products TGBAs when both operands share the - /// same acceptance variables but they need to be distinguished in - /// the result. - /// @{ - int register_clone_acc(int var, const void* for_me); - - template - int register_clone_acc(int var, std::shared_ptr for_me) - { - return register_clone_acc(var, for_me.get()); - } - /// @} - /// \brief Register BDD variables as acceptance variables. /// /// Register all variables occurring in \a f as acceptance variables