mCRL2
Loading...
Searching...
No Matches
type_checker.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//
11
12#ifndef MCRL2_DATA_TYPE_CHECKER_H
13#define MCRL2_DATA_TYPE_CHECKER_H
14
16
17namespace mcrl2 {
18
19namespace data {
20
21namespace detail {
22
23inline
25{
26 char c = Number.function().name()[0];
27 return isdigit(c) && c > '0';
28}
29
30inline
32{
33 return isdigit(Number.function().name()[0]) != 0;
34}
35
36inline
38{
39 return function_sort({ domain }, codomain);
40}
41
42template <typename Function, typename T>
44{
46 for (const T& t: x)
47 {
48 result.push_front(f(t));
49 }
50 return atermpp::reverse(result);
51}
52
53inline
55{
56 if (is_container_sort(x))
57 {
58 const container_sort& cs = atermpp::down_cast<const container_sort>(x);
60 }
61 else if (is_function_sort(x))
62 {
63 const function_sort& fs = atermpp::down_cast<function_sort>(x);
64 auto new_arguments = detail::transform_aterm_list([&](const sort_expression& s) { return unwind_sort_expression(s, aliases); }, fs.domain());
65 return function_sort(new_arguments, unwind_sort_expression(fs.codomain(), aliases));
66 }
67 else if (is_basic_sort(x))
68 {
69 const basic_sort& bs = atermpp::down_cast<const basic_sort>(x);
70 for(const alias& a: aliases)
71 {
72 if (bs == a.name())
73 {
74 return unwind_sort_expression(a.reference(), aliases);
75 }
76 return x;
77 }
78 }
79 return x;
80}
81
82inline
84{
86 {
87 return false;
88 }
89 return sort_bool::is_bool(x) ||
94}
95
96} // namespace detail
97
99{
100 protected:
101 std::map<core::identifier_string, sort_expression_list> m_system_constants;
102 std::map<core::identifier_string, function_sort_list> m_system_functions;
103 std::map<core::identifier_string, sort_expression> m_user_constants;
104 std::map<core::identifier_string, function_sort_list> m_user_functions;
105
107 {
108 // append the Type to the entry of the Name of the OpId in system constants table
109 auto i = m_system_constants.find(f.name());
111 if (i != m_system_constants.end())
112 {
113 sorts = i->second;
114 }
115 sorts = push_back(sorts, f.sort());
116 m_system_constants[f.name()] = sorts;
117 }
118
120 {
121 m_system_functions[f.name()] = m_system_functions[f.name()] + function_sort_list({ atermpp::down_cast<function_sort>(f.sort()) });
122 }
123
125 {
126 return detail::unwind_sort_expression(x, get_sort_specification().user_defined_aliases());
127 }
128
129 bool equal_types(const sort_expression& x1, const sort_expression& x2) const
130 {
131 if (x1 == x2)
132 {
133 return true;
134 }
136 }
137
138 bool find_sort(const sort_expression& x, const function_sort_list& sorts) const
139 {
140 return std::any_of(sorts.begin(), sorts.end(), [&](const function_sort& s) { return equal_types(x, s); });
141 }
142
144 {
145 //Creation of operation identifiers for system defined operations.
146 //Bool
160 //Numbers
162#ifndef MCRL2_ENABLE_MACHINENUMBERS
164#endif
178 //Square root for the natural numbers.
180 //more about numbers
191 //more
196 //more
197 // add_system_function(sort_real::abs(sort_pos::pos()));
198 // add_system_function(sort_real::abs(sort_nat::nat()));
201 //more
220 //more
229 //more
230 // add_system_function(sort_int::div(sort_pos::pos(), sort_pos::pos()));
233 // add_system_function(sort_int::mod(sort_pos::pos(), sort_pos::pos()));
247 //Lists
259
260 //Sets
261
271 add_system_function(sort_set::false_function(data::untyped_sort())); // Needed as it is used within the typechecker.
272 add_system_function(sort_set::constructor(data::untyped_sort())); // Needed as it is used within the typechecker.
273 //**** add_system_function(sort_bag::set2bag(data::untyped_sort()));
274 // add_system_constant(sort_set::empty(data::untyped_sort()));
275 // add_system_function(sort_set::in(data::untyped_sort()));
276 // add_system_function(sort_set::union_(data::untyped_sort()));
277 // add_system_function(sort_set::difference(data::untyped_sort()));
278 // add_system_function(sort_set::intersection(data::untyped_sort()));
280
281 //FSets
283 // add_system_function(sort_fset::in(data::untyped_sort()));
284 // add_system_function(sort_fset::union_(data::untyped_sort()));
285 // add_system_function(sort_fset::intersection(data::untyped_sort()));
286 // add_system_function(sort_fset::difference(data::untyped_sort()));
288 add_system_function(sort_fset::insert(data::untyped_sort())); // Needed as it is used within the typechecker.
289
290 //Bags
302 // add_system_constant(sort_bag::empty(data::untyped_sort()));
303 // add_system_function(sort_bag::in(data::untyped_sort()));
304 //**** add_system_function(sort_bag::count(data::untyped_sort()));
305 // add_system_function(sort_bag::count(data::untyped_sort(), data::untyped_sort(), sort_fset::fset(data::untyped_sort())));
306 //add_system_function(sort_bag::join(data::untyped_sort()));
307 // add_system_function(sort_bag::difference(data::untyped_sort()));
308 // add_system_function(sort_bag::intersection(data::untyped_sort()));
309 add_system_function(sort_bag::zero_function(data::untyped_sort())); // Needed as it is used within the typechecker.
310 add_system_function(sort_bag::constructor(data::untyped_sort())); // Needed as it is used within the typechecker.
311
312 //FBags
314 // add_system_function(sort_fbag::count(data::untyped_sort()));
315 // add_system_function(sort_fbag::in(data::untyped_sort()));
316 // add_system_function(sort_fbag::union_(data::untyped_sort()));
317 // add_system_function(sort_fbag::intersection(data::untyped_sort()));
318 // add_system_function(sort_fbag::difference(data::untyped_sort()));
320 add_system_function(sort_fbag::cinsert(data::untyped_sort())); // Needed as it is used within the typechecker.
321
322 // function update
324 }
325
326 void add_constant(const data::function_symbol& f, const std::string& msg)
327 {
328 if (m_user_constants.count(f.name()) > 0)
329 {
330 throw mcrl2::runtime_error("double declaration of " + msg + " " + core::pp(f.name()));
331 }
332 if (m_system_constants.count(f.name()) > 0 || m_system_functions.count(f.name()) > 0)
333 {
334 throw mcrl2::runtime_error("attempt to declare a constant with the name that is a built-in identifier (" + core::pp(f.name()) + ")");
335 }
336 m_user_constants[f.name()] = f.sort();
337 }
338
339 void add_function(const data::function_symbol& f, const std::string& msg, bool allow_double_decls = false)
340 {
341 if (m_system_constants.count(f.name()) > 0)
342 {
343 throw mcrl2::runtime_error("attempt to redeclare the system constant with a " + msg + " " + data::pp(f));
344 }
345
346 if (m_system_functions.count(f.name()) > 0)
347 {
348 throw mcrl2::runtime_error("attempt to redeclare a system function with a " + msg + " " + data::pp(f));
349 }
350
351 auto j = m_user_functions.find(f.name());
352 const function_sort& fsort = atermpp::down_cast<function_sort>(f.sort());
353
354 // the table m_user_functions contains a list of types for each
355 // function name. We need to check if there is already such a type
356 // in the list. If so -- error, otherwise -- add
357 if (j != m_user_functions.end())
358 {
359 auto& sorts = j->second;
360 if (find_sort(fsort, sorts))
361 {
362 if (!allow_double_decls)
363 {
364 throw mcrl2::runtime_error("double declaration of " + msg + " " + core::pp(f.name()));
365 }
366 }
367 }
369 }
370
371 // Adds constants and functions corresponding to the sort x
373 {
374 if (is_basic_sort(x))
375 {
376 // This should be checked elsewhere
377 // check_basic_sort_is_declared(atermpp::down_cast<basic_sort>(x).name());
378 }
379 else if (is_container_sort(x))
380 {
381 read_sort(atermpp::down_cast<container_sort>(x).element_sort());
382 }
383 else if (is_function_sort(x))
384 {
385 const function_sort& fs = atermpp::down_cast<function_sort>(x);
386 read_sort(fs.codomain());
387 for (const sort_expression& sort: fs.domain())
388 {
389 read_sort(sort);
390 }
391 }
392 else if (is_structured_sort(x))
393 {
394 const structured_sort& struct_sort = atermpp::down_cast<structured_sort>(x);
395 for (const structured_sort_constructor& constructor: struct_sort.constructors())
396 {
397 // recognizer -- if present -- a function from SortExpr to Bool
398 core::identifier_string name = constructor.recogniser();
399 if (name != core::empty_identifier_string())
400 {
402 }
403
404 // constructor type and projections
405 structured_sort_constructor_argument_list arguments = constructor.arguments();
406 name = constructor.name();
407 if (arguments.empty())
408 {
409 add_constant(data::function_symbol(name, x), "constructor constant");
410 continue;
411 }
412
414 for (const structured_sort_constructor_argument& arg: arguments)
415 {
416 read_sort(arg.sort());
417 if (arg.name() != core::empty_identifier_string())
418 {
419 add_function(function_symbol(arg.name(), function_sort({ x }, arg.sort())), "projection", true);
420 }
421 sorts.push_front(arg.sort());
422 }
423 add_function(data::function_symbol(name, function_sort(atermpp::reverse(sorts), x)), "constructor");
424 }
425 }
426 // other sorts can be ignored
427 }
428
429 void read_constructors_and_mappings(const function_symbol_vector& constructors, const function_symbol_vector& mappings, const function_symbol_vector& normalized_constructors)
430 {
431 mCRL2log(log::debug) << "Start Read-in Func" << std::endl;
432
433 std::size_t constr_number=constructors.size();
434 function_symbol_vector functions_and_constructors=constructors;
435 functions_and_constructors.insert(functions_and_constructors.end(),mappings.begin(),mappings.end());
436 for (const function_symbol& f: functions_and_constructors)
437 {
438 sort_expression fsort = f.sort();
439
440 // This should be checked elsewhere
441 // check_sort_is_declared(fsort);
442
443 //if fsort is a defined function sort, unwind it
444 if (is_basic_sort(fsort))
445 {
447 if (is_function_sort(s))
448 {
449 fsort = s;
450 }
451 }
452
453 if (is_function_sort(fsort))
454 {
455 add_function(data::function_symbol(f.name(), fsort), "function");
456 }
457 else
458 {
459 try
460 {
461 add_constant(data::function_symbol(f.name(), fsort), "constant");
462 }
463 catch (mcrl2::runtime_error& e)
464 {
465 throw mcrl2::runtime_error(std::string(e.what()) + "\ncould not add constant");
466 }
467 }
468
469 if (constr_number)
470 {
471 constr_number--;
472
473 //Here checks for the constructors
474 sort_expression s = fsort;
475 if (is_function_sort(s))
476 {
477 s = atermpp::down_cast<function_sort>(s).codomain();
478 }
480 if (!is_basic_sort(s) ||
486 )
487 {
488 throw mcrl2::runtime_error("Could not add constructor " + core::pp(f.name()) + " of sort " + data::pp(fsort) + ". Constructors of built-in sorts are not allowed.");
489 }
490 }
491
492 mCRL2log(log::debug) << "Read-in Func " << f.name() << ", Types " << fsort << "" << std::endl;
493 }
494
495 // Check that the constructors are defined such that they cannot generate an empty sort.
496 // E.g. in the specification sort D; cons f:D->D; the sort D must be necessarily empty, which is
497 // forbidden. The function below checks whether such malicious specifications occur.
498 check_for_empty_constructor_domains(normalized_constructors); // throws exception if not ok.
499 }
500
501 public:
503 : sort_type_checker(data_spec)
504 {
506 try
507 {
509 {
510 read_sort(a.reference());
511 }
513 }
514 catch (mcrl2::runtime_error& e)
515 {
516 throw mcrl2::runtime_error(std::string(e.what()) + "\ntype checking of data expression failed");
517 }
518 }
519
520 const std::map<core::identifier_string, sort_expression_list>& system_constants() const
521 {
522 return m_system_constants;
523 }
524
525 const std::map<core::identifier_string, function_sort_list>& system_functions() const
526 {
527 return m_system_functions;
528 }
529
530 const std::map<core::identifier_string, sort_expression>& user_constants() const
531 {
532 return m_user_constants;
533 }
534
535 const std::map<core::identifier_string, function_sort_list>& user_functions() const
536 {
537 return m_user_functions;
538 }
539};
540
541} // namespace data
542
543} // namespace mcrl2
544
545#endif // MCRL2_DATA_TYPE_CHECKER_H
546
Term containing a string.
const function_symbol & function() const
Returns the function symbol belonging to an aterm.
Definition aterm.h:144
const std::string & name() const
Return the name of the function_symbol.
A list of aterm objects.
Definition aterm_list.h:24
const_iterator end() const
Returns a const_iterator pointing to the end of the term_list.
Definition aterm_list.h:282
const_iterator begin() const
Returns a const_iterator pointing to the beginning of the term_list.
Definition aterm_list.h:275
bool empty() const
Returns true if the list's size is 0.
Definition aterm_list.h:268
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
const core::identifier_string & name() const
Definition basic_sort.h:57
\brief A container sort
const container_type & container_name() const
const sort_expression & element_sort() const
sort_expression sort() const
Returns the sort of the data expression.
Definition data.cpp:108
const function_symbol_vector & user_defined_constructors() const
Gets the constructors defined by the user, excluding those that are system defined.
const function_symbol_vector & user_defined_mappings() const
Gets all user defined mappings in this specification.
const function_symbol_vector & constructors() const
Gets all constructors including those that are system defined.
\brief A function sort
const sort_expression & codomain() const
const sort_expression_list & domain() const
\brief A function symbol
const core::identifier_string & name() const
const sort_expression & sort() const
\brief A sort expression
const alias_vector & user_defined_aliases() const
Gets the user defined aliases.
const sort_specification & get_sort_specification() const
void check_for_empty_constructor_domains(const function_symbol_vector &constructors)
\brief An argument of a constructor of a structured sort
\brief A constructor for a structured sort
const structured_sort_constructor_list & constructors() const
sort_expression unwind_sort_expression(const sort_expression &x) const
const std::map< core::identifier_string, sort_expression > & user_constants() const
void add_system_function(const data::function_symbol &f)
type_checker(const data_specification &data_spec)
void add_constant(const data::function_symbol &f, const std::string &msg)
const std::map< core::identifier_string, sort_expression_list > & system_constants() const
void read_constructors_and_mappings(const function_symbol_vector &constructors, const function_symbol_vector &mappings, const function_symbol_vector &normalized_constructors)
std::map< core::identifier_string, function_sort_list > m_system_functions
void read_sort(const sort_expression &x)
bool equal_types(const sort_expression &x1, const sort_expression &x2) const
void add_function(const data::function_symbol &f, const std::string &msg, bool allow_double_decls=false)
void add_system_constant(const data::function_symbol &f)
std::map< core::identifier_string, function_sort_list > m_user_functions
const std::map< core::identifier_string, function_sort_list > & user_functions() const
const std::map< core::identifier_string, function_sort_list > & system_functions() const
std::map< core::identifier_string, sort_expression > m_user_constants
bool find_sort(const sort_expression &x, const function_sort_list &sorts) const
std::map< core::identifier_string, sort_expression_list > m_system_constants
\brief Unknown sort expression
Standard exception class for reporting runtime errors.
Definition exception.h:27
add your file description here.
#define mCRL2log(LEVEL)
mCRL2log(LEVEL) provides the stream used to log.
Definition logger.h:395
term_list< Term > reverse(const term_list< Term > &l)
Returns the list with the elements in reversed order.
identifier_string empty_identifier_string()
Provides the empty identifier string.
std::string pp(const identifier_string &x)
Definition core.cpp:26
sort_expression unwind_sort_expression(const sort_expression &x, const alias_vector &aliases)
bool is_nat(const core::identifier_string &Number)
function_sort make_function_sort_(const sort_expression &domain, const sort_expression &codomain)
bool is_pos(const core::identifier_string &Number)
bool is_numeric_type(const sort_expression &x)
atermpp::term_list< T > transform_aterm_list(const Function &f, const atermpp::term_list< T > &x)
function_symbol difference(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:596
function_symbol bag2set(const sort_expression &s)
Constructor for function symbol Bag2Set.
Definition bag1.h:683
function_symbol intersection(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:511
function_symbol count(const sort_expression &, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:298
function_symbol set2bag(const sort_expression &s)
Constructor for function symbol Set2Bag.
Definition bag1.h:745
function_symbol constructor(const sort_expression &s)
Constructor for function symbol @bag.
Definition bag1.h:78
function_symbol in(const sort_expression &, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:362
function_symbol union_(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition bag1.h:426
container_sort bag(const sort_expression &s)
Constructor for sort expression Bag(S)
Definition bag1.h:44
function_symbol zero_function(const sort_expression &s)
Constructor for function symbol @zero_.
Definition bag1.h:807
bool is_bool(const sort_expression &e)
Recogniser for sort expression Bool.
Definition bool.h:54
const basic_sort & bool_()
Constructor for sort expression Bool.
Definition bool.h:44
const function_symbol & implies()
Constructor for function symbol =>.
Definition bool.h:363
const function_symbol & and_()
Constructor for function symbol &&.
Definition bool.h:235
const function_symbol & false_()
Constructor for function symbol false.
Definition bool.h:109
const function_symbol & or_()
Constructor for function symbol ||.
Definition bool.h:299
const function_symbol & not_()
Constructor for function symbol !.
Definition bool.h:173
const function_symbol & true_()
Constructor for function symbol true.
Definition bool.h:77
container_sort fbag(const sort_expression &s)
Constructor for sort expression FBag(S)
Definition fbag1.h:43
function_symbol count_all(const sort_expression &s)
Constructor for function symbol #.
Definition fbag1.h:725
function_symbol empty(const sort_expression &s)
Constructor for function symbol {:}.
Definition fbag1.h:77
function_symbol cinsert(const sort_expression &s)
Constructor for function symbol @fbag_cinsert.
Definition fbag1.h:277
function_symbol insert(const sort_expression &s)
Constructor for function symbol @fset_insert.
Definition fset1.h:107
function_symbol empty(const sort_expression &s)
Constructor for function symbol {}.
Definition fset1.h:75
function_symbol count(const sort_expression &s)
Constructor for function symbol #.
Definition fset1.h:593
container_sort fset(const sort_expression &s)
Constructor for sort expression FSet(S)
Definition fset1.h:41
const function_symbol & int2nat()
Constructor for function symbol Int2Nat.
Definition int1.h:298
bool is_int(const sort_expression &e)
Recogniser for sort expression Int.
Definition int1.h:57
const function_symbol & nat2int()
Constructor for function symbol Nat2Int.
Definition int1.h:236
const function_symbol & int2pos()
Constructor for function symbol Int2Pos.
Definition int1.h:422
const function_symbol & cint()
Constructor for function symbol @cInt.
Definition int1.h:80
function_symbol mod(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:1261
function_symbol div(const sort_expression &s0, const sort_expression &s1)
Definition int1.h:1184
const basic_sort & int_()
Constructor for sort expression Int.
Definition int1.h:47
function_symbol in(const sort_expression &s)
Constructor for function symbol in.
Definition list1.h:208
function_symbol rtail(const sort_expression &s)
Constructor for function symbol rtail.
Definition list1.h:712
function_symbol empty(const sort_expression &s)
Constructor for function symbol [].
Definition list1.h:76
function_symbol element_at(const sort_expression &s)
Constructor for function symbol ..
Definition list1.h:462
function_symbol head(const sort_expression &s)
Constructor for function symbol head.
Definition list1.h:526
function_symbol snoc(const sort_expression &s)
Constructor for function symbol <|.
Definition list1.h:334
function_symbol count(const sort_expression &s)
Constructor for function symbol #.
Definition list1.h:272
function_symbol rhead(const sort_expression &s)
Constructor for function symbol rhead.
Definition list1.h:650
function_symbol tail(const sort_expression &s)
Constructor for function symbol tail.
Definition list1.h:588
function_symbol cons_(const sort_expression &s)
Constructor for function symbol |>.
Definition list1.h:108
function_symbol concat(const sort_expression &s)
Constructor for function symbol ++.
Definition list1.h:398
const function_symbol & cnat()
Constructor for function symbol @cNat.
Definition nat1.h:140
const basic_sort & nat()
Constructor for sort expression Nat.
Definition nat1.h:46
bool is_nat(const sort_expression &e)
Recogniser for sort expression Nat.
Definition nat1.h:56
const function_symbol & sqrt()
Constructor for function symbol sqrt.
Definition nat1.h:1663
const function_symbol & nat2pos()
Constructor for function symbol Nat2Pos.
Definition nat1.h:362
const function_symbol & pos2nat()
Constructor for function symbol Pos2Nat.
Definition nat1.h:300
bool is_pos(const sort_expression &e)
Recogniser for sort expression Pos.
Definition pos1.h:55
const function_symbol & c1()
Constructor for function symbol @c1.
Definition pos1.h:78
const basic_sort & pos()
Constructor for sort expression Pos.
Definition pos1.h:45
function_symbol minimum(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:650
function_symbol plus(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1059
const function_symbol & creal()
Constructor for function symbol @cReal.
Definition real1.h:107
const function_symbol & pos2real()
Constructor for function symbol Pos2Real.
Definition real1.h:171
const function_symbol & round()
Constructor for function symbol round.
Definition real1.h:1597
function_symbol times(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1237
function_symbol divides(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1407
const function_symbol & real2nat()
Constructor for function symbol Real2Nat.
Definition real1.h:419
const function_symbol & ceil()
Constructor for function symbol ceil.
Definition real1.h:1535
function_symbol succ(const sort_expression &s0)
Definition real1.h:893
const function_symbol & real2int()
Constructor for function symbol Real2Int.
Definition real1.h:481
function_symbol pred(const sort_expression &s0)
Definition real1.h:976
function_symbol minus(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1152
const basic_sort & real_()
Constructor for sort expression Real.
Definition real1.h:48
const function_symbol & floor()
Constructor for function symbol floor.
Definition real1.h:1473
bool is_real(const sort_expression &e)
Recogniser for sort expression Real.
Definition real1.h:58
const function_symbol & nat2real()
Constructor for function symbol Nat2Real.
Definition real1.h:233
function_symbol abs(const sort_expression &s0)
Definition real1.h:735
function_symbol negate(const sort_expression &s0)
Definition real1.h:810
const function_symbol & int2real()
Constructor for function symbol Int2Real.
Definition real1.h:295
function_symbol exp(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:1322
const function_symbol & real2pos()
Constructor for function symbol Real2Pos.
Definition real1.h:357
function_symbol maximum(const sort_expression &s0, const sort_expression &s1)
Definition real1.h:541
function_symbol intersection(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition set1.h:499
container_sort set_(const sort_expression &s)
Constructor for sort expression Set(S)
Definition set1.h:42
function_symbol constructor(const sort_expression &s)
Constructor for function symbol @set.
Definition set1.h:76
function_symbol false_function(const sort_expression &s)
Constructor for function symbol @false_.
Definition set1.h:655
function_symbol in(const sort_expression &, const sort_expression &s0, const sort_expression &s1)
Definition set1.h:296
function_symbol union_(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition set1.h:422
function_symbol difference(const sort_expression &s, const sort_expression &s0, const sort_expression &s1)
Definition set1.h:576
function_symbol complement(const sort_expression &s)
Constructor for function symbol !.
Definition set1.h:362
atermpp::term_list< function_sort > function_sort_list
list of function sorts
bool is_structured_sort(const atermpp::aterm &x)
Returns true if the term t is a structured sort.
function_symbol less_equal(const sort_expression &s)
Constructor for function symbol <=.
Definition standard.h:277
function_symbol not_equal_to(const sort_expression &s)
Constructor for function symbol !=.
Definition standard.h:163
std::vector< alias > alias_vector
\brief vector of aliass
Definition alias.h:75
function_symbol less(const sort_expression &s)
Constructor for function symbol <.
Definition standard.h:240
bool is_untyped_sort(const atermpp::aterm &x)
Returns true if the term t is the unknown sort.
function_sort make_function_sort_(const sort_expression &dom1, const sort_expression &codomain)
Convenience constructor for function sort with domain size 1.
std::string pp(const abstraction &x)
Definition data.cpp:39
function_symbol greater_equal(const sort_expression &s)
Constructor for function symbol >=.
Definition standard.h:351
bool is_container_sort(const atermpp::aterm &x)
Returns true if the term t is a container sort.
bool is_basic_sort(const atermpp::aterm &x)
Returns true if the term t is a basic sort.
bool is_function_sort(const atermpp::aterm &x)
Returns true if the term t is a function sort.
function_symbol equal_to(const sort_expression &s)
Constructor for function symbol ==.
Definition standard.h:126
function_symbol function_update(const sort_expression &s, const sort_expression &t)
Constructor for function symbol @func_update.
std::vector< function_symbol > function_symbol_vector
\brief vector of function_symbols
function_symbol if_(const sort_expression &s)
Constructor for function symbol if.
Definition standard.h:200
function_symbol greater(const sort_expression &s)
Constructor for function symbol >
Definition standard.h:314
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72