NuSMV/code/nusmv/core/utils/Sset.h

Go to the documentation of this file.

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


  This file is part of the ``compile'' package of NuSMV version 2.
  Copyright (C) 2008 by FBK.

  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_UTILS_SSET_H__
#define __NUSMV_CORE_UTILS_SSET_H__

#include "nusmv/core/utils/defs.h"
#include "nusmv/core/cinit/NuSMVEnv.h"

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

typedef struct Sset_TAG* Sset_ptr;

#define SSET(x) \
         ((Sset_ptr) x)

#define SSET_CHECK_INSTANCE(x) \
         ( nusmv_assert(SSET(x) != SSET(NULL)) )

#define SSET_FOREACH(sset, iter)  \
   for (iter=SSet_first(sset); SSiter_is_valid(iter); \
        iter=SSiter_next(iter))

/* internal type. it cannot be used outside. */

typedef struct Ssnode_TAG* Ssnode_ptr;

typedef void* Sset_key;

/* Iterator type.
   here a struct definition is used only to create a new type. Thus
   C type checker will be able to catch incorrect use of iterators.
   This does not influence the efficiency */
typedef struct Ssiter_TAG {
    Ssnode_ptr node;
} Ssiter;

/* ---------------------------------------------------------------------- */
/* Public interface                                                       */
/* ---------------------------------------------------------------------- */

Sset_ptr Sset_create(void);

Sset_ptr Sset_create_with_param(PFIVPVP compare);

void Sset_destroy(Sset_ptr self);

Sset_ptr Sset_copy(const Sset_ptr self);

Sset_ptr Sset_copy_func(const Sset_ptr self,
                               void* (*func)(void*, void*), void* arg);

boolean Sset_insert(Sset_ptr self, Sset_key key,
                           void* element);

Ssiter Sset_find(Sset_ptr self, Sset_key key);

Ssiter Sset_find_le(Sset_ptr self, Sset_key key);

Ssiter Sset_find_ge(Sset_ptr self, Sset_key key);

Ssiter Sset_find_insert(Sset_ptr self, Sset_key key,
                               boolean* is_found);

void* Sset_delete(Sset_ptr self, Sset_key key,
                         boolean* is_found);

void Sset_delete_iter(Sset_ptr self, Ssiter iter);

size_t Sset_get_size(Sset_ptr self);

boolean Sset_is_empty(Sset_ptr self);

Ssiter Sset_first(Sset_ptr self);

Ssiter Sset_last(Sset_ptr self);

Ssiter Ssiter_next(Ssiter iter);

Ssiter Ssiter_prev(Ssiter iter);

boolean Ssiter_is_valid(Ssiter iter);

void* Ssiter_element(Ssiter iter);

Sset_key Ssiter_key(Ssiter iter);

void Ssiter_set_element(Ssiter iter, void* element);

#ifndef NDEBUG

void Sset_test(const NuSMVEnv_ptr env);
#endif

#endif /* __NUSMV_CORE_UTILS_SSET_H__ */

---