NuSMV/code/nusmv/core/wff/ExprMgr.h

Go to the documentation of this file.

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


   This file is part of the ``wff'' package of NuSMV version 2.
   Copyright (C) 2011 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_WFF_EXPR_MGR_H__
#define __NUSMV_CORE_WFF_EXPR_MGR_H__

#if HAVE_CONFIG_H
#  include "nusmv-config.h"
#endif

#include "nusmv/core/utils/utils.h"
#include "nusmv/core/cinit/NuSMVEnv.h"
#include "nusmv/core/node/node.h"
#include "nusmv/core/compile/symb_table/SymbTable.h"


/* Don't change these values (used to handle NEXT untimed case and FROZEN) */

#define EXPR_UNTIMED_CURRENT -2

#define EXPR_UNTIMED_NEXT -1

#define EXPR_UNTIMED_DONTCARE -3

#define EXPR_TIME_OFS 10

typedef enum {
  EXPR_SIMPLE,
  EXPR_NEXT,
  EXPR_LTL,
  EXPR_CTL
} ExprKind;

typedef node_ptr Expr_ptr;

#define EXPR(x)                                 \
  ((Expr_ptr) x)

#define EXPR_CHECK_INSTANCE(x)                  \
  (nusmv_assert(EXPR(x) != EXPR(NULL)))

typedef struct ExprMgr_TAG*  ExprMgr_ptr;

#define EXPR_MGR(self)                          \
  ((ExprMgr_ptr) self)

#define EXPR_MGR_CHECK_INSTANCE(self)                   \
  (nusmv_assert(EXPR_MGR(self) != EXPR_MGR(NULL)))

#define Expr_get_type(t)                        \
  node_get_type(t)


/*---------------------------------------------------------------------------*/
/* Function prototypes                                                       */
/*---------------------------------------------------------------------------*/
/* Constructors, Destructors, Copiers and Cleaners ****************************/

ExprMgr_ptr ExprMgr_create(const NuSMVEnv_ptr env);

void ExprMgr_destroy(ExprMgr_ptr self);


NodeMgr_ptr ExprMgr_get_node_manager(const ExprMgr_ptr self);


/* Top level functions ********************************************************/

Expr_ptr ExprMgr_simplify(const ExprMgr_ptr self, SymbTable_ptr st, Expr_ptr expr);

Expr_ptr ExprMgr_resolve(const ExprMgr_ptr self, SymbTable_ptr st,
                                int type, Expr_ptr left, Expr_ptr right);


/* Queries ********************************************************************/

boolean ExprMgr_is_equal_to_zero(const ExprMgr_ptr self, const Expr_ptr input);

boolean
ExprMgr_is_ge_to_number(const ExprMgr_ptr self, const Expr_ptr input,
                        const Expr_ptr number);

boolean ExprMgr_is_true(const ExprMgr_ptr self, const Expr_ptr expr);

boolean ExprMgr_is_false(const ExprMgr_ptr self, const Expr_ptr expr);

boolean ExprMgr_is_boolean_range(const ExprMgr_ptr self, Expr_ptr expr);

boolean ExprMgr_is_number(const ExprMgr_ptr self, const Expr_ptr expr, const int value);

boolean ExprMgr_is_timed(const ExprMgr_ptr self, Expr_ptr expr, hash_ptr cache);

boolean ExprMgr_is_syntax_correct(Expr_ptr exp, ExprKind expectedKind);

/* Builders/Simplifiers *******************************************************/

Expr_ptr ExprMgr_boolean_range(const ExprMgr_ptr self);

Expr_ptr ExprMgr_true(const ExprMgr_ptr self);

Expr_ptr ExprMgr_false(const ExprMgr_ptr self);

Expr_ptr ExprMgr_number(const ExprMgr_ptr self, int value);

Expr_ptr ExprMgr_word_max_value(const ExprMgr_ptr self,
                                const int size, const int type);

Expr_ptr ExprMgr_next(const ExprMgr_ptr self, const Expr_ptr a, const SymbTable_ptr st);

