mcrl2::data::enumerator_algorithm
===============================================================================


Include file:

.. code-block:: c++

   #include "mcrl2/data/enumerator.h

.. cpp:class:: mcrl2::data::enumerator_algorithm

  An enumerator algorithm that generates solutions of a condition. 

  

Protected attributes
-------------------------------------------------------------------------------

.. cpp:member:: const data::data_specification & mcrl2::data::enumerator_algorithm::dataspec
  
  A data specification. 

  

.. cpp:member:: enumerator_identifier_generator & mcrl2::data::enumerator_algorithm::id_generator
  
  

  

.. cpp:member:: bool mcrl2::data::enumerator_algorithm::m_accept_solutions_with_variables
  
  If true, solutions with a non-empty list of variables may be reported. 

  

.. cpp:member:: std::size_t mcrl2::data::enumerator_algorithm::m_max_count
  
  max_count The enumeration is aborted after max_count iterations 

  

.. cpp:member:: const Rewriter & mcrl2::data::enumerator_algorithm::R
  
  

  

.. cpp:member:: const DataRewriter & mcrl2::data::enumerator_algorithm::r
  
  

  

Protected member functions
-------------------------------------------------------------------------------

.. cpp:function:: std::string print(const data::variable &x) const
  
  

  

.. cpp:function:: Expression rewrite(const Expression &phi, MutableSubstitution &sigma) const
  
  

  

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

.. cpp:function:: std::size_t enumerate(const EnumeratorListElement &p, MutableSubstitution &sigma, ReportSolution report_solution, Reject reject=Reject(), Accept accept=Accept()) const
  
  Enumerates the element p. Solutions are reported using the callback function report_solution. The enumeration is interrupted when report_solution returns true for the reported solution. 

  
  
  **Parameters:**

  * **p** An enumerator element, i.e. an expression with a list of variables. 

  * **sigma** A substitution. 

  * **reject** Elements p for which reject(p) is true are discarded. 

  * **accept** Elements p for which accept(p) is true are reported as a solution, even if the list of variables of the enumerator element is non-empty. 

  * **report_solution** A callback function that is called whenever a solution is found. It takes an enumerator element as argument. If report_solution returns true, the enumeration is interrupted. N.B. If the enumeration is resumed after an interruption, the element p that was interrupted will be enumerated again. 


      
  **Returns:** The number of elements that have been processed 

.. cpp:function:: std::size_t enumerate_all(enumerator_queue< EnumeratorListElement > &P, MutableSubstitution &sigma, ReportSolution report_solution, Reject reject=Reject(), Accept accept=Accept()) const
  
  Enumerates until P is empty. Solutions are reported using the callback function report_solution. The enumeration is interrupted when report_solution returns true for the reported solution. 

  
  
  **Parameters:**

  * **P** The todo list of the algorithm. 

  * **sigma** A substitution. 

  * **reject** Elements p for which reject(p) is true are discarded. 

  * **accept** Elements p for which accept(p) is true are reported as a solution, even if the list of variables of the enumerator element is non-empty. 

  * **report_solution** A callback function that is called whenever a solution is found. It takes an enumerator element as argument. If report_solution returns true, the enumeration is interrupted. N.B. If the enumeration is resumed after an interruption, the element p that was interrupted will be enumerated again. 


      
  **Returns:** The number of elements that have been processed 

.. cpp:function:: bool enumerate_front(enumerator_queue< EnumeratorListElement > &P, MutableSubstitution &sigma, ReportSolution report_solution, Reject reject=Reject(), Accept accept=Accept()) const
  
  Enumerates the front element of the todo list P. The enumeration is interrupted when report_solution returns true for the reported solution. 

  
  
  **Parameters:**

  * **P** The todo list of the algorithm. 

  * **sigma** A mutable substitution that is applied by the rewriter. 

  * **reject** Elements p for which reject(p) is true are discarded. 

  * **accept** Elements p for which accept(p) is true are reported as a solution, even if the list of variables of the enumerator element is non-empty. 

  * **report_solution** A callback function that is called whenever a solution is found. It takes an enumerator element as argument. If report_solution returns true, the enumeration is interrupted. N.B. If the enumeration is resumed after an interruption, the element p that was interrupted will be enumerated again. 


      
  **Pre:** !P.empty()
      
  **Returns:** If the return value is true, enumeration will be interrupted 

.. cpp:function:: enumerator_algorithm(const Rewriter &R_, const data::data_specification &dataspec_, const DataRewriter &datar_, enumerator_identifier_generator &id_generator_, bool accept_solutions_with_variables, std::size_t max_count=(std::numeric_limits< std::size_t >::max)())
  
  

  

.. cpp:function:: enumerator_algorithm(const enumerator_algorithm< Rewriter, DataRewriter > &)=delete
  
  

  

.. cpp:function:: std::size_t max_count() const
  
  

  

.. cpp:function:: ~enumerator_algorithm()