Commit bf6c9067 authored by Alexandre Duret-Lutz's avatar Alexandre Duret-Lutz
Browse files

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.
parent 51151ab2
...@@ -604,7 +604,7 @@ namespace spot ...@@ -604,7 +604,7 @@ namespace spot
{ {
public: 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) const prop_set* ps, const ltl::formula* dead, int compress)
: d_(d), : d_(d),
state_size_(d_->get_state_variable_count()), state_size_(d_->get_state_variable_count()),
...@@ -998,7 +998,7 @@ namespace spot ...@@ -998,7 +998,7 @@ namespace spot
kripke_ptr 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::atomic_prop_set* to_observe,
const ltl::formula* dead, const ltl::formula* dead,
int compress, int compress,
......
...@@ -57,7 +57,7 @@ namespace spot ...@@ -57,7 +57,7 @@ namespace spot
// dead states // dead states
// \a verbose whether to output verbose messages // \a verbose whether to output verbose messages
SPOT_API kripke_ptr 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::atomic_prop_set* to_observe,
const ltl::formula* dead = ltl::constant::true_instance(), const ltl::formula* dead = ltl::constant::true_instance(),
int compress = 0, bool verbose = true); int compress = 0, bool verbose = true);
......
...@@ -126,7 +126,7 @@ namespace spot ...@@ -126,7 +126,7 @@ namespace spot
// kripke_explicit // kripke_explicit
kripke_explicit::kripke_explicit(bdd_dict_ptr dict, kripke_explicit::kripke_explicit(const bdd_dict_ptr& dict,
state_kripke* init) state_kripke* init)
: dict_(dict), : dict_(dict),
init_ (init) init_ (init)
......
...@@ -114,7 +114,7 @@ namespace spot ...@@ -114,7 +114,7 @@ namespace spot
class SPOT_API kripke_explicit : public kripke class SPOT_API kripke_explicit : public kripke
{ {
public: public:
kripke_explicit(bdd_dict_ptr, state_kripke* = nullptr); kripke_explicit(const bdd_dict_ptr&, state_kripke* = nullptr);
~kripke_explicit(); ~kripke_explicit();
bdd_dict_ptr get_dict() const; bdd_dict_ptr get_dict() const;
......
...@@ -37,7 +37,7 @@ namespace spot ...@@ -37,7 +37,7 @@ namespace spot
{ {
language_containment_checker::language_containment_checker 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) bool branching_postponement, bool fair_loop_approx)
: dict_(dict), exprop_(exprop), symb_merge_(symb_merge), : dict_(dict), exprop_(exprop), symb_merge_(symb_merge),
branching_postponement_(branching_postponement), branching_postponement_(branching_postponement),
......
...@@ -46,7 +46,7 @@ namespace spot ...@@ -46,7 +46,7 @@ namespace spot
public: public:
/// This class uses spot::ltl_to_tgba_fm to translate LTL /// This class uses spot::ltl_to_tgba_fm to translate LTL
/// formulae. See that function for the meaning of these options. /// 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 symb_merge,
bool branching_postponement, bool branching_postponement,
bool fair_loop_approx); bool fair_loop_approx);
......
...@@ -130,12 +130,13 @@ namespace spot ...@@ -130,12 +130,13 @@ namespace spot
dict->unregister_all_my_variables(this); 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) : 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) : dict(d), options(opt), lcc(d, true, true, false, false)
{ {
options.containment_checks |= options.containment_checks_stronger; options.containment_checks |= options.containment_checks_stronger;
...@@ -4694,7 +4695,7 @@ namespace spot ...@@ -4694,7 +4695,7 @@ namespace spot
///////////////////////////////////////////////////////////////////// /////////////////////////////////////////////////////////////////////
// ltl_simplifier // 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); cache_ = new ltl_simplifier_cache(d);
} }
......
...@@ -79,7 +79,7 @@ namespace spot ...@@ -79,7 +79,7 @@ namespace spot
class SPOT_API ltl_simplifier class SPOT_API ltl_simplifier
{ {
public: 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, ltl_simplifier(const ltl_simplifier_options& opt,
bdd_dict_ptr dict = make_bdd_dict()); bdd_dict_ptr dict = make_bdd_dict());
~ltl_simplifier(); ~ltl_simplifier();
......
...@@ -98,7 +98,7 @@ namespace spot ...@@ -98,7 +98,7 @@ namespace spot
} }
std::ostream& 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; dict = d;
where = &os; where = &os;
...@@ -120,7 +120,7 @@ namespace spot ...@@ -120,7 +120,7 @@ namespace spot
} }
std::ostream& 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; dict = d;
where = &os; where = &os;
...@@ -143,7 +143,7 @@ namespace spot ...@@ -143,7 +143,7 @@ namespace spot
} }
std::ostream& 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; dict = d;
where = &os; where = &os;
...@@ -156,7 +156,7 @@ namespace spot ...@@ -156,7 +156,7 @@ namespace spot
} }
std::string std::string
bdd_format_accset(bdd_dict_ptr d, bdd b) bdd_format_accset(const bdd_dict_ptr& d, bdd b)
{ {
std::ostringstream os; std::ostringstream os;
bdd_print_accset(os, d, b); bdd_print_accset(os, d, b);
...@@ -164,7 +164,7 @@ namespace spot ...@@ -164,7 +164,7 @@ namespace spot
} }
std::string std::string
bdd_format_sat(bdd_dict_ptr d, bdd b) bdd_format_sat(const bdd_dict_ptr& d, bdd b)
{ {
std::ostringstream os; std::ostringstream os;
bdd_print_sat(os, d, b); bdd_print_sat(os, d, b);
...@@ -172,7 +172,7 @@ namespace spot ...@@ -172,7 +172,7 @@ namespace spot
} }
std::ostream& 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; dict = d;
want_acc = true; want_acc = true;
...@@ -183,7 +183,7 @@ namespace spot ...@@ -183,7 +183,7 @@ namespace spot
} }
std::string 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; std::ostringstream os;
bdd_print_set(os, d, b); bdd_print_set(os, d, b);
...@@ -191,7 +191,7 @@ namespace spot ...@@ -191,7 +191,7 @@ namespace spot
} }
std::ostream& 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); const ltl::formula* f = bdd_to_formula(b, d);
print_ltl(f, os); print_ltl(f, os);
...@@ -200,7 +200,7 @@ namespace spot ...@@ -200,7 +200,7 @@ namespace spot
} }
std::string std::string
bdd_format_formula(bdd_dict_ptr d, bdd b) bdd_format_formula(const bdd_dict_ptr& d, bdd b)
{ {
std::ostringstream os; std::ostringstream os;
bdd_print_formula(os, d, b); bdd_print_formula(os, d, b);
...@@ -208,7 +208,7 @@ namespace spot ...@@ -208,7 +208,7 @@ namespace spot
} }
std::ostream& 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; dict = d;
want_acc = true; want_acc = true;
...@@ -219,7 +219,7 @@ namespace spot ...@@ -219,7 +219,7 @@ namespace spot
} }
std::ostream& 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; dict = d;
want_acc = true; want_acc = true;
...@@ -236,7 +236,7 @@ namespace spot ...@@ -236,7 +236,7 @@ namespace spot
} }
std::ostream& 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; dict = d;
want_acc = true; want_acc = true;
...@@ -252,7 +252,7 @@ namespace spot ...@@ -252,7 +252,7 @@ namespace spot
} }
std::string std::string
bdd_format_isop(bdd_dict_ptr d, bdd b) bdd_format_isop(const bdd_dict_ptr& d, bdd b)
{ {
std::ostringstream os; std::ostringstream os;
bdd_print_isop(os, d, b); bdd_print_isop(os, d, b);
......
...@@ -38,7 +38,7 @@ namespace spot ...@@ -38,7 +38,7 @@ namespace spot
/// \param dict The dictionary to use, to lookup variables. /// \param dict The dictionary to use, to lookup variables.
/// \param b The BDD to print. /// \param b The BDD to print.
SPOT_API std::ostream& 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. /// \brief Format a BDD as a list of literals.
/// ///
...@@ -47,7 +47,7 @@ namespace spot ...@@ -47,7 +47,7 @@ namespace spot
/// \param b The BDD to print. /// \param b The BDD to print.
/// \return The BDD formated as a string. /// \return The BDD formated as a string.
SPOT_API std::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. /// \brief Print a BDD as a list of acceptance conditions.
/// ///
...@@ -57,7 +57,7 @@ namespace spot ...@@ -57,7 +57,7 @@ namespace spot
/// \param b The BDD to print. /// \param b The BDD to print.
/// \return The BDD formated as a string. /// \return The BDD formated as a string.
SPOT_API std::ostream& 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. /// \brief Print a BDD as a set of acceptance conditions.
/// ///
...@@ -67,7 +67,7 @@ namespace spot ...@@ -67,7 +67,7 @@ namespace spot
/// \param b The BDD to print. /// \param b The BDD to print.
/// \return The BDD formated as a string. /// \return The BDD formated as a string.
SPOT_API std::ostream& 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. /// \brief Format a BDD as a set of acceptance conditions.
/// ///
...@@ -76,49 +76,49 @@ namespace spot ...@@ -76,49 +76,49 @@ namespace spot
/// \param b The BDD to print. /// \param b The BDD to print.
/// \return The BDD formated as a string. /// \return The BDD formated as a string.
SPOT_API std::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. /// \brief Print a BDD as a set.
/// \param os The output stream. /// \param os The output stream.
/// \param dict The dictionary to use, to lookup variables. /// \param dict The dictionary to use, to lookup variables.
/// \param b The BDD to print. /// \param b The BDD to print.
SPOT_API std::ostream& 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. /// \brief Format a BDD as a set.
/// \param dict The dictionary to use, to lookup variables. /// \param dict The dictionary to use, to lookup variables.
/// \param b The BDD to print. /// \param b The BDD to print.
/// \return The BDD formated as a string. /// \return The BDD formated as a string.
SPOT_API std::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. /// \brief Print a BDD as a formula.
/// \param os The output stream. /// \param os The output stream.
/// \param dict The dictionary to use, to lookup variables. /// \param dict The dictionary to use, to lookup variables.
/// \param b The BDD to print. /// \param b The BDD to print.
SPOT_API std::ostream& 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. /// \brief Format a BDD as a formula.
/// \param dict The dictionary to use, to lookup variables. /// \param dict The dictionary to use, to lookup variables.
/// \param b The BDD to print. /// \param b The BDD to print.
/// \return The BDD formated as a string. /// \return The BDD formated as a string.
SPOT_API std::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. /// \brief Print a BDD as a diagram in dotty format.
/// \param os The output stream. /// \param os The output stream.
/// \param dict The dictionary to use, to lookup variables. /// \param dict The dictionary to use, to lookup variables.
/// \param b The BDD to print. /// \param b The BDD to print.
SPOT_API std::ostream& 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. /// \brief Print a BDD as a table.
/// \param os The output stream. /// \param os The output stream.
/// \param dict The dictionary to use, to lookup variables. /// \param dict The dictionary to use, to lookup variables.
/// \param b The BDD to print. /// \param b The BDD to print.
SPOT_API std::ostream& 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. /// \brief Enable UTF-8 output for bdd printers.
SPOT_API void enable_utf8(); SPOT_API void enable_utf8();
...@@ -129,7 +129,7 @@ namespace spot ...@@ -129,7 +129,7 @@ namespace spot
/// \param b The BDD to print. /// \param b The BDD to print.
/// \return The BDD formated as a string. /// \return The BDD formated as a string.
SPOT_API std::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. /// \brief Print a BDD as an irredundant sum of product.
...@@ -137,7 +137,7 @@ namespace spot ...@@ -137,7 +137,7 @@ namespace spot
/// \param dict The dictionary to use, to lookup variables. /// \param dict The dictionary to use, to lookup variables.
/// \param b The BDD to print. /// \param b The BDD to print.
SPOT_API std::ostream& 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);
} }
......
...@@ -35,7 +35,7 @@ namespace spot ...@@ -35,7 +35,7 @@ namespace spot
class formula_to_bdd_visitor: public ltl::visitor class formula_to_bdd_visitor: public ltl::visitor
{ {
public: 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) : d_(d), owner_(owner)
{ {
} }
...@@ -207,7 +207,7 @@ namespace spot ...@@ -207,7 +207,7 @@ namespace spot
} // anonymous } // anonymous
bdd 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); formula_to_bdd_visitor v(d, for_me);
f->accept(v); f->accept(v);
......
...@@ -40,11 +40,11 @@ namespace spot ...@@ -40,11 +40,11 @@ namespace spot
/// for_me. See bdd_dict::unregister_all_my_variables(). /// for_me. See bdd_dict::unregister_all_my_variables().
/// @{ /// @{
SPOT_API bdd 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<typename T> template<typename T>
SPOT_API bdd 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<T>& for_me) const std::shared_ptr<T>& for_me)
{ {
return formula_to_bdd(f, d, for_me.get()); return formula_to_bdd(f, d, for_me.get());
......
...@@ -33,7 +33,7 @@ namespace spot ...@@ -33,7 +33,7 @@ namespace spot
| taa_tgba | | taa_tgba |
`--------*/ `--------*/
taa_tgba::taa_tgba(bdd_dict_ptr dict) taa_tgba::taa_tgba(const bdd_dict_ptr& dict)
: dict_(dict), : dict_(dict),
all_acceptance_conditions_(bddfalse), all_acceptance_conditions_(bddfalse),
all_acceptance_conditions_computed_(false), all_acceptance_conditions_computed_(false),
......
...@@ -35,7 +35,7 @@ namespace spot ...@@ -35,7 +35,7 @@ namespace spot
class SPOT_API taa_tgba : public tgba class SPOT_API taa_tgba : public tgba
{ {
public: public:
taa_tgba(bdd_dict_ptr dict); taa_tgba(const bdd_dict_ptr& dict);
struct transition; struct transition;
typedef std::list<transition*> state; typedef std::list<transition*> state;
......
...@@ -167,7 +167,7 @@ namespace spot ...@@ -167,7 +167,7 @@ namespace spot
mutable unsigned init_number_; mutable unsigned init_number_;
public: public:
tgba_digraph(bdd_dict_ptr dict) tgba_digraph(const bdd_dict_ptr& dict)
: dict_(dict), : dict_(dict),
all_acceptance_conditions_(bddfalse), all_acceptance_conditions_(bddfalse),
neg_acceptance_conditions_(bddtrue), neg_acceptance_conditions_(bddtrue),
...@@ -432,7 +432,7 @@ namespace spot ...@@ -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<tgba_digraph>(dict); return std::make_shared<tgba_digraph>(dict);
} }
......
...@@ -345,7 +345,7 @@ namespace spot ...@@ -345,7 +345,7 @@ namespace spot
tgba_digraph_ptr 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 no_wdba, bool no_simulation,
bool early_susp, bool no_susp_product, bool wdba_smaller, bool early_susp, bool no_susp_product, bool wdba_smaller,
bool oblig) bool oblig)
......