enumerate_quantifiers_rewriter.h

Go to the documentation of this file.

// Author(s): Wieger Wesselink
// Copyright: see the accompanying file COPYING or copy at
// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
//
/// \file mcrl2/pbes/rewriters/enumerate_quantifiers_rewriter.h
/// \brief add your file description here.
 
#ifndef MCRL2_PBES_REWRITERS_ENUMERATE_QUANTIFIERS_REWRITER_H
#define MCRL2_PBES_REWRITERS_ENUMERATE_QUANTIFIERS_REWRITER_H
 
#include <numeric>
#include "mcrl2/atermpp/standard_containers/vector.h"
#include "mcrl2/data/detail/split_finite_variables.h"
#include "mcrl2/data/rewriters/enumerate_quantifiers_rewriter.h"
#include "mcrl2/pbes/enumerator.h"
#include "mcrl2/pbes/pbes.h"
#include "mcrl2/pbes/rewriters/quantifier_expansion_mode.h"
#include "mcrl2/pbes/rewriters/simplify_rewriter.h"
#include "mcrl2/pbes/substitutions.h"
 
namespace mcrl2::pbes_system
{
 
namespace detail {
 
// Simplifying PBES rewriter that eliminates quantifiers using enumeration.
/// \param MutableSubstitution This must be a MapSubstitution.
template <typename Derived, typename DataRewriter, typename MutableSubstitution, typename PbesSubstitution>
struct enumerate_quantifiers_builder: public simplify_data_rewriter_builder<Derived, DataRewriter, MutableSubstitution, PbesSubstitution>
{
  using super = simplify_data_rewriter_builder<Derived, DataRewriter, MutableSubstitution, PbesSubstitution>;
  using self = enumerate_quantifiers_builder<Derived, DataRewriter, MutableSubstitution, PbesSubstitution>;
  using enumerator_element = data::enumerator_list_element<pbes_expression>;
  using super::enter;
  using super::leave;
  using super::update;
  using super::apply;
  using super::sigma;
  using super::R;
 
/*   MutableSubstitution& m_sigma;
  const DataRewriter& m_R;
  const PbesSubstitution& m_sigma_pbes; */
  const data::data_specification& m_dataspec;
 
  /// If false, only quantifier variables over finite sorts are enumerated.
  enumerate_quantifiers_mode m_enum_mode;
 
  /// identifier generator
  data::enumerator_identifier_generator& m_id_generator;
 
  /// The enumerator
  data::enumerator_algorithm<self> E;
 
  /// \brief Constructor.
  /// \param R A data rewriter.
  /// \param sigma A mutable substitution.
  /// \param sigma_pbes A substitution for pbes variables.
  /// \param dataspec A data specification.
  /// \param id_generator A generator to generate fresh variable names.
  /// \param enumerate_infinite_sorts If true, quantifier variables of infinite sort are enumerated as well.
  enumerate_quantifiers_builder(const DataRewriter& R,
    MutableSubstitution& sigma,
    const PbesSubstitution& sigma_pbes,
    const data::data_specification& dataspec,
    data::enumerator_identifier_generator& id_generator,
    enumerate_quantifiers_mode enum_mode = enumerate_quantifiers_mode::expand_infinite_sorts_and_use_data_rewriter )
    : super(R, sigma, sigma_pbes),
      // m_R(R),
      // m_sigma(sigma),
      // m_sigma_pbes(sigma_pbes),
      m_dataspec(dataspec),
      m_enum_mode(enum_mode),
      m_id_generator(id_generator),
      E(*this, m_dataspec, R, id_generator, (std::numeric_limits<std::size_t>::max)())
 
  { }
 
  Derived& derived()
  {
    return static_cast<Derived&>(*this);
  }
 
  atermpp::vector<data::data_expression> undo_substitution(const data::variable_list& variables)
  {
    atermpp::vector<data::data_expression> result;
    for (const data::variable& v : variables)
    {
      result.push_back(sigma(v));
      sigma[v] = v;
    }
    return result;
  }
 
  void redo_substitution(const data::variable_list& v, const atermpp::vector<data::data_expression>& undo)
  {
    assert(v.size() == undo.size());
    auto i = v.begin();
    auto j = undo.begin();
    while (i != v.end())
    {
      sigma[*i++] = *j++;
    }
  }
 
