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

00001 /* ---------------------------------------------------------------------------
00002 
00003 
00004   This file is part of the ``enc.utils'' package of NuSMV version 2. 
00005   Copyright (C) 2005 by FBK-irst. 
00006 
00007   NuSMV version 2 is free software; you can redistribute it and/or 
00008   modify it under the terms of the GNU Lesser General Public 
00009   License as published by the Free Software Foundation; either 
00010   version 2 of the License, or (at your option) any later version.
00011 
00012   NuSMV version 2 is distributed in the hope that it will be useful, 
00013   but WITHOUT ANY WARRANTY; without even the implied warranty of 
00014   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU 
00015   Lesser General Public License for more details.
00016 
00017   You should have received a copy of the GNU Lesser General Public 
00018   License along with this library; if not, write to the Free Software 
00019   Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307  USA.
00020 
00021   For more information on NuSMV see <http://nusmv.fbk.eu>
00022   or email to <nusmv-users@fbk.eu>.
00023   Please report bugs to <nusmv-users@fbk.eu>.
00024 
00025   To contact the NuSMV development board, email to <nusmv@fbk.eu>. 
00026 
00027 -----------------------------------------------------------------------------*/
00028 
00046 #ifndef __NUSMV_CORE_ENC_UTILS_ADD_ARRAY_H__
00047 #define __NUSMV_CORE_ENC_UTILS_ADD_ARRAY_H__
00048 
00049 #include "nusmv/core/dd/DDMgr.h"
00050 #include "nusmv/core/dd/dd.h"
00051 #include "nusmv/core/utils/array.h"
00052 #include "nusmv/core/utils/WordNumber.h"
00053 
00054 
00055 /*---------------------------------------------------------------------------*/
00056 /* Types                                                                     */
00057 /*---------------------------------------------------------------------------*/
00058 
00065 typedef struct AddArray_TAG* AddArray_ptr;
00066 
00067 /*---------------------------------------------------------------------------*/
00068 /* Macros                                                                    */
00069 /*---------------------------------------------------------------------------*/
00070 
00076 #define ADD_ARRAY(x)  \
00077         ((AddArray_ptr) (x))
00078 
00084 #define ADD_ARRAY_CHECK_INSTANCE(x)  \
00085         (nusmv_assert(ADD_ARRAY(x) != ADD_ARRAY(NULL)))
00086 
00087 /*---------------------------------------------------------------------------*/
00088 /* Definition of external funcions                                           */
00089 /*---------------------------------------------------------------------------*/
00090 
00091 /* constructor-converters */
00092 
00100 AddArray_ptr AddArray_create(int number);
00101 
00108 void AddArray_destroy(DDMgr_ptr dd, AddArray_ptr self);
00109 
00116 AddArray_ptr 
00117 AddArray_from_word_number(DDMgr_ptr dd, WordNumber_ptr wn);
00118 
00125 AddArray_ptr AddArray_from_add(add_ptr add);
00126 
00133 AddArray_ptr AddArray_duplicate(AddArray_ptr self);
00134 
00135 /* access function */
00136 
00143 int AddArray_get_size(AddArray_ptr self);
00144 
00151 size_t AddArray_get_add_size(const AddArray_ptr self, 
00152                                     DDMgr_ptr dd);
00153 
00161 add_ptr AddArray_get_add(AddArray_ptr self);
00162 
00171 add_ptr AddArray_get_n(AddArray_ptr self, int number);
00172 
00180 void AddArray_set_n(AddArray_ptr self, int number, 
00181                            add_ptr add);
00182 
00189 array_t* AddArray_get_array(AddArray_ptr self);
00190 
00191 /* --------------------------------------------------------- */
00192 /* auxiliary arithmetic functions */
00193 /* --------------------------------------------------------- */
00194 
00195 /* arithemtic Word operations */
00196 
00203 AddArray_ptr 
00204 AddArray_word_apply_unary(DDMgr_ptr dd,
00205                           AddArray_ptr arg1,
00206                           FP_A_DA op);
00207 
00214 AddArray_ptr 
00215 AddArray_word_apply_binary(DDMgr_ptr dd,
00216                            AddArray_ptr arg1,
00217                            AddArray_ptr arg2, 
00218                            FP_A_DAA op);
00219 
00225 add_ptr 
00226 AddArray_make_disjunction(DDMgr_ptr dd,
00227                           AddArray_ptr arg);
00228 
00234 add_ptr 
00235 AddArray_make_conjunction(DDMgr_ptr dd,
00236                           AddArray_ptr arg);
00237 
00245 AddArray_ptr AddArray_word_plus(DDMgr_ptr dd,
00246                                        AddArray_ptr arg1,
00247                                        AddArray_ptr arg2);
00248 
00256 AddArray_ptr AddArray_word_minus(DDMgr_ptr dd,
00257                                         AddArray_ptr arg1,
00258                                         AddArray_ptr arg2);
00259 
00265 AddArray_ptr AddArray_word_unary_minus(DDMgr_ptr dd, 
00266                                               AddArray_ptr arg);
00267 
00275 AddArray_ptr AddArray_word_times(DDMgr_ptr dd,
00276                                         AddArray_ptr arg1,
00277                                         AddArray_ptr arg2);
00278 
00286 AddArray_ptr AddArray_word_unsigned_divide(DDMgr_ptr dd,
00287                                          AddArray_ptr arg1,
00288                                          AddArray_ptr arg2);
00289 
00297 AddArray_ptr AddArray_word_unsigned_mod(DDMgr_ptr dd,
00298                                       AddArray_ptr arg1,
00299                                       AddArray_ptr arg2);
00300 
00308 AddArray_ptr AddArray_word_signed_divide(DDMgr_ptr dd,
00309                                                 AddArray_ptr arg1,
00310                                                 AddArray_ptr arg2);
00311 
00319 AddArray_ptr AddArray_word_signed_mod(DDMgr_ptr dd,
00320                                              AddArray_ptr arg1,
00321                                              AddArray_ptr arg2);
00322 
00343 AddArray_ptr AddArray_word_left_shift(DDMgr_ptr dd,
00344                                              AddArray_ptr arg,
00345                                              AddArray_ptr number);
00346 
00355 AddArray_ptr AddArray_word_unsigned_right_shift(DDMgr_ptr dd,
00356                                               AddArray_ptr arg,
00357                                               AddArray_ptr number);
00358 
00367 AddArray_ptr AddArray_word_signed_right_shift(DDMgr_ptr dd,
00368                                               AddArray_ptr arg,
00369                                               AddArray_ptr number);
00370 
00391 AddArray_ptr AddArray_word_left_rotate(DDMgr_ptr dd,
00392                                               AddArray_ptr arg,
00393                                               AddArray_ptr number);
00394 
00415 AddArray_ptr AddArray_word_right_rotate(DDMgr_ptr dd,
00416                                                AddArray_ptr arg,
00417                                                AddArray_ptr number);
00418 
00429 AddArray_ptr AddArray_word_unsigned_less(DDMgr_ptr dd,
00430                                                AddArray_ptr arg1,
00431                                                AddArray_ptr arg2);
00432 
00443 AddArray_ptr AddArray_word_unsigned_less_equal(DDMgr_ptr dd,
00444                                                      AddArray_ptr arg1,
00445                                                      AddArray_ptr arg2);
00446 
00457 AddArray_ptr AddArray_word_unsigned_greater(DDMgr_ptr dd,
00458                                                   AddArray_ptr arg1,
00459                                                   AddArray_ptr arg2);
00460 
00471 AddArray_ptr AddArray_word_unsigned_greater_equal(DDMgr_ptr dd,
00472                                                         AddArray_ptr arg1,
00473                                                         AddArray_ptr arg2);
00474 
00484 AddArray_ptr AddArray_word_signed_less(DDMgr_ptr dd, 
00485                                               AddArray_ptr arg1,
00486                                               AddArray_ptr arg2);
00487 
00497 AddArray_ptr AddArray_word_signed_less_equal(DDMgr_ptr dd, 
00498                                                     AddArray_ptr arg1,
00499                                                     AddArray_ptr arg2);
00500 
00510 AddArray_ptr AddArray_word_signed_greater(DDMgr_ptr dd, 
00511                                                  AddArray_ptr arg1,
00512                                                  AddArray_ptr arg2);
00513 
00523 AddArray_ptr AddArray_word_signed_greater_equal(DDMgr_ptr dd, 
00524                                                        AddArray_ptr arg1, 
00525                                                        AddArray_ptr arg2);
00526 
00538 AddArray_ptr 
00539 AddArray_word_signed_extend(DDMgr_ptr dd,
00540                           AddArray_ptr arg, AddArray_ptr repeat);
00541 
00553 AddArray_ptr 
00554 AddArray_word_unsigned_extend(DDMgr_ptr dd,
00555                               AddArray_ptr arg, AddArray_ptr repeat);
00556 
00568 AddArray_ptr
00569 AddArray_word_signed_resize(DDMgr_ptr dd,
00570                           AddArray_ptr arg, AddArray_ptr new_size);
00571 
00583 AddArray_ptr
00584 AddArray_word_unsigned_resize(DDMgr_ptr dd,
00585                               AddArray_ptr arg, AddArray_ptr new_size);
00586 
00597 AddArray_ptr AddArray_word_equal(DDMgr_ptr dd,
00598                                         AddArray_ptr arg1,
00599                                         AddArray_ptr arg2);
00600 
00611 AddArray_ptr AddArray_word_not_equal(DDMgr_ptr dd,
00612                                             AddArray_ptr arg1,
00613                                             AddArray_ptr arg2);
00614 
00631 AddArray_ptr AddArray_word_ite(DDMgr_ptr dd,
00632                                       AddArray_ptr _if,
00633                                       AddArray_ptr _then, 
00634                                       AddArray_ptr _else);
00635 
00648 AddArray_ptr AddArray_word_bit_selection(DDMgr_ptr dd,
00649                                                 AddArray_ptr word,
00650                                                 AddArray_ptr range);
00651 
00661 AddArray_ptr AddArray_word_concatenation(DDMgr_ptr dd,
00662                                                 AddArray_ptr arg1,
00663                                                 AddArray_ptr arg2);
00664 
00665 #endif /* __NUSMV_CORE_ENC_UTILS_ADD_ARRAY_H__ */