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/bqnf_rewriter.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_REWRITERS_BQNF_REWRITER_H
      13             : #define MCRL2_PBES_REWRITERS_BQNF_REWRITER_H
      14             : 
      15             : #include "mcrl2/pbes/detail/bqnf_quantifier_rewriter.h"
      16             : 
      17             : namespace mcrl2 {
      18             : 
      19             : namespace pbes_system {
      20             : 
      21             : /// \brief A rewriter that rewrites universal quantifiers over conjuncts
      22             : /// in BQNF expressions to conjuncts over universal quantifiers.
      23             : class bqnf_rewriter
      24             : {
      25             :   public:
      26             :     /// \brief The equation type
      27             :     typedef pbes_equation equation_type;
      28             :     /// \brief The term type
      29             :     typedef pbes_expression term_type;
      30             : 
      31             :     /// \brief Constructor
      32           1 :     bqnf_rewriter() {
      33           1 :       bqnf_checker = std::unique_ptr<pbes_system::detail::bqnf_visitor>(new pbes_system::detail::bqnf_visitor());
      34           1 :       bqnf_quantifier_rewriter = std::unique_ptr<pbes_system::detail::bqnf_quantifier_rewriter>(new pbes_system::detail::bqnf_quantifier_rewriter());
      35           1 :     }
      36             : 
      37             :     /// \brief Rewrites a PBES expression in BQNF such that universal quantifier over conjuncts
      38             :     /// are replaced by conjuncts over universal quantifiers.
      39             :     /// \param t A term.
      40             :     /// \return The expression resulting from the transformation.
      41           4 :     term_type operator()(const term_type& t) const
      42             :     {
      43           4 :       bool is_bqnf = false;
      44             :       try {
      45           4 :         is_bqnf = bqnf_checker->visit_bqnf_expression(t);
      46           0 :       } catch(std::runtime_error& e) {
      47           0 :         std::clog << e.what() << std::endl;
      48           0 :       }
      49           4 :       if (!is_bqnf)
      50             :       {
      51           0 :         throw(std::runtime_error("Input expression not in BQNF."));
      52             :       }
      53           4 :       term_type result = bqnf_quantifier_rewriter->rewrite_bqnf_expression(t);
      54           4 :       return result;
      55             :     }
      56             : 
      57             :     /// \brief Rewrites a pbes expression.
      58             :     /// \param x A term
      59             :     /// \param sigma A substitution function
      60             :     /// \return The rewrite result.
      61             :     template <typename SubstitutionFunction>
      62             :     term_type operator()(const term_type& x, SubstitutionFunction sigma) const
      63             :     {
      64             :       return sigma(this->operator()(x));
      65             :     }
      66             : 
      67             : private:
      68             :     std::unique_ptr<pbes_system::detail::bqnf_visitor> bqnf_checker;
      69             :     std::unique_ptr<pbes_system::detail::bqnf_quantifier_rewriter> bqnf_quantifier_rewriter;
      70             : };
      71             : 
      72             : } // namespace pbes_system
      73             : 
      74             : } // namespace mcrl2
      75             : 
      76             : #endif // MCRL2_PBES_REWRITERS_BQNF_REWRITER_H