mCRL2
Loading...
Searching...
No Matches
mcrl2::pbes_system::detail::quantifier Class Reference

#include <quantifier_propagate.h>

Public Member Functions

 quantifier (bool is_forall, const data::variable_list &vars)
 
void add_variables (const data::variable_list &vars)
 
bool is_forall () const
 
const std::set< data::variable > & variables () const
 
bool operator== (const quantifier &other) const
 
bool operator< (const quantifier &other) const
 
pbes_expression make_expr_include_only (const std::set< data::variable > &include, const pbes_expression &expr) const
 
pbes_expression make_expr_exclude (const std::set< data::variable > &exclude, const pbes_expression &expr) const
 
std::string to_string () const
 

Protected Member Functions

pbes_expression make_expr (const std::set< data::variable > &vars, const pbes_expression &expr) const
 

Protected Attributes

bool m_is_forall
 
std::set< data::variable > m_vars
 

Detailed Description

Definition at line 44 of file quantifier_propagate.h.

Constructor & Destructor Documentation

◆ quantifier()

mcrl2::pbes_system::detail::quantifier::quantifier ( bool  is_forall,
const data::variable_list &  vars 
)
inline

Definition at line 56 of file quantifier_propagate.h.

Member Function Documentation

◆ add_variables()

void mcrl2::pbes_system::detail::quantifier::add_variables ( const data::variable_list &  vars)
inline

Definition at line 61 of file quantifier_propagate.h.

◆ is_forall()

bool mcrl2::pbes_system::detail::quantifier::is_forall ( ) const
inline

Definition at line 66 of file quantifier_propagate.h.

◆ make_expr()

pbes_expression mcrl2::pbes_system::detail::quantifier::make_expr ( const std::set< data::variable > &  vars,
const pbes_expression &  expr 
) const
inlineprotected

Definition at line 50 of file quantifier_propagate.h.

◆ make_expr_exclude()

pbes_expression mcrl2::pbes_system::detail::quantifier::make_expr_exclude ( const std::set< data::variable > &  exclude,
const pbes_expression &  expr 
) const
inline

Definition at line 91 of file quantifier_propagate.h.

◆ make_expr_include_only()

pbes_expression mcrl2::pbes_system::detail::quantifier::make_expr_include_only ( const std::set< data::variable > &  include,
const pbes_expression &  expr 
) const
inline

Definition at line 86 of file quantifier_propagate.h.

◆ operator<()

bool mcrl2::pbes_system::detail::quantifier::operator< ( const quantifier &  other) const
inline

Definition at line 81 of file quantifier_propagate.h.

◆ operator==()

bool mcrl2::pbes_system::detail::quantifier::operator== ( const quantifier &  other) const
inline

Definition at line 76 of file quantifier_propagate.h.

◆ to_string()

std::string mcrl2::pbes_system::detail::quantifier::to_string ( ) const
inline

Definition at line 96 of file quantifier_propagate.h.

◆ variables()

const std::set< data::variable > & mcrl2::pbes_system::detail::quantifier::variables ( ) const
inline

Definition at line 71 of file quantifier_propagate.h.

Member Data Documentation

◆ m_is_forall

bool mcrl2::pbes_system::detail::quantifier::m_is_forall
protected

Definition at line 47 of file quantifier_propagate.h.

◆ m_vars

std::set<data::variable> mcrl2::pbes_system::detail::quantifier::m_vars
protected

Definition at line 48 of file quantifier_propagate.h.


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