From bf6c9067725d7b055d67a1f9ea1508db11a4dd38 Mon Sep 17 00:00:00 2001 From: Alexandre Duret-Lutz Date: Fri, 15 Aug 2014 11:04:16 +0200 Subject: [PATCH] Fix some bdd_dict_ptr not being passed by const reference. * iface/dve2/dve2.cc, iface/dve2/dve2.hh, src/kripke/kripkeexplicit.cc, src/kripke/kripkeexplicit.hh, src/ltlvisit/contain.cc, src/ltlvisit/contain.hh, src/ltlvisit/simplify.cc, src/ltlvisit/simplify.hh, src/tgba/bddprint.cc, src/tgba/bddprint.hh, src/tgba/formula2bdd.cc, src/tgba/formula2bdd.hh, src/tgba/taatgba.cc, src/tgba/taatgba.hh, src/tgba/tgbagraph.hh, src/tgbaalgos/compsusp.cc, src/tgbaalgos/compsusp.hh, src/tgbaalgos/lbtt.cc, src/tgbaalgos/lbtt.hh, src/tgbaalgos/ltl2tgba_fm.cc, src/tgbaalgos/ltl2tgba_fm.hh, src/tgbaalgos/randomgraph.cc, src/tgbaalgos/randomgraph.hh, src/tgbaalgos/translate.cc, src/tgbaalgos/translate.hh, src/tgbaalgos/word.cc, src/tgbaalgos/word.hh: Pass shared_ptr to functions by const ref. --- iface/dve2/dve2.cc | 4 ++-- iface/dve2/dve2.hh | 2 +- src/kripke/kripkeexplicit.cc | 2 +- src/kripke/kripkeexplicit.hh | 2 +- src/ltlvisit/contain.cc | 2 +- src/ltlvisit/contain.hh | 2 +- src/ltlvisit/simplify.cc | 7 ++++--- src/ltlvisit/simplify.hh | 2 +- src/tgba/bddprint.cc | 26 +++++++++++++------------- src/tgba/bddprint.hh | 26 +++++++++++++------------- src/tgba/formula2bdd.cc | 4 ++-- src/tgba/formula2bdd.hh | 4 ++-- src/tgba/taatgba.cc | 2 +- src/tgba/taatgba.hh | 2 +- src/tgba/tgbagraph.hh | 4 ++-- src/tgbaalgos/compsusp.cc | 2 +- src/tgbaalgos/compsusp.hh | 2 +- src/tgbaalgos/lbtt.cc | 6 +++--- src/tgbaalgos/lbtt.hh | 2 +- src/tgbaalgos/ltl2tgba_fm.cc | 4 ++-- src/tgbaalgos/ltl2tgba_fm.hh | 2 +- src/tgbaalgos/randomgraph.cc | 2 +- src/tgbaalgos/randomgraph.hh | 2 +- src/tgbaalgos/translate.cc | 2 +- src/tgbaalgos/translate.hh | 4 ++-- src/tgbaalgos/word.cc | 2 +- src/tgbaalgos/word.hh | 2 +- 27 files changed, 62 insertions(+), 61 deletions(-) diff --git a/iface/dve2/dve2.cc b/iface/dve2/dve2.cc index dfe6001e6..e3d499e7d 100644 --- a/iface/dve2/dve2.cc +++ b/iface/dve2/dve2.cc @@ -604,7 +604,7 @@ namespace spot { public: - dve2_kripke(const dve2_interface* d, bdd_dict_ptr dict, + dve2_kripke(const dve2_interface* d, const bdd_dict_ptr& dict, const prop_set* ps, const ltl::formula* dead, int compress) : d_(d), state_size_(d_->get_state_variable_count()), @@ -998,7 +998,7 @@ namespace spot kripke_ptr - load_dve2(const std::string& file_arg, bdd_dict_ptr dict, + load_dve2(const std::string& file_arg, const bdd_dict_ptr& dict, const ltl::atomic_prop_set* to_observe, const ltl::formula* dead, int compress, diff --git a/iface/dve2/dve2.hh b/iface/dve2/dve2.hh index 1913781e6..26c274fa3 100644 --- a/iface/dve2/dve2.hh +++ b/iface/dve2/dve2.hh @@ -57,7 +57,7 @@ namespace spot // dead states // \a verbose whether to output verbose messages SPOT_API kripke_ptr - load_dve2(const std::string& file, bdd_dict_ptr dict, + load_dve2(const std::string& file, const bdd_dict_ptr& dict, const ltl::atomic_prop_set* to_observe, const ltl::formula* dead = ltl::constant::true_instance(), int compress = 0, bool verbose = true); diff --git a/src/kripke/kripkeexplicit.cc b/src/kripke/kripkeexplicit.cc index 5ed89ef07..4e5f5eaed 100644 --- a/src/kripke/kripkeexplicit.cc +++ b/src/kripke/kripkeexplicit.cc @@ -126,7 +126,7 @@ namespace spot // kripke_explicit - kripke_explicit::kripke_explicit(bdd_dict_ptr dict, + kripke_explicit::kripke_explicit(const bdd_dict_ptr& dict, state_kripke* init) : dict_(dict), init_ (init) diff --git a/src/kripke/kripkeexplicit.hh b/src/kripke/kripkeexplicit.hh index 5e6c26cf3..fb0f1f684 100644 --- a/src/kripke/kripkeexplicit.hh +++ b/src/kripke/kripkeexplicit.hh @@ -114,7 +114,7 @@ namespace spot class SPOT_API kripke_explicit : public kripke { public: - kripke_explicit(bdd_dict_ptr, state_kripke* = nullptr); + kripke_explicit(const bdd_dict_ptr&, state_kripke* = nullptr); ~kripke_explicit(); bdd_dict_ptr get_dict() const; diff --git a/src/ltlvisit/contain.cc b/src/ltlvisit/contain.cc index 13ce4529c..f083f3c3e 100644 --- a/src/ltlvisit/contain.cc +++ b/src/ltlvisit/contain.cc @@ -37,7 +37,7 @@ namespace spot { language_containment_checker::language_containment_checker - (bdd_dict_ptr dict, bool exprop, bool symb_merge, + (const bdd_dict_ptr& dict, bool exprop, bool symb_merge, bool branching_postponement, bool fair_loop_approx) : dict_(dict), exprop_(exprop), symb_merge_(symb_merge), branching_postponement_(branching_postponement), diff --git a/src/ltlvisit/contain.hh b/src/ltlvisit/contain.hh index d21d20010..579390525 100644 --- a/src/ltlvisit/contain.hh +++ b/src/ltlvisit/contain.hh @@ -46,7 +46,7 @@ namespace spot public: /// This class uses spot::ltl_to_tgba_fm to translate LTL /// formulae. See that function for the meaning of these options. - language_containment_checker(bdd_dict_ptr dict, bool exprop, + language_containment_checker(const bdd_dict_ptr& dict, bool exprop, bool symb_merge, bool branching_postponement, bool fair_loop_approx); diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index 0fb89dd7a..fd33b639c 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -130,12 +130,13 @@ namespace spot dict->unregister_all_my_variables(this); } - ltl_simplifier_cache(bdd_dict_ptr d) + ltl_simplifier_cache(const bdd_dict_ptr& d) : dict(d), lcc(d, true, true, false, false) { } - ltl_simplifier_cache(bdd_dict_ptr d, const ltl_simplifier_options& opt) + ltl_simplifier_cache(const bdd_dict_ptr& d, + const ltl_simplifier_options& opt) : dict(d), options(opt), lcc(d, true, true, false, false) { options.containment_checks |= options.containment_checks_stronger; @@ -4694,7 +4695,7 @@ namespace spot ///////////////////////////////////////////////////////////////////// // ltl_simplifier - ltl_simplifier::ltl_simplifier(bdd_dict_ptr d) + ltl_simplifier::ltl_simplifier(const bdd_dict_ptr& d) { cache_ = new ltl_simplifier_cache(d); } diff --git a/src/ltlvisit/simplify.hh b/src/ltlvisit/simplify.hh index 05ae752c6..19e62bdc4 100644 --- a/src/ltlvisit/simplify.hh +++ b/src/ltlvisit/simplify.hh @@ -79,7 +79,7 @@ namespace spot class SPOT_API ltl_simplifier { public: - ltl_simplifier(bdd_dict_ptr dict = make_bdd_dict()); + ltl_simplifier(const bdd_dict_ptr& dict = make_bdd_dict()); ltl_simplifier(const ltl_simplifier_options& opt, bdd_dict_ptr dict = make_bdd_dict()); ~ltl_simplifier(); diff --git a/src/tgba/bddprint.cc b/src/tgba/bddprint.cc index 1927d6944..395609276 100644 --- a/src/tgba/bddprint.cc +++ b/src/tgba/bddprint.cc @@ -98,7 +98,7 @@ namespace spot } std::ostream& - bdd_print_sat(std::ostream& os, bdd_dict_ptr d, bdd b) + bdd_print_sat(std::ostream& os, const bdd_dict_ptr& d, bdd b) { dict = d; where = &os; @@ -120,7 +120,7 @@ namespace spot } std::ostream& - bdd_print_acc(std::ostream& os, bdd_dict_ptr d, bdd b) + bdd_print_acc(std::ostream& os, const bdd_dict_ptr& d, bdd b) { dict = d; where = &os; @@ -143,7 +143,7 @@ namespace spot } std::ostream& - bdd_print_accset(std::ostream& os, bdd_dict_ptr d, bdd b) + bdd_print_accset(std::ostream& os, const bdd_dict_ptr& d, bdd b) { dict = d; where = &os; @@ -156,7 +156,7 @@ namespace spot } std::string - bdd_format_accset(bdd_dict_ptr d, bdd b) + bdd_format_accset(const bdd_dict_ptr& d, bdd b) { std::ostringstream os; bdd_print_accset(os, d, b); @@ -164,7 +164,7 @@ namespace spot } std::string - bdd_format_sat(bdd_dict_ptr d, bdd b) + bdd_format_sat(const bdd_dict_ptr& d, bdd b) { std::ostringstream os; bdd_print_sat(os, d, b); @@ -172,7 +172,7 @@ namespace spot } std::ostream& - bdd_print_set(std::ostream& os, bdd_dict_ptr d, bdd b) + bdd_print_set(std::ostream& os, const bdd_dict_ptr& d, bdd b) { dict = d; want_acc = true; @@ -183,7 +183,7 @@ namespace spot } std::string - bdd_format_set(const bdd_dict_ptr d, bdd b) + bdd_format_set(const bdd_dict_ptr& d, bdd b) { std::ostringstream os; bdd_print_set(os, d, b); @@ -191,7 +191,7 @@ namespace spot } std::ostream& - bdd_print_formula(std::ostream& os, bdd_dict_ptr d, bdd b) + bdd_print_formula(std::ostream& os, const bdd_dict_ptr& d, bdd b) { const ltl::formula* f = bdd_to_formula(b, d); print_ltl(f, os); @@ -200,7 +200,7 @@ namespace spot } std::string - bdd_format_formula(bdd_dict_ptr d, bdd b) + bdd_format_formula(const bdd_dict_ptr& d, bdd b) { std::ostringstream os; bdd_print_formula(os, d, b); @@ -208,7 +208,7 @@ namespace spot } std::ostream& - bdd_print_dot(std::ostream& os, bdd_dict_ptr d, bdd b) + bdd_print_dot(std::ostream& os, const bdd_dict_ptr& d, bdd b) { dict = d; want_acc = true; @@ -219,7 +219,7 @@ namespace spot } std::ostream& - bdd_print_table(std::ostream& os, bdd_dict_ptr d, bdd b) + bdd_print_table(std::ostream& os, const bdd_dict_ptr& d, bdd b) { dict = d; want_acc = true; @@ -236,7 +236,7 @@ namespace spot } std::ostream& - bdd_print_isop(std::ostream& os, bdd_dict_ptr d, bdd b) + bdd_print_isop(std::ostream& os, const bdd_dict_ptr& d, bdd b) { dict = d; want_acc = true; @@ -252,7 +252,7 @@ namespace spot } std::string - bdd_format_isop(bdd_dict_ptr d, bdd b) + bdd_format_isop(const bdd_dict_ptr& d, bdd b) { std::ostringstream os; bdd_print_isop(os, d, b); diff --git a/src/tgba/bddprint.hh b/src/tgba/bddprint.hh index a71bfab31..f8930ef6e 100644 --- a/src/tgba/bddprint.hh +++ b/src/tgba/bddprint.hh @@ -38,7 +38,7 @@ namespace spot /// \param dict The dictionary to use, to lookup variables. /// \param b The BDD to print. SPOT_API std::ostream& - bdd_print_sat(std::ostream& os, bdd_dict_ptr dict, bdd b); + bdd_print_sat(std::ostream& os, const bdd_dict_ptr& dict, bdd b); /// \brief Format a BDD as a list of literals. /// @@ -47,7 +47,7 @@ namespace spot /// \param b The BDD to print. /// \return The BDD formated as a string. SPOT_API std::string - bdd_format_sat(bdd_dict_ptr dict, bdd b); + bdd_format_sat(const bdd_dict_ptr& dict, bdd b); /// \brief Print a BDD as a list of acceptance conditions. /// @@ -57,7 +57,7 @@ namespace spot /// \param b The BDD to print. /// \return The BDD formated as a string. SPOT_API std::ostream& - bdd_print_acc(std::ostream& os, bdd_dict_ptr dict, bdd b); + bdd_print_acc(std::ostream& os, const bdd_dict_ptr& dict, bdd b); /// \brief Print a BDD as a set of acceptance conditions. /// @@ -67,7 +67,7 @@ namespace spot /// \param b The BDD to print. /// \return The BDD formated as a string. SPOT_API std::ostream& - bdd_print_accset(std::ostream& os, bdd_dict_ptr dict, bdd b); + bdd_print_accset(std::ostream& os, const bdd_dict_ptr& dict, bdd b); /// \brief Format a BDD as a set of acceptance conditions. /// @@ -76,49 +76,49 @@ namespace spot /// \param b The BDD to print. /// \return The BDD formated as a string. SPOT_API std::string - bdd_format_accset(bdd_dict_ptr dict, bdd b); + bdd_format_accset(const bdd_dict_ptr& dict, bdd b); /// \brief Print a BDD as a set. /// \param os The output stream. /// \param dict The dictionary to use, to lookup variables. /// \param b The BDD to print. SPOT_API std::ostream& - bdd_print_set(std::ostream& os, bdd_dict_ptr dict, bdd b); + bdd_print_set(std::ostream& os, const bdd_dict_ptr& dict, bdd b); /// \brief Format a BDD as a set. /// \param dict The dictionary to use, to lookup variables. /// \param b The BDD to print. /// \return The BDD formated as a string. SPOT_API std::string - bdd_format_set(bdd_dict_ptr dict, bdd b); + bdd_format_set(const bdd_dict_ptr& dict, bdd b); /// \brief Print a BDD as a formula. /// \param os The output stream. /// \param dict The dictionary to use, to lookup variables. /// \param b The BDD to print. SPOT_API std::ostream& - bdd_print_formula(std::ostream& os, bdd_dict_ptr dict, bdd b); + bdd_print_formula(std::ostream& os, const bdd_dict_ptr& dict, bdd b); /// \brief Format a BDD as a formula. /// \param dict The dictionary to use, to lookup variables. /// \param b The BDD to print. /// \return The BDD formated as a string. SPOT_API std::string - bdd_format_formula(bdd_dict_ptr dict, bdd b); + bdd_format_formula(const bdd_dict_ptr& dict, bdd b); /// \brief Print a BDD as a diagram in dotty format. /// \param os The output stream. /// \param dict The dictionary to use, to lookup variables. /// \param b The BDD to print. SPOT_API std::ostream& - bdd_print_dot(std::ostream& os, bdd_dict_ptr dict, bdd b); + bdd_print_dot(std::ostream& os, const bdd_dict_ptr& dict, bdd b); /// \brief Print a BDD as a table. /// \param os The output stream. /// \param dict The dictionary to use, to lookup variables. /// \param b The BDD to print. SPOT_API std::ostream& - bdd_print_table(std::ostream& os, bdd_dict_ptr dict, bdd b); + bdd_print_table(std::ostream& os, const bdd_dict_ptr& dict, bdd b); /// \brief Enable UTF-8 output for bdd printers. SPOT_API void enable_utf8(); @@ -129,7 +129,7 @@ namespace spot /// \param b The BDD to print. /// \return The BDD formated as a string. SPOT_API std::string - bdd_format_isop(bdd_dict_ptr dict, bdd b); + bdd_format_isop(const bdd_dict_ptr& dict, bdd b); /// \brief Print a BDD as an irredundant sum of product. @@ -137,7 +137,7 @@ namespace spot /// \param dict The dictionary to use, to lookup variables. /// \param b The BDD to print. SPOT_API std::ostream& - bdd_print_isop(std::ostream& os, bdd_dict_ptr dict, bdd b); + bdd_print_isop(std::ostream& os, const bdd_dict_ptr& dict, bdd b); } diff --git a/src/tgba/formula2bdd.cc b/src/tgba/formula2bdd.cc index 4f3648941..78779fb04 100644 --- a/src/tgba/formula2bdd.cc +++ b/src/tgba/formula2bdd.cc @@ -35,7 +35,7 @@ namespace spot class formula_to_bdd_visitor: public ltl::visitor { public: - formula_to_bdd_visitor(bdd_dict_ptr d, void* owner) + formula_to_bdd_visitor(const bdd_dict_ptr& d, void* owner) : d_(d), owner_(owner) { } @@ -207,7 +207,7 @@ namespace spot } // anonymous bdd - formula_to_bdd(const formula* f, bdd_dict_ptr d, void* for_me) + formula_to_bdd(const formula* f, const bdd_dict_ptr& d, void* for_me) { formula_to_bdd_visitor v(d, for_me); f->accept(v); diff --git a/src/tgba/formula2bdd.hh b/src/tgba/formula2bdd.hh index f6c138989..ca93b485c 100644 --- a/src/tgba/formula2bdd.hh +++ b/src/tgba/formula2bdd.hh @@ -40,11 +40,11 @@ namespace spot /// for_me. See bdd_dict::unregister_all_my_variables(). /// @{ SPOT_API bdd - formula_to_bdd(const ltl::formula* f, bdd_dict_ptr d, void* for_me); + formula_to_bdd(const ltl::formula* f, const bdd_dict_ptr& d, void* for_me); template SPOT_API bdd - formula_to_bdd(const ltl::formula* f, bdd_dict_ptr d, + formula_to_bdd(const ltl::formula* f, const bdd_dict_ptr& d, const std::shared_ptr& for_me) { return formula_to_bdd(f, d, for_me.get()); diff --git a/src/tgba/taatgba.cc b/src/tgba/taatgba.cc index c0b554520..97bf72b5c 100644 --- a/src/tgba/taatgba.cc +++ b/src/tgba/taatgba.cc @@ -33,7 +33,7 @@ namespace spot | taa_tgba | `--------*/ - taa_tgba::taa_tgba(bdd_dict_ptr dict) + taa_tgba::taa_tgba(const bdd_dict_ptr& dict) : dict_(dict), all_acceptance_conditions_(bddfalse), all_acceptance_conditions_computed_(false), diff --git a/src/tgba/taatgba.hh b/src/tgba/taatgba.hh index c458a5bf9..3e06eacc8 100644 --- a/src/tgba/taatgba.hh +++ b/src/tgba/taatgba.hh @@ -35,7 +35,7 @@ namespace spot class SPOT_API taa_tgba : public tgba { public: - taa_tgba(bdd_dict_ptr dict); + taa_tgba(const bdd_dict_ptr& dict); struct transition; typedef std::list state; diff --git a/src/tgba/tgbagraph.hh b/src/tgba/tgbagraph.hh index 91c84f8ce..c6a2ad91d 100644 --- a/src/tgba/tgbagraph.hh +++ b/src/tgba/tgbagraph.hh @@ -167,7 +167,7 @@ namespace spot mutable unsigned init_number_; public: - tgba_digraph(bdd_dict_ptr dict) + tgba_digraph(const bdd_dict_ptr& dict) : dict_(dict), all_acceptance_conditions_(bddfalse), neg_acceptance_conditions_(bddtrue), @@ -432,7 +432,7 @@ namespace spot }; - inline tgba_digraph_ptr make_tgba_digraph(bdd_dict_ptr dict) + inline tgba_digraph_ptr make_tgba_digraph(const bdd_dict_ptr& dict) { return std::make_shared(dict); } diff --git a/src/tgbaalgos/compsusp.cc b/src/tgbaalgos/compsusp.cc index 43a101eb0..5e3212891 100644 --- a/src/tgbaalgos/compsusp.cc +++ b/src/tgbaalgos/compsusp.cc @@ -345,7 +345,7 @@ namespace spot tgba_digraph_ptr - compsusp(const ltl::formula* f, bdd_dict_ptr dict, + compsusp(const ltl::formula* f, const bdd_dict_ptr& dict, bool no_wdba, bool no_simulation, bool early_susp, bool no_susp_product, bool wdba_smaller, bool oblig) diff --git a/src/tgbaalgos/compsusp.hh b/src/tgbaalgos/compsusp.hh index 4000393c7..7309f3e5b 100644 --- a/src/tgbaalgos/compsusp.hh +++ b/src/tgbaalgos/compsusp.hh @@ -51,7 +51,7 @@ namespace spot /// long-term stability should better use the services of the /// spot::translator class instead. SPOT_API tgba_digraph_ptr - compsusp(const ltl::formula* f, bdd_dict_ptr dict, + compsusp(const ltl::formula* f, const bdd_dict_ptr& dict, bool no_wdba = false, bool no_simulation = false, bool early_susp = false, bool no_susp_product = false, bool wdba_smaller = false, bool oblig = false); diff --git a/src/tgbaalgos/lbtt.cc b/src/tgbaalgos/lbtt.cc index 95825bd28..5396d5794 100644 --- a/src/tgbaalgos/lbtt.cc +++ b/src/tgbaalgos/lbtt.cc @@ -172,7 +172,7 @@ namespace spot tgba_digraph_ptr lbtt_read_tgba(unsigned num_states, unsigned num_acc, std::istream& is, std::string& error, - bdd_dict_ptr dict, + const bdd_dict_ptr& dict, ltl::environment& env, ltl::environment& envacc) { auto aut = make_tgba_digraph(dict); @@ -237,7 +237,7 @@ namespace spot tgba_digraph_ptr lbtt_read_gba(unsigned num_states, unsigned num_acc, std::istream& is, std::string& error, - bdd_dict_ptr dict, + const bdd_dict_ptr& dict, ltl::environment& env, ltl::environment& envacc) { auto aut = make_tgba_digraph(dict); @@ -313,7 +313,7 @@ namespace spot tgba_digraph_ptr - lbtt_parse(std::istream& is, std::string& error, bdd_dict_ptr dict, + lbtt_parse(std::istream& is, std::string& error, const bdd_dict_ptr& dict, ltl::environment& env, ltl::environment& envacc) { is >> std::skipws; diff --git a/src/tgbaalgos/lbtt.hh b/src/tgbaalgos/lbtt.hh index 0f3919f3a..d9b8688bb 100644 --- a/src/tgbaalgos/lbtt.hh +++ b/src/tgbaalgos/lbtt.hh @@ -53,7 +53,7 @@ namespace spot /// \return the read tgba or 0 on error. SPOT_API tgba_digraph_ptr lbtt_parse(std::istream& is, std::string& error, - bdd_dict_ptr dict, + const bdd_dict_ptr& dict, ltl::environment& env = ltl::default_environment::instance(), ltl::environment& envacc = ltl::default_environment::instance()); } diff --git a/src/tgbaalgos/ltl2tgba_fm.cc b/src/tgbaalgos/ltl2tgba_fm.cc index 1004140f7..7e59ef84d 100644 --- a/src/tgbaalgos/ltl2tgba_fm.cc +++ b/src/tgbaalgos/ltl2tgba_fm.cc @@ -141,7 +141,7 @@ namespace spot { public: - translate_dict(bdd_dict_ptr dict, ltl_simplifier* ls, bool exprop, + translate_dict(const bdd_dict_ptr& dict, ltl_simplifier* ls, bool exprop, bool single_acc) : dict(dict), ls(ls), @@ -2027,7 +2027,7 @@ namespace spot tgba_digraph_ptr - ltl_to_tgba_fm(const formula* f, bdd_dict_ptr dict, + ltl_to_tgba_fm(const formula* f, const bdd_dict_ptr& dict, bool exprop, bool symb_merge, bool branching_postponement, bool fair_loop_approx, const atomic_prop_set* unobs, ltl_simplifier* simplifier) diff --git a/src/tgbaalgos/ltl2tgba_fm.hh b/src/tgbaalgos/ltl2tgba_fm.hh index 3461ee48b..2467f0c94 100644 --- a/src/tgbaalgos/ltl2tgba_fm.hh +++ b/src/tgbaalgos/ltl2tgba_fm.hh @@ -123,7 +123,7 @@ namespace spot /// /// \return A spot::tgba_digraph that recognizes the language of \a f. SPOT_API tgba_digraph_ptr - ltl_to_tgba_fm(const ltl::formula* f, bdd_dict_ptr dict, + ltl_to_tgba_fm(const ltl::formula* f, const bdd_dict_ptr& dict, bool exprop = false, bool symb_merge = true, bool branching_postponement = false, bool fair_loop_approx = false, diff --git a/src/tgbaalgos/randomgraph.cc b/src/tgbaalgos/randomgraph.cc index 9fa80a47e..911d0827f 100644 --- a/src/tgbaalgos/randomgraph.cc +++ b/src/tgbaalgos/randomgraph.cc @@ -82,7 +82,7 @@ namespace spot tgba_digraph_ptr random_graph(int n, float d, - const ltl::atomic_prop_set* ap, bdd_dict_ptr dict, + const ltl::atomic_prop_set* ap, const bdd_dict_ptr& dict, int n_acc, float a, float t, ltl::environment* env) { diff --git a/src/tgbaalgos/randomgraph.hh b/src/tgbaalgos/randomgraph.hh index 67a3ec7d2..c128a9c05 100644 --- a/src/tgbaalgos/randomgraph.hh +++ b/src/tgbaalgos/randomgraph.hh @@ -80,7 +80,7 @@ namespace spot /// successors one by one.) SPOT_API tgba_digraph_ptr random_graph(int n, float d, - const ltl::atomic_prop_set* ap, bdd_dict_ptr dict, + const ltl::atomic_prop_set* ap, const bdd_dict_ptr& dict, int n_acc = 0, float a = 0.1, float t = 0.5, ltl::environment* env = <l::default_environment::instance()); } diff --git a/src/tgbaalgos/translate.cc b/src/tgbaalgos/translate.cc index 3f8ce0d4d..542e1dc65 100644 --- a/src/tgbaalgos/translate.cc +++ b/src/tgbaalgos/translate.cc @@ -41,7 +41,7 @@ namespace spot } } - void translator::build_simplifier(bdd_dict_ptr dict) + void translator::build_simplifier(const bdd_dict_ptr& dict) { ltl::ltl_simplifier_options options(false, false, false); switch (level_) diff --git a/src/tgbaalgos/translate.hh b/src/tgbaalgos/translate.hh index e2b1e7a89..e3bd6623d 100644 --- a/src/tgbaalgos/translate.hh +++ b/src/tgbaalgos/translate.hh @@ -55,7 +55,7 @@ namespace spot setup_opt(opt); } - translator(bdd_dict_ptr dict, const option_map* opt = 0) + translator(const bdd_dict_ptr& dict, const option_map* opt = 0) : postprocessor(opt) { build_simplifier(dict); @@ -114,7 +114,7 @@ namespace spot protected: void setup_opt(const option_map* opt); - void build_simplifier(bdd_dict_ptr dict); + void build_simplifier(const bdd_dict_ptr& dict); private: ltl::ltl_simplifier* simpl_; diff --git a/src/tgbaalgos/word.cc b/src/tgbaalgos/word.cc index 8ae2ed502..50445b3a7 100644 --- a/src/tgbaalgos/word.cc +++ b/src/tgbaalgos/word.cc @@ -84,7 +84,7 @@ namespace spot } std::ostream& - tgba_word::print(std::ostream& os, bdd_dict_ptr d) const + tgba_word::print(std::ostream& os, const bdd_dict_ptr& d) const { if (!prefix.empty()) for (seq_t::const_iterator i = prefix.begin(); i != prefix.end(); ++i) diff --git a/src/tgbaalgos/word.hh b/src/tgbaalgos/word.hh index b463a73db..c5ab33860 100644 --- a/src/tgbaalgos/word.hh +++ b/src/tgbaalgos/word.hh @@ -31,7 +31,7 @@ namespace spot { tgba_word(const tgba_run* run); void simplify(); - std::ostream& print(std::ostream& os, bdd_dict_ptr d) const; + std::ostream& print(std::ostream& os, const bdd_dict_ptr& d) const; typedef std::list seq_t; seq_t prefix;