NuSMV/code/nusmv/core/set/set.h

Go to the documentation of this file.

/* ---------------------------------------------------------------------------


  This file is part of the ``set'' package of NuSMV version 2.
  Copyright (C) 2000-2001 by FBK-irst.

  NuSMV version 2 is free software; you can redistribute it and/or
  modify it under the terms of the GNU Lesser General Public
  License as published by the Free Software Foundation; either
  version 2 of the License, or (at your option) any later version.

  NuSMV version 2 is distributed in the hope that it will be useful,
  but WITHOUT ANY WARRANTY; without even the implied warranty of
  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
  Lesser General Public License for more details.

  You should have received a copy of the GNU Lesser General Public
  License along with this library; if not, write to the Free Software
  Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307  USA.

  For more information on NuSMV see <http://nusmv.fbk.eu>
  or email to <nusmv-users@fbk.eu>.
  Please report bugs to <nusmv-users@fbk.eu>.

  To contact the NuSMV development board, email to <nusmv@fbk.eu>.

-----------------------------------------------------------------------------*/

#ifndef __NUSMV_CORE_SET_SET_H__
#define __NUSMV_CORE_SET_SET_H__

#include "nusmv/core/utils/utils.h"
#include "nusmv/core/utils/NodeList.h"
#include "nusmv/core/node/printers/MasterPrinter.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

typedef struct Set_TAG* Set_t;

typedef node_ptr Set_Element_t;

typedef ListIter_ptr Set_Iterator_t;

/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

#define SET_FOREACH(set, iter)                               \
   for (iter=Set_GetFirstIter(set); !Set_IsEndIter(iter);    \
        iter=Set_GetNextIter(iter))

#define SET_T(self) \
  ((Set_t)self)

#define SET_ELEMENT_T(self) \
  ((Set_Element_t)self)


/*---------------------------------------------------------------------------*/
/* Function prototypes                                                       */
/*---------------------------------------------------------------------------*/
/* Constructors, Destructors, Copiers and Cleaners ****************************/

Set_t Set_MakeEmpty(void);

Set_t Set_Make(node_ptr list);

Set_t Set_MakeFromUnion(NodeMgr_ptr nodemgr, node_ptr _union);

Set_t Set_MakeSingleton(Set_Element_t elem);

Set_t Set_Copy(const Set_t set);

void Set_ReleaseSet(Set_t set);

void Set_ReleaseSetOfSet(Set_t set);


/* Getters and Setters ********************************************************/

int Set_GiveCardinality(const Set_t set);

Set_t Set_AddMember(Set_t set, Set_Element_t el);

Set_t Set_RemoveMember(Set_t set, Set_Element_t el);


/* Queries ********************************************************************/

boolean Set_IsEmpty(const Set_t set);

boolean Set_IsMember(const Set_t set, Set_Element_t elem);

boolean Set_Contains(const Set_t set1, const Set_t set2);

boolean Set_Equals(const Set_t set1, const Set_t set2);

boolean Set_Intersects(const Set_t set1, const Set_t set2);

boolean Set_IsFrozen(Set_t const set);

boolean Set_IsSingleton(Set_t const set);


/* Package handling ***********************************************************/

void set_pkg_init(void);

void set_pkg_quit(void);


/* Converters *****************************************************************/

NodeList_ptr Set_Set2List(const Set_t set);

node_ptr Set_Set2Union(const Set_t set, NodeMgr_ptr nodemgr);

node_ptr Set_Set2Node(const Set_t set, NodeMgr_ptr nodemgr);


/* Printers *******************************************************************/

void Set_PrintSet(MasterPrinter_ptr mprinter,
                         FILE *, const Set_t set,
                         void (*printer)(FILE* file,
                                         Set_Element_t el, void* arg),
                         void* printer_arg);


/* SubInterface: Set_Iterator_t ***********************************************/

Set_Iterator_t Set_GetNextIter(Set_Iterator_t iter);

boolean Set_IsEndIter(Set_Iterator_t iter);

Set_Iterator_t Set_GetFirstIter(Set_t set1);


/* Methods using both Set and Set_Iterator_t **********************************/

Set_Element_t Set_GetMember(const Set_t set, Set_Iterator_t iter);

Set_t Set_GetRest(const Set_t set, Set_Iterator_t from);


/* Miscellaneous **************************************************************/

Set_t Set_Freeze(Set_t set);

Set_t Set_AddMembersFromList(Set_t set, const NodeList_ptr list);

Set_t Set_Union(Set_t set1, const Set_t set2);

Set_t Set_Intersection(Set_t set1, const Set_t set2);

Set_t Set_Difference(Set_t set1, const Set_t set2);


#endif /* __NUSMV_CORE_SET_SET_H__ */

---