mCRL2
Loading...
Searching...
No Matches
Public Member Functions | Private Member Functions | Private Attributes | List of all members
mcrl2::data::detail::Induction Class Reference

The class Induction generates statements corresponding to. More...

#include <induction.h>

Public Member Functions

void initialize (const data_expression &a_formula)
 
bool can_apply_induction () const
 
data_expression apply_induction ()
 \requires can_apply_induction()
 

Private Member Functions

variable_vector recurse_expression_for_lists (const data_expression &a_expression) const
 
sort_expression get_sort_of_list_elements (const variable &a_list_variable) const
 
variable get_fresh_dummy (const sort_expression &a_sort)
 
data_expression apply_induction_one (const core::identifier_string &fresh_name) const
 
data_expression create_hypotheses (const data_expression &a_hypothesis, variable_list a_list_of_variables, variable_list a_list_of_dummies) const
 
data_expression_list create_clauses (const data_expression &a_formula, const data_expression &a_hypothesis, const std::size_t a_variable_number, const std::size_t a_number_of_variables, const variable_list &a_list_of_variables, const variable_list &a_list_of_dummies)
 

Private Attributes

set_identifier_generator fresh_identifier_generator
 
std::size_t f_count = 0UL
 The number of variables used during the last application of induction.
 
data_expression f_formula
 An expression of sort Bool in mCRL2 format.
 
variable_vector f_list_variables
 

Detailed Description

The class Induction generates statements corresponding to.

Definition at line 24 of file induction.h.

Member Function Documentation

◆ apply_induction()

data_expression mcrl2::data::detail::Induction::apply_induction ( )
inline

\requires can_apply_induction()

Definition at line 173 of file induction.h.

◆ apply_induction_one()

data_expression mcrl2::data::detail::Induction::apply_induction_one ( const core::identifier_string &  fresh_name) const
inlineprivate

Definition at line 67 of file induction.h.

◆ can_apply_induction()

bool mcrl2::data::detail::Induction::can_apply_induction ( ) const
inline

Definition at line 167 of file induction.h.

◆ create_clauses()

data_expression_list mcrl2::data::detail::Induction::create_clauses ( const data_expression &  a_formula,
const data_expression &  a_hypothesis,
const std::size_t  a_variable_number,
const std::size_t  a_number_of_variables,
const variable_list &  a_list_of_variables,
const variable_list &  a_list_of_dummies 
)
inlineprivate

Definition at line 117 of file induction.h.

◆ create_hypotheses()

data_expression mcrl2::data::detail::Induction::create_hypotheses ( const data_expression &  a_hypothesis,
variable_list  a_list_of_variables,
variable_list  a_list_of_dummies 
) const
inlineprivate

Definition at line 87 of file induction.h.

◆ get_fresh_dummy()

variable mcrl2::data::detail::Induction::get_fresh_dummy ( const sort_expression &  a_sort)
inlineprivate

Definition at line 60 of file induction.h.

◆ get_sort_of_list_elements()

sort_expression mcrl2::data::detail::Induction::get_sort_of_list_elements ( const variable &  a_list_variable) const
inlineprivate

Definition at line 53 of file induction.h.

◆ initialize()

void mcrl2::data::detail::Induction::initialize ( const data_expression &  a_formula)
inline

Definition at line 160 of file induction.h.

◆ recurse_expression_for_lists()

variable_vector mcrl2::data::detail::Induction::recurse_expression_for_lists ( const data_expression &  a_expression) const
inlineprivate

Definition at line 39 of file induction.h.

Member Data Documentation

◆ f_count

std::size_t mcrl2::data::detail::Induction::f_count = 0UL
private

The number of variables used during the last application of induction.

Definition at line 30 of file induction.h.

◆ f_formula

data_expression mcrl2::data::detail::Induction::f_formula
private

An expression of sort Bool in mCRL2 format.

Definition at line 33 of file induction.h.

◆ f_list_variables

variable_vector mcrl2::data::detail::Induction::f_list_variables
private

Definition at line 36 of file induction.h.

◆ fresh_identifier_generator

set_identifier_generator mcrl2::data::detail::Induction::fresh_identifier_generator
private

Definition at line 27 of file induction.h.

The documentation for this class was generated from the following file: