mCRL2
Loading...
Searching...
No Matches
mcrl2::pbes_system::absinthe_algorithm::absinthe_data_expression_builder Struct Reference

#include <absinthe.h>

Inheritance diagram for mcrl2::pbes_system::absinthe_algorithm::absinthe_data_expression_builder:
mcrl2::pbes_system::pbes_expression_builder< absinthe_data_expression_builder > mcrl2::pbes_system::add_pbes_expressions< Builder, Derived >

Public Types

typedef pbes_expression_builder< absinthe_data_expression_buildersuper
 
- Public Types inherited from mcrl2::pbes_system::add_pbes_expressions< Builder, Derived >
typedef Builder< Derived > super
 

Public Member Functions

data::variable_list make_variables (const data::data_expression_list &x, const std::string &hint, sort_function sigma) const
 
data::data_expression lift (const data::data_expression &x)
 
data::data_expression_list lift (const data::data_expression_list &x)
 
data::variable_list lift (const data::variable_list &x)
 
pbes_system::propositional_variable lift (const pbes_system::propositional_variable &x)
 
 absinthe_data_expression_builder (const abstraction_map &sigmaA_, const sort_expression_substitution_map &sigmaS_, const function_symbol_substitution_map &sigmaF_, data::set_identifier_generator &generator_, bool is_over_approximation)
 
template<class T >
void apply (T &result, const data::data_expression &x)
 
template<class T >
void apply (T &result, const propositional_variable_instantiation &x)
 
template<class T >
void apply (T &result, const pbes_system::forall &x)
 
template<class T >
void apply (T &result, const pbes_system::exists &x)
 
void update (pbes_system::pbes_equation &x)
 
void update (pbes_system::pbes &x)
 
- Public Member Functions inherited from mcrl2::pbes_system::add_pbes_expressions< Builder, Derived >
void update (pbes_system::pbes_equation &x)
 
void update (pbes_system::pbes &x)
 
template<class T >
void apply (T &result, const pbes_system::propositional_variable_instantiation &x)
 
template<class T >
void apply (T &result, const pbes_system::not_ &x)
 
template<class T >
void apply (T &result, const pbes_system::and_ &x)
 
template<class T >
void apply (T &result, const pbes_system::or_ &x)
 
template<class T >
void apply (T &result, const pbes_system::imp &x)
 
template<class T >
void apply (T &result, const pbes_system::forall &x)
 
template<class T >
void apply (T &result, const pbes_system::exists &x)
 
template<class T >
void apply (T &result, const pbes_system::pbes_expression &x)
 

Public Attributes

const abstraction_mapsigmaH
 
const sort_expression_substitution_mapsigmaS
 
const function_symbol_substitution_mapsigmaF
 
data::set_identifier_generatorgenerator
 
bool m_is_over_approximation
 

Detailed Description

Definition at line 270 of file absinthe.h.

Member Typedef Documentation

◆ super

Constructor & Destructor Documentation

◆ absinthe_data_expression_builder()

mcrl2::pbes_system::absinthe_algorithm::absinthe_data_expression_builder::absinthe_data_expression_builder ( const abstraction_map sigmaA_,
const sort_expression_substitution_map sigmaS_,
const function_symbol_substitution_map sigmaF_,
data::set_identifier_generator generator_,
bool  is_over_approximation 
)
inline

Definition at line 321 of file absinthe.h.

Member Function Documentation

◆ apply() [1/4]

template<class T >
void mcrl2::pbes_system::absinthe_algorithm::absinthe_data_expression_builder::apply ( T &  result,
const data::data_expression x 
)
inline

Definition at line 334 of file absinthe.h.

◆ apply() [2/4]

template<class T >
void mcrl2::pbes_system::absinthe_algorithm::absinthe_data_expression_builder::apply ( T &  result,
const pbes_system::exists x 
)
inline

Definition at line 379 of file absinthe.h.

◆ apply() [3/4]

template<class T >
void mcrl2::pbes_system::absinthe_algorithm::absinthe_data_expression_builder::apply ( T &  result,
const pbes_system::forall x 
)
inline

Definition at line 371 of file absinthe.h.

◆ apply() [4/4]

template<class T >
void mcrl2::pbes_system::absinthe_algorithm::absinthe_data_expression_builder::apply ( T &  result,
const propositional_variable_instantiation x 
)
inline

Definition at line 348 of file absinthe.h.

◆ lift() [1/4]

data::data_expression mcrl2::pbes_system::absinthe_algorithm::absinthe_data_expression_builder::lift ( const data::data_expression x)
inline

Definition at line 293 of file absinthe.h.

◆ lift() [2/4]

data::data_expression_list mcrl2::pbes_system::absinthe_algorithm::absinthe_data_expression_builder::lift ( const data::data_expression_list x)
inline

Definition at line 300 of file absinthe.h.

◆ lift() [3/4]

data::variable_list mcrl2::pbes_system::absinthe_algorithm::absinthe_data_expression_builder::lift ( const data::variable_list x)
inline

Definition at line 307 of file absinthe.h.

◆ lift() [4/4]

pbes_system::propositional_variable mcrl2::pbes_system::absinthe_algorithm::absinthe_data_expression_builder::lift ( const pbes_system::propositional_variable x)
inline

Definition at line 314 of file absinthe.h.

◆ make_variables()

data::variable_list mcrl2::pbes_system::absinthe_algorithm::absinthe_data_expression_builder::make_variables ( const data::data_expression_list x,
const std::string &  hint,
sort_function  sigma 
) const
inline

Definition at line 276 of file absinthe.h.

◆ update() [1/2]

void mcrl2::pbes_system::absinthe_algorithm::absinthe_data_expression_builder::update ( pbes_system::pbes x)
inline

Definition at line 394 of file absinthe.h.

◆ update() [2/2]

void mcrl2::pbes_system::absinthe_algorithm::absinthe_data_expression_builder::update ( pbes_system::pbes_equation x)
inline

Definition at line 386 of file absinthe.h.

Member Data Documentation

◆ generator

data::set_identifier_generator& mcrl2::pbes_system::absinthe_algorithm::absinthe_data_expression_builder::generator

Definition at line 290 of file absinthe.h.

◆ m_is_over_approximation

bool mcrl2::pbes_system::absinthe_algorithm::absinthe_data_expression_builder::m_is_over_approximation

Definition at line 291 of file absinthe.h.

◆ sigmaF

const function_symbol_substitution_map& mcrl2::pbes_system::absinthe_algorithm::absinthe_data_expression_builder::sigmaF

Definition at line 289 of file absinthe.h.

◆ sigmaH

const abstraction_map& mcrl2::pbes_system::absinthe_algorithm::absinthe_data_expression_builder::sigmaH

Definition at line 287 of file absinthe.h.

◆ sigmaS

const sort_expression_substitution_map& mcrl2::pbes_system::absinthe_algorithm::absinthe_data_expression_builder::sigmaS

Definition at line 288 of file absinthe.h.


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