NuSMV Developers Manual: NuSMV/code/nusmv/core/utils/WordNumberMgr.h Source File

00001 /* ---------------------------------------------------------------------------
00002 
00003    This file is part of the ``utils'' package of NuSMV version 2.
00004    Copyright (C) 2011 by FBK-irst.
00005 
00006    NuSMV version 2 is free software; you can redistribute it and/or
00007    modify it under the terms of the GNU Lesser General Public
00008    License as published by the Free Software Foundation; either
00009    version 2 of the License, or (at your option) any later version.
00010 
00011    NuSMV version 2 is distributed in the hope that it will be useful,
00012    but WITHOUT ANY WARRANTY; without even the implied warranty of
00013    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU
00014    Lesser General Public License for more details.
00015 
00016    You should have received a copy of the GNU Lesser General Public
00017    License along with this library; if not, write to the Free Software
00018    Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307  USA.
00019 
00020    For more information on NuSMV see <http://nusmv.fbk.eu>
00021    or email to <nusmv-users@fbk.eu>.
00022    Please report bugs to <nusmv-users@fbk.eu>.
00023 
00024    To contact the NuSMV development board, email to <nusmv@fbk.eu>.
00025 
00026 -----------------------------------------------------------------------------*/
00027 
00038 #ifndef __NUSMV_CORE_UTILS_WORD_NUMBER_MGR_H__
00039 #define __NUSMV_CORE_UTILS_WORD_NUMBER_MGR_H__
00040 
00041 
00042 #include "nusmv/core/utils/utils.h"
00043 #include "nusmv/core/utils/WordNumber.h"
00044 #include "nusmv/core/cinit/NuSMVEnv.h"
00045 
00046 #if defined(_MSC_VER)
00047 # include "nusmv/core/utils/portability.h"  /* for strtoull */
00048 #endif
00049 
00056 typedef struct WordNumberMgr_TAG*  WordNumberMgr_ptr;
00057 
00064 #define WORD_NUMBER_MGR(self)                   \
00065   ((WordNumberMgr_ptr) self)
00066 
00072 #define WORD_NUMBER_MGR_CHECK_INSTANCE(self)                            \
00073   (nusmv_assert(WORD_NUMBER_MGR(self) != WORD_NUMBER_MGR(NULL)))
00074 
00075 
00076 
00079 /*---------------------------------------------------------------------------*/
00080 /* Function prototypes                                                       */
00081 /*---------------------------------------------------------------------------*/
00082 
00091 WordNumberMgr_ptr WordNumberMgr_create(const NuSMVEnv_ptr env);
00092 
00101 void WordNumberMgr_destroy(WordNumberMgr_ptr self);
00102 
00109 int WordNumberMgr_max_width(void);
00110 
00118 WordNumber_ptr
00119 WordNumberMgr_max_unsigned_value(WordNumberMgr_ptr self, int width);
00120 
00128 WordNumber_ptr
00129 WordNumberMgr_max_signed_value(WordNumberMgr_ptr self, int width);
00130 
00138 WordNumber_ptr
00139 WordNumberMgr_min_signed_value(WordNumberMgr_ptr self, int width);
00140 
00157 WordNumber_ptr
00158 WordNumberMgr_string_to_word_number(WordNumberMgr_ptr self,
00159                                     char* str, int base);
00160 
00175 WordNumber_ptr
00176 WordNumberMgr_sized_string_to_word_number(WordNumberMgr_ptr self,
00177                                           char* str, int base,
00178                                           int width);
00179 
00201 WordNumber_ptr
00202 WordNumberMgr_parsed_string_to_word_number(WordNumberMgr_ptr self,
00203                                            char* str,
00204                                            char** errorString);
00205 
00219 WordNumber_ptr
00220 WordNumberMgr_integer_to_word_number(WordNumberMgr_ptr self,
00221                                      WordNumberValue value,
00222                                      int width);
00223 
00241 WordNumber_ptr
00242 WordNumberMgr_signed_integer_to_word_number(WordNumberMgr_ptr self,
00243                                             WordNumberValue value,
00244                                             int width);
00245 
00252 WordNumber_ptr
00253 WordNumberMgr_normalize_word_number(WordNumberMgr_ptr self,
00254                                     WordNumber_ptr v);
00255 
00262 WordNumber_ptr
00263 WordNumberMgr_unary_minus(WordNumberMgr_ptr self,
00264                           WordNumber_ptr v);
00265 
00272 WordNumber_ptr
00273 WordNumberMgr_plus(WordNumberMgr_ptr self,
00274                    WordNumber_ptr v1, WordNumber_ptr v2);
00275 
00282 WordNumber_ptr
00283 WordNumberMgr_minus(WordNumberMgr_ptr self,
00284                     WordNumber_ptr v1, WordNumber_ptr v2);
00285 
00292 WordNumber_ptr
00293 WordNumberMgr_times(WordNumberMgr_ptr self,
00294                     WordNumber_ptr v1, WordNumber_ptr v2);
00295 
00303 WordNumber_ptr
00304 WordNumberMgr_unsigned_divide(WordNumberMgr_ptr self,
00305                               WordNumber_ptr v1,
00306                               WordNumber_ptr v2);
00307 
00315 WordNumber_ptr
00316 WordNumberMgr_signed_divide(WordNumberMgr_ptr self,
00317                             WordNumber_ptr v1,  WordNumber_ptr v2);
00318 
00327 WordNumber_ptr
00328 WordNumberMgr_unsigned_mod(WordNumberMgr_ptr self,
00329                            WordNumber_ptr v1, WordNumber_ptr v2);
00330 
00338 WordNumber_ptr
00339 WordNumberMgr_signed_mod(WordNumberMgr_ptr self,
00340                          WordNumber_ptr v1,  WordNumber_ptr v2);
00341 
00348 WordNumber_ptr
00349 WordNumberMgr_not(WordNumberMgr_ptr self,
00350                   WordNumber_ptr v);
00351 
00358 WordNumber_ptr
00359 WordNumberMgr_and(WordNumberMgr_ptr self,
00360                   WordNumber_ptr v1, WordNumber_ptr v2);
00361 
00368 WordNumber_ptr
00369 WordNumberMgr_or(WordNumberMgr_ptr self,
00370                  WordNumber_ptr v1, WordNumber_ptr v2);
00371 
00378 WordNumber_ptr
00379 WordNumberMgr_xor(WordNumberMgr_ptr self,
00380                   WordNumber_ptr v1, WordNumber_ptr v2);
00381 
00388 WordNumber_ptr
00389 WordNumberMgr_xnor(WordNumberMgr_ptr self,
00390                    WordNumber_ptr v1, WordNumber_ptr v2);
00391 
00398 WordNumber_ptr
00399 WordNumberMgr_implies(WordNumberMgr_ptr self,
00400                       WordNumber_ptr v1, WordNumber_ptr v2);
00401 
00408 WordNumber_ptr
00409 WordNumberMgr_iff(WordNumberMgr_ptr self,
00410                   WordNumber_ptr v1, WordNumber_ptr v2);
00411 
00418 WordNumber_ptr
00419 WordNumberMgr_concatenate(WordNumberMgr_ptr self,
00420                           WordNumber_ptr v1, WordNumber_ptr v2);
00421 
00430 WordNumber_ptr
00431 WordNumberMgr_bit_select(WordNumberMgr_ptr self,
00432                          WordNumber_ptr v, int highBit, int lowBit);
00433 
00441 WordNumber_ptr
00442 WordNumberMgr_unsigned_right_shift(WordNumberMgr_ptr self,
00443                                    WordNumber_ptr v, int numberOfBits);
00444 
00452 WordNumber_ptr
00453 WordNumberMgr_signed_right_shift(WordNumberMgr_ptr self,
00454                                  WordNumber_ptr v, int numberOfBits);
00455 
00463 WordNumber_ptr
00464 WordNumberMgr_left_shift(WordNumberMgr_ptr self,
00465                          WordNumber_ptr v, int numberOfBits);
00466 
00474 WordNumber_ptr
00475 WordNumberMgr_right_rotate(WordNumberMgr_ptr self,
00476                            WordNumber_ptr v, int numberOfBits);
00477 
00485 WordNumber_ptr
00486 WordNumberMgr_left_rotate(WordNumberMgr_ptr self,
00487                           WordNumber_ptr v, int numberOfBits);
00488 
00496 WordNumber_ptr
00497 WordNumberMgr_signed_extend(WordNumberMgr_ptr self,
00498                             WordNumber_ptr v, int numberOfTimes);
00499 
00506 WordNumber_ptr
00507 WordNumberMgr_unsigned_extend(WordNumberMgr_ptr self,
00508                               WordNumber_ptr v, int numberOfTimes);
00509 
00510 
00515 #endif /* __NUSMV_CORE_UTILS_WORD_NUMBER_MGR_H__ */