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/assignment_sequence_substitution.h 10 : /// \brief add your file description here. 11 : 12 : #ifndef MCRL2_DATA_SUBSTITUTIONS_ASSIGNMENT_SEQUENCE_SUBSTITUTION_H 13 : #define MCRL2_DATA_SUBSTITUTIONS_ASSIGNMENT_SEQUENCE_SUBSTITUTION_H 14 : 15 : #include "mcrl2/data/assignment.h" 16 : #include "mcrl2/data/is_simple_substitution.h" 17 : 18 : namespace mcrl2 { 19 : 20 : namespace data { 21 : 22 : /// \brief Substitution that maps data variables to data expressions. The substitution is stored as an 23 : /// assignment_list. 24 : struct assignment_sequence_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 assignment_list& assignments; 32 : 33 3291 : explicit assignment_sequence_substitution(const assignment_list& assignments_) 34 3291 : : assignments(assignments_) 35 3291 : {} 36 : 37 25188 : const data_expression& operator()(const variable& v) const 38 : { 39 86799 : for (const assignment& a: assignments) 40 : { 41 70699 : if (a.lhs() == v) 42 : { 43 9088 : return a.rhs(); 44 : } 45 : } 46 16100 : return v; 47 : } 48 : }; 49 : 50 : template <> 51 : inline 52 : bool is_simple_substitution(const assignment_sequence_substitution& sigma) 53 : { 54 : for (const assignment& a: sigma.assignments) 55 : { 56 : if (!is_simple_substitution(a.lhs(), a.rhs())) 57 : { 58 : return false; 59 : } 60 : } 61 : return true; 62 : } 63 : 64 : } // namespace data 65 : 66 : } // namespace mcrl2 67 : 68 : #endif // MCRL2_DATA_SUBSTITUTIONS_ASSIGNMENT_SEQUENCE_SUBSTITUTION_H