LCOV - code coverage report
Current view: top level - pbes/include/mcrl2/pbes/rewriters - enumerate_quantifiers_rewriter.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 78 85 91.8 %
Date: 2020-01-19 00:33:35 Functions: 28 33 84.8 %
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/enumerate_quantifiers_rewriter.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_REWRITERS_ENUMERATE_QUANTIFIERS_REWRITER_H
      13             : #define MCRL2_PBES_REWRITERS_ENUMERATE_QUANTIFIERS_REWRITER_H
      14             : 
      15             : #include "mcrl2/data/detail/split_finite_variables.h"
      16             : #include "mcrl2/pbes/enumerator.h"
      17             : #include "mcrl2/pbes/rewriters/simplify_rewriter.h"
      18             : #include <numeric>
      19             : 
      20             : namespace mcrl2 {
      21             : 
      22             : namespace pbes_system {
      23             : 
      24             : namespace detail {
      25             : 
      26             : // Simplifying PBES rewriter that eliminates quantifiers using enumeration.
      27             : /// \param MutableSubstitution This must be a MapSubstitution.
      28             : template <typename Derived, typename DataRewriter, typename MutableSubstitution>
      29        5768 : struct enumerate_quantifiers_builder: public simplify_data_rewriter_builder<Derived, DataRewriter, MutableSubstitution>
      30             : {
      31             :   typedef simplify_data_rewriter_builder<Derived, DataRewriter, MutableSubstitution> super;
      32             :   typedef enumerate_quantifiers_builder<Derived, DataRewriter, MutableSubstitution> self;
      33             :   typedef data::enumerator_list_element<pbes_expression> enumerator_element;
      34             :   using super::enter;
      35             :   using super::leave;
      36             :   using super::update;
      37             :   using super::apply;
      38             :   using super::sigma;
      39             : 
      40             :   const data::data_specification& m_dataspec;
      41             : 
      42             :   /// If true, quantifier variables of infinite sort are enumerated.
      43             :   bool m_enumerate_infinite_sorts;
      44             : 
      45             :   /// The enumerator
      46             :   data::enumerator_algorithm<self> E;
      47             : 
      48             :   /// \brief Constructor.
      49             :   /// \param r A data rewriter.
      50             :   /// \param sigma A mutable substitution.
      51             :   /// \param dataspec A data specification.
      52             :   /// \param id_generator A generator to generate fresh variable names.
      53             :   /// \param enumerate_infinite_sorts If true, quantifier variables of infinite sort are enumerated as well.
      54        5768 :   enumerate_quantifiers_builder(const DataRewriter& r,
      55             :                                 MutableSubstitution& sigma,
      56             :                                 const data::data_specification& dataspec,
      57             :                                 data::enumerator_identifier_generator& id_generator,
      58             :                                 bool enumerate_infinite_sorts = true)
      59        5768 :     : super(r, sigma), m_dataspec(dataspec), m_enumerate_infinite_sorts(enumerate_infinite_sorts), E(*this, m_dataspec, r, id_generator, (std::numeric_limits<std::size_t>::max)())
      60             :   {
      61        5768 :     id_generator.clear();
      62        5768 :   }
      63             : 
      64        4793 :   Derived& derived()
      65             :   {
      66        4793 :     return static_cast<Derived&>(*this);
      67             :   }
      68             : 
      69        2580 :   std::vector<data::data_expression> undo_substitution(const data::variable_list& variables)
      70             :   {
      71        2580 :     std::vector<data::data_expression> result;
      72        5165 :     for (const data::variable& v : variables)
      73             :     {
      74        2585 :       result.push_back(sigma(v));
      75        2585 :       sigma[v] = v;
      76             :     }
      77        2580 :     return result;
      78             :   }
      79             : 
      80        2580 :   void redo_substitution(const data::variable_list& v, const std::vector<data::data_expression>& undo)
      81             :   {
      82        2580 :     assert(v.size() == undo.size());
      83        2580 :     auto i = v.begin();
      84        2580 :     auto j = undo.begin();
      85        7750 :     while (i != v.end())
      86             :     {
      87        2585 :       sigma[*i++] = *j++;
      88             :     }
      89        2580 :   }
      90             : 
      91        2044 :   pbes_expression enumerate_forall(const data::variable_list& v, const pbes_expression& phi)
      92             :   {
      93        4088 :     auto undo = undo_substitution(v);
      94        2044 :     pbes_expression result = true_();
      95        2044 :     E.enumerate(enumerator_element(v, derived().apply(phi)),
      96             :                 sigma,
      97        1665 :                 [&](const enumerator_element& p)
      98             :                 {
      99        1665 :                   result = data::optimized_and(result, p.expression());
     100        1665 :                   return is_false(result);
     101             :                 },
     102             :                 is_true,
     103             :                 is_false
     104             :                );
     105             : 
     106        2044 :     redo_substitution(v, undo);
     107        4088 :     return result;
     108             :   }
     109             : 
     110         536 :   pbes_expression enumerate_exists(const data::variable_list& v, const pbes_expression& phi)
     111             :   {
     112        1072 :     auto undo = undo_substitution(v);
     113         536 :     pbes_expression result = false_();
     114         536 :     E.enumerate(enumerator_element(v, derived().apply(phi)),
     115             :                 sigma,
     116         332 :                 [&](const enumerator_element& p)
     117             :                 {
     118         332 :                   result = data::optimized_or(result, p.expression());
     119         332 :                   return is_true(result);
     120             :                 },
     121             :                 is_false,
     122             :                 is_true
     123             :     );
     124             : 
     125         536 :     redo_substitution(v, undo);
     126        1072 :     return result;
     127             :   }
     128             : 
     129        2046 :   pbes_expression apply(const forall& x)
     130             :   {
     131        2046 :     pbes_expression result;
     132        2046 :     if (m_enumerate_infinite_sorts)
     133             :     {
     134        4086 :       data::variable_list enumerable;
     135        4086 :       data::variable_list non_enumerable;
     136        2043 :       data::detail::split_enumerable_variables(x.variables(), m_dataspec, super::R, enumerable, non_enumerable);
     137        2043 :       result = data::optimized_forall_no_empty_domain(non_enumerable, enumerate_forall(enumerable, x.body()));
     138             :     }
     139             :     else
     140             :     {
     141           6 :       data::variable_list finite;
     142           6 :       data::variable_list infinite;
     143           3 :       data::detail::split_finite_variables(x.variables(), m_dataspec, finite, infinite);
     144           3 :       if (finite.empty())
     145             :       {
     146           2 :         result = data::optimized_forall(infinite, derived().apply(x.body()));
     147             :       }
     148             :       else
     149             :       {
     150           1 :         result = enumerate_forall(finite, x.body());
     151           1 :         result = data::optimized_forall_no_empty_domain(infinite, result);
     152             :       }
     153             :     }
     154        2046 :     return result;
     155             :   }
     156             : 
     157         536 :   pbes_expression apply(const exists& x)
     158             :   {
     159         536 :     pbes_expression result;
     160         536 :     if (m_enumerate_infinite_sorts)
     161             :     {
     162        1072 :       data::variable_list enumerable;
     163        1072 :       data::variable_list non_enumerable;
     164         536 :       data::detail::split_enumerable_variables(x.variables(), m_dataspec, super::R, enumerable, non_enumerable);
     165         536 :       result = data::optimized_exists_no_empty_domain(non_enumerable, enumerate_exists(enumerable, x.body()));
     166             :     }
     167             :     else
     168             :     {
     169           0 :       data::variable_list finite;
     170           0 :       data::variable_list infinite;
     171           0 :       data::detail::split_finite_variables(x.variables(), m_dataspec, finite, infinite);
     172           0 :       if (finite.empty())
     173             :       {
     174           0 :         result = data::optimized_exists(infinite, derived().apply(x.body()));
     175             :       }
     176             :       else
     177             :       {
     178           0 :         result = enumerate_exists(finite, x.body());
     179           0 :         result = data::optimized_exists_no_empty_domain(infinite, result);
     180             :       }
     181             :     }
     182         536 :     return result;
     183             :   }
     184             : 
     185             :   // N.B. This function has been added to make this class operate well with the enumerator.
     186        2211 :   pbes_expression operator()(const pbes_expression& x, MutableSubstitution&)
     187             :   {
     188        2211 :     return derived().apply(x);
     189             :   }
     190             : };
     191             : 
     192             : template <template <class, class, class> class Builder, class DataRewriter, class MutableSubstitution>
     193        5768 : struct apply_enumerate_builder: public Builder<apply_enumerate_builder<Builder, DataRewriter, MutableSubstitution>, DataRewriter, MutableSubstitution>
     194             : {
     195             :   typedef Builder<apply_enumerate_builder<Builder, DataRewriter, MutableSubstitution>, DataRewriter, MutableSubstitution> super;
     196             :   using super::enter;
     197             :   using super::leave;
     198             : 
     199        5768 :   apply_enumerate_builder(const DataRewriter& R, MutableSubstitution& sigma, const data::data_specification& dataspec, data::enumerator_identifier_generator& id_generator, bool enumerate_infinite_sorts)
     200        5768 :     : super(R, sigma, dataspec, id_generator, enumerate_infinite_sorts)
     201        5768 :   {}
     202             : };
     203             : 
     204             : template <template <class, class, class> class Builder, class DataRewriter, class MutableSubstitution>
     205             : apply_enumerate_builder<Builder, DataRewriter, MutableSubstitution>
     206             : make_apply_enumerate_builder(const DataRewriter& R, MutableSubstitution& sigma, const data::data_specification& dataspec, data::enumerator_identifier_generator& id_generator, bool enumerate_infinite_sorts)
     207             : {
     208             :   return apply_enumerate_builder<Builder, DataRewriter, MutableSubstitution>(R, sigma, dataspec, id_generator, enumerate_infinite_sorts);
     209             : }
     210             : 
     211             : } // namespace detail
     212             : 
     213             : /// \brief An attempt for improving the efficiency.
     214         187 : struct enumerate_quantifiers_rewriter
     215             : {
     216             :   /// \brief A data rewriter
     217             :   data::rewriter m_rewriter;
     218             : 
     219             :   /// \brief A data specification
     220             :   data::data_specification m_dataspec;
     221             : 
     222             :   /// \brief If true, quantifier variables of infinite sort are enumerated.
     223             :   bool m_enumerate_infinite_sorts;
     224             : 
     225             :   mutable data::enumerator_identifier_generator m_id_generator;
     226             : 
     227             :   typedef pbes_expression term_type;
     228             :   typedef data::variable variable_type;
     229             : 
     230         187 :   enumerate_quantifiers_rewriter(const data::rewriter& R, const data::data_specification& dataspec, bool enumerate_infinite_sorts = true)
     231         187 :     : m_rewriter(R), m_dataspec(dataspec), m_enumerate_infinite_sorts(enumerate_infinite_sorts)
     232         187 :   {}
     233             : 
     234         110 :   pbes_expression operator()(const pbes_expression& x) const
     235             :   {
     236         220 :     data::rewriter::substitution_type sigma;
     237         110 :     m_id_generator.clear();
     238         220 :     return detail::apply_enumerate_builder<detail::enumerate_quantifiers_builder, data::rewriter, data::rewriter::substitution_type>(m_rewriter, sigma, m_dataspec, m_id_generator, m_enumerate_infinite_sorts).apply(x);
     239             :   }
     240             : 
     241             :   template <typename MutableSubstitution>
     242        5658 :   pbes_expression operator()(const pbes_expression& x, MutableSubstitution& sigma) const
     243             :   {
     244        5658 :     m_id_generator.clear();
     245        5658 :     return detail::apply_enumerate_builder<detail::enumerate_quantifiers_builder, data::rewriter, MutableSubstitution>(m_rewriter, sigma, m_dataspec, m_id_generator, m_enumerate_infinite_sorts).apply(x);
     246             :   }
     247             : };
     248             : 
     249             : } // namespace pbes_system
     250             : 
     251             : } // namespace mcrl2
     252             : 
     253             : #endif // MCRL2_PBES_REWRITERS_ENUMERATE_QUANTIFIERS_REWRITER_H
     254             : 

Generated by: LCOV version 1.13