  // We assume that phi is already rewritten.
  void enumerate_forall(pbes_expression& result, const data::variable_list& v, const pbes_expression& phi)
  {
    assert(!v.empty());
    assert(&result!=&phi);
    atermpp::vector<data::data_expression> undo = undo_substitution(v);
    result = true_();
    E.enumerate(enumerator_element(v, phi),
                sigma,
                [&](const enumerator_element& p)
                {
                  pbes_system::make_optimized_and(result, result, p.expression());
                  return is_false(result);
                },
                is_true,
                is_false
               );
 
    redo_substitution(v, undo);
  }
 
  void enumerate_exists(pbes_expression& result, const data::variable_list& v, const pbes_expression& phi)
  {
    assert(!v.empty());
    assert(&result!=&phi);
    atermpp::vector<data::data_expression> undo = undo_substitution(v);
    result = false_();
    E.enumerate(enumerator_element(v, phi),
                sigma,
                [&](const enumerator_element& p)
                {
                  pbes_system::make_optimized_or(result, result, p.expression());
                  return is_false(result);
                },
                is_false,
                is_true
    );
 
    redo_substitution(v, undo);
  }
 
  template <class T>
  void apply(T& result, const forall& x)
  {
    const bool remove_unused_variables=true;
    atermpp::vector<data::data_expression> undo = undo_substitution(x.variables());
    derived().apply(result, x.body());
    std::set<data::variable> free_variables = find_free_variables(result);
    data::variable_list enumerable;
    data::variable_list non_enumerable;
    data::variable_list unused;
 
    if (m_enum_mode==enumerate_quantifiers_mode::expand_finite_sorts)
    {
      data::detail::split_finite_variables(x.variables(), m_dataspec,
                                           enumerable, non_enumerable, unused,
                                           [&free_variables](const data::variable& v){ return free_variables.count(v)>0; });
    }
    else
    {
      data::detail::split_enumerable_variables(x.variables(), m_dataspec, R,
                                               enumerable, non_enumerable, unused,
                                               [&free_variables](const data::variable& v){ return free_variables.count(v)>0; });
    }
    if (enumerable.empty())
    {
      pbes_system::make_optimized_forall(result, non_enumerable, result, remove_unused_variables);
    }
    else
    {
      pbes_expression phi_;
      enumerate_forall(phi_, enumerable, result);
      if constexpr (!std::is_same_v<PbesSubstitution, no_substitution>)
      {
        // we need to rewrite the new body again to deal properly with PBES substitutions
        // TODO: update enumerate_forall such that it uses the rewriter in derived() during enumeration
        derived().apply(result, phi_);
      }
      else
      {
        result = phi_;
      }
      pbes_system::make_optimized_forall(result, non_enumerable, result, remove_unused_variables);
    }
    redo_substitution(x.variables(), undo);
  }
 
  template <class T>
  void apply(T& result, const exists& x)
  {
    const bool remove_unused_variables=true;
    atermpp::vector<data::data_expression> undo = undo_substitution(x.variables());
    derived().apply(result, x.body());
    std::set<data::variable> free_variables = find_free_variables(result);
    data::variable_list enumerable;
    data::variable_list non_enumerable;
    data::variable_list unused;
 
    if (m_enum_mode==enumerate_quantifiers_mode::expand_finite_sorts)
    {
      data::detail::split_finite_variables(x.variables(), m_dataspec,
                                           enumerable, non_enumerable, unused,
                                           [&free_variables](const data::variable& v){ return free_variables.count(v)>0; });
    }
    else
    {
      data::detail::split_enumerable_variables(x.variables(), m_dataspec, R,
                                               enumerable, non_enumerable, unused,
                                               [&free_variables](const data::variable& v){ return free_variables.count(v)>0; });
    }
    if (enumerable.empty())
    {
      pbes_system::make_optimized_exists(result, non_enumerable, result, remove_unused_variables);
    }
    else
    {
      pbes_expression phi_;
      enumerate_exists(phi_, enumerable, result);
      if constexpr (!std::is_same_v<PbesSubstitution, no_substitution>)
      {
        // we need to rewrite the new body again to deal properly with PBES substitutions
        // TODO: update enumerate_exists such that it uses the rewriter in derived() during enumeration
        derived().apply(result, phi_);
      }
      else
      {
        result = phi_;
      }
      pbes_system::make_optimized_exists(result, non_enumerable, phi_, remove_unused_variables);
    }
    redo_substitution(x.variables(), undo);
  }
 
