mcrl2::pbes_system::bqnf_rewriter
===============================================================================


Include file:

.. code-block:: c++

   #include "mcrl2/pbes/rewriters/bqnf_rewriter.h

.. cpp:class:: mcrl2::pbes_system::bqnf_rewriter

  A rewriter that rewrites universal quantifiers over conjuncts in BQNF expressions to conjuncts over universal quantifiers. 

  

Public types
-------------------------------------------------------------------------------

.. cpp:type:: mcrl2::pbes_system::bqnf_rewriter::equation_type

  typedef for :cpp:type:`pbes_equation`
  
  The equation type. 

  

.. cpp:type:: mcrl2::pbes_system::bqnf_rewriter::term_type

  typedef for :cpp:type:`pbes_expression`
  
  The term type. 

  

Private attributes
-------------------------------------------------------------------------------

.. cpp:member:: std::unique_ptr< pbes_system::detail::bqnf_visitor > mcrl2::pbes_system::bqnf_rewriter::bqnf_checker
  
  

  

.. cpp:member:: std::unique_ptr< pbes_system::detail::bqnf_quantifier_rewriter > mcrl2::pbes_system::bqnf_rewriter::bqnf_quantifier_rewriter
  
  

  

Public member functions
-------------------------------------------------------------------------------

.. cpp:function:: bqnf_rewriter()
  
  Constructor. 

  

.. cpp:function:: term_type operator()(const term_type &t) const
  
  Rewrites a PBES expression in BQNF such that universal quantifier over conjuncts are replaced by conjuncts over universal quantifiers. 

  
  
  **Parameters:**

  * **t** A term. 


      
  **Returns:** The expression resulting from the transformation. 

.. cpp:function:: term_type operator()(const term_type &x, SubstitutionFunction sigma) const
  
  Rewrites a pbes expression. 

  
  
  **Parameters:**

  * **x** A term 

  * **sigma** A substitution function 


      
  **Returns:** The rewrite result.