12#ifndef MCRL2_PBES_NORMALIZE_SORTS_H
13#define MCRL2_PBES_NORMALIZE_SORTS_H
15#include "mcrl2/data/normalize_sorts.h"
16#include "mcrl2/pbes/builder.h"
Term containing a string.
aterm_string(const aterm &t)
Constructor.
aterm(const aterm &other) noexcept=default
This class has user-declared copy constructor so declare default copy and move operators.
A unordered_map class in which aterms can be stored.
parse_node_unexpected_exception(const parser &p, const parse_node &node)
An abstraction expression.
abstraction(const atermpp::aterm &term)
Constructor.
void translate_user_notation()
Translate user notation within the equations of the data specification.
bool is_well_typed() const
Returns true if.
data_specification()=default
Default constructor. Generate a data specification that contains only booleans and positive numbers.
Components for generating an arbitrary element of a sort.
representative_generator(const data_specification &specification)
Constructor with data specification as context.
Identifier generator that stores the identifiers of the context in a set. Using the operator()() and ...
\brief An untyped parameter
const core::identifier_string & name() const
\brief A where expression
where_clause & operator=(where_clause &&) noexcept=default
const data_expression & body() const
const assignment_expression_list & declarations() const
\brief The and operator for pbes expressions
and_(const pbes_expression &left, const pbes_expression &right)
\brief Constructor Z14.
and_(const and_ &) noexcept=default
Move semantics.
and_(and_ &&) noexcept=default
and_ & operator=(and_ &&) noexcept=default
and_(const atermpp::aterm &term)
and_ & operator=(const and_ &) noexcept=default
const pbes_expression & left() const
const pbes_expression & right() const
and_()
\brief Default constructor X3.
std::map< core::identifier_string, propositional_variable > m_propositional_variables
data::sort_expression_list propositional_variable_sorts(const core::identifier_string &name) const
bool is_declared(const core::identifier_string &name) const
void add_propositional_variables(const PropositionalVariableContainer &propositional_variables, const data::sort_type_checker &sort_typechecker)
\brief The existential quantification operator for pbes expressions
exists(const atermpp::aterm &term)
exists & operator=(exists &&) noexcept=default
exists(exists &&) noexcept=default
exists(const data::variable_list &variables, const pbes_expression &body)
\brief Constructor Z14.
const data::variable_list & variables() const
exists()
\brief Default constructor X3.
exists(const exists &) noexcept=default
Move semantics.
const pbes_expression & body() const
exists & operator=(const exists &) noexcept=default
static fixpoint_symbol nu()
Returns the nu symbol.
fixpoint_symbol()
\brief Default constructor X3.
fixpoint_symbol & operator=(fixpoint_symbol &&) noexcept=default
fixpoint_symbol(const fixpoint_symbol &) noexcept=default
Move semantics.
bool is_nu() const
Returns true if the symbol is nu.
bool is_mu() const
Returns true if the symbol is mu.
fixpoint_symbol(fixpoint_symbol &&) noexcept=default
static fixpoint_symbol mu()
Returns the mu symbol.
fixpoint_symbol & operator=(const fixpoint_symbol &) noexcept=default
fixpoint_symbol(const atermpp::aterm &term)
\brief The universal quantification operator for pbes expressions
forall()
\brief Default constructor X3.
const pbes_expression & body() const
forall(const data::variable_list &variables, const pbes_expression &body)
\brief Constructor Z14.
forall(const atermpp::aterm &term)
const data::variable_list & variables() const
forall & operator=(const forall &) noexcept=default
forall & operator=(forall &&) noexcept=default
forall(const forall &) noexcept=default
Move semantics.
forall(forall &&) noexcept=default
\brief The implication operator for pbes expressions
imp & operator=(imp &&) noexcept=default
imp(const imp &) noexcept=default
Move semantics.
const pbes_expression & left() const
imp(imp &&) noexcept=default
imp(const atermpp::aterm &term)
imp()
\brief Default constructor X3.
imp(const pbes_expression &left, const pbes_expression &right)
\brief Constructor Z14.
const pbes_expression & right() const
imp & operator=(const imp &) noexcept=default
\brief The not operator for pbes expressions
not_()
\brief Default constructor X3.
not_(const pbes_expression &operand)
\brief Constructor Z14.
not_(const not_ &) noexcept=default
Move semantics.
const pbes_expression & operand() const
not_ & operator=(const not_ &) noexcept=default
not_(not_ &&) noexcept=default
not_(const atermpp::aterm &term)
not_ & operator=(not_ &&) noexcept=default
\brief The or operator for pbes expressions
const pbes_expression & left() const
or_(const or_ &) noexcept=default
Move semantics.
or_(const pbes_expression &left, const pbes_expression &right)
\brief Constructor Z14.
const pbes_expression & right() const
or_(or_ &&) noexcept=default
or_ & operator=(or_ &&) noexcept=default
or_ & operator=(const or_ &) noexcept=default
or_(const atermpp::aterm &term)
or_()
\brief Default constructor X3.
const pbes_expression & formula() const
Returns the predicate formula on the right hand side of the equation.
fixpoint_symbol & symbol()
Returns the fixpoint symbol of the equation.
pbes_equation(const fixpoint_symbol &symbol, const propositional_variable &variable, const pbes_expression &expr)
Constructor.
bool is_solved() const
Returns true if the predicate formula on the right hand side contains no predicate variables.
fixpoint_symbol m_symbol
The fixpoint symbol of the equation.
propositional_variable m_variable
The variable on the left hand side of the equation.
const fixpoint_symbol & symbol() const
Returns the fixpoint symbol of the equation.
bool operator<(const pbes_equation &other) const
A comparison operator on pbes equations. \detail The comparison is on the addresses of aterm objects ...
propositional_variable & variable()
Returns the pbes variable of the equation.
pbes_expression m_formula
The expression on the right hand side of the equation.
void swap(pbes_equation &other) noexcept
Swaps the contents.
pbes_equation()=default
Constructor.
pbes_expression & formula()
Returns the predicate formula on the right hand side of the equation.
const propositional_variable & variable() const
Returns the pbes variable of the equation.
pbes_expression & operator=(pbes_expression &&) noexcept=default
pbes_expression & operator=(const pbes_expression &) noexcept=default
pbes_expression(const atermpp::aterm &term)
pbes_expression(const pbes_expression &) noexcept=default
Move semantics.
pbes_expression(const data::data_expression &x)
\brief Constructor Z6.
pbes_expression(const data::untyped_data_parameter &x)
\brief Constructor Z6.
pbes_expression()
\brief Default constructor X3.
pbes_expression(pbes_expression &&) noexcept=default
void operator()(pbes &pbesspec)
Typecheck the pbes pbesspec.
pbes_expression operator()(const pbes_expression &x)
Type check a process expression. Throws a mcrl2::runtime_error exception if the expression is not wel...
detail::pbes_context m_pbes_context
pbes_type_checker(const data::data_specification &dataspec, const VariableContainer &global_variables, const PropositionalVariableContainer &propositional_variables)
Constructor.
pbes_expression typecheck(const pbes_expression &x, const data::variable_list ¶meters)
pbes_type_checker(const data::data_specification &dataspec=data::data_specification())
Default constructor.
data::data_type_checker m_data_type_checker
std::vector< propositional_variable > equation_variables(const std::vector< pbes_equation > &equations)
data::detail::variable_context m_variable_context
parameterized boolean equation system
std::set< data::variable > & global_variables()
Returns the declared free variables of the pbes.
bool is_closed() const
True if the pbes is closed.
data::data_specification m_data
The data specification.
pbes(const data::data_specification &data, const std::vector< pbes_equation > &equations, propositional_variable_instantiation initial_state)
Constructor.
std::set< data::variable > m_global_variables
The set of global variables.
std::set< propositional_variable > compute_declared_variables() const
Returns the predicate variables appearing in the left hand side of an equation.
pbes(const data::data_specification &data, const std::set< data::variable > &global_variables, const std::vector< pbes_equation > &equations, propositional_variable_instantiation initial_state)
Constructor.
const propositional_variable_instantiation & initial_state() const
Returns the initial state.
std::set< propositional_variable > binding_variables() const
Returns the set of binding variables of the pbes. This is the set variables that occur on the left ha...
std::set< propositional_variable > occurring_variables() const
Returns the set of occurring propositional variable declarations of the pbes, i.e....
std::set< propositional_variable_instantiation > occurring_variable_instantiations() const
Returns the set of occurring propositional variable instantiations of the pbes. This is the set of va...
const std::set< data::variable > & global_variables() const
Returns the declared free variables of the pbes.
std::vector< pbes_equation > & equations()
Returns the equations.
propositional_variable_instantiation & initial_state()
Returns the initial state.
propositional_variable_instantiation m_initial_state
The initial state.
pbes()=default
Constructor.
std::vector< pbes_equation > m_equations
The sequence of pbes equations.
bool is_declared_in(Iter first, Iter last, const propositional_variable_instantiation &v, const data::data_specification &data_spec) const
Checks if the propositional variable instantiation v appears with the right type in the sequence of p...
const std::vector< pbes_equation > & equations() const
Returns the equations.
bool is_well_typed() const
Checks if the PBES is well typed.
\brief A propositional variable instantiation
const data::data_expression_list & parameters() const
propositional_variable_instantiation(const propositional_variable_instantiation &) noexcept=default
Move semantics.
propositional_variable_instantiation(const std::string &name)
Constructor.
propositional_variable_instantiation()
Default constructor.
propositional_variable_instantiation(propositional_variable_instantiation &&) noexcept=default
propositional_variable_instantiation(const core::identifier_string &name, const data::data_expression_list ¶meters)
Constructor.
const core::identifier_string & name() const
propositional_variable_instantiation & operator=(propositional_variable_instantiation &&) noexcept=default
propositional_variable_instantiation(const core::identifier_string &name)
Constructor.
propositional_variable_instantiation & operator=(const propositional_variable_instantiation &) noexcept=default
propositional_variable_instantiation(const std::string &name, const data::data_expression_list ¶meters)
Constructor.
propositional_variable_instantiation(const atermpp::aterm &term)
Constructor.
Wrapper class for internal storage and substitution updates using operator()
assignment(const propositional_variable &v, map_type &m)
Constructor.
assignment & operator=(const pbes_expression &e)
Assigns expression on the right-hand side.
const propositional_variable & m_variable
Substitution function for propositional variables.
propositional_variable_substitution(const map_type &other)
const_iterator end() const
Returns an iterator pointing past the end of the sequence of assignments.
iterator begin()
Returns an iterator pointing to the beginning of the sequence of assignments.
pbes_expression operator()(const variable_type &v) const
Apply this substitution to a single variable expression.
iterator end()
Returns an iterator pointing past the end of the sequence of assignments.
map_type::size_type erase(const propositional_variable &v)
Removes the substitution to the propositional variable v.
const_iterator find(variable_type const &v) const
Returns an iterator that references the expression associated with v or is equal to m_map....
bool empty() const
Returns true if the sequence of assignments is empty.
propositional_variable_substitution()=default
propositional_variable_substitution(const propositional_variable &X, const pbes_expression &phi)
Constructor. Initializes the substitution with the assignment X := phi.
const_iterator begin() const
Returns an iterator pointing to the beginning of the sequence of assignments.
assignment operator[](const propositional_variable &v)
Update substitution for a single variable.
iterator find(const variable_type &v)
Returns an iterator that references the expression associated with v or is equal to m_map....
\brief A propositional variable declaration
const data::variable_list & parameters() const
propositional_variable(const atermpp::aterm &term)
propositional_variable(const std::string &name)
propositional_variable(const std::string &name, const data::variable_list ¶meters)
\brief Constructor Z1.
propositional_variable(const propositional_variable &) noexcept=default
Move semantics.
const core::identifier_string & name() const
propositional_variable & operator=(propositional_variable &&) noexcept=default
propositional_variable()
\brief Default constructor X3.
propositional_variable & operator=(const propositional_variable &) noexcept=default
propositional_variable(propositional_variable &&) noexcept=default
propositional_variable(const atermpp::aterm_string &name)
propositional_variable(const core::identifier_string &name, const data::variable_list ¶meters)
\brief Constructor Z12.
D_ParserTables parser_tables_mcrl2
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
void warn_and_or(const parse_node &)
Prints a warning for each occurrence of 'x && y || z' in the parse tree.
bool equal_sorts(const data::variable_list &v, const data::data_expression_list &w, const data::data_specification &data_spec)
Checks if the sorts of the variables/expressions in both lists are equal.
void parse_substitution(std::string text, MutableSubstitution &sigma, const data_specification &data_spec=data::data_specification())
Parses a string of the form "b: Bool := true, n: Nat := 0", and adds the substitutions to the substit...
Namespace for system defined sort bool_.
bool is_false_function_symbol(const atermpp::aterm &e)
Recogniser for function false.
bool is_or_application(const atermpp::aterm &e)
Recogniser for application of ||.
const function_symbol & false_()
Constructor for function symbol false.
bool is_and_application(const atermpp::aterm &e)
Recogniser for application of &&.
bool is_true_function_symbol(const atermpp::aterm &e)
Recogniser for function true.
bool is_not_application(const atermpp::aterm &e)
Recogniser for application of !.
const function_symbol & true_()
Constructor for function symbol true.
bool is_data_expression(const atermpp::aterm &x)
Test for a data_expression expression.
bool is_abstraction(const atermpp::aterm &x)
Returns true if the term t is an abstraction.
const data_expression & false_()
const data_expression & true_()
bool is_forall(const atermpp::aterm &x)
Returns true if the term t is a universal quantification.
bool is_untyped_data_parameter(const atermpp::aterm &x)
bool is_exists(const atermpp::aterm &x)
Returns true if the term t is an existential quantification.
bool is_application(const atermpp::aterm &x)
Returns true if the term t is an application.
bool is_variable(const atermpp::aterm &x)
Returns true if the term t is a variable.
The namespace for accessor functions on pbes expressions.
const pbes_expression & data_arg(const pbes_expression &t)
Returns the pbes expression argument of expressions of type not, exists and forall.
const pbes_expression & arg(const pbes_expression &t)
Returns the pbes expression argument of expressions of type not, exists and forall.
const pbes_expression & data_right(const pbes_expression &x)
Returns the left hand side of an expression of type and, or or imp.
const pbes_expression & data_left(const pbes_expression &x)
Returns the left hand side of an expression of type and, or or imp.
const pbes_expression & left(const pbes_expression &t)
Returns the left hand side of an expression of type and, or or imp.
const pbes_expression & right(const pbes_expression &t)
Returns the right hand side of an expression of type and, or or imp.
const data::data_expression_list & param(const pbes_expression &t)
Returns the parameters of a propositional variable instantiation.
const core::identifier_string & name(const pbes_expression &t)
Returns the name of a propositional variable expression.
const data::variable_list & var(const pbes_expression &t)
Returns the variables of a quantification expression.
void instantiate_global_variables(pbes &p)
Attempts to eliminate the free variables of a PBES, by substituting a constant value for them....
bool is_bes(const pbes &x)
Returns true if a PBES is in BES form.
untyped_pbes parse_pbes_new(const std::string &text)
bool has_quantifier_name_clashes(const pbes_expression &x)
void replace_global_variables(pbes &p, const data::mutable_map_substitution<> &sigma)
Applies a global variable substitution to a PBES.
void complete_pbes(pbes &x)
data::mutable_map_substitution instantiate_global_variables(pbes &p)
Eliminates the global variables of a PBES, by substituting a constant value for them....
bool is_well_typed_pbes(const std::set< data::sort_expression > &declared_sorts, const std::set< data::variable > &declared_global_variables, const std::set< data::variable > &occurring_global_variables, const std::set< propositional_variable > &declared_variables, const std::set< propositional_variable_instantiation > &occ, const propositional_variable_instantiation &init, const data::data_specification &data_spec)
bool has_conflicting_type(Iter first, Iter last, const propositional_variable_instantiation &v, const data::data_specification &data_spec)
Checks if the propositional variable instantiation v has a conflict with the sequence of propositiona...
find_propositional_variables_traverser< Traverser, OutputIterator > make_find_propositional_variables_traverser(OutputIterator out)
bool has_propositional_variables(const pbes_expression &x)
propositional_variable parse_propositional_variable(const std::string &text)
std::set< data::variable > find_quantifier_variables(const pbes_expression &x)
typecheck_builder make_typecheck_builder(data::data_type_checker &data_typechecker, const data::detail::variable_context &variables, const detail::pbes_context &propositional_variables)
pbes_expression parse_pbes_expression(const std::string &text)
bool is_well_typed(const pbes_equation &eqn)
Checks if the equation is well typed.
bool is_well_typed_equation(const pbes_equation &eqn, const std::set< data::sort_expression > &declared_sorts, const std::set< data::variable > &declared_global_variables, const data::data_specification &data_spec)
pbes_expression parse_pbes_expression_new(const std::string &text)
The main namespace for the PBES library.
bool is_pbes_exists(const pbes_expression &t)
Returns true if the term t is an existential quantification.
std::set< data::function_symbol > find_function_symbols(const T &x)
std::ostream & operator<<(std::ostream &out, const exists &x)
std::ostream & operator<<(std::ostream &out, const pbes_equation &x)
bool is_universal_or(const pbes_expression &t)
Test for a disjunction.
std::set< data::variable > find_free_variables(const pbes_system::pbes_equation &x)
std::string pp(const pbes_system::propositional_variable_list &x, bool arg0)
std::set< data::variable > find_free_variables(const T &x)
bool is_bes(const T &x)
Returns true if a PBES object is in BES form.
std::string pp(const pbes_system::or_ &x, bool arg0)
bool is_data(const pbes_expression &t)
Returns true if the term t is a data expression.
bool operator!=(const pbes_equation &x, const pbes_equation &y)
void swap(propositional_variable_instantiation &t1, propositional_variable_instantiation &t2) noexcept
\brief swap overload
propositional_variable typecheck_propositional_variable(const propositional_variable &x, const VariableContainer &variables, const data::data_specification &dataspec=data::data_specification())
Type check a parsed mCRL2 propositional variable. Throws an exception if something went wrong.
std::set< data::variable > find_free_variables(const pbes_system::pbes &x)
void normalize_sorts(pbes_system::pbes_equation_vector &x, const data::sort_specification &sortspec)
std::string pp(const pbes_system::imp &x, bool arg0)
std::string pp(const pbes_system::propositional_variable_instantiation_list &x, bool arg0)
void make_propositional_variable(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_propositional_variable(const atermpp::aterm &x)
pbes_system::pbes_expression normalize_sorts(const pbes_system::pbes_expression &x, const data::sort_specification &sortspec)
std::set< data::sort_expression > find_sort_expressions(const pbes_system::pbes &x)
bool is_universal_and(const pbes_expression &t)
Test for a conjunction.
bool is_pbes_expression(const atermpp::aterm &x)
bool is_pbes_not(const pbes_expression &t)
Returns true if the term t is a not expression.
std::string pp(const pbes_system::pbes_equation_vector &x, bool arg0)
const pbes_expression & true_()
bool is_pbes_forall(const pbes_expression &t)
Returns true if the term t is a universal quantification.
pbes_expression make_exists_(const data::variable_list &l, const pbes_expression &p)
Make an existential quantification. It checks for an empty variable list, which is not allowed.
std::string pp(const pbes_system::pbes_expression_list &x, bool arg0)
std::ostream & operator<<(std::ostream &out, const not_ &x)
bool is_not(const atermpp::aterm &x)
std::set< data::variable > find_free_variables_with_bound(const T &x, VariableContainer const &bound)
void optimized_not(pbes_expression &result, const pbes_expression &p)
Make a negation.
void make_and_(atermpp::aterm &t, const ARGUMENTS &... args)
std::set< pbes_system::propositional_variable_instantiation > find_propositional_variable_instantiations(const pbes_system::pbes_expression &x)
void find_identifiers(const T &x, OutputIterator o)
T replace_variables_capture_avoiding(const T &x, Substitution &sigma, data::set_identifier_generator &id_generator)
void replace_variables_capture_avoiding(T &x, Substitution &sigma, data::set_identifier_generator &id_generator)
void make_not_(atermpp::aterm &t, const ARGUMENTS &... args)
bool is_exists(const atermpp::aterm &x)
data::variable_list free_variables(const pbes_expression &x)
std::ostream & operator<<(std::ostream &out, const forall &x)
std::ostream & operator<<(std::ostream &out, const fixpoint_symbol &x)
bool operator==(const pbes_equation &x, const pbes_equation &y)
bool is_constant(const pbes_expression &x)
void find_free_variables(const T &x, OutputIterator o)
void normalize_sorts(pbes_system::pbes &x, const data::sort_specification &)
std::ostream & operator<<(std::ostream &out, const pbes &x)
bool is_or(const atermpp::aterm &x)
const data::variable_list & quantifier_variables(const pbes_expression &x)
std::ostream & operator<<(std::ostream &out, const and_ &x)
std::function< pbes_expression(const propositional_variable_instantiation &)> compose_substitutions(const std::function< pbes_expression(const propositional_variable_instantiation &)> sigma1, const std::function< pbes_expression(const propositional_variable_instantiation &)> sigma2)
bool is_well_typed_pbes(const std::set< data::sort_expression > &declared_sorts, const std::set< data::variable > &declared_global_variables, const std::set< data::variable > &occurring_global_variables, const std::set< propositional_variable > &declared_variables, const std::set< propositional_variable_instantiation > &occ, const propositional_variable_instantiation &init, const data::data_specification &data_spec)
void optimized_exists(pbes_expression &result, const data::variable_list &l, const pbes_expression &p)
Make an existential quantification If l is empty, p is returned.
std::set< data::function_symbol > find_function_symbols(const pbes_system::pbes &x)
pbes_expression typecheck_pbes_expression(pbes_expression &x, const VariableContainer &variables, const PropositionalVariableContainer &propositional_variables, const data::data_specification &dataspec=data::data_specification())
Type check a parsed mCRL2 pbes expression. Throws an exception if something went wrong.
bool has_propositional_variables(const pbes_expression &x)
bool is_forall(const atermpp::aterm &x)
void typecheck_pbes(pbes &pbesspec)
Type check a parsed mCRL2 pbes specification. Throws an exception if something went wrong.
std::ostream & operator<<(std::ostream &out, const or_ &x)
void swap(not_ &t1, not_ &t2) noexcept
\brief swap overload
void make_propositional_variable_instantiation(atermpp::aterm &t, const ARGUMENTS &... args)
std::string pp(const pbes_system::propositional_variable &x, bool arg0)
std::string pp(const pbes_system::exists &x, bool arg0)
void make_or_(atermpp::aterm &t, const ARGUMENTS &... args)
std::string pp(const pbes_system::pbes_expression &x, bool arg0)
atermpp::aterm pbes_to_aterm(const pbes &p)
Conversion to atermappl.
std::set< data::variable > find_all_variables(const T &x)
bool is_universal_not(const pbes_expression &t)
Test for a conjunction.
bool operator==(const pbes &p1, const pbes &p2)
Equality operator on PBESs.
void swap(pbes_equation &t1, pbes_equation &t2) noexcept
\brief swap overload
bool is_well_typed(const pbes_equation &eqn)
std::ostream & operator<<(std::ostream &out, const propositional_variable_instantiation &x)
T replace_sort_expressions(const T &x, const Substitution &sigma, bool innermost)
std::set< core::identifier_string > find_identifiers(const T &x)
void swap(exists &t1, exists &t2) noexcept
\brief swap overload
void find_function_symbols(const T &x, OutputIterator o)
void find_sort_expressions(const T &x, OutputIterator o)
bool search_variable(const T &x, const data::variable &v)
Returns true if the term has a given variable as subterm.
std::set< data::variable > find_free_variables(const pbes_system::pbes_expression &x)
void swap(or_ &t1, or_ &t2) noexcept
\brief swap overload
pbes_system::pbes_expression translate_user_notation(const pbes_system::pbes_expression &x)
bool is_pbes_or(const pbes_expression &t)
Returns true if the term t is an or expression.
std::set< propositional_variable_instantiation > find_propositional_variable_instantiations(Container const &container)
Returns all data variables that occur in a range of expressions.
bool is_false(const pbes_expression &t)
Test for the value false.
void optimized_forall(pbes_expression &result, const data::variable_list &l, const pbes_expression &p)
Make a universal quantification If l is empty, p is returned.
bool is_pbes_imp(const pbes_expression &t)
Returns true if the term t is an imp expression.
void swap(forall &t1, forall &t2) noexcept
\brief swap overload
void optimized_or(pbes_expression &result, const pbes_expression &p, const pbes_expression &q)
Make a disjunction.
bool is_pbes_and(const pbes_expression &t)
Returns true if the term t is an and expression.
void swap(propositional_variable &t1, propositional_variable &t2) noexcept
\brief swap overload
atermpp::aterm pbes_equation_to_aterm(const pbes_equation &eqn)
Conversion to atermaPpl.
pbes_expression make_forall_(const data::variable_list &l, const pbes_expression &p)
Make a universal quantification. It checks for an empty variable list, which is not allowed.
void find_all_variables(const T &x, OutputIterator o)
bool search_variable(const pbes_system::pbes_expression &x, const data::variable &v)
std::set< data::variable > find_all_variables(const pbes_system::pbes &x)
std::string pp(const pbes_system::not_ &x, bool arg0)
void complete_data_specification(pbes &)
Adds all sorts that appear in the PBES p to the data specification of p.
void swap(pbes_expression &t1, pbes_expression &t2) noexcept
\brief swap overload
std::string pp(const pbes_system::pbes_equation &x, bool arg0)
void swap(imp &t1, imp &t2) noexcept
\brief swap overload
std::ostream & operator<<(std::ostream &out, const pbes_expression &x)
void make_exists(atermpp::aterm &t, const ARGUMENTS &... args)
std::set< core::identifier_string > find_identifiers(const pbes_system::pbes_expression &x)
std::ostream & operator<<(std::ostream &out, const imp &x)
bool is_propositional_variable_instantiation(const atermpp::aterm &x)
bool is_well_typed_equation(const pbes_equation &eqn, const std::set< data::sort_expression > &declared_sorts, const std::set< data::variable > &declared_global_variables, const data::data_specification &data_spec)
std::set< data::sort_expression > find_sort_expressions(const T &x)
std::string pp(const pbes_system::propositional_variable_instantiation &x, bool arg0)
bool is_and(const atermpp::aterm &x)
std::string pp(const pbes_equation_vector &x)
void optimized_and(pbes_expression &result, const pbes_expression &p, const pbes_expression &q)
Make a conjunction.
void swap(and_ &t1, and_ &t2) noexcept
\brief swap overload
void translate_user_notation(pbes_system::pbes &x)
void find_propositional_variable_instantiations(Container const &container, OutputIterator o)
Returns all data variables that occur in a range of expressions.
void swap(fixpoint_symbol &t1, fixpoint_symbol &t2) noexcept
\brief swap overload
std::string pp(const pbes_system::pbes &x, bool arg0)
bool is_imp(const atermpp::aterm &x)
std::ostream & operator<<(std::ostream &out, const propositional_variable &x)
void optimized_imp(pbes_expression &result, const pbes_expression &p, const pbes_expression &q)
Make an implication.
void make_imp(atermpp::aterm &t, const ARGUMENTS &... args)
void replace_sort_expressions(T &x, const Substitution &sigma, bool innermost)
bool is_true(const pbes_expression &t)
Test for the value true.
const pbes_expression & false_()
std::string pp(const pbes_system::and_ &x, bool arg0)
std::string pp(const pbes_system::fixpoint_symbol &x, bool arg0)
void make_forall(atermpp::aterm &t, const ARGUMENTS &... args)
std::string pp(const pbes_system::forall &x, bool arg0)
void find_free_variables_with_bound(const T &x, OutputIterator o, const VariableContainer &bound)
expression builder that visits all sub expressions
static const atermpp::aterm PBESForall
static const atermpp::aterm PBExpr
static const atermpp::aterm PBESOr
static const atermpp::aterm PBESExists
static const atermpp::aterm PBESImp
static const atermpp::aterm PBESNot
static const atermpp::aterm FixPoint
static const atermpp::aterm PropVarInst
static const atermpp::aterm PropVarDecl
static const atermpp::aterm PBESAnd
expression traverser that visits all sub expressions
data_specification_actions(const core::parser &parser_)
untyped_data_specification parse_DataSpec(const core::parse_node &node) const
void apply(T &result, const pbes_system::imp &x)
void apply(T &result, const pbes_system::forall &x)
void apply(T &result, const pbes_system::and_ &x)
void apply(T &result, const pbes_system::pbes_expression &x)
void apply(T &result, const pbes_system::or_ &x)
void update(pbes_system::pbes_equation &x)
void apply(T &result, const pbes_system::propositional_variable_instantiation &x)
void update(pbes_system::pbes &x)
void apply(T &result, const pbes_system::exists &x)
void apply(T &result, const pbes_system::not_ &x)
Maintains a multiset of bound data variables during traversal.
void enter(pbes_equation const &x)
void enter(const pbes &x)
void enter(forall const &x)
void leave(exists const &x)
void leave(pbes_equation const &x)
void leave(const pbes &x)
void leave(forall const &x)
void enter(exists const &x)
void apply(data::where_clause &result, const data::where_clause &x)
void apply(const data::where_clause &x)
void update(pbes_system::pbes &x)
void apply(T &result, const pbes_system::pbes_expression &x)
void apply(T &result, const pbes_system::forall &x)
void update(pbes_system::pbes_equation &x)
void apply(T &result, const pbes_system::not_ &x)
void apply(T &result, const pbes_system::propositional_variable_instantiation &x)
void apply(T &result, const pbes_system::and_ &x)
void apply(T &result, const pbes_system::imp &x)
void apply(T &result, const pbes_system::exists &x)
void apply(T &result, const pbes_system::or_ &x)
void apply(T &result, const pbes_system::exists &x)
void apply(T &result, const pbes_system::and_ &x)
void apply(T &result, const pbes_system::or_ &x)
void apply(T &result, const pbes_system::forall &x)
void apply(T &result, const pbes_system::propositional_variable_instantiation &x)
void apply(T &result, const pbes_system::propositional_variable &x)
void apply(T &result, const pbes_system::imp &x)
void update(pbes_system::pbes_equation &x)
void update(pbes_system::pbes &x)
void apply(T &result, const pbes_system::pbes_expression &x)
void apply(T &result, const pbes_system::not_ &x)
void apply(const pbes_system::imp &x)
void apply(const pbes_system::not_ &x)
void apply(const pbes_system::propositional_variable_instantiation &x)
void apply(const pbes_system::exists &x)
void apply(const pbes_system::pbes &x)
void apply(const pbes_system::pbes_equation &x)
void apply(const pbes_system::pbes_expression &x)
void apply(const pbes_system::or_ &x)
void apply(const pbes_system::and_ &x)
void apply(const pbes_system::forall &x)
void apply(const pbes_system::pbes &x)
void apply(const pbes_system::pbes_expression &x)
void apply(const pbes_system::exists &x)
void apply(const pbes_system::and_ &x)
void apply(const pbes_system::not_ &x)
void apply(const pbes_system::propositional_variable &x)
void apply(const pbes_system::imp &x)
void apply(const pbes_system::forall &x)
void apply(const pbes_system::or_ &x)
void apply(const pbes_system::pbes_equation &x)
void apply(const pbes_system::propositional_variable_instantiation &x)
void apply(const pbes_system::propositional_variable_instantiation &x)
void apply(const pbes_system::and_ &x)
void apply(const pbes_system::forall &x)
void apply(const pbes_system::pbes_equation &x)
void apply(const pbes_system::or_ &x)
void apply(const pbes_system::imp &x)
void apply(const pbes_system::pbes_expression &x)
void apply(const pbes_system::exists &x)
void apply(const pbes_system::not_ &x)
void apply(const pbes_system::pbes &x)
void apply(const pbes_system::exists &x)
void apply(const pbes_system::or_ &x)
void apply(const pbes_system::propositional_variable_instantiation &x)
void apply(const pbes_system::propositional_variable &x)
void apply(const pbes_system::imp &x)
void apply(const pbes_system::and_ &x)
void apply(const pbes_system::pbes &x)
void apply(const pbes_system::forall &x)
void apply(const pbes_system::pbes_equation &x)
void apply(const pbes_system::pbes_expression &x)
void apply(const pbes_system::not_ &x)
void apply(const pbes_system::pbes &x)
void apply(const pbes_system::propositional_variable &x)
void apply(const pbes_system::or_ &x)
void apply(const pbes_system::propositional_variable_instantiation &x)
void apply(const pbes_system::not_ &x)
void apply(const pbes_system::exists &x)
void apply(const pbes_system::and_ &x)
void apply(const pbes_system::imp &x)
void apply(const pbes_system::pbes_expression &x)
void apply(const pbes_system::pbes_equation &x)
void apply(const pbes_system::forall &x)
void apply(T &result, const pbes_system::imp &x)
void update(pbes_system::pbes &x)
void apply(T &result, const pbes_system::pbes_expression &x)
void apply(T &result, const pbes_system::forall &x)
void apply(T &result, const pbes_system::propositional_variable &x)
void apply(T &result, const pbes_system::not_ &x)
void apply(T &result, const pbes_system::and_ &x)
void apply(T &result, const pbes_system::or_ &x)
void update(pbes_system::pbes_equation &x)
void apply(T &result, const pbes_system::exists &x)
void apply(T &result, const pbes_system::propositional_variable_instantiation &x)
void update(pbes_equation &x)
void apply(T &result, const exists &x)
add_capture_avoiding_replacement(data::detail::capture_avoiding_substitution_updater< Substitution > &sigma)
void apply(T &result, const forall &x)
find_propositional_variables_traverser(OutputIterator out_)
void apply(const propositional_variable_instantiation &v)
void apply(const data::data_expression &)
Visitor for collecting the quantifier variables that occur in a pbes expression.
void enter(const forall &x)
std::set< data::variable > result
void enter(const exists &x)
void enter(const propositional_variable_instantiation &)
Visitor for determining if within the scope of a quantifier there are quantifier variables of free va...
void push(const data::variable_list &variables)
Adds variables to the quantifier stack, and adds replacements for the name clashes to replacements.
void pop()
Pops the quantifier stack.
void leave(const forall &)
void enter(const exists &x)
void leave(const exists &)
data::variable name_clash
void enter(const forall &x)
std::vector< data::variable_list > quantifier_stack
bool is_in_quantifier_stack(const core::identifier_string &name) const
Returns true if the quantifier_stack contains a data variable with the given name.
std::set< propositional_variable_instantiation > variables
void apply(const propositional_variable_instantiation &x)
pbes_system::propositional_variable_instantiation parse_PropVarInst(const core::parse_node &node) const
pbes_system::propositional_variable parse_PropVarDecl(const core::parse_node &node) const
pbes_system::propositional_variable_instantiation parse_PbesInit(const core::parse_node &node) const
std::vector< pbes_equation > parse_PbesEqnSpec(const core::parse_node &node) const
pbes_system::fixpoint_symbol parse_FixedPointOperator(const core::parse_node &node) const
pbes_actions(const core::parser &parser_)
untyped_pbes parse_PbesSpec(const core::parse_node &node) const
std::vector< pbes_equation > parse_PbesEqnDeclList(const core::parse_node &node) const
pbes_equation parse_PbesEqnDecl(const core::parse_node &node) const
pbes_system::pbes_expression parse_PbesExpr(const core::parse_node &node) const
data::data_type_checker & m_data_type_checker
void apply(T &result, const propositional_variable_instantiation &x)
void apply(T &result, const data::untyped_data_parameter &x)
const detail::pbes_context & m_pbes_context
data::detail::variable_context m_variable_context
void apply(T &result, const forall &x)
void apply(T &result, const exists &x)
void apply(T &result, const data::data_expression &x)
typecheck_builder(data::data_type_checker &data_typechecker, const data::detail::variable_context &variables, const detail::pbes_context &pbes_context)
An empty struct that can be used to indicate that there is no substitution that should be applied to ...
const propositional_variable_instantiation & operator()(const propositional_variable_instantiation &v)
void apply(T &result, const data::untyped_data_parameter &x)
void apply(T &result, const data::data_expression &x)
Traversal class for pbes_expressions. Used as a base class for pbes_expression_traverser.
void apply(const data::data_expression &x)
void apply(const data::untyped_data_parameter &x)
propositional_variable_instantiation initial_state
std::size_t operator()(const mcrl2::pbes_system::pbes_expression &x) const
std::size_t operator()(const mcrl2::pbes_system::propositional_variable_instantiation &x) const