LCOV - code coverage report
Current view: top level - pbes/include/mcrl2/pbes/rewriters - simplify_quantifiers_rewriter.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 54 58 93.1 %
Date: 2019-06-26 00:32:26 Functions: 10 12 83.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/rewriters/simplify_quantifiers_rewriter.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_REWRITERS_SIMPLIFY_QUANTIFIERS_REWRITER_H
      13             : #define MCRL2_PBES_REWRITERS_SIMPLIFY_QUANTIFIERS_REWRITER_H
      14             : 
      15             : #include "mcrl2/data/detail/data_sequence_algorithm.h"
      16             : #include "mcrl2/data/optimized_boolean_operators.h"
      17             : #include "mcrl2/pbes/rewriters/simplify_rewriter.h"
      18             : 
      19             : namespace mcrl2 {
      20             : 
      21             : namespace pbes_system {
      22             : 
      23             : namespace detail {
      24             : 
      25             : template <template <class> class Builder, class Derived>
      26         627 : struct add_simplify_quantifiers: public Builder<Derived>
      27             : {
      28             :   typedef Builder<Derived> super;
      29             :   using super::apply;
      30             : 
      31         101 :   pbes_expression apply(const forall& x)
      32             :   {
      33         101 :     pbes_expression result;
      34         202 :     pbes_expression body = super::apply(x.body());
      35         101 :     auto const& variables = x.variables();
      36             : 
      37         101 :     if (variables.empty())
      38             :     {
      39           0 :       result = true_();
      40             :     }
      41         101 :     else if (is_not(body))
      42             :     {
      43           0 :       result = data::optimized_not(data::optimized_exists(variables, atermpp::down_cast<not_>(body).operand(), true));
      44             :     }
      45         101 :     if (is_and(body))
      46             :     {
      47           9 :       auto const& left = atermpp::down_cast<and_>(body).left();
      48           9 :       auto const& right = atermpp::down_cast<and_>(body).right();
      49           9 :       result = data::optimized_and(data::optimized_forall(variables, left, true), data::optimized_forall(variables, right, true));
      50             :     }
      51          92 :     else if (is_or(body))
      52             :     {
      53          64 :       auto const& left = atermpp::down_cast<or_>(body).left();
      54          64 :       auto const& right = atermpp::down_cast<or_>(body).right();
      55         128 :       data::variable_list lv = data::detail::set_intersection(variables, free_variables(left));
      56         128 :       data::variable_list rv = data::detail::set_intersection(variables, free_variables(right));
      57          64 :       if (lv.empty())
      58             :       {
      59          55 :         result = data::optimized_or(left, data::optimized_forall_no_empty_domain(rv, right, true));
      60             :       }
      61           9 :       else if (rv.empty())
      62             :       {
      63           3 :         result = data::optimized_or(right, data::optimized_forall_no_empty_domain(lv, left, true));
      64             :       }
      65             :       else
      66             :       {
      67           6 :         result = data::optimized_forall(variables, body, true);
      68             :       }
      69             :     }
      70             :     else
      71             :     {
      72          28 :       result = data::optimized_forall(variables, body, true);
      73             :     }
      74         202 :     return result;
      75             :   }
      76             : 
      77         267 :   pbes_expression apply(const exists& x)
      78             :   {
      79         267 :     pbes_expression result;
      80         534 :     pbes_expression body = super::apply(x.body());
      81         267 :     auto const& variables = x.variables();
      82             : 
      83         267 :     if (variables.empty())
      84             :     {
      85           0 :       result = false_();
      86             :     }
      87         267 :     else if (is_not(body))
      88             :     {
      89           0 :       result = data::optimized_not(data::optimized_forall(variables, atermpp::down_cast<not_>(body).operand(), true));
      90             :     }
      91         267 :     if (is_or(body))
      92             :     {
      93           9 :       auto const& left = atermpp::down_cast<or_>(body).left();
      94           9 :       auto const& right = atermpp::down_cast<or_>(body).right();
      95           9 :       result = data::optimized_or(data::optimized_exists(variables, left, true), data::optimized_exists(variables, right, true));
      96             :     }
      97         258 :     else if (is_and(body))
      98             :     {
      99          64 :       auto const& left = atermpp::down_cast<and_>(body).left();
     100          64 :       auto const& right = atermpp::down_cast<and_>(body).right();
     101         128 :       data::variable_list lv = data::detail::set_intersection(variables, free_variables(left));
     102         128 :       data::variable_list rv = data::detail::set_intersection(variables, free_variables(right));
     103          64 :       if (lv.empty())
     104             :       {
     105          20 :         result = data::optimized_and(left, data::optimized_exists_no_empty_domain(rv, right, true));
     106             :       }
     107          44 :       else if (rv.empty())
     108             :       {
     109           3 :         result = data::optimized_and(right, data::optimized_exists_no_empty_domain(lv, left, true));
     110             :       }
     111             :       else
     112             :       {
     113          41 :         result = data::optimized_exists(variables, body, true);
     114             :       }
     115             :     }
     116             :     else
     117             :     {
     118         194 :       result = data::optimized_exists(variables, body, true);
     119             :     }
     120         534 :     return result;
     121             :   }
     122             : };
     123             : 
     124             : template <typename Derived>
     125         627 : struct simplify_quantifiers_builder: public add_simplify_quantifiers<pbes_system::detail::simplify_builder, Derived>
     126             : { };
     127             : 
     128             : template <typename Derived, typename DataRewriter, typename SubstitutionFunction>
     129             : struct simplify_quantifiers_data_rewriter_builder: public add_data_rewriter<pbes_system::detail::simplify_quantifiers_builder, Derived, DataRewriter, SubstitutionFunction>
     130             : {
     131             :   typedef add_data_rewriter<pbes_system::detail::simplify_quantifiers_builder, Derived, DataRewriter, SubstitutionFunction> super;
     132             :   using super::enter;
     133             :   using super::leave;
     134             : 
     135         627 :   simplify_quantifiers_data_rewriter_builder(const DataRewriter& R, SubstitutionFunction& sigma)
     136         627 :     : super(R, sigma)
     137         627 :   {}
     138             : };
     139             : 
     140             : } // namespace detail
     141             : 
     142             : /// \brief A rewriter that simplifies boolean expressions and quantifiers.
     143             : struct simplify_quantifiers_rewriter
     144             : {
     145             :   typedef pbes_expression term_type;
     146             :   typedef data::variable variable_type;
     147             : 
     148             :   pbes_expression operator()(const pbes_expression& x) const
     149             :   {
     150             :     return core::make_apply_builder<detail::simplify_quantifiers_builder>().apply(x);
     151             :   }
     152             : };
     153             : 
     154             : /// \brief A rewriter that simplifies boolean expressions and quantifiers, and rewrites data expressions.
     155             : template <typename DataRewriter>
     156             : struct simplify_quantifiers_data_rewriter
     157             : {
     158             :   typedef pbes_expression term_type;
     159             :   typedef data::variable variable_type;
     160             : 
     161             :   const DataRewriter& R;
     162             : 
     163         138 :   simplify_quantifiers_data_rewriter(const DataRewriter& R_)
     164         138 :     : R(R_)
     165         138 :   {}
     166             : 
     167         519 :   pbes_expression operator()(const pbes_expression& x) const
     168             :   {
     169             :     data::no_substitution sigma;
     170         519 :     return detail::make_apply_rewriter_builder<detail::simplify_quantifiers_data_rewriter_builder>(R, sigma).apply(x);
     171             :   }
     172             : 
     173             :   template <typename SubstitutionFunction>
     174             :   pbes_expression operator()(const pbes_expression& x, SubstitutionFunction& sigma) const
     175             :   {
     176             :     return detail::make_apply_rewriter_builder<detail::simplify_quantifiers_data_rewriter_builder>(R, sigma).apply(x);
     177             :   }
     178             : };
     179             : 
     180             : } // namespace pbes_system
     181             : 
     182             : } // namespace mcrl2
     183             : 
     184             : #endif // MCRL2_PBES_REWRITERS_SIMPLIFY_QUANTIFIERS_REWRITER_H

Generated by: LCOV version 1.12