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

00001 /* ---------------------------------------------------------------------------
00002 
00003 
00004   This file is part of the ``enc'' package of NuSMV version 2.
00005   Copyright (C) 2003 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 
00038 #ifndef __NUSMV_CORE_ENC_OPERATORS_H__
00039 #define __NUSMV_CORE_ENC_OPERATORS_H__
00040 
00041 
00042 #include "nusmv/core/utils/utils.h"
00043 #include "nusmv/core/utils/WordNumber.h"
00044 #include "nusmv/core/utils/array.h"
00045 #include "nusmv/core/node/node.h"
00046 
00047 
00048 /*---------------------------------------------------------------------------*/
00049 /* Macro declarations                                                        */
00050 /*---------------------------------------------------------------------------*/
00051 
00052 
00053 /*---------------------------------------------------------------------------*/
00054 /* Variable declarations                                                     */
00055 /*---------------------------------------------------------------------------*/
00056 
00057 /*---------------------------------------------------------------------------*/
00058 /* Function prototypes                                                       */
00059 /*---------------------------------------------------------------------------*/
00060 
00067 node_ptr node_and(node_ptr n1, node_ptr n2, const NuSMVEnv_ptr env);
00068 
00075 node_ptr node_or(node_ptr n1, node_ptr n2, const NuSMVEnv_ptr env);
00076 
00087 node_ptr node_not(node_ptr n, node_ptr this_node_not_used, const NuSMVEnv_ptr env);
00088 
00095 node_ptr node_iff(node_ptr n1, node_ptr n2, const NuSMVEnv_ptr env);
00096 
00103 node_ptr node_xor(node_ptr n1, node_ptr n2, const NuSMVEnv_ptr env);
00104 
00111 node_ptr node_implies(node_ptr n1, node_ptr n2, const NuSMVEnv_ptr env);
00112 
00124 node_ptr node_equal(node_ptr n1, node_ptr n2, const NuSMVEnv_ptr env);
00125 
00137 node_ptr node_not_equal(node_ptr n1, node_ptr n2, const NuSMVEnv_ptr env);
00138 
00145 node_ptr node_lt(node_ptr n1, node_ptr n2, const NuSMVEnv_ptr env);
00146 
00153 node_ptr node_gt(node_ptr n1, node_ptr n2, const NuSMVEnv_ptr env);
00154 
00161 node_ptr node_le(node_ptr n1, node_ptr n2, const NuSMVEnv_ptr env);
00162 
00169 node_ptr node_ge(node_ptr n1, node_ptr n2, const NuSMVEnv_ptr env);
00170 
00176 node_ptr node_unary_minus(node_ptr n1, node_ptr n2, const NuSMVEnv_ptr env);
00177 
00183 node_ptr node_plus(node_ptr n1, node_ptr n2, const NuSMVEnv_ptr env);
00184 
00190 node_ptr node_minus(node_ptr n1, node_ptr n2, const NuSMVEnv_ptr env);
00191 
00197 node_ptr node_times(node_ptr n1, node_ptr n2, const NuSMVEnv_ptr env);
00198 
00204 node_ptr node_divide(node_ptr n1, node_ptr n2, const NuSMVEnv_ptr env);
00205 
00211 node_ptr node_mod(node_ptr n1, node_ptr n2, const NuSMVEnv_ptr env);
00212 
00220 node_ptr node_bit_range(node_ptr n1, node_ptr n2, const NuSMVEnv_ptr env);
00221 
00229 node_ptr node_union(node_ptr n1, node_ptr n2, const NuSMVEnv_ptr env);
00230 
00243 node_ptr node_setin(node_ptr n1, node_ptr n2, const NuSMVEnv_ptr env);
00244 
00245 /* ---------------------------------------------------------------------- */
00246 /* WORD related                                                           */
00247 /* ---------------------------------------------------------------------- */
00248 /* RC: some function may be moved away */
00249 
00255 size_t node_word_get_width(node_ptr w);
00256 
00257 #define _CHECK_WORD(w)                                      \
00258   nusmv_assert(((node_get_type(w) == UNSIGNED_WORD ||       \
00259                  node_get_type(w) == SIGNED_WORD) &&        \
00260                  node_word_get_width(w) > 0) ||             \
00261                (node_get_type(w) == NUMBER_UNSIGNED_WORD || \
00262                 node_get_type(w) == NUMBER_SIGNED_WORD))
00263 
00264 
00265 #define _CHECK_WORDS(w1, w2)                                          \
00266   _CHECK_WORD(w1); _CHECK_WORD(w2);                                   \
00267   if ((node_get_type(w1) == UNSIGNED_WORD ||                          \
00268        node_get_type(w1) == SIGNED_WORD)  &&                          \
00269       (node_get_type(w2) == UNSIGNED_WORD ||                          \
00270        node_get_type(w2) == SIGNED_WORD)) /* all words */             \
00271     nusmv_assert(node_word_get_width(w1) == node_word_get_width(w2)); \
00272   else if ((node_get_type(w1) == UNSIGNED_WORD ||                       \
00273             node_get_type(w1) == SIGNED_WORD)  &&                       \
00274            (node_get_type(w2) == NUMBER_UNSIGNED_WORD ||                \
00275             node_get_type(w2) == NUMBER_SIGNED_WORD)) /* word and const */ \
00276     nusmv_assert(node_word_get_width(w1) ==                             \
00277                  WordNumber_get_width(WORD_NUMBER(car(w2))));           \
00278   else if ((node_get_type(w2) == UNSIGNED_WORD ||                       \
00279             node_get_type(w2) == SIGNED_WORD)  &&                       \
00280            (node_get_type(w1) == NUMBER_UNSIGNED_WORD ||                \
00281             node_get_type(w1) == NUMBER_SIGNED_WORD)) /* const and word */ \
00282     nusmv_assert(node_word_get_width(w2) ==                             \
00283                  WordNumber_get_width(WORD_NUMBER(car(w1))));           \
00284   else if ((node_get_type(w2) == NUMBER_UNSIGNED_WORD ||                \
00285             node_get_type(w2) == NUMBER_SIGNED_WORD)  &&                \
00286            (node_get_type(w1) == NUMBER_UNSIGNED_WORD ||                \
00287             node_get_type(w1) == NUMBER_SIGNED_WORD)) /* const and const */ \
00288     nusmv_assert(WordNumber_get_width(WORD_NUMBER(car(w2))) ==          \
00289                  WordNumber_get_width(WORD_NUMBER(car(w1))));           \
00290   else error_unreachable_code();
00291 
00299 node_ptr node_word_create(node_ptr bitval, size_t w,
00300                                  const NuSMVEnv_ptr env);
00301 
00310 node_ptr node_word_create_from_list(node_ptr l, size_t w,
00311                                            const NuSMVEnv_ptr env);
00312 
00319 node_ptr node_word_create_from_wordnumber(WordNumber_ptr wn,
00320                                                  const NuSMVEnv_ptr env);
00321 
00328 node_ptr
00329 node_word_create_from_integer(unsigned long long value, size_t width,
00330                               const NuSMVEnv_ptr env);
00331 
00338 node_ptr node_word_create_from_array(array_t* arr,
00339                                             const NuSMVEnv_ptr env);
00340 
00348 array_t* node_word_to_array(node_ptr w);
00349 
00350 /* operations: */
00351 
00358 node_ptr node_word_apply_unary(node_ptr wenc, int op,
00359                                       const NuSMVEnv_ptr env);
00360 
00367 node_ptr node_word_apply_attime(node_ptr wenc, int time,
00368                                        const NuSMVEnv_ptr env);
00369 
00376 node_ptr
00377 node_word_apply_binary(node_ptr wenc1, node_ptr wenc2, int op,
00378                        const NuSMVEnv_ptr env);
00379 
00386 node_ptr node_word_make_conjuction(node_ptr w,
00387                                           const NuSMVEnv_ptr env);
00388 
00395 node_ptr node_word_make_disjunction(node_ptr w,
00396                                            const NuSMVEnv_ptr env);
00397 
00403 node_ptr node_word_cast_bool(node_ptr w, const NuSMVEnv_ptr env);
00404 
00411 node_ptr node_word_not(node_ptr w, const NuSMVEnv_ptr env);
00412 
00419 node_ptr node_word_and(node_ptr a, node_ptr b, const NuSMVEnv_ptr env);
00420 
00427 node_ptr node_word_or(node_ptr a, node_ptr b, const NuSMVEnv_ptr env);
00428 
00435 node_ptr node_word_xor(node_ptr a, node_ptr b, const NuSMVEnv_ptr env);
00436 
00443 node_ptr node_word_xnor(node_ptr a, node_ptr b, const NuSMVEnv_ptr env);
00444 
00451 node_ptr node_word_implies(node_ptr a, node_ptr b, const NuSMVEnv_ptr env);
00452 
00459 node_ptr node_word_iff(node_ptr a, node_ptr b, const NuSMVEnv_ptr env);
00460 
00466 node_ptr node_word_equal(node_ptr a, node_ptr b, const NuSMVEnv_ptr env);
00467 
00474 node_ptr node_word_notequal(node_ptr a, node_ptr b, const NuSMVEnv_ptr env);
00475 
00483 node_ptr node_word_concat(node_ptr a, node_ptr b, const NuSMVEnv_ptr env);
00484 
00492 node_ptr node_word_selection(node_ptr word, node_ptr range, const NuSMVEnv_ptr env);
00493 
00501 node_ptr node_word_extend(node_ptr a, node_ptr b,
00502                                  boolean isSigned, const NuSMVEnv_ptr env);
00503 
00510 node_ptr
00511 node_word_adder(node_ptr a, node_ptr b, node_ptr carry_in,
00512                 node_ptr* carry_out, const NuSMVEnv_ptr env);
00513 
00520 node_ptr node_word_plus(node_ptr a, node_ptr b, const NuSMVEnv_ptr env);
00521 
00528 node_ptr node_word_minus(node_ptr a, node_ptr b, const NuSMVEnv_ptr env);
00529 
00536 node_ptr node_word_uminus(node_ptr a, const NuSMVEnv_ptr env);
00537 
00544 node_ptr node_word_times(node_ptr a, node_ptr b, const NuSMVEnv_ptr env);
00545 
00552 node_ptr node_word_unsigned_divide(node_ptr a, node_ptr b, const NuSMVEnv_ptr env);
00553 
00560 node_ptr node_word_unsigned_mod(node_ptr a, node_ptr b, const NuSMVEnv_ptr env);
00561 
00568 node_ptr node_word_signed_divide(node_ptr a, node_ptr b, const NuSMVEnv_ptr env);
00569 
00576 node_ptr node_word_signed_mod(node_ptr a, node_ptr b, const NuSMVEnv_ptr env);
00577 
00583 node_ptr node_word_unsigned_less(node_ptr a, node_ptr b, const NuSMVEnv_ptr env);
00584 
00590 node_ptr node_word_unsigned_less_equal(node_ptr a, node_ptr b, const NuSMVEnv_ptr env);
00591 
00597 node_ptr node_word_unsigned_greater(node_ptr a, node_ptr b, const NuSMVEnv_ptr env);
00598 
00604 node_ptr node_word_unsigned_greater_equal(node_ptr a, node_ptr b, const NuSMVEnv_ptr env);
00605 
00611 node_ptr node_word_signed_less(node_ptr a, node_ptr b, const NuSMVEnv_ptr env);
00612 
00618 node_ptr node_word_signed_less_equal(node_ptr a, node_ptr b, const NuSMVEnv_ptr env);
00619 
00625 node_ptr node_word_signed_greater(node_ptr a, node_ptr b, const NuSMVEnv_ptr env);
00626 
00632 node_ptr node_word_signed_greater_equal(node_ptr a, node_ptr b, const NuSMVEnv_ptr env);
00633 
00639 node_ptr map2_param(node_ptr (*fun)(node_ptr, node_ptr, int, const NuSMVEnv_ptr),
00640                            node_ptr l1, node_ptr l2, int op, const NuSMVEnv_ptr env);
00641 
00642 #endif /* __NUSMV_CORE_ENC_OPERATORS_H__ */