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

Generated by: LCOV version 1.13