mCRL2
Loading...
Searching...
No Matches
data_specification.h
Go to the documentation of this file.
1// Author(s): Jeroen Keiren, Jeroen van der Wulp, Jan Friso Groote
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//
11
12#ifndef MCRL2_DATA_DATA_SPECIFICATION_H
13#define MCRL2_DATA_DATA_SPECIFICATION_H
14
17
18namespace mcrl2
19{
20
21namespace data
22{
23
24// template function overloads
25data_expression normalize_sorts(const data_expression& x, const data::sort_specification& sortspec);
26variable_list normalize_sorts(const variable_list& x, const data::sort_specification& sortspec);
27data::data_equation normalize_sorts(const data::data_equation& x, const data::sort_specification& sortspec);
28data_equation_list normalize_sorts(const data_equation_list& x, const data::sort_specification& sortspec);
29void normalize_sorts(data_equation_vector& x, const data::sort_specification& sortspec);
30
31// prototype
32class data_specification;
33
34std::string pp(const data::data_specification& x);
35
39inline
41{
43}
44
46
48{
49 public:
50 typedef std::map<function_symbol,std::pair<std::function<void(data_expression&, const data_expression&)>, std::string> > implementation_map;
51
52 private:
53
56 struct target_sort_to_function_map
57 {
58 bool _outdated;
59 std::map<sort_expression, std::vector<function_symbol> > _mapping;
60
61 target_sort_to_function_map()
62 : _outdated(true)
63 {}
64
68 template <typename Container>
69 void group_functions_by_target_sort(std::map<sort_expression, std::vector<function_symbol> >& c, const Container& functions)
70 {
71 for (const function_symbol& f: functions)
72 {
73 const sort_expression s=f.sort();
74 const sort_expression& index_sort = s.target_sort();
75 if(c.find(index_sort) == c.end() || std::find(c[index_sort].begin(), c[index_sort].end(), f) == c[index_sort].end())
76 {
77 // Insert the constructors, such that those with the smallest number of elements occur first.
78 // As there are in general only few constructors, this linear insertion should not take too much time.
79 std::vector<function_symbol>& relevant_rhs = c[index_sort]; // .push_back(f);
80 const std::size_t f_arity=(is_function_sort(s)?atermpp::down_cast<function_sort>(s).size():0);
81 std::vector<function_symbol>::iterator i=
82 std::find_if(relevant_rhs.begin(),
83 relevant_rhs.end(),
84 [f_arity](const function_symbol& g)
85 { const std::size_t g_arity=(is_function_sort(g.sort())?
86 atermpp::down_cast<function_sort>(g.sort()).size():0);
87 return f_arity<g_arity;
88 });
89 relevant_rhs.insert(i,f);
90 }
91 }
92 }
93
94 template <typename FunctionContainer>
95 void reset(const FunctionContainer& c)
96 {
97 if(_outdated)
98 {
99 _mapping.clear();
100 group_functions_by_target_sort(_mapping, c);
101 _outdated = false;
102 }
103 }
104
105 void expire()
106 {
107 _outdated = true;
108 }
109
110 std::map<sort_expression, std::vector<function_symbol> >&mapping()
111 {
112 assert(!_outdated);
113 return _mapping;
114 }
115 };
116
118 void build_from_aterm(const atermpp::aterm& term);
120
121 protected:
122
125
128
131
135
137 mutable target_sort_to_function_map m_grouped_normalised_constructors;
138
142
144 mutable target_sort_to_function_map m_grouped_normalised_mappings;
145 //
151 mutable std::set<data_equation> m_normalised_equations;
152
161
162
163
165 {
167 }
168
169 protected:
170
178 inline
180 {
181 function_symbol g(normalize_sorts(f, *this));
182 if (std::find(m_normalised_constructors.begin(),m_normalised_constructors.end(),g)==m_normalised_constructors.end()) // not found
183 {
184 m_normalised_constructors.push_back(g);
185 }
186 }
187
196 {
197 function_symbol g(normalize_sorts(f, *this));
198 if (std::find(m_normalised_mappings.begin(),m_normalised_mappings.end(),g)==m_normalised_mappings.end()) // not found
199 {
200 m_normalised_mappings.push_back(g);
201 }
202 }
203
212 {
214 }
215
216 template < class Iterator >
217 void add_normalised_constructors(Iterator begin, Iterator end) const
218 {
219 for(Iterator i=begin; i!=end; ++i)
220 {
222 }
223 }
224
225 template < class Iterator >
226 void add_normalised_mappings(Iterator begin, Iterator end) const
227 {
228 for(Iterator i=begin; i!=end; ++i)
229 {
231 }
232 }
233
234 template < class Iterator >
235 void add_normalised_equations(Iterator begin, Iterator end) const
236 {
237 for(Iterator i=begin; i!=end; ++i)
238 {
240 }
241 }
242
244 {
245 typedef std::pair < function_symbol, std::pair<std::function<void(data_expression&, const data_expression&)>, std::string> > map_result_type;
246 for(const map_result_type f: c)
247 {
248 const function_symbol g(normalize_sorts(f.first,*this));
249 m_cpp_implemented_functions[g]=f.second;
250 }
251 }
252
261
263 const structured_sort& sort,
264 std::set < function_symbol >& constructors,
265 std::set < function_symbol >& mappings,
266 std::set < data_equation >& equations,
267 const bool skip_equations) const
268 {
269 const structured_sort& s_sort(sort);
271 constructors.insert(f.begin(),f.end());
272 f = s_sort.projection_functions(sort);
273 mappings.insert(f.begin(),f.end());
274 f = s_sort.recogniser_functions(sort);
275 mappings.insert(f.begin(),f.end());
276 f = s_sort.comparison_functions(sort);
277 mappings.insert(f.begin(),f.end());
278
279 if (!skip_equations)
280 {
282 equations.insert(e.begin(),e.end());
283 e = s_sort.projection_equations(sort);
284 equations.insert(e.begin(),e.end());
285 e = s_sort.recogniser_equations(sort);
286 equations.insert(e.begin(),e.end());
287 e = s_sort.comparison_equations(sort);
288 equations.insert(e.begin(),e.end());
289 }
290 }
291
293 const sort_expression& sort,
294 std::set < function_symbol >& mappings,
295 std::set < data_equation >& equations,
296 const bool skip_equations) const
297 {
299 mappings.insert(f.begin(), f.end());
300
301 if (!skip_equations)
302 {
304 equations.insert(eq.begin(), eq.end());
305 }
306 }
307
308 public:
309
313 {
314 }
315
319 {
320 build_from_aterm(t);
321 }
322
325 const alias_vector& aliases,
329
334 inline
336 {
339 }
340
344 inline
346 {
348 }
349
355 inline
356 const function_symbol_vector& constructors(const sort_expression& s, const bool do_not_normalize=false) const
357 {
360 if (do_not_normalize)
361 {
362 assert(normalize_sorts(s,*this)==s);
363 return m_grouped_normalised_constructors.mapping()[s];
364 }
365 return m_grouped_normalised_constructors.mapping()[normalize_sorts(s,*this)];
366 }
367
373 inline
375 {
378 }
379
385 inline
387 {
389 }
390
396 inline
398 {
401 return m_grouped_normalised_mappings.mapping()[normalize_sorts(s, *this)];
402 }
403
409 inline
410 const std::set<data_equation>& equations() const
411 {
414 }
415
421 inline
423 {
426 }
427
433 inline
435 {
437 }
438
439 // A variant that allows to replace the user defined equations.
440 inline
442 {
445 }
446
453 {
455 {
456 m_user_defined_constructors.push_back(f);
459 }
460 }
461
468 {
469 if (std::find(m_user_defined_mappings.begin(),m_user_defined_mappings.end(),f)==m_user_defined_mappings.end())
470 {
471 m_user_defined_mappings.push_back(f);
474 }
475 }
476
483 {
485 {
486 m_user_defined_equations.push_back(e);
489 }
490 }
491
496 {
498 {
500 }
502 }
503
504 private:
505
511 {
512 // Normalise the sorts of the constructors.
514 m_normalised_mappings.clear();
517
518 for (const sort_expression& sort: sorts())
519 {
521 }
522
523 for (const alias& a: user_defined_aliases())
524 {
526 }
527
528
529 // Normalise the constructors.
531 {
533 }
534
535 // Normalise the sorts of the mappings.
537 {
539 }
540
541 // Normalise the sorts of the expressions and variables in equations.
543 {
544 add_normalised_equation(data::translate_user_notation(eq)); // in due time (after 2025) this translate user notation can be removed.
545 }
546 }
547
551 {
553 {
558 }
559 }
560
562 // a given sort. If the boolean skip_equations is true, no equations are added.
564 const sort_expression& sort,
565 std::set < function_symbol >& constructors,
566 std::set < function_symbol >& mappings,
567 std::set < data_equation >& equations,
569 const bool skip_equations=false) const;
570
579 {
580 std::set < function_symbol > constructors;
581 std::set < function_symbol > mappings;
582 std::set < data_equation > equations;
583 implementation_map cpp_function_symbols;
585
586 // add normalised constructors, mappings and equations
590 add_normalised_cpp_implemented_functions(cpp_function_symbols);
591 }
592
593 public:
594
602 std::set < sort_expression >& sorts,
603 std::set < function_symbol >& constructors,
604 std::set <function_symbol >& mappings) const;
605
615 {
616 detail::remove(m_normalised_constructors, normalize_sorts(f,*this));
617 detail::remove(m_user_defined_constructors, f);
618 }
619
628 {
629 detail::remove(m_normalised_mappings, normalize_sorts(f,*this));
630 detail::remove(m_user_defined_mappings, f);
631 }
632
640 {
641 const data_equation e1=data::translate_user_notation(e); // in due time (after 2025) this translate user notation could possibly be removed.
642 // as it stands this function is not used.
643 detail::remove(m_normalised_equations, normalize_sorts(e1,*this));
644 detail::remove(m_user_defined_equations, e);
645 }
646
651 bool equal_sorts(sort_expression const& s1, sort_expression const& s2) const
652 {
654 const sort_expression normalised_sort1=normalize_sorts(s1,*this);
655 const sort_expression normalised_sort2=normalize_sorts(s2,*this);
656 return (normalised_sort1 == normalised_sort2);
657 }
658
664 bool is_certainly_finite(const sort_expression& s) const;
665
672 {
673 for(const data::sort_expression& s: l)
674 {
675 if (!is_certainly_finite(s))
676 {
677 return false;
678 }
679 }
680 return true;
681 }
682
688 {
690 const sort_expression normalised_sort=normalize_sorts(s,*this);
691 return !is_function_sort(normalised_sort) && !constructors(normalised_sort).empty();
692 }
693
700 bool is_well_typed() const;
701
702 bool operator==(const data_specification& other) const
703 {
706 return
711 }
712
713}; // class data_specification
714
715//--- start generated class data_specification ---//
716// prototype declaration
717std::string pp(const data_specification& x);
718
723inline
724std::ostream& operator<<(std::ostream& out, const data_specification& x)
725{
726 return out << data::pp(x);
727}
728//--- end generated class data_specification ---//
729
737{
738 for(const basic_sort& bsort: spec2.user_defined_sorts())
739 {
740 spec1.add_sort(bsort);
741 }
742
743 for(const sort_expression& sort: spec2.context_sorts())
744 {
745 spec1.add_context_sort(sort);
746 }
747
748 for(const alias& a: spec2.user_defined_aliases())
749 {
750 spec1.add_alias(a);
751 }
752
753 for(const function_symbol& f: spec2.user_defined_constructors())
754 {
755 spec1.add_constructor(f);
756 }
757
758 for(const function_symbol& f: spec2.user_defined_mappings())
759 {
760 spec1.add_mapping(f);
761 }
762
763 for(const data_equation& e: spec2.user_defined_equations())
764 {
765 spec1.add_equation(e);
766 }
767
768 return spec1;
769}
770
775
776inline
777function_symbol find_mapping(data_specification const& data, std::string const& s)
778{
779 const function_symbol_vector& r(data.mappings());
780 function_symbol_vector::const_iterator i = std::find_if(r.begin(), r.end(), detail::function_symbol_has_name(s));
781 return (i == r.end()) ? function_symbol() : *i;
782}
783
788
789inline
790function_symbol find_constructor(data_specification const& data, std::string const& s)
791{
792 const function_symbol_vector& r(data.constructors());
793 function_symbol_vector::const_iterator i = std::find_if(r.begin(), r.end(), detail::function_symbol_has_name(s));
794 return (i == r.end()) ? function_symbol() : *i;
795}
796
801
802inline
803sort_expression find_sort(data_specification const& data, std::string const& s)
804{
805 const std::set<sort_expression>& r(data.sorts());
806 const std::set<sort_expression>::const_iterator i = std::find_if(r.begin(), r.end(), detail::sort_has_name(s));
807 return (i == r.end()) ? sort_expression() : *i;
808}
809
816
817inline
819{
821 for (const data_equation& eq: specification.equations())
822 {
823 if (eq.lhs() == d || eq.rhs() == d)
824 {
825 result.push_back(eq);
826 }
827 else if (is_application(eq.lhs()))
828 {
829 if (atermpp::down_cast<application>(eq.lhs()).head() == d)
830 {
831 result.push_back(eq);
832 }
833 }
834 else if (is_application(eq.rhs()))
835 {
836 if (atermpp::down_cast<application>(eq.rhs()).head() == d)
837 {
838 result.push_back(eq);
839 }
840 }
841 }
842 return result;
843}
844
845
846
848// \detail This routine is experimental, and may benefit from further investigation. The rule of thumb that is
849// now used is that first variables of enumerated types are put in the variable list. These are sorts with
850// constructors that have no arguments, typically resulting from declarations such as sort Enum = struct e1 | e2 | e3.
851// The variables with the largest number of elements are put in front.
852// Subsequently, the other data types with a finite number of elements are listed, in arbitrary sequence. At the
853// end all other variables are put in an arbitrary sequence.
857
858
860{
861 // Put variables with enumerated types with the largest number of elements in front.
862 // Put variables of finite types as second.
863 // Finally put the other variables in the list.
864 std::map < std::size_t,variable_list> vars_of_enumerated_type;
865 variable_list vars_of_finite_type;
866 variable_list rest_vars;
867 for(const variable& v: l)
868 {
869 if (data_spec.is_certainly_finite(v.sort()))
870 {
871 bool is_enumerated_type=true;
872 for(const function_symbol& f: data_spec.constructors(v.sort()))
873 {
874 if (is_function_sort(f.sort()) && function_sort(f.sort()).domain().size()>0)
875 {
876 is_enumerated_type=false;
877 break;
878 }
879 }
880 if (is_enumerated_type)
881 {
882 vars_of_enumerated_type[data_spec.constructors(v.sort()).size()].push_front(v);
883 }
884 else
885 {
886 vars_of_finite_type.push_front(v);
887 }
888 }
889 else
890 {
891 // variable *i has no finite type
892 rest_vars.push_front(v);
893 }
894 }
895
896 // Accumulate the result in rest_vars
897 rest_vars=vars_of_finite_type + rest_vars;
898 for(std::map <std::size_t,variable_list>::const_reverse_iterator k=vars_of_enumerated_type.rbegin(); k!=vars_of_enumerated_type.rend(); ++k)
899 {
900 rest_vars = k->second + rest_vars;
901 }
902 return rest_vars;
903}
904
907inline
908std::set<core::identifier_string> function_and_mapping_identifiers(const data_specification& dataspec)
909{
910 std::set<core::identifier_string> result;
911 for (const function_symbol& f: dataspec.constructors())
912 {
913 result.insert(f.name());
914 }
915 for (const function_symbol& f: dataspec.mappings())
916 {
917 result.insert(f.name());
918 }
919 return result;
920}
921
922} // namespace data
923
924} // namespace mcrl2
925
926#endif // MCRL2_DATA_DATA_SPECIFICATION_H
const function_symbol & function() const
Returns the function symbol belonging to an aterm.
Definition aterm.h:144
A list of aterm objects.
Definition aterm_list.h:24
size_type size() const
Returns the size of the term_list.
Definition aterm_list.h:256
void push_front(const Term &el)
Inserts a new element at the beginning of the current list.
\brief A sort alias
Definition alias.h:26
\brief A basic sort
Definition basic_sort.h:26
\brief A data equation
void add_normalised_mappings(Iterator begin, Iterator end) const
bool is_constructor_sort(const sort_expression &s) const
Checks whether a sort is a constructor sort.
void add_normalised_cpp_implemented_functions(const implementation_map &c) const
const function_symbol_vector & user_defined_constructors() const
Gets the constructors defined by the user, excluding those that are system defined.
void add_data_types_for_sorts() const
Puts the constructors, functions and equations in normalised form in de data type.
void add_mapping(const function_symbol &f)
Adds a mapping to this specification.
void add_equation(const data_equation &e)
Adds an equation to this specification.
void remove_constructor(const function_symbol &f)
Removes constructor from specification.
void remove_equation(const data_equation &e)
Removes equation from specification.
void translate_user_notation()
Translate user notation within the equations of the data specification.
bool equal_sorts(sort_expression const &s1, sort_expression const &s2) const
Checks whether two sort expressions represent the same sort.
void add_standard_mappings_and_equations(const sort_expression &sort, std::set< function_symbol > &mappings, std::set< data_equation > &equations, const bool skip_equations) const
implementation_map m_cpp_implemented_functions
A map that for function symbols gives how it can be implemented.
data_equation_vector m_user_defined_equations
The equations of the specification.
const implementation_map & cpp_implemented_functions() const
Gets all equations in this specification including those that are system defined.
const function_symbol_vector & user_defined_mappings() const
Gets all user defined mappings in this specification.
const std::set< data_equation > & equations() const
Gets all equations in this specification including those that are system defined.
void find_associated_system_defined_data_types_for_a_sort(const sort_expression &sort, std::set< function_symbol > &constructors, std::set< function_symbol > &mappings, std::set< data_equation > &equations, implementation_map &cpp_implemented_functions, const bool skip_equations=false) const
Adds the system defined sorts to the sets with constructors, mappings, and equations for.
void add_normalised_constructor(const function_symbol &f) const
Adds a constructor to this specification, and marks it as system defined.
void add_normalised_constructors(Iterator begin, Iterator end) const
data_equation_vector & user_defined_equations()
void remove_mapping(const function_symbol &f)
Removes mapping from specification.
const function_symbol_vector & mappings(const sort_expression &s) const
Gets all mappings of a sort including those that are system defined.
target_sort_to_function_map m_grouped_normalised_constructors
Cache normalised constructors grouped by target sort.
void insert_mappings_constructors_for_structured_sort(const structured_sort &sort, std::set< function_symbol > &constructors, std::set< function_symbol > &mappings, std::set< data_equation > &equations, const bool skip_equations) const
Adds constructors, mappings and equations for a structured sort to this specification,...
function_symbol_vector m_normalised_mappings
Set containing system defined all mappings, including the system defined ones. The types in these map...
bool is_well_typed() const
Returns true if.
function_symbol_vector m_user_defined_constructors
A mapping of sort expressions to the constructors corresponding to that sort.
data_specification()
Default constructor. Generate a data specification that contains only booleans and positive numbers.
const data_equation_vector & user_defined_equations() const
Gets all user defined equations.
std::map< function_symbol, std::pair< std::function< void(data_expression &, const data_expression &)>, std::string > > implementation_map
std::set< data_equation > m_normalised_equations
Table containing all equations, including the system defined ones. The sorts in these equations are n...
void add_constructor(const function_symbol &f)
Adds a constructor to this specification.
void import_data_type_for_system_defined_sort(const sort_expression &sort) const
Adds the system defined sorts in a sequence. The second argument is used to check which sorts are add...
void add_normalised_mapping(const function_symbol &f) const
Adds a mapping to this specification, and marks it as system defined.
void get_system_defined_sorts_constructors_and_mappings(std::set< sort_expression > &sorts, std::set< function_symbol > &constructors, std::set< function_symbol > &mappings) const
This function provides a sample of all system defined sorts, constructors and mappings that contains ...
data_specification(const atermpp::aterm &t)
Constructor from an aterm.
void add_normalised_equation(const data_equation &e) const
Adds an equation to this specification, and marks it as system defined.
bool is_certainly_finite(const sort_expression &s) const
Checks whether a sort is certainly finite.
const function_symbol_vector & constructors() const
Gets all constructors including those that are system defined.
function_symbol_vector m_user_defined_mappings
The mappings of the specification.
const function_symbol_vector & constructors(const sort_expression &s, const bool do_not_normalize=false) const
Gets all constructors of a sort including those that are system defined.
function_symbol_vector m_normalised_constructors
Set containing all constructors, including the system defined ones. The types in these constructors a...
void add_normalised_equations(Iterator begin, Iterator end) const
bool operator==(const data_specification &other) const
void data_is_not_necessarily_normalised_anymore() const
target_sort_to_function_map m_grouped_normalised_mappings
Cache normalised mappings grouped by target sort.
bool is_certainly_finite(const sort_expression_list &l) const
Checks whether all sorts are certainly finite in a sort_expression_list.
const function_symbol_vector & mappings() const
Gets all mappings in this specification including those that are system defined.
\brief A function sort
const sort_expression_list & domain() const
\brief A function symbol
const sort_expression & sort() const
\brief A sort expression
const sort_expression & target_sort() const
Returns the target sort of this expression.
const std::set< sort_expression > & context_sorts() const
Return the user defined context sorts of the current specification.
bool operator==(const sort_specification &other) const
const std::set< sort_expression > & sorts() const
Gets the normalised sort declarations including those that are system defined. This is the set with a...
const basic_sort_vector & user_defined_sorts() const
Gets all sorts defined by a user (excluding the system defined sorts).
bool m_normalised_data_is_up_to_date
The variable below indicates whether a surrounding data specification is up to data with respect to s...
void add_alias(const alias &a)
Adds an alias (new name for a sort) to this specification.
void add_sort(const basic_sort &s)
Adds a sort to this specification.
void add_context_sort(const sort_expression &s)
Adds the sort s to the context sorts.
void import_system_defined_sorts(const CONTAINER &sorts)
const alias_vector & user_defined_aliases() const
Gets the user defined aliases.
void import_system_defined_sort(const sort_expression &sort)
Adds the system defined sorts in a sequence. The second argument is used to check which sorts are add...
function_symbol_vector recogniser_functions(const sort_expression &s) const
function_symbol_vector constructor_functions(const sort_expression &s) const
data_equation_vector constructor_equations(const sort_expression &s) const
data_equation_vector recogniser_equations(const sort_expression &s) const
function_symbol_vector comparison_functions(const sort_expression &s) const
data_equation_vector comparison_equations(const sort_expression &s) const
function_symbol_vector projection_functions(const sort_expression &s) const
data_equation_vector projection_equations(const sort_expression &s) const
\brief A data variable
Definition variable.h:28
Add your file description here.
function_symbol_vector standard_generate_functions_code(const sort_expression &s)
Give all standard system defined functions for sort s.
Definition standard.h:388
function_symbol find_mapping(data_specification const &data, std::string const &s)
Finds a mapping in a data specification.
data::data_equation translate_user_notation(const data::data_equation &x)
Definition data.cpp:90
std::vector< alias > alias_vector
\brief vector of aliass
Definition alias.h:75
std::vector< data_equation > data_equation_vector
\brief vector of data_equations
data_equation_vector standard_generate_equations_code(const sort_expression &s)
Give all standard system defined equations for sort s.
Definition standard.h:405
data_equation_vector find_equations(data_specification const &specification, const data_expression &d)
Gets all equations with a data expression as head on one of its sides.
std::string pp(const abstraction &x)
Definition data.cpp:39
function_symbol find_constructor(data_specification const &data, std::string const &s)
Finds a constructor in a data specification.
sort_expression find_sort(data_specification const &data, std::string const &s)
Finds a sort in a data specification.
atermpp::term_list< data_equation > data_equation_list
\brief list of data_equations
std::set< data::sort_expression > find_sort_expressions(const data::data_equation &x)
Definition data.cpp:91
atermpp::term_list< variable > variable_list
\brief list of variables
std::set< core::identifier_string > function_and_mapping_identifiers(const data_specification &dataspec)
Returns the names of functions and mappings that occur in a data specification.
bool is_function_sort(const atermpp::aterm &x)
Returns true if the term t is a function sort.
bool is_data_specification(const atermpp::aterm &x)
Test for a data specification expression.
data_expression normalize_sorts(const data_expression &x, const data::sort_specification &sortspec)
Definition data.cpp:86
std::map< function_symbol, std::pair< std::function< void(data_expression &, const data_expression &)>, std::string > > implementation_map
std::vector< basic_sort > basic_sort_vector
vector of basic sorts
Definition basic_sort.h:94
variable_list order_variables_to_optimise_enumeration(const variable_list &l, const data_specification &data_spec)
Order the variables in a variable list such that enumeration over these variables becomes more effici...
data_specification operator+(data_specification spec1, const data_specification &spec2)
Merges two data specifications into one.
bool is_application(const atermpp::aterm &x)
Returns true if the term t is an application.
std::vector< function_symbol > function_symbol_vector
\brief vector of function_symbols
std::ostream & operator<<(std::ostream &out, const abstraction &x)
Definition abstraction.h:94
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
This file describes the a sort_specification,.
static const atermpp::function_symbol DataSpec