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/pbes/transformations.h 10 : /// \brief add your file description here. 11 : 12 : #ifndef MCRL2_PBES_TRANSFORMATIONS_H 13 : #define MCRL2_PBES_TRANSFORMATIONS_H 14 : 15 : #include "mcrl2/pbes/builder.h" 16 : 17 : namespace mcrl2 { 18 : 19 : namespace pbes_system { 20 : 21 : namespace detail { 22 : 23 : struct order_quantified_variables_builder: public pbes_expression_builder<order_quantified_variables_builder> 24 : { 25 : typedef pbes_expression_builder<order_quantified_variables_builder> super; 26 : using super::apply; 27 : 28 : const data::data_specification& dataspec; 29 : 30 473 : order_quantified_variables_builder(const data::data_specification& dataspec_) 31 473 : : dataspec(dataspec_) 32 473 : {} 33 : 34 : template <class T> 35 59 : void apply(T& result, const forall& x) 36 : { 37 59 : pbes_expression body; 38 59 : apply(body, x.body()); 39 59 : result = make_forall_(data::order_variables_to_optimise_enumeration(x.variables(), dataspec), body); 40 59 : } 41 : 42 : template <class T> 43 30 : void apply(T& result, const exists& x) 44 : { 45 30 : pbes_expression body; 46 30 : apply(body, x.body()); 47 30 : result = make_exists_(data::order_variables_to_optimise_enumeration(x.variables(), dataspec), body); 48 30 : } 49 : }; 50 : 51 : } // namespace detail 52 : 53 : inline 54 473 : pbes_expression order_quantified_variables(const pbes_expression& x, const data::data_specification& dataspec) 55 : { 56 473 : detail::order_quantified_variables_builder f(dataspec); 57 473 : pbes_expression result; 58 473 : f.apply(result, x); 59 946 : return result; 60 0 : } 61 : 62 : } // namespace pbes_system 63 : 64 : } // namespace mcrl2 65 : 66 : #endif // MCRL2_PBES_TRANSFORMATIONS_H