LCOV - code coverage report
Current view: top level - pbes/include/mcrl2/pbes/rewriters - bqnf_rewriter.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 11 14 78.6 %
Date: 2019-08-22 00:56:55 Functions: 3 3 100.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/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             : #include "mcrl2/pbes/detail/bqnf_visitor.h"
      17             : 
      18             : #include <memory>
      19             : 
      20             : namespace mcrl2 {
      21             : 
      22             : namespace pbes_system {
      23             : 
      24             : /// \brief A rewriter that rewrites universal quantifiers over conjuncts
      25             : /// in BQNF expressions to conjuncts over universal quantifiers.
      26           1 : class bqnf_rewriter
      27             : {
      28             :   public:
      29             :     /// \brief The equation type
      30             :     typedef pbes_equation equation_type;
      31             :     /// \brief The term type
      32             :     typedef pbes_expression term_type;
      33             : 
      34             :     /// \brief Constructor
      35           1 :     bqnf_rewriter() {
      36           1 :       bqnf_checker = std::unique_ptr<pbes_system::detail::bqnf_visitor>(new pbes_system::detail::bqnf_visitor());
      37           1 :       bqnf_quantifier_rewriter = std::unique_ptr<pbes_system::detail::bqnf_quantifier_rewriter>(new pbes_system::detail::bqnf_quantifier_rewriter());
      38           1 :     }
      39             : 
      40             :     /// \brief Rewrites a PBES expression in BQNF such that universal quantifier over conjuncts
      41             :     /// are replaced by conjuncts over universal quantifiers.
      42             :     /// \param t A term.
      43             :     /// \return The expression resulting from the transformation.
      44           3 :     term_type operator()(const term_type& t) const
      45             :     {
      46           3 :       bool is_bqnf = false;
      47             :       try {
      48           3 :         is_bqnf = bqnf_checker->visit_bqnf_expression(t);
      49           0 :       } catch(std::runtime_error& e) {
      50           0 :         std::clog << e.what() << std::endl;
      51             :       }
      52           3 :       if (!is_bqnf)
      53             :       {
      54           0 :         throw(std::runtime_error("Input expression not in BQNF."));
      55             :       }
      56           3 :       term_type result = bqnf_quantifier_rewriter->rewrite_bqnf_expression(t);
      57           3 :       return result;
      58             :     }
      59             : 
      60             :     /// \brief Rewrites a pbes expression.
      61             :     /// \param x A term
      62             :     /// \param sigma A substitution function
      63             :     /// \return The rewrite result.
      64             :     template <typename SubstitutionFunction>
      65             :     term_type operator()(const term_type& x, SubstitutionFunction sigma) const
      66             :     {
      67             :       return sigma(this->operator()(x));
      68             :     }
      69             : 
      70             : private:
      71             :     std::unique_ptr<pbes_system::detail::bqnf_visitor> bqnf_checker;
      72             :     std::unique_ptr<pbes_system::detail::bqnf_quantifier_rewriter> bqnf_quantifier_rewriter;
      73             : };
      74             : 
      75             : } // namespace pbes_system
      76             : 
      77             : } // namespace mcrl2
      78             : 
      79             : #endif // MCRL2_PBES_REWRITERS_BQNF_REWRITER_H

Generated by: LCOV version 1.12