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

Generated by: LCOV version 1.12