diff --git a/src/ltlast/binop.hh b/src/ltlast/binop.hh index 7b7b80d74..b71c3c321 100644 --- a/src/ltlast/binop.hh +++ b/src/ltlast/binop.hh @@ -1,5 +1,5 @@ -// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -149,6 +149,91 @@ namespace spot formula* second_; }; + /// \brief Cast \a f into a binop + /// + /// Cast \a f into a binop iff it is a binop instance. Return 0 + /// otherwise. This is faster than \c dynamic_cast. + inline + binop* + is_binop(formula* f) + { + if (f->kind() != formula::BinOp) + return 0; + return static_cast(f); + } + + /// \brief Cast \a f into a binop if it has type \a op. + /// + /// Cast \a f into a binop iff it is a unop instance with operator \a op. + /// Returns 0 otherwise. + inline + binop* + is_binop(formula* f, binop::type op) + { + if (f->kind() != formula::BinOp) + return 0; + binop* bo = static_cast(f); + if (bo->op() != op) + return 0; + return bo; + } + + /// \brief Cast \a f into a binop if it has type \a op1 or \a op2. + /// + /// Cast \a f into a binop iff it is a unop instance with operator \a op1 or + /// \a op2. Returns 0 otherwise. + inline + binop* + is_binop(formula* f, binop::type op1, binop::type op2) + { + if (f->kind() != formula::BinOp) + return 0; + binop* bo = static_cast(f); + binop::type op = bo->op(); + if (op == op1 || op == op2) + return bo; + return 0; + } + + /// \brief Cast \a f into a binop if it is a U. + /// + /// Return 0 otherwise. + inline + binop* + is_U(formula* f) + { + return is_binop(f, binop::U); + } + + /// \brief Cast \a f into a binop if it is a M. + /// + /// Return 0 otherwise. + inline + binop* + is_M(formula* f) + { + return is_binop(f, binop::M); + } + + /// \brief Cast \a f into a binop if it is a R. + /// + /// Return 0 otherwise. + inline + binop* + is_R(formula* f) + { + return is_binop(f, binop::R); + } + + /// \brief Cast \a f into a binop if it is a W. + /// + /// Return 0 otherwise. + inline + binop* + is_W(formula* f) + { + return is_binop(f, binop::W); + } } } diff --git a/src/ltlast/constant.hh b/src/ltlast/constant.hh index 2d3a8fe87..058777d01 100644 --- a/src/ltlast/constant.hh +++ b/src/ltlast/constant.hh @@ -1,5 +1,5 @@ -// Copyright (C) 2009, 2010 Laboratoire de Recherche et D�veloppement -// de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris 6 (LIP6), // // This file is part of Spot, a model checking library. @@ -68,6 +68,19 @@ namespace spot // formula::formula() constructor. }; + + /// \brief Cast \a f into a constant. + /// + /// Cast \a f into a constant iff it is a constant instance. + /// Return 0 otherwise. This is faster than \c dynamic_cast. + inline + constant* + is_constant(formula* f) + { + if (f->kind() != formula::Constant) + return 0; + return static_cast(f); + } } } diff --git a/src/ltlast/multop.hh b/src/ltlast/multop.hh index 1cfe4bebb..033de21e9 100644 --- a/src/ltlast/multop.hh +++ b/src/ltlast/multop.hh @@ -165,6 +165,71 @@ namespace spot vec* children_; }; + + /// \brief Cast \a f into a multop. + /// + /// Cast \a f into a multop iff it is a multop instance. Return 0 + /// otherwise. This is faster than \c dynamic_cast. + inline + multop* + is_multop(formula* f) + { + if (f->kind() != formula::MultOp) + return 0; + return static_cast(f); + } + + /// \brief Cast \a f into a multop if it has type \a op. + /// + /// Cast \a f into a multop iff it is a multop instance with operator \a op. + /// Returns 0 otherwise. + inline + multop* + is_multop(formula* f, multop::type op) + { + if (f->kind() != formula::MultOp) + return 0; + multop* mo = static_cast(f); + if (mo->op() != op) + return 0; + return mo; + } + + /// \brief Cast \a f into a multop if it has type \a op1 or \a op2. + /// + /// Cast \a f into a multop iff it is a multop instance with operator \a op1 + /// or \a op2. Returns 0 otherwise. + inline + multop* + is_multop(const formula* f, multop::type op1, multop::type op2) + { + if (f->kind() != formula::MultOp) + return 0; + multop* mo = static_cast(const_cast(f)); + if (mo->op() != op1 && mo->op() != op2) + return 0; + return mo; + } + + /// \brief Cast \a f into a multop if it is an And. + /// + /// Return 0 otherwise. + inline + multop* + is_And(formula* f) + { + return is_multop(f, multop::And); + } + + /// \brief Cast \a f into a multop if it is an Or. + /// + /// Return 0 otherwise. + inline + multop* + is_Or(formula* f) + { + return is_multop(f, multop::Or); + } } } diff --git a/src/ltlast/unop.hh b/src/ltlast/unop.hh index cc72f7674..dd322dc35 100644 --- a/src/ltlast/unop.hh +++ b/src/ltlast/unop.hh @@ -1,5 +1,5 @@ -// Copyright (C) 2009, 2010, 2011 Laboratoire de Recherche et Développement -// de l'Epita (LRDE). +// Copyright (C) 2009, 2010, 2011, 2012 Laboratoire de Recherche et +// Développement de l'Epita (LRDE). // Copyright (C) 2003, 2004 Laboratoire d'Informatique de Paris // 6 (LIP6), département Systèmes Répartis Coopératifs (SRC), // Université Pierre et Marie Curie. @@ -124,6 +124,91 @@ namespace spot formula* child_; }; + + /// \brief Cast \a f into a unop + /// + /// Cast \a f into a unop iff it is a unop instance. Return 0 + /// otherwise. This is faster than \c dynamic_cast. + inline + unop* + is_unop(formula* f) + { + if (f->kind() != formula::UnOp) + return 0; + return static_cast(f); + } + + /// \brief Cast \a f into a unop if it has type \a op. + /// + /// Cast \a f into a unop iff it is a unop instance with operator \a op. + /// Returns 0 otherwise. + inline + unop* + is_unop(formula* f, unop::type op) + { + if (f->kind() != formula::UnOp) + return 0; + unop* uo = static_cast(f); + if (uo->op() != op) + return 0; + return uo; + } + + /// \brief Cast \a f into a unop if it is a X. + /// + /// Return 0 otherwise. + inline + unop* + is_X(formula* f) + { + return is_unop(f, unop::X); + } + + /// \brief Cast \a f into a unop if it is a F. + /// + /// Return 0 otherwise. + inline + unop* + is_F(formula* f) + { + return is_unop(f, unop::F); + } + + /// \brief Cast \a f into a unop if it is a G. + /// + /// Return 0 otherwise. + inline + unop* + is_G(formula* f) + { + return is_unop(f, unop::G); + } + + /// \brief Cast \a f into a unop if has the form GF(...). + /// + /// Return 0 otherwise. + inline + unop* + is_GF(formula* f) + { + unop* op = is_G(f); + if (!op) + return 0; + return is_F(op->child()); + } + + /// \brief Cast \a f into a unop if has the form FG(...). + /// + /// Return 0 otherwise. + inline + unop* + is_FG(formula* f) + { + unop* op = is_F(f); + if (!op) + return 0; + return is_G(op->child()); + } } } diff --git a/src/ltlvisit/simplify.cc b/src/ltlvisit/simplify.cc index be194eb1b..38eaa507b 100644 --- a/src/ltlvisit/simplify.cc +++ b/src/ltlvisit/simplify.cc @@ -664,126 +664,8 @@ namespace spot formula* simplify_recursively(const formula* f, ltl_simplifier_cache* c); - constant* - is_constant(formula* f) - { - if (f->kind() != formula::Constant) - return 0; - return static_cast(f); - } - unop* - is_unop(formula* f) - { - if (f->kind() != formula::UnOp) - return 0; - return static_cast(f); - } - - unop* - is_unop(formula* f, unop::type op) - { - if (f->kind() != formula::UnOp) - return 0; - unop* uo = static_cast(f); - if (uo->op() != op) - return 0; - return uo; - } - - unop* - is_X(formula* f) - { - return is_unop(f, unop::X); - } - - unop* - is_F(formula* f) - { - return is_unop(f, unop::F); - } - - unop* - is_G(formula* f) - { - return is_unop(f, unop::G); - } - - unop* - is_GF(formula* f) - { - unop* op = is_G(f); - if (!op) - return 0; - return is_F(op->child()); - } - - unop* - is_FG(formula* f) - { - unop* op = is_F(f); - if (!op) - return 0; - return is_G(op->child()); - } - - binop* - is_binop(formula* f) - { - if (f->kind() != formula::BinOp) - return 0; - return static_cast(f); - } - - binop* - is_binop(formula* f, binop::type op) - { - if (f->kind() != formula::BinOp) - return 0; - binop* bo = static_cast(f); - if (bo->op() != op) - return 0; - return bo; - } - - // Same with two choices. - binop* - is_binop(formula* f, binop::type op1, binop::type op2) - { - if (f->kind() != formula::BinOp) - return 0; - binop* bo = static_cast(f); - binop::type op = bo->op(); - if (op == op1 || op == op2) - return bo; - return 0; - } - - binop* - is_U(formula* f) - { - return is_binop(f, binop::U); - } - - binop* - is_M(formula* f) - { - return is_binop(f, binop::M); - } - - binop* - is_R(formula* f) - { - return is_binop(f, binop::R); - } - - binop* - is_W(formula* f) - { - return is_binop(f, binop::W); - } - // X(a) R b or X(a) M b // This returns a. formula* @@ -812,29 +694,6 @@ namespace spot return uo->child(); } - multop* - is_multop(formula* f, multop::type op) - { - if (f->kind() != formula::MultOp) - return 0; - multop* mo = static_cast(f); - if (mo->op() != op) - return 0; - return mo; - } - - multop* - is_And(formula* f) - { - return is_multop(f, multop::And); - } - - multop* - is_Or(formula* f) - { - return is_multop(f, multop::Or); - } - // b & X(b W a) or b & X(b U a) // This returns (b W a) or (b U a). binop*