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

Go to the documentation of this file.

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


  This file is part of the ``enc.utils'' package of NuSMV version 2.
  Copyright (C) 2005 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_UTILS_WORD_NUMBER_H__
#define __NUSMV_CORE_UTILS_WORD_NUMBER_H__


#include "nusmv/core/utils/utils.h"

typedef struct WordNumber_TAG* WordNumber_ptr;

typedef unsigned long long  WordNumberValue;


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

#define WORD_NUMBER(x)  \
        ((WordNumber_ptr) (x))

#define WORD_NUMBER_CHECK_INSTANCE(x)  \
        (nusmv_assert(WORD_NUMBER(x) != WORD_NUMBER(NULL)))

/*---------------------------------------------------------------------------*/
/* Function prototypes                                                       */
/*---------------------------------------------------------------------------*/

/* Initialisation and de-initialisation of the WordNumber class
   (the manager) */

void WordNumber_init(NuSMVEnv_ptr env);

void WordNumber_quit(NuSMVEnv_ptr env);


/* implementation limit */

int WordNumber_max_width(void);

/* access function */

unsigned 
long long WordNumber_get_unsigned_value(WordNumber_ptr self);

signed 
long long WordNumber_get_signed_value(WordNumber_ptr self);

int WordNumber_get_width(WordNumber_ptr self);

boolean WordNumber_get_bit(WordNumber_ptr self, int n);

boolean WordNumber_get_sign(WordNumber_ptr self);

const char* WordNumber_get_parsed_string(WordNumber_ptr self);

/* output functions */

int WordNumber_based_print(FILE* output_stream,
                                  WordNumber_ptr self,
                                  int base,
                                  boolean isSigned);

char* WordNumber_to_based_string(WordNumber_ptr self, int base,
                                        boolean isSigned);


/* relational operations */

boolean WordNumber_is_zero(WordNumber_ptr v);

boolean WordNumber_equal(WordNumber_ptr v1, WordNumber_ptr v2);

boolean WordNumber_not_equal(WordNumber_ptr v1,
                                    WordNumber_ptr v2);

boolean WordNumber_unsigned_less(WordNumber_ptr v1,
                                        WordNumber_ptr v2);

boolean WordNumber_unsigned_less_or_equal(WordNumber_ptr v1,
                                                 WordNumber_ptr v2);

boolean WordNumber_unsigned_greater(WordNumber_ptr v1,
                                           WordNumber_ptr v2);

boolean WordNumber_unsigned_greater_or_equal(WordNumber_ptr v1,
                                                    WordNumber_ptr v2);

boolean WordNumber_signed_less(WordNumber_ptr v1,
                                      WordNumber_ptr v2);

boolean WordNumber_signed_less_or_equal(WordNumber_ptr v1,
                                               WordNumber_ptr v2);

boolean WordNumber_signed_greater(WordNumber_ptr v1,
                                         WordNumber_ptr v2);

boolean WordNumber_signed_greater_or_equal(WordNumber_ptr v1,
                                           WordNumber_ptr v2);

WordNumber_ptr WordNumber_max(WordNumber_ptr v1,
                                     WordNumber_ptr v2,
                                     boolean isSigned);

WordNumber_ptr WordNumber_min(WordNumber_ptr v1,
                                     WordNumber_ptr v2,
                                     boolean isSigned);

#endif /* __NUSMV_CORE_UTILS_WORD_NUMBER_H__ */

---