mCRL2
Loading...
Searching...
No Matches
equal_sorts.h
Go to the documentation of this file.
1// Author(s): Wieger Wesselink
2// Copyright: see the accompanying file COPYING or copy at
3// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
4//
5// Distributed under the Boost Software License, Version 1.0.
6// (See accompanying file LICENSE_1_0.txt or copy at
7// http://www.boost.org/LICENSE_1_0.txt)
8//
9/// \file mcrl2/data/detail/equal_sorts.h
10/// \brief add your file description here.
11
12#ifndef MCRL2_DATA_DETAIL_EQUAL_SORTS_H
13#define MCRL2_DATA_DETAIL_EQUAL_SORTS_H
14
15#include "mcrl2/data/data_specification.h"
16
17namespace mcrl2::data::detail
18{
19
20/// \brief Checks if the sorts of the variables/expressions in both lists are equal.
21/// \param v A sequence of data variables
22/// \param w A sequence of data expressions
23/// \return True if the sorts match pairwise
24inline
25bool equal_sorts(const data::variable_list& v, const data::data_expression_list& w, const data::data_specification& data_spec)
26{
27 if (v.size() != w.size())
28 {
29 return false;
30 }
31 data::variable_list::iterator i = v.begin();
32 data::data_expression_list::iterator j = w.begin();
33 for (; i != v.end(); ++i, ++j)
34 {
35 if (!data_spec.equal_sorts(i->sort(), j->sort()))
36 {
37 return false;
38 }
39 }
40 return true;
41}
42
43} // namespace mcrl2::data::detail
44
45#endif // MCRL2_DATA_DETAIL_EQUAL_SORTS_H
A unordered_map class in which aterms can be stored.
bool is_well_typed() const
Returns true if.
\brief A data variable
Definition variable.h:25
\brief The and operator for pbes expressions
const pbes_expression & left() const
const pbes_expression & right() const
\brief The existential quantification operator for pbes expressions
const data::variable_list & variables() const
const pbes_expression & body() const
\brief The universal quantification operator for pbes expressions
const pbes_expression & body() const
const data::variable_list & variables() const
\brief The implication operator for pbes expressions
const pbes_expression & left() const
const pbes_expression & right() const
\brief The not operator for pbes expressions
const pbes_expression & operand() const
\brief The or operator for pbes expressions
const pbes_expression & left() const
const pbes_expression & right() const
const pbes_expression & formula() const
Returns the predicate formula on the right hand side of the equation.
bool is_solved() const
Returns true if the predicate formula on the right hand side contains no predicate variables.
Definition pbes.cpp:102
const propositional_variable & variable() const
Returns the pbes variable of the equation.
parameterized boolean equation system
Definition pbes.h:54
std::set< data::variable > & global_variables()
Returns the declared free variables of the pbes.
Definition pbes.h:181
bool is_closed() const
True if the pbes is closed.
Definition pbes.h:239
data::data_specification m_data
The data specification.
Definition pbes.h:60
pbes(const data::data_specification &data, const std::vector< pbes_equation > &equations, propositional_variable_instantiation initial_state)
Constructor.
Definition pbes.h:112
std::set< data::variable > m_global_variables
The set of global variables.
Definition pbes.h:66
std::set< propositional_variable > compute_declared_variables() const
Returns the predicate variables appearing in the left hand side of an equation.
Definition pbes.h:73
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.
Definition pbes.h:130
const propositional_variable_instantiation & initial_state() const
Returns the initial state.
Definition pbes.h:188
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...
Definition pbes.h:203
std::set< propositional_variable > occurring_variables() const
Returns the set of occurring propositional variable declarations of the pbes, i.e....
Definition pbes.h:221
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...
Definition pbes.cpp:107
const std::set< data::variable > & global_variables() const
Returns the declared free variables of the pbes.
Definition pbes.h:174
std::vector< pbes_equation > & equations()
Returns the equations.
Definition pbes.h:167
propositional_variable_instantiation & initial_state()
Returns the initial state.
Definition pbes.h:195
propositional_variable_instantiation m_initial_state
The initial state.
Definition pbes.h:69
pbes()=default
Constructor.
std::vector< pbes_equation > m_equations
The sequence of pbes equations.
Definition pbes.h:63
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...
Definition pbes.h:92
const std::vector< pbes_equation > & equations() const
Returns the equations.
Definition pbes.h:160
bool is_well_typed() const
Checks if the PBES is well typed.
Definition pbes.h:261
\brief A propositional variable instantiation
const data::data_expression_list & parameters() const
propositional_variable_instantiation(const propositional_variable_instantiation &) noexcept=default
Move semantics.
\brief A propositional variable declaration
const data::variable_list & parameters() const
const core::identifier_string & name() const
D_ParserTables parser_tables_mcrl2
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.
Definition equal_sorts.h:25
bool is_data_expression(const atermpp::aterm &x)
Test for a data_expression expression.
bool is_untyped_data_parameter(const atermpp::aterm &x)
void instantiate_global_variables(pbes &p)
Attempts to eliminate the free variables of a PBES, by substituting a constant value for them....
Definition pbes.cpp:64
bool is_bes(const pbes &x)
Returns true if a PBES is in BES form.
Definition pbes.cpp:69
untyped_pbes parse_pbes_new(const std::string &text)
Definition pbes.cpp:132
void complete_pbes(pbes &x)
Definition pbes.cpp:143
bool has_propositional_variables(const pbes_expression &x)
propositional_variable parse_propositional_variable(const std::string &text)
Definition pbes.cpp:150
pbes_expression parse_pbes_expression(const std::string &text)
Definition pbes.cpp:159
bool is_well_typed(const pbes_equation &eqn)
Checks if the equation is well typed.
pbes_expression parse_pbes_expression_new(const std::string &text)
Definition pbes.cpp:121
The main namespace for the PBES library.
std::set< data::variable > find_free_variables(const pbes_system::pbes_equation &x)
Definition pbes.cpp:55
std::string pp(const pbes_system::propositional_variable_list &x, bool arg0)
Definition pbes.cpp:30
std::string pp(const pbes_system::or_ &x, bool arg0)
Definition pbes.cpp:40
std::set< data::variable > find_free_variables(const pbes_system::pbes &x)
Definition pbes.cpp:53
void normalize_sorts(pbes_system::pbes_equation_vector &x, const data::sort_specification &sortspec)
Definition pbes.cpp:46
std::string pp(const pbes_system::imp &x, bool arg0)
Definition pbes.cpp:38
std::string pp(const pbes_system::propositional_variable_instantiation_list &x, bool arg0)
Definition pbes.cpp:32
pbes_system::pbes_expression normalize_sorts(const pbes_system::pbes_expression &x, const data::sort_specification &sortspec)
Definition pbes.cpp:48
std::set< data::sort_expression > find_sort_expressions(const pbes_system::pbes &x)
Definition pbes.cpp:51
std::string pp(const pbes_system::pbes_equation_vector &x, bool arg0)
Definition pbes.cpp:27
std::string pp(const pbes_system::pbes_expression_list &x, bool arg0)
Definition pbes.cpp:28
bool is_not(const atermpp::aterm &x)
std::set< pbes_system::propositional_variable_instantiation > find_propositional_variable_instantiations(const pbes_system::pbes_expression &x)
Definition pbes.cpp:57
bool is_exists(const atermpp::aterm &x)
void normalize_sorts(pbes_system::pbes &x, const data::sort_specification &)
Definition pbes.cpp:47
std::ostream & operator<<(std::ostream &out, const pbes &x)
Definition pbes.h:298
bool is_or(const atermpp::aterm &x)
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)
Definition pbes.cpp:90
std::set< data::function_symbol > find_function_symbols(const pbes_system::pbes &x)
Definition pbes.cpp:56
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.
Definition typecheck.h:272
std::string pp(const pbes_system::propositional_variable &x, bool arg0)
Definition pbes.cpp:44
std::string pp(const pbes_system::exists &x, bool arg0)
Definition pbes.cpp:35
std::string pp(const pbes_system::pbes_expression &x, bool arg0)
Definition pbes.cpp:43
atermpp::aterm pbes_to_aterm(const pbes &p)
Conversion to atermappl.
Definition io.cpp:315
bool operator==(const pbes &p1, const pbes &p2)
Equality operator on PBESs.
Definition pbes.h:319
bool is_well_typed(const pbes_equation &eqn)
Definition pbes.cpp:76
std::set< data::variable > find_free_variables(const pbes_system::pbes_expression &x)
Definition pbes.cpp:54
pbes_system::pbes_expression translate_user_notation(const pbes_system::pbes_expression &x)
Definition pbes.cpp:50
bool search_variable(const pbes_system::pbes_expression &x, const data::variable &v)
Definition pbes.cpp:59
std::set< data::variable > find_all_variables(const pbes_system::pbes &x)
Definition pbes.cpp:52
std::string pp(const pbes_system::not_ &x, bool arg0)
Definition pbes.cpp:39
void complete_data_specification(pbes &)
Adds all sorts that appear in the PBES p to the data specification of p.
Definition pbes.h:308
std::string pp(const pbes_system::pbes_equation &x, bool arg0)
Definition pbes.cpp:42
std::set< core::identifier_string > find_identifiers(const pbes_system::pbes_expression &x)
Definition pbes.cpp:58
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)
Definition pbes.cpp:81
std::string pp(const pbes_system::propositional_variable_instantiation &x, bool arg0)
Definition pbes.cpp:45
bool is_and(const atermpp::aterm &x)
void translate_user_notation(pbes_system::pbes &x)
Definition pbes.cpp:49
std::string pp(const pbes_system::pbes &x, bool arg0)
Definition pbes.cpp:41
bool is_imp(const atermpp::aterm &x)
std::string pp(const pbes_system::and_ &x, bool arg0)
Definition pbes.cpp:34
std::string pp(const pbes_system::fixpoint_symbol &x, bool arg0)
Definition pbes.cpp:36
std::string pp(const pbes_system::forall &x, bool arg0)
Definition pbes.cpp:37
expression traverser that visits all sub expressions
Definition traverser.h:29
void apply(const pbes_system::imp &x)
Definition traverser.h:236
void apply(const pbes_system::not_ &x)
Definition traverser.h:213
void apply(const pbes_system::propositional_variable_instantiation &x)
Definition traverser.h:206
void apply(const pbes_system::exists &x)
Definition traverser.h:251
void apply(const pbes_system::pbes &x)
Definition traverser.h:198
void apply(const pbes_system::pbes_equation &x)
Definition traverser.h:191
void apply(const pbes_system::pbes_expression &x)
Definition traverser.h:258
void apply(const pbes_system::or_ &x)
Definition traverser.h:228
void apply(const pbes_system::and_ &x)
Definition traverser.h:220
void apply(const pbes_system::forall &x)
Definition traverser.h:244
void apply(const pbes_system::pbes_expression &x)
Definition traverser.h:662
void apply(const pbes_system::exists &x)
Definition traverser.h:654
void apply(const pbes_system::propositional_variable &x)
Definition traverser.h:582
void apply(const pbes_system::forall &x)
Definition traverser.h:646
void apply(const pbes_system::pbes_equation &x)
Definition traverser.h:590
void apply(const pbes_system::propositional_variable_instantiation &x)
Definition traverser.h:607
void apply(const pbes_system::propositional_variable_instantiation &x)
Definition traverser.h:332
void apply(const pbes_system::and_ &x)
Definition traverser.h:346
void apply(const pbes_system::forall &x)
Definition traverser.h:370
void apply(const pbes_system::pbes_equation &x)
Definition traverser.h:318
void apply(const pbes_system::or_ &x)
Definition traverser.h:354
void apply(const pbes_system::imp &x)
Definition traverser.h:362
void apply(const pbes_system::pbes_expression &x)
Definition traverser.h:384
void apply(const pbes_system::exists &x)
Definition traverser.h:377
void apply(const pbes_system::not_ &x)
Definition traverser.h:339
void apply(const pbes_system::pbes &x)
Definition traverser.h:325
void apply(const pbes_system::exists &x)
Definition traverser.h:123
void apply(const pbes_system::or_ &x)
Definition traverser.h:99
void apply(const pbes_system::propositional_variable_instantiation &x)
Definition traverser.h:77
void apply(const pbes_system::propositional_variable &x)
Definition traverser.h:53
void apply(const pbes_system::imp &x)
Definition traverser.h:107
void apply(const pbes_system::and_ &x)
Definition traverser.h:91
void apply(const pbes_system::pbes &x)
Definition traverser.h:68
void apply(const pbes_system::forall &x)
Definition traverser.h:115
void apply(const pbes_system::pbes_equation &x)
Definition traverser.h:60
void apply(const pbes_system::pbes_expression &x)
Definition traverser.h:131
void apply(const pbes_system::not_ &x)
Definition traverser.h:84
void apply(const pbes_system::pbes &x)
Definition traverser.h:459
void apply(const pbes_system::propositional_variable &x)
Definition traverser.h:444
void apply(const pbes_system::or_ &x)
Definition traverser.h:490
void apply(const pbes_system::propositional_variable_instantiation &x)
Definition traverser.h:468
void apply(const pbes_system::not_ &x)
Definition traverser.h:475
void apply(const pbes_system::exists &x)
Definition traverser.h:514
void apply(const pbes_system::and_ &x)
Definition traverser.h:482
void apply(const pbes_system::imp &x)
Definition traverser.h:498
void apply(const pbes_system::pbes_expression &x)
Definition traverser.h:522
void apply(const pbes_system::pbes_equation &x)
Definition traverser.h:451
void apply(const pbes_system::forall &x)
Definition traverser.h:506
pbes_system::propositional_variable parse_PropVarDecl(const core::parse_node &node) const
Definition parse_impl.h:47
pbes_actions(const core::parser &parser_)
Definition parse_impl.h:25
untyped_pbes parse_PbesSpec(const core::parse_node &node) const
Definition parse_impl.h:84
pbes_system::pbes_expression parse_PbesExpr(const core::parse_node &node) const
Definition parse_impl.h:29
Traversal class for pbes_expressions. Used as a base class for pbes_expression_traverser.
Definition traverser.h:23
void apply(const data::data_expression &x)
Definition traverser.h:29
void apply(const data::untyped_data_parameter &x)
Definition traverser.h:36