Line data    Source code

       1             : // Author(s): Wieger Wesselink
       2             : // Copyright: see the accompanying file COPYING or copy at
       3             : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
       4             : //
       5             : // Distributed under the Boost Software License, Version 1.0.
       6             : // (See accompanying file LICENSE_1_0.txt or copy at
       7             : // http://www.boost.org/LICENSE_1_0.txt)
       8             : //
       9             : /// \file mcrl2/data/is_simple_substitution.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_DATA_IS_SIMPLE_SUBSTITUTION_H
      13             : #define MCRL2_DATA_IS_SIMPLE_SUBSTITUTION_H
      14             : 
      15             : #include "mcrl2/data/data_expression.h"
      16             : 
      17             : namespace mcrl2 {
      18             : 
      19             : namespace data {
      20             : 
      21             : /// \brief Returns \c true if the substitution \a sigma satisfies the property that
      22             : /// <tt>FV(sigma(x))</tt> is included in <tt>{x}</tt> for all variables x.
      23             : ///
      24             : /// \note The default return value is \c true, so a template specialization is
      25             : /// required to enable this check for substitutions.
      26             : template <typename Substitution>
      27         124 : bool is_simple_substitution(const Substitution& /*sigma*/)
      28             : {
      29         124 :   return true;
      30             : }
      31             : 
      32             : /// \brief Returns true if FV(rhs) is included in {lhs}.
      33             : inline
      34        1075 : bool is_simple_substitution(const data::variable& lhs, const data::data_expression& rhs)
      35             : {
      36        1075 :   std::set<data::variable> v = data::find_free_variables(rhs);
      37        1075 :   if (v.empty())
      38             :   {
      39        1075 :     return true;
      40             :   }
      41           0 :   if (v.size() == 1)
      42             :   {
      43           0 :     return *(v.begin()) == lhs;
      44             :   }
      45           0 :   return false;
      46        1075 : }
      47             : 
      48             : } // namespace data
      49             : 
      50             : } // namespace mcrl2
      51             : 
      52             : #endif // MCRL2_DATA_IS_SIMPLE_SUBSTITUTION_H