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

ltlast: move all accessor methods to headers to help the optimizer

* src/ltlast/atomic_prop.cc, src/ltlast/atomic_prop.hh,
src/ltlast/automatop.cc, src/ltlast/automatop.hh, src/ltlast/binop.cc,
src/ltlast/binop.hh, src/ltlast/bunop.cc, src/ltlast/bunop.hh,
src/ltlast/constant.cc, src/ltlast/constant.hh, src/ltlast/multop.cc,
src/ltlast/multop.hh, src/ltlast/unop.cc, src/ltlast/unop.hh: Move all
one-line accessors methods like nth(), child(), op()... from *.cc files
to their respective *.hh files.
parent 9020ac8b
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche // Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
// et Développement de l'Epita (LRDE). // Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie. // Université Pierre et Marie Curie.
...@@ -85,18 +85,6 @@ namespace spot ...@@ -85,18 +85,6 @@ namespace spot
v.visit(this); v.visit(this);
} }
const std::string&
atomic_prop::name() const
{
return name_;
}
environment&
atomic_prop::env() const
{
return *env_;
}
atomic_prop::map atomic_prop::instances; atomic_prop::map atomic_prop::instances;
const atomic_prop* const atomic_prop*
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2009, 2012, 2013 Laboratoire de Recherche et // Copyright (C) 2009, 2012, 2013, 2014 Laboratoire de Recherche et
// Développement de l'Epita (LRDE). // Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// département Systèmes Répartis Coopératifs (SRC), Université Pierre // département Systèmes Répartis Coopératifs (SRC), Université Pierre
...@@ -49,9 +49,16 @@ namespace spot ...@@ -49,9 +49,16 @@ namespace spot
virtual void accept(visitor& visitor) const; virtual void accept(visitor& visitor) const;
/// Get the name of the atomic proposition. /// Get the name of the atomic proposition.
const std::string& name() const; const std::string& name() const
{
return name_;
}
/// Get the environment of the atomic proposition. /// Get the environment of the atomic proposition.
environment& env() const; environment& env() const
{
return *env_;
}
/// Return a canonic representation of the atomic proposition /// Return a canonic representation of the atomic proposition
virtual std::string dump() const; virtual std::string dump() const;
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013 Laboratoire de // Copyright (C) 2008, 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire
// Recherche et Développement de l'Epita (LRDE) // de Recherche et Développement de l'Epita (LRDE)
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
...@@ -30,6 +30,8 @@ namespace spot ...@@ -30,6 +30,8 @@ namespace spot
automatop::automatop(const nfa::ptr nfa, vec* v, bool negated) automatop::automatop(const nfa::ptr nfa, vec* v, bool negated)
: ref_formula(AutomatOp), nfa_(nfa), children_(v), negated_(negated) : ref_formula(AutomatOp), nfa_(nfa), children_(v), negated_(negated)
{ {
assert(nfa);
is.boolean = false; is.boolean = false;
is.sugar_free_boolean = true; is.sugar_free_boolean = true;
is.in_nenoform = true; is.in_nenoform = true;
...@@ -64,7 +66,8 @@ namespace spot ...@@ -64,7 +66,8 @@ namespace spot
instances.erase(i); instances.erase(i);
// Dereference children. // Dereference children.
for (unsigned n = 0; n < size(); ++n) unsigned s = size();
for (unsigned n = 0; n < s; ++n)
nth(n)->destroy(); nth(n)->destroy();
delete children_; delete children_;
...@@ -115,31 +118,6 @@ namespace spot ...@@ -115,31 +118,6 @@ namespace spot
return res; return res;
} }
unsigned
automatop::size() const
{
return children_->size();
}
const formula*
automatop::nth(unsigned n) const
{
return (*children_)[n];
}
const spot::ltl::nfa::ptr
automatop::get_nfa() const
{
assert(nfa_ != 0);
return nfa_;
}
bool
automatop::is_negated() const
{
return negated_;
}
unsigned unsigned
automatop::instance_count() automatop::instance_count()
{ {
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2008, 2009, 2012, 2013 Laboratoire de Recherche et // Copyright (C) 2008, 2009, 2012, 2013, 2014 Laboratoire de Recherche et
// Développement de l'Epita (LRDE) // Développement de l'Epita (LRDE)
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
...@@ -52,18 +52,31 @@ namespace spot ...@@ -52,18 +52,31 @@ namespace spot
virtual void accept(visitor& v) const; virtual void accept(visitor& v) const;
/// Get the number of argument. /// Get the number of arguments.
unsigned size() const; unsigned size() const
{
return children_->size();
}
/// \brief Get the nth argument. /// \brief Get the nth argument.
/// ///
/// Starting with \a n = 0. /// Starting with \a n = 0.
const formula* nth(unsigned n) const; const formula* nth(unsigned n) const
{
return (*children_)[n];
}
/// Get the NFA of this operator. /// Get the NFA of this operator.
const spot::ltl::nfa::ptr get_nfa() const; const spot::ltl::nfa::ptr get_nfa() const
{
return nfa_;
}
/// Whether the automaton is negated. /// Whether the automaton is negated.
bool is_negated() const; bool is_negated() const
{
return negated_;
}
/// Return a canonic representation of the atomic proposition /// Return a canonic representation of the atomic proposition
std::string dump() const; std::string dump() const;
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche // Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
// et Développement de l'Epita (LRDE). // Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris // Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie. // Université Pierre et Marie Curie.
...@@ -275,24 +275,6 @@ namespace spot ...@@ -275,24 +275,6 @@ namespace spot
v.visit(this); v.visit(this);
} }
const formula*
binop::first() const
{
return first_;
}
const formula*
binop::second() const
{
return second_;
}
binop::type
binop::op() const
{
return op_;
}
const char* const char*
binop::op_name() const binop::op_name() const
{ {
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche // Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
// et Développement de l'Epita (LRDE). // Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie. // Université Pierre et Marie Curie.
...@@ -112,12 +112,23 @@ namespace spot ...@@ -112,12 +112,23 @@ namespace spot
virtual void accept(visitor& v) const; virtual void accept(visitor& v) const;
/// Get the first operand. /// Get the first operand.
const formula* first() const; const formula* first() const
{
return first_;
}
/// Get the second operand. /// Get the second operand.
const formula* second() const; const formula* second() const
{
return second_;
}
/// Get the type of this operator. /// Get the type of this operator.
type op() const; type op() const
{
return op_;
}
/// Get the type of this operator, as a string. /// Get the type of this operator, as a string.
const char* op_name() const; const char* op_name() const;
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche // Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
// et Développement de l'Epita (LRDE). // Recherche et Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
...@@ -100,30 +100,6 @@ namespace spot ...@@ -100,30 +100,6 @@ namespace spot
v.visit(this); v.visit(this);
} }
const formula*
bunop::child() const
{
return child_;
}
unsigned
bunop::min() const
{
return min_;
}
unsigned
bunop::max() const
{
return max_;
}
bunop::type
bunop::op() const
{
return op_;
}
const char* const char*
bunop::op_name() const bunop::op_name() const
{ {
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2010, 2011, 2012, 2013 Laboratoire de Recherche et // Copyright (C) 2010, 2011, 2012, 2013, 2014 Laboratoire de Recherche
// Développement de l'Epita (LRDE). // et Développement de l'Epita (LRDE).
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
// //
...@@ -87,12 +87,22 @@ namespace spot ...@@ -87,12 +87,22 @@ namespace spot
virtual void accept(visitor& v) const; virtual void accept(visitor& v) const;
/// Get the sole operand of this operator. /// Get the sole operand of this operator.
const formula* child() const; const formula* child() const
{
return child_;
}
/// Minimum number of repetition. /// Minimum number of repetition.
unsigned min() const; unsigned min() const
{
return min_;
}
/// Minimum number of repetition. /// Minimum number of repetition.
unsigned max() const; unsigned max() const
{
return max_;
}
/// \brief A string representation of the operator. /// \brief A string representation of the operator.
/// ///
...@@ -100,7 +110,11 @@ namespace spot ...@@ -100,7 +110,11 @@ namespace spot
std::string format() const; std::string format() const;
/// Get the type of this operator. /// Get the type of this operator.
type op() const; type op() const
{
return op_;
}
/// Get the type of this operator, as a string. /// Get the type of this operator, as a string.
const char* op_name() const; const char* op_name() const;
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche // Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
// et Développement de l'Epita (LRDE). // Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris // Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie. // Université Pierre et Marie Curie.
...@@ -111,12 +111,6 @@ namespace spot ...@@ -111,12 +111,6 @@ namespace spot
v.visit(this); v.visit(this);
} }
constant::type
constant::val() const
{
return val_;
}
const char* const char*
constant::val_name() const constant::val_name() const
{ {
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2012, 2013 Laboratoire de Recherche et // Copyright (C) 2009, 2010, 2012, 2013, 2014 Laboratoire de Recherche
// Développement de l'Epita (LRDE). // et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6),
// //
// This file is part of Spot, a model checking library. // This file is part of Spot, a model checking library.
...@@ -39,7 +39,11 @@ namespace spot ...@@ -39,7 +39,11 @@ namespace spot
virtual void accept(visitor& v) const; virtual void accept(visitor& v) const;
/// Return the value of the constant. /// Return the value of the constant.
type val() const; type val() const
{
return val_;
}
/// Return the value of the constant as a string. /// Return the value of the constant as a string.
const char* val_name() const; const char* val_name() const;
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche // Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
// et Développement de l'Epita (LRDE). // Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de // Copyright (C) 2003, 2004, 2005 Laboratoire d'Informatique de
// Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Paris 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie. // Université Pierre et Marie Curie.
...@@ -100,7 +100,8 @@ namespace spot ...@@ -100,7 +100,8 @@ namespace spot
instances.erase(i); instances.erase(i);
// Dereference children. // Dereference children.
for (unsigned n = 0; n < size(); ++n) unsigned s = size();
for (unsigned n = 0; n < s; ++n)
nth(n)->destroy(); nth(n)->destroy();
delete children_; delete children_;
...@@ -124,18 +125,6 @@ namespace spot ...@@ -124,18 +125,6 @@ namespace spot
v.visit(this); v.visit(this);
} }
unsigned
multop::size() const
{
return children_->size();
}
const formula*
multop::nth(unsigned n) const
{
return (*children_)[n];
}
const formula* const formula*
multop::all_but(unsigned n) const multop::all_but(unsigned n) const
{ {
...@@ -176,12 +165,6 @@ namespace spot ...@@ -176,12 +165,6 @@ namespace spot
return instance(op_, v); return instance(op_, v);
} }
multop::type
multop::op() const
{
return op_;
}
const char* const char*
multop::op_name() const multop::op_name() const
{ {
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche // Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
// et Développement de l'Epita (LRDE). // Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie. // Université Pierre et Marie Curie.
...@@ -125,11 +125,18 @@ namespace spot ...@@ -125,11 +125,18 @@ namespace spot
virtual void accept(visitor& v) const; virtual void accept(visitor& v) const;
/// Get the number of children. /// Get the number of children.
unsigned size() const; unsigned size() const
{
return children_->size();
}
/// \brief Get the nth child. /// \brief Get the nth child.
/// ///
/// Starting with \a n = 0. /// Starting with \a n = 0.
const formula* nth(unsigned n) const; const formula* nth(unsigned n) const
{
return (*children_)[n];
}
/// \brief construct a formula without the nth child. /// \brief construct a formula without the nth child.
/// ///
...@@ -156,7 +163,11 @@ namespace spot ...@@ -156,7 +163,11 @@ namespace spot
const formula* boolean_operands(unsigned* width = 0) const; const formula* boolean_operands(unsigned* width = 0) const;
/// Get the type of this operator. /// Get the type of this operator.
type op() const; type op() const
{
return op_;
}
/// Get the type of this operator, as a string. /// Get the type of this operator, as a string.
const char* op_name() const; const char* op_name() const;
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche // Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
// et Développement de l'Epita (LRDE). // Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris // Copyright (C) 2003, 2005 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie. // Université Pierre et Marie Curie.
...@@ -167,18 +167,6 @@ namespace spot ...@@ -167,18 +167,6 @@ namespace spot
v.visit(this); v.visit(this);
} }
const formula*
unop::child() const
{
return child_;
}
unop::type
unop::op() const
{
return op_;
}
const char* const char*
unop::op_name() const unop::op_name() const
{ {
......
// -*- coding: utf-8 -*- // -*- coding: utf-8 -*-
// Copyright (C) 2009, 2010, 2011, 2012, 2013 Laboratoire de Recherche // Copyright (C) 2009, 2010, 2011, 2012, 2013, 2014 Laboratoire de
// et Développement de l'Epita (LRDE). // Recherche et Développement de l'Epita (LRDE).
// Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris
// 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC),
// Université Pierre et Marie Curie. // Université Pierre et Marie Curie.
...@@ -91,10 +91,17 @@ namespace spot ...@@ -91,10 +91,17 @@ namespace spot
virtual void accept(visitor& v) const; virtual void accept(visitor& v) const;
/// Get the sole operand of this operator. /// Get the sole operand of this operator.
const formula* child() const; const formula* child() const
{
return child_;