Expr_ptr ExprMgr_ite(const ExprMgr_ptr self, const Expr_ptr cond,
                            const Expr_ptr t,
                            const Expr_ptr e,
                            const SymbTable_ptr st);

Expr_ptr ExprMgr_equal(const ExprMgr_ptr self, const Expr_ptr a,
                              const Expr_ptr b,
                              const SymbTable_ptr st);

Expr_ptr ExprMgr_notequal(const ExprMgr_ptr self, const Expr_ptr a,
                                 const Expr_ptr b,
                                 const SymbTable_ptr st);

Expr_ptr ExprMgr_le(const ExprMgr_ptr self, const Expr_ptr a,
                           const Expr_ptr b,
                           const SymbTable_ptr st);

Expr_ptr ExprMgr_ge(const ExprMgr_ptr self, const Expr_ptr a,
                           const Expr_ptr b,
                           const SymbTable_ptr st);

Expr_ptr ExprMgr_simplify_word_extend(const ExprMgr_ptr self, const SymbTable_ptr st,
                                             Expr_ptr w, Expr_ptr i);

Expr_ptr ExprMgr_attime(const ExprMgr_ptr self, Expr_ptr e, int time,
                               const SymbTable_ptr st);

Expr_ptr ExprMgr_word_constant(const ExprMgr_ptr self, const SymbTable_ptr st,
                                      int type,
                                      Expr_ptr w,
                                      Expr_ptr i);

Expr_ptr ExprMgr_and_from_list(const ExprMgr_ptr self, node_ptr list,
                                      const SymbTable_ptr st);

Expr_ptr ExprMgr_and(const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b);

Expr_ptr ExprMgr_and_nil(const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b);

Expr_ptr ExprMgr_not(const ExprMgr_ptr self, const Expr_ptr expr);

Expr_ptr ExprMgr_or(const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b);

Expr_ptr ExprMgr_xor(const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b);

Expr_ptr ExprMgr_xnor(const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b);

Expr_ptr ExprMgr_iff(const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b);

Expr_ptr ExprMgr_implies(const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b);

Expr_ptr ExprMgr_lt(const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b);

Expr_ptr ExprMgr_simplify_lt(const ExprMgr_ptr self, const SymbTable_ptr st,
                                    const Expr_ptr a,
                                    const Expr_ptr b);

Expr_ptr ExprMgr_gt(const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b);

Expr_ptr ExprMgr_simplify_gt(const ExprMgr_ptr self, const SymbTable_ptr st,
                                    const Expr_ptr a,
                                    const Expr_ptr b);

Expr_ptr ExprMgr_plus(const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b);

Expr_ptr ExprMgr_minus(const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b);

Expr_ptr ExprMgr_times(const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b);

Expr_ptr ExprMgr_divide(const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b);

Expr_ptr ExprMgr_mod(const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b);

Expr_ptr ExprMgr_unary_minus(const ExprMgr_ptr self, const Expr_ptr a);

Expr_ptr ExprMgr_array_read(const ExprMgr_ptr self,
                            const Expr_ptr a, const Expr_ptr i);

Expr_ptr ExprMgr_array_write(const ExprMgr_ptr self,
                             const Expr_ptr a, const Expr_ptr i, 
                             const Expr_ptr v);

Expr_ptr ExprMgr_array_const(const ExprMgr_ptr self,
                             const Expr_ptr a, const Expr_ptr v);

Expr_ptr ExprMgr_word_left_shift(const ExprMgr_ptr self, const Expr_ptr a,
                                        const Expr_ptr b);

Expr_ptr ExprMgr_word_right_shift(const ExprMgr_ptr self, const Expr_ptr a,
                                         const Expr_ptr b);

Expr_ptr ExprMgr_word_left_rotate(const ExprMgr_ptr self, const Expr_ptr a,
                                         const Expr_ptr b);

Expr_ptr ExprMgr_word_right_rotate(const ExprMgr_ptr self, const Expr_ptr a,
                                          const Expr_ptr b);

Expr_ptr ExprMgr_word_bit_select(const ExprMgr_ptr self, const Expr_ptr w,
                                        const Expr_ptr r);

