#include "nusmv/core/utils/utils.h"#include "nusmv/core/utils/NodeList.h"#include "nusmv/core/node/printers/MasterPrinter.h"Go to the source code of this file.
Defines | |
| #define | SET_ELEMENT_T(self) ((Set_Element_t)self) |
| #define | SET_FOREACH(set, iter) |
| use this to iterate over a set | |
| #define | SET_T(self) ((Set_t)self) |
Typedefs | |
| typedef node_ptr | Set_Element_t |
| typedef ListIter_ptr | Set_Iterator_t |
| typedef struct Set_TAG * | Set_t |
Functions | |
| Set_t | Set_AddMember (Set_t set, Set_Element_t el) |
| Adds a new element to the set. | |
| Set_t | Set_AddMembersFromList (Set_t set, const NodeList_ptr list) |
| Adds all new elements found in list. | |
| boolean | Set_Contains (const Set_t set1, const Set_t set2) |
| Checks if set1 contains set2. | |
| Set_t | Set_Copy (const Set_t set) |
| Returns the independent copy of a set. | |
| Set_t | Set_Difference (Set_t set1, const Set_t set2) |
| Set Difference. | |
| boolean | Set_Equals (const Set_t set1, const Set_t set2) |
| Checks if set1 = set2. | |
| Set_t | Set_Freeze (Set_t set) |
| Freezes a set. | |
| Set_Iterator_t | Set_GetFirstIter (Set_t set1) |
| Provides an iterator to the "first" element of the set. | |
| Set_Element_t | Set_GetMember (const Set_t set, Set_Iterator_t iter) |
| Returns the element at given iterator. | |
| Set_Iterator_t | Set_GetNextIter (Set_Iterator_t iter) |
| Given an iterator of a set, returns the iterator pointing to the next chronological element in that set. | |
| Set_t | Set_GetRest (const Set_t set, Set_Iterator_t from) |
| Returns the rest of a set from a starting point. | |
| int | Set_GiveCardinality (const Set_t set) |
| Set Cardinality. | |
| Set_t | Set_Intersection (Set_t set1, const Set_t set2) |
| Set intersection. | |
| boolean | Set_Intersects (const Set_t set1, const Set_t set2) |
| Checks set1 and set2 has at least one common element. | |
| boolean | Set_IsEmpty (const Set_t set) |
| Set Emptiness. | |
| boolean | Set_IsEndIter (Set_Iterator_t iter) |
| Returns true if the set iterator is at the end of the iteration. | |
| boolean | Set_IsFrozen (Set_t const set) |
| Checks if a set is frozen. | |
| boolean | Set_IsMember (const Set_t set, Set_Element_t elem) |
| Set memberships. | |
| boolean | Set_IsSingleton (Set_t const set) |
| Checks if the set cointains only one element. | |
| Set_t | Set_Make (node_ptr list) |
| Given a list, builds a corresponding set. | |
| Set_t | Set_MakeEmpty (void) |
| Create a generic empty set. | |
| Set_t | Set_MakeFromUnion (NodeMgr_ptr nodemgr, node_ptr _union) |
| Given an union node, builds a corresponding set. | |
| Set_t | Set_MakeSingleton (Set_Element_t elem) |
| Creates a Singleton. | |
| void | set_pkg_init (void) |
| Initializes the set package. | |
| void | set_pkg_quit (void) |
| De-Initializes the set package. | |
| void | Set_PrintSet (MasterPrinter_ptr mprinter, FILE *, const Set_t set, void(*printer)(FILE *file, Set_Element_t el, void *arg), void *printer_arg) |
| Prints a set. | |
| void | Set_ReleaseSet (Set_t set) |
| Frees a set. | |
| void | Set_ReleaseSetOfSet (Set_t set) |
| Frees a set of sets. | |
| Set_t | Set_RemoveMember (Set_t set, Set_Element_t el) |
| Removes the given element from the set, if found. | |
| NodeList_ptr | Set_Set2List (const Set_t set) |
| Given a set, returns the corresponding list. | |
| node_ptr | Set_Set2Node (const Set_t set, NodeMgr_ptr nodemgr) |
| Returns a node list expression out of all set elements. | |
| node_ptr | Set_Set2Union (const Set_t set, NodeMgr_ptr nodemgr) |
| Returns a UNION expression out of all set elements. | |
| Set_t | Set_Union (Set_t set1, const Set_t set2) |
| Set Union. | |
| #define SET_ELEMENT_T | ( | self | ) | ((Set_Element_t)self) |
| #define SET_FOREACH | ( | set, | |||
| iter | ) |
for (iter=Set_GetFirstIter(set); !Set_IsEndIter(iter); \ iter=Set_GetNextIter(iter))
use this to iterate over a set
| typedef node_ptr Set_Element_t |
| typedef ListIter_ptr Set_Iterator_t |
| typedef struct Set_TAG* Set_t |
| Set_t Set_AddMember | ( | Set_t | set, | |
| Set_Element_t | el | |||
| ) |
Adds a new element to the set.
Add in order (at the end) a new element. Constant time if not frozen, linear time if frozen. See description about the structure Set_t for further information
If set is not frozen, set is changed internally
| Set_t Set_AddMembersFromList | ( | Set_t | set, | |
| const NodeList_ptr | list | |||
| ) |
Adds all new elements found in list.
Add in order (at the end) all new elements. Linear time in the size of list if not frozen, linear time in size of set + size of list if frozen. See description about the structure Set_t for further information
If set is not frozen, set is changed internally
Checks if set1 contains set2.
Returns true iff set2 is a subset of set1. Linear in the size of set2
Returns the independent copy of a set.
If the set was frozen, returned set is equal to the set given as input, and its reference counting is incremented. See description about the structure Set_t for further information
Checks if set1 = set2.
Returns true iff set1 contains the same elements of set2. Linear in the size of set2
Freezes a set.
Use when a set has to be memoized or stored in memory permanently. When frozen, a set content is frozen, meaning that no change can occur later on this set. If the set is tried to be changed later, a new copy will be created and changes will be applied to that copy. When a frozen set is copied, a reference counter is incremented and the same instance is returned in constant time. When a frozen set is destroyed, it is destroyed only when its ref counter reaches 0 (meaning it is the very last instance of that set). Set is also returned for a functional flavour. See description about the structure Set_t for further information
set is changed internally if not already frozen
| Set_Iterator_t Set_GetFirstIter | ( | Set_t | set1 | ) |
Provides an iterator to the "first" element of the set.
Returns an iterator to the "first" element of the set. Since sets are ordered, iterating through a set means to traverse the elements into the set in the same chronological ordering they have been previoulsy added to the set. If a set is changed, any previous stored iterator on that set might become invalid.
| Set_Element_t Set_GetMember | ( | const Set_t | set, | |
| Set_Iterator_t | iter | |||
| ) |
Returns the element at given iterator.
| Set_Iterator_t Set_GetNextIter | ( | Set_Iterator_t | iter | ) |
Given an iterator of a set, returns the iterator pointing to the next chronological element in that set.
Returns the next iterator. Since sets are ordered, iterating through a set means to traverse the elements into the set in the same chronological ordering they have been previoulsy added to the set. If a set is changed, any previous stored iterator on that set might become invalid.
| Set_t Set_GetRest | ( | const Set_t | set, | |
| Set_Iterator_t | from | |||
| ) |
Returns the rest of a set from a starting point.
Given a set and an iterator within that set, returns a new set containing all the elements that are found in to the input set from the iterator to then end of the set. Returned set must be disposed by the caller.
WARNING!! Deprecated method. This method is provided only for backward compatibility and should be no longer used in new code.
| int Set_GiveCardinality | ( | const Set_t | set | ) |
Set Cardinality.
Computes the cardinality of the given set. Constant time
Checks set1 and set2 has at least one common element.
Returns true iff set1 contains at least one element from set2. Linear in the size of set1
| boolean Set_IsEndIter | ( | Set_Iterator_t | iter | ) |
Returns true if the set iterator is at the end of the iteration.
| boolean Set_IsMember | ( | const Set_t | set, | |
| Set_Element_t | elem | |||
| ) |
Set memberships.
Checks if the given element is a member of the set. It returns True if it is a member, False otherwise. Constant time
Checks if the set cointains only one element.
Checks if the set cointains only one element
| Set_t Set_Make | ( | node_ptr | list | ) |
Given a list, builds a corresponding set.
Given a list, builds a corresponding set
| Set_t Set_MakeEmpty | ( | void | ) |
Create a generic empty set.
AutomaticStart
This function creates an empty set.
| Set_t Set_MakeFromUnion | ( | NodeMgr_ptr | nodemgr, | |
| node_ptr | _union | |||
| ) |
| Set_t Set_MakeSingleton | ( | Set_Element_t | elem | ) |
Creates a Singleton.
Creates a set with a unique element.
| void set_pkg_init | ( | void | ) |
Initializes the set package.
Initializes the set package. See also Set_Quit() to deinitialize it
| void set_pkg_quit | ( | void | ) |
De-Initializes the set package.
De-Initializes the set package. Use after Set_init()
| void Set_PrintSet | ( | MasterPrinter_ptr | mprinter, | |
| FILE * | , | |||
| const Set_t | set, | |||
| void(*)(FILE *file, Set_Element_t el, void *arg) | printer, | |||
| void * | printer_arg | |||
| ) |
Prints a set.
Prints a set to the specified file stream. Third parameter printer is a callback to be used when printing elements. If NULL, elements will be assumed to be node_ptr and print_node is called. printer_arg is an optional argument to be passed to the printer (can be NULL)
| void Set_ReleaseSet | ( | Set_t | set | ) |
Frees a set.
Releases the memory associated to the given set. If the set was frozen, reference counting is taken into account. See description about the structure Set_t for further information
| void Set_ReleaseSetOfSet | ( | Set_t | set | ) |
Frees a set of sets.
Assuming that an input set consists of elements each of which is also a set this function applies Set_ReleaseSet to the input set and every set in it.
Set_ReleaseSet
| Set_t Set_RemoveMember | ( | Set_t | set, | |
| Set_Element_t | el | |||
| ) |
Removes the given element from the set, if found.
The new set is returned. Linear time. See description about the structure Set_t for further information
If set is not frozen, set is changed internally. If after removal set is empty, it is also released.
| NodeList_ptr Set_Set2List | ( | const Set_t | set | ) |
Given a set, returns the corresponding list.
Given a set, returns a corresponding list. Returned list belongs to self and must be NOT freed nor changed by the caller.
| node_ptr Set_Set2Node | ( | const Set_t | set, | |
| NodeMgr_ptr | nodemgr | |||
| ) |
| node_ptr Set_Set2Union | ( | const Set_t | set, | |
| NodeMgr_ptr | nodemgr | |||
| ) |
Returns a UNION expression out of all set elements.
Returns a UNION expression out of all set elements. Order of entries is reversed in the returned UNION
Set Union.
Computes the Union of two sets. If set1 is not frozen, set1 is changed by adding members of set2. If set1 is frozen, it is before copied into a new set.
If set1 is not frozen, complexity is linear in the cardinality od set2, otherwise it is linear in the cardinality(set1) + cardinality(set2)
See description about the structure Set_t for further information
If set is not frozen, set is changed internally.
1.6.1