LCOV - code coverage report
Current view: top level - pbes/include/mcrl2/pbes - find_equalities.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 42 45 93.3 %
Date: 2020-02-19 00:44:21 Functions: 12 13 92.3 %
Legend: Lines: hit not hit

          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         448 : 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         128 :   void leave(const and_&)
      42             :   {
      43         128 :     auto& left = below_top();
      44         128 :     auto const& right = top();
      45         128 :     left.join_and(right);
      46         128 :     pop();
      47         128 :   }
      48             : 
      49          37 :   void leave(const or_&)
      50             :   {
      51          37 :     auto& left = below_top();
      52          37 :     auto const& right = top();
      53          37 :     left.join_or(right);
      54          37 :     pop();
      55          37 :   }
      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           6 :   void leave(const forall& x)
      72             :   {
      73           6 :     top().delete_(x.variables());
      74           6 :   }
      75             : 
      76           8 :   void leave(const exists& x)
      77             :   {
      78           8 :     top().delete_(x.variables());
      79           8 :   }
      80             : 
      81             :   // N.B. Use apply here, to avoid going into the recursion
      82         143 :   void apply(const propositional_variable_instantiation&)
      83             :   {
      84         143 :     push(data::detail::find_equalities_expression());
      85         143 :   }
      86             : 
      87             : #if BOOST_MSVC
      88             : #include "mcrl2/core/detail/traverser_msvc.inc.h"
      89             : #endif
      90             : };
      91             : 
      92         448 : 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         115 : std::map<data::variable, std::set<data::data_expression> > find_equalities(const pbes_expression& x)
     105             : {
     106         230 :   detail::find_equalities_traverser_inst f;
     107         115 :   f.apply(x);
     108         115 :   assert(f.expression_stack.size() == 1);
     109         115 :   f.top().close();
     110         230 :   return f.top().equalities;
     111             : }
     112             : 
     113             : inline
     114         109 : std::map<data::variable, std::set<data::data_expression> > find_inequalities(const pbes_expression& x)
     115             : {
     116         218 :   detail::find_equalities_traverser_inst f;
     117         109 :   f.apply(x);
     118         109 :   assert(f.expression_stack.size() == 1);
     119         109 :   f.top().close();
     120         218 :   return f.top().inequalities;
     121             : }
     122             : 
     123             : } // namespace pbes_system
     124             : 
     125             : } // namespace mcrl2
     126             : 
     127             : #endif // MCRL2_PBES_FIND_EQUALITIES_H

Generated by: LCOV version 1.13