mCRL2
Loading...
Searching...
No Matches
mcrl2::core::term_traits_optimized< pbes_system::pbes_expression > Struct Reference

Contains type information for pbes expressions. More...

#include <term_traits_optimized.h>

Inheritance diagram for mcrl2::core::term_traits_optimized< pbes_system::pbes_expression >:
mcrl2::core::term_traits< pbes_system::pbes_expression >

Public Types

typedef core::term_traits< pbes_system::pbes_expressionsuper
 
- Public Types inherited from mcrl2::core::term_traits< pbes_system::pbes_expression >
typedef pbes_system::pbes_expression term_type
 The term type.
 
typedef data::data_expression data_term_type
 The data term type.
 
typedef data::data_expression_list data_term_sequence_type
 The data term sequence type.
 
typedef data::variable variable_type
 The variable type.
 
typedef data::variable_list variable_sequence_type
 The variable sequence type.
 
typedef pbes_system::propositional_variable propositional_variable_decl_type
 The propositional variable declaration type.
 
typedef pbes_system::propositional_variable_instantiation propositional_variable_type
 The propositional variable instantiation type.
 
typedef core::identifier_string string_type
 The string type.
 

Static Public Member Functions

static term_type not_ (const term_type &x)
 
static void make_not_ (term_type &result, const term_type &x)
 
static term_type and_ (const term_type &x, const term_type &y)
 
static void make_and_ (term_type &result, const term_type &x, const term_type &y)
 
static term_type or_ (const term_type &x, const term_type &y)
 
static void make_or_ (term_type &result, const term_type &x, const term_type &y)
 
static term_type imp (const term_type &x, const term_type &y)
 
static void make_imp (term_type &result, const term_type &x, const term_type &y)
 
static void make_forall (term_type &result, const variable_sequence_type &d, const term_type &x)
 
static void make_exists (term_type &result, const variable_sequence_type &d, const term_type &x)
 
template<typename FwdIt >
static term_type join_or (FwdIt first, FwdIt last)
 
template<typename FwdIt >
static term_type join_and (FwdIt first, FwdIt last)
 
- Static Public Member Functions inherited from mcrl2::core::term_traits< pbes_system::pbes_expression >
static term_type true_ ()
 Make the value true.
 
static term_type false_ ()
 Make the value false.
 
static term_type not_ (const term_type &p)
 Make a negation.
 
static void make_not_ (term_type &result, const term_type &p)
 Make a negation.
 
static term_type and_ (const term_type &p, const term_type &q)
 Make a conjunction.
 
static void make_and_ (term_type &result, const term_type &p, const term_type &q)
 Make a conjunction.
 
static term_type or_ (const term_type &p, const term_type &q)
 Make a disjunction.
 
static void make_or_ (term_type &result, const term_type &p, const term_type &q)
 Make a disjunction.
 
template<typename FwdIt >
static term_type join_or (FwdIt first, FwdIt last)
 
template<typename FwdIt >
static term_type join_and (FwdIt first, FwdIt last)
 
static term_type imp (const term_type &p, const term_type &q)
 Make an implication.
 
static void make_imp (term_type &result, const term_type &p, const term_type &q)
 Make an implication.
 
static term_type forall (const variable_sequence_type &l, const term_type &p)
 Make a universal quantification.
 
static void make_forall (term_type &result, const variable_sequence_type &l, const term_type &p)
 Make a universal quantification.
 
static term_type exists (const variable_sequence_type &l, const term_type &p)
 Make an existential quantification.
 
static void make_exists (term_type &result, const variable_sequence_type &l, const term_type &p)
 Make an existential quantification.
 
static bool is_true (const term_type &t)
 Test for the value true.
 
static bool is_false (const term_type &t)
 Test for the value false.
 
static bool is_not (const term_type &t)
 Test for a negation.
 
static bool is_and (const term_type &t)
 Test for a conjunction.
 
static bool is_or (const term_type &t)
 Test for a disjunction.
 
static bool is_imp (const term_type &t)
 Test for an implication.
 
static bool is_forall (const term_type &t)
 Test for an universal quantification.
 