Expr_ptr ExprMgr_simplify_word_bit_select(const ExprMgr_ptr self, const SymbTable_ptr st,
                                                 const Expr_ptr w,
                                                 const Expr_ptr r);

Expr_ptr ExprMgr_word_concatenate(const ExprMgr_ptr self, const Expr_ptr a,
                                         const Expr_ptr b);

Expr_ptr ExprMgr_word1_to_bool(const ExprMgr_ptr self, Expr_ptr w);

Expr_ptr ExprMgr_bool_to_word1(const ExprMgr_ptr self, Expr_ptr a);

Expr_ptr ExprMgr_signed_word_to_unsigned(const ExprMgr_ptr self, Expr_ptr w);

Expr_ptr ExprMgr_unsigned_word_to_signed(const ExprMgr_ptr self, Expr_ptr w);

Expr_ptr ExprMgr_word_extend(const ExprMgr_ptr self, Expr_ptr w,
                                    Expr_ptr i,
                                    const SymbTable_ptr st);

int ExprMgr_attime_get_time(const ExprMgr_ptr self, Expr_ptr e);

Expr_ptr ExprMgr_attime_get_untimed(const ExprMgr_ptr self, Expr_ptr e);

Expr_ptr ExprMgr_union(const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b);

Expr_ptr ExprMgr_setin(const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b, const SymbTable_ptr st);

Expr_ptr ExprMgr_range(const ExprMgr_ptr self, const Expr_ptr a, const Expr_ptr b);

Expr_ptr ExprMgr_function(const ExprMgr_ptr self, const Expr_ptr name,
                                 const Expr_ptr params);

int ExprMgr_get_time(const ExprMgr_ptr self, SymbTable_ptr st, Expr_ptr expr);

int* ExprMgr_get_time_interval(const ExprMgr_ptr self,
                                      const SymbTable_ptr st,
                                      Expr_ptr expr);

Expr_ptr ExprMgr_untimed(const ExprMgr_ptr self, SymbTable_ptr st, Expr_ptr expr);

Expr_ptr ExprMgr_untimed_explicit_time(const ExprMgr_ptr self, SymbTable_ptr st,
                                              Expr_ptr expr,
                                              int time);

Expr_ptr ExprMgr_wsizeof(const ExprMgr_ptr self, Expr_ptr l, Expr_ptr r);

Expr_ptr ExprMgr_cast_toint(const ExprMgr_ptr self, Expr_ptr l, Expr_ptr r);

Expr_ptr ExprMgr_simplify_floor(const ExprMgr_ptr self, const SymbTable_ptr symb_table,
                                       Expr_ptr body);


Expr_ptr ExprMgr_floor(const ExprMgr_ptr self, Expr_ptr l);


Expr_ptr ExprMgr_plus_one(const ExprMgr_ptr self,
                                 const Expr_ptr a);

Expr_ptr ExprMgr_minus_one(const ExprMgr_ptr self,
                                  const Expr_ptr a);

Expr_ptr ExprMgr_plus_number(const ExprMgr_ptr self,
                                    const Expr_ptr a,
                                    const Expr_ptr b);

Expr_ptr ExprMgr_simplify_iff(const ExprMgr_ptr self,
                                     const SymbTable_ptr st,
                                     const Expr_ptr a,
                                     const Expr_ptr b);

Expr_ptr ExprMgr_simplify_word_resize(const ExprMgr_ptr self, const SymbTable_ptr st,
                                             Expr_ptr w,
                                             Expr_ptr i);


Expr_ptr ExprMgr_cast_to_unsigned_word(const ExprMgr_ptr self,
                                       Expr_ptr width, Expr_ptr arg);

boolean ExprMgr_time_is_dont_care(const ExprMgr_ptr self, int time);

boolean ExprMgr_time_is_current(const ExprMgr_ptr self, int time);

boolean ExprMgr_time_is_next(const ExprMgr_ptr self, int time);

Expr_ptr ExprMgr_move_next_to_leaves(const ExprMgr_ptr self, SymbTable_ptr st, Expr_ptr expr);

#endif /* __NUSMV_CORE_WFF_EXPR_MGR_H__ */

---