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/substitutions/variable_assignment.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_DATA_SUBSTITUTIONS_VARIABLE_SUBSTITUTION_H
      13             : #define MCRL2_DATA_SUBSTITUTIONS_VARIABLE_SUBSTITUTION_H
      14             : 
      15             : #include "mcrl2/data/is_simple_substitution.h"
      16             : #include "mcrl2/data/find.h"
      17             : #include "mcrl2/data/undefined.h"
      18             : 
      19             : namespace mcrl2 {
      20             : 
      21             : namespace data {
      22             : 
      23             : /// \brief Substitution that maps a single variable to a data expression
      24             : struct variable_substitution
      25             : {
      26             :   using variable_type = variable;
      27             :   using expression_type = data_expression;
      28             :   using argument_type = variable;
      29             :   using result_type = data_expression;
      30             : 
      31             :   const variable& lhs;
      32             :   const data_expression& rhs;
      33             : 
      34           1 :   variable_substitution(const variable& lhs_, const data_expression& rhs_)
      35           1 :   : lhs(lhs_),
      36           1 :     rhs(rhs_)
      37           1 :   {}
      38             : 
      39           2 :   const data_expression& operator()(const variable& x) const
      40             :   {
      41           2 :     if (x == lhs)
      42             :     {
      43           1 :       return rhs;
      44             :     }
      45           1 :     return x;
      46             :   }
      47             : };
      48             : 
      49             : inline
      50           0 : std::set<data::variable> substitution_variables(const variable_substitution& sigma)
      51             : {
      52           0 :   std::set<data::variable> result;
      53           0 :   data::find_free_variables(sigma.rhs, std::inserter(result, result.end()));
      54           0 :   return result;
      55           0 : }
      56             : 
      57             : } // namespace data
      58             : 
      59             : } // namespace mcrl2
      60             : 
      61             : #endif // MCRL2_DATA_SUBSTITUTIONS_VARIABLE_SUBSTITUTION_H