static bool is_exists (const term_type &t)
 Test for an existential quantification.
 
static bool is_data (const term_type &t)
 Test for data term.
 
static bool is_prop_var (const term_type &t)
 Test for propositional variable instantiation.
 
static term_type left (const term_type &t)
 Returns the left argument of a term of type and, or or imp.
 
static term_type right (const term_type &t)
 Returns the right argument of a term of type and, or or imp.
 
static const term_typenot_arg (const term_type &t)
 Returns the argument of a term of type not.
 
static const variable_sequence_typevar (const term_type &t)
 Returns the quantifier variables of a quantifier expression.
 
static const string_typename (const term_type &t)
 Returns the name of a propositional variable instantiation.
 
static const data_term_sequence_typeparam (const term_type &t)
 Returns the parameter list of a propositional variable instantiation.
 
static const term_typevariable2term (const variable_type &v)
 Conversion from variable to term.
 
static bool is_variable (const term_type &t)
 Test if a term is a variable.
 
static std::string pp (const term_type &t)
 Pretty print function.
 

Detailed Description

Contains type information for pbes expressions.

Definition at line 29 of file term_traits_optimized.h.

Member Typedef Documentation

◆ super

Member Function Documentation

◆ and_()

static term_type mcrl2::core::term_traits_optimized< pbes_system::pbes_expression >::and_ ( const term_type x,
const term_type y 
)
inlinestatic

Definition at line 48 of file term_traits_optimized.h.

◆ imp()

static term_type mcrl2::core::term_traits_optimized< pbes_system::pbes_expression >::imp ( const term_type x,
const term_type y 
)
inlinestatic

Definition at line 76 of file term_traits_optimized.h.

◆ join_and()

template<typename FwdIt >
static term_type mcrl2::core::term_traits_optimized< pbes_system::pbes_expression >::join_and ( FwdIt  first,
FwdIt  last 
)
inlinestatic

Definition at line 110 of file term_traits_optimized.h.

◆ join_or()

template<typename FwdIt >
static term_type mcrl2::core::term_traits_optimized< pbes_system::pbes_expression >::join_or ( FwdIt  first,
FwdIt  last 
)
inlinestatic

Definition at line 103 of file term_traits_optimized.h.

◆ make_and_()

static void mcrl2::core::term_traits_optimized< pbes_system::pbes_expression >::make_and_ ( term_type result,
const term_type x,
const term_type y 
)
inlinestatic

Definition at line 56 of file term_traits_optimized.h.

◆ make_exists()

static void mcrl2::core::term_traits_optimized< pbes_system::pbes_expression >::make_exists ( term_type result,
const variable_sequence_type d,
const term_type x 
)
inlinestatic

Definition at line 96 of file term_traits_optimized.h.

◆ make_forall()

static void mcrl2::core::term_traits_optimized< pbes_system::pbes_expression >::make_forall ( term_type result,
const variable_sequence_type d,
const term_type x 
)
inlinestatic

Definition at line 90 of file term_traits_optimized.h.

◆ make_imp()

static void mcrl2::core::term_traits_optimized< pbes_system::pbes_expression >::make_imp ( term_type result,
const term_type x,
const term_type y 
)
inlinestatic

Definition at line 84 of file term_traits_optimized.h.

◆ make_not_()

static void mcrl2::core::term_traits_optimized< pbes_system::pbes_expression >::make_not_ ( term_type result,
const term_type x 
)
inlinestatic

Definition at line 42 of file term_traits_optimized.h.

◆ make_or_()

static void mcrl2::core::term_traits_optimized< pbes_system::pbes_expression >::make_or_ ( term_type result,
const term_type x,
const term_type y 
)
inlinestatic

Definition at line 70 of file term_traits_optimized.h.

◆ not_()

Definition at line 34 of file term_traits_optimized.h.

◆ or_()

static term_type mcrl2::core::term_traits_optimized< pbes_system::pbes_expression >::or_ ( const term_type x,
const term_type y 
)
inlinestatic

Definition at line 62 of file term_traits_optimized.h.


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