  template <atermpp::IsATerm T>
  void apply(T& result, const data::data_expression& x)
  {
    if (m_enum_mode==enumerate_quantifiers_mode::expand_infinite_sorts_and_use_data_rewriter)
    {
      R(atermpp::assign_cast<data::data_expression>(result),x,sigma);
    }
    else
    {
      data::data_expression temporary_result;
      data::enumerate_quantifiers_rewriter(R,m_dataspec,m_id_generator,m_enum_mode==enumerate_quantifiers_mode::expand_infinite_sorts)(temporary_result, x, sigma);
      R(atermpp::assign_cast<data::data_expression>(result),temporary_result,sigma);
    }
  }
 
 
  // N.B. This function has been added to make this class operate well with the enumerator.
  pbes_expression operator()(const pbes_expression& x, MutableSubstitution&)
  {
    pbes_expression result;
    derived().apply(result, x);
    return result;
  }
 
  // N.B. This function has been added to make this class operate well with the enumerator.
  //      that employs the "make_rewrite" variant with an explicit result.
  void operator()(pbes_expression& result, const pbes_expression& x, MutableSubstitution&)
  {
    derived().apply(result, x);
  }
};
 
template <template <class, class, class, class> class Builder, class DataRewriter, class MutableSubstitution, class PbesSubstitution = no_substitution>
struct apply_enumerate_builder: public Builder<apply_enumerate_builder<Builder, DataRewriter, MutableSubstitution, PbesSubstitution>, DataRewriter, MutableSubstitution, PbesSubstitution>
{
  using super = Builder<apply_enumerate_builder<Builder, DataRewriter, MutableSubstitution, PbesSubstitution>,
    DataRewriter,
    MutableSubstitution,
    PbesSubstitution>;
  using super::enter;
  using super::leave;
 
  apply_enumerate_builder(const DataRewriter& R,
    MutableSubstitution& sigma,
    const PbesSubstitution& sigma_pbes,
    const data::data_specification& dataspec,
    data::enumerator_identifier_generator& id_generator,
    const enumerate_quantifiers_mode enum_mode)
    : super(R, sigma, sigma_pbes, dataspec, id_generator, enum_mode)
  {}
};
 
template<template<class, class, class, class> class Builder,
  class DataRewriter,
  class MutableSubstitution,
  class PbesSubstitution>
apply_enumerate_builder<Builder, DataRewriter, MutableSubstitution, PbesSubstitution> make_apply_enumerate_builder(
  const DataRewriter& R,
  MutableSubstitution& sigma,
  const PbesSubstitution& sigma_pbes,
  const data::data_specification& dataspec,
  data::enumerator_identifier_generator& id_generator,
  bool enumerate_infinite_sorts)
{
  return apply_enumerate_builder<Builder, DataRewriter, MutableSubstitution, PbesSubstitution>(R,
    sigma,
    sigma_pbes,
    dataspec,
    id_generator,
    enumerate_infinite_sorts);
}
 
template<template<class, class, class, class> class Builder,
  class DataRewriter,
  class MutableSubstitution>
apply_enumerate_builder<Builder, DataRewriter, MutableSubstitution, no_substitution> make_apply_enumerate_builder(
  const DataRewriter& R,
  MutableSubstitution& sigma,
  const data::data_specification& dataspec,
  data::enumerator_identifier_generator& id_generator,
  bool enumerate_infinite_sorts)
{
  return apply_enumerate_builder<Builder, DataRewriter, MutableSubstitution, no_substitution>(R,
    sigma,
    no_substitution(),
    dataspec,
    id_generator,
    enumerate_infinite_sorts);
}
 
} // namespace detail
 
/// \brief An attempt for improving the efficiency.
struct enumerate_quantifiers_rewriter
{
  protected:
    /// \brief A data rewriter
    data::rewriter m_rewriter;
 
    /// \brief A data specification
    data::data_specification m_dataspec;
 
    /// \brief If true, quantifier variables of infinite sort are enumerated.
    enumerate_quantifiers_mode m_enum_mode;
 
    mutable data::enumerator_identifier_generator m_id_generator;
 
  public:
    using term_type = pbes_expression;
    using variable_type = data::variable;
 
    enumerate_quantifiers_rewriter(const data::rewriter& R,
                                   const data::data_specification& dataspec,
                                   const enumerate_quantifiers_mode enum_mode = enumerate_quantifiers_mode::expand_infinite_sorts_and_use_data_rewriter)
      : m_rewriter(R),
        m_dataspec(dataspec),
        m_enum_mode(enum_mode)
    {}
 
    pbes_expression operator()(const pbes_expression& x) const
    {
      data::rewriter::substitution_type sigma;
      pbes_expression result;
      detail::apply_enumerate_builder<detail::enumerate_quantifiers_builder, data::rewriter, data::rewriter::substitution_type>(m_rewriter, sigma, no_substitution(), m_dataspec, m_id_generator, m_enum_mode).apply(result, x);
      return result;
    }
 
    template <typename MutableSubstitution>
    pbes_expression operator()(const pbes_expression& x, MutableSubstitution& sigma) const
    {
      pbes_expression result;
      detail::apply_enumerate_builder<detail::enumerate_quantifiers_builder, data::rewriter, MutableSubstitution>(m_rewriter, sigma, no_substitution(), m_dataspec, m_id_generator, m_enum_mode).apply(result, x);
      return result;
    }
 
    template <typename MutableSubstitution>
    void operator()(pbes_expression& result, const pbes_expression& x, MutableSubstitution& sigma) const
    {
      detail::apply_enumerate_builder<detail::enumerate_quantifiers_builder, data::rewriter, MutableSubstitution>(m_rewriter, sigma, no_substitution(), m_dataspec, m_id_generator, m_enum_mode).apply(result, x);
    }
 
    template<typename MutableSubstitution, typename PbesSubstitution>
    pbes_expression operator()(const pbes_expression& x, MutableSubstitution& sigma, const PbesSubstitution& sigma_pbes) const
    {
      pbes_expression result;
      detail::apply_enumerate_builder<detail::enumerate_quantifiers_builder,
        data::rewriter,
        MutableSubstitution,
        PbesSubstitution>(m_rewriter,
        sigma,
        sigma_pbes,
        m_dataspec,
        m_id_generator,
        m_enum_mode)
        .apply(result, x);
      return result;
    }
 
    template<typename MutableSubstitution, typename PbesSubstitution>
    void operator()(pbes_expression& result, const pbes_expression& x, MutableSubstitution& sigma, const PbesSubstitution& sigma_pbes) const
    {
      detail::apply_enumerate_builder<detail::enumerate_quantifiers_builder, data::rewriter, MutableSubstitution, PbesSubstitution>(
        m_rewriter,
        sigma,
        sigma_pbes,
        m_dataspec,
        m_id_generator,
        m_enum_mode)
        .apply(result, x);
    }
 
    void clear_identifier_generator()
    {
      m_id_generator.clear();
    }
 
    /// \brief Create a clone of the rewriter in which the underlying rewriter is copied, and not passed as a shared pointer.
    /// \details This is useful when the rewriter is used in different parallel processes. One rewriter can only be used sequentially.
    /// \return A rewriter, with a copy of the underlying jitty, jittyc or jittyp rewriting engine.
    enumerate_quantifiers_rewriter clone()
    {
      return enumerate_quantifiers_rewriter(m_rewriter.clone(), m_dataspec, m_enum_mode);
    }
 
    /// \brief Initialises this rewriter with thread dependent information.
    /// \details This function sets a pointer to the m_busy_flag and m_forbidden_flag of this.
    ///          process, such that rewriter can access these faster than via the general thread.
    ///          local mechanism. It is expected that this is not needed when compilers become.
    ///          faster, and should be removed in due time.
    void thread_initialise()
    {
      m_rewriter.thread_initialise();
    }
};
 
} // namespace mcrl2::pbes_system
 
#endif // MCRL2_PBES_REWRITERS_ENUMERATE_QUANTIFIERS_REWRITER_H