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/find_equalities.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_FIND_EQUALITIES_H
      13             : #define MCRL2_PBES_FIND_EQUALITIES_H
      14             : 
      15             : #include "mcrl2/data/find_equalities.h"
      16             : #include "mcrl2/pbes/traverser.h"
      17             : 
      18             : namespace mcrl2 {
      19             : 
      20             : namespace pbes_system {
      21             : 
      22             : namespace detail {
      23             : 
      24             : template <template <class> class Traverser, class Derived>
      25             : struct find_equalities_traverser: public data::detail::find_equalities_traverser<Traverser, Derived>
      26             : {
      27             :   typedef data::detail::find_equalities_traverser<Traverser, Derived> super;
      28             :   using super::enter;
      29             :   using super::leave;
      30             :   using super::apply;
      31             :   using super::push;
      32             :   using super::pop;
      33             :   using super::top;
      34             :   using super::below_top;
      35             : 
      36             :   Derived& derived()
      37             :   {
      38             :     return static_cast<Derived&>(*this);
      39             :   }
      40             : 
      41         137 :   void leave(const and_&)
      42             :   {
      43         137 :     auto& left = below_top();
      44         137 :     auto const& right = top();
      45         137 :     left.join_and(right);
      46         137 :     pop();
      47         137 :   }
      48             : 
      49          44 :   void leave(const or_&)
      50             :   {
      51          44 :     auto& left = below_top();
      52          44 :     auto const& right = top();
      53          44 :     left.join_or(right);
      54          44 :     pop();
      55          44 :   }
      56             : 
      57           3 :   void leave(const imp&)
      58             :   {
      59           3 :     auto& left = below_top();
      60           3 :     auto const& right = top();
      61           3 :     left.swap();
      62           3 :     left.join_or(right);
      63           3 :     pop();
      64           3 :   }
      65             : 
      66           0 :   void leave(const not_&)
      67             :   {
      68           0 :     top().swap();
      69           0 :   }
      70             : 
      71          12 :   void leave(const forall& x)
      72             :   {
      73          12 :     top().delete_(x.variables());
      74          12 :   }
      75             : 
      76          14 :   void leave(const exists& x)
      77             :   {
      78          14 :     top().delete_(x.variables());
      79          14 :   }
      80             : 
      81             :   // N.B. Use apply here, to avoid going into the recursion
      82         144 :   void apply(const propositional_variable_instantiation&)
      83             :   {
      84         144 :     push(data::detail::find_equalities_expression());
      85         144 :   }
      86             : 
      87             : #if BOOST_MSVC
      88             : #include "mcrl2/core/detail/traverser_msvc.inc.h"
      89             : #endif
      90             : };
      91             : 
      92             : struct find_equalities_traverser_inst: public pbes_system::detail::find_equalities_traverser<pbes_system::data_expression_traverser, find_equalities_traverser_inst>
      93             : {
      94             :   typedef pbes_system::detail::find_equalities_traverser<pbes_system::data_expression_traverser, find_equalities_traverser_inst> super;
      95             : 
      96             :   using super::enter;
      97             :   using super::leave;
      98             :   using super::apply;
      99             : };
     100             : 
     101             : } // namespace detail
     102             : 
     103             : inline
     104         126 : std::map<data::variable, std::set<data::data_expression> > find_equalities(const pbes_expression& x)
     105             : {
     106         126 :   detail::find_equalities_traverser_inst f;
     107         126 :   f.apply(x);
     108         126 :   assert(f.expression_stack.size() == 1);
     109         126 :   f.top().close();
     110         252 :   return f.top().equalities.assignments;
     111         126 : }
     112             : 
     113             : inline
     114         119 : std::map<data::variable, std::set<data::data_expression> > find_inequalities(const pbes_expression& x)
     115             : {
     116         119 :   detail::find_equalities_traverser_inst f;
     117         119 :   f.apply(x);
     118         119 :   assert(f.expression_stack.size() == 1);
     119         119 :   f.top().close();
     120         238 :   return f.top().inequalities.assignments;
     121         119 : }
     122             : 
     123             : } // namespace pbes_system
     124             : 
     125             : } // namespace mcrl2
     126             : 
     127             : #endif // MCRL2_PBES_FIND_EQUALITIES_H