NuSMV/code/nusmv/core/compile/symb_table/SymbType.h

Go to the documentation of this file.

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


  This file is part of the ``compile.symb_table'' 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_COMPILE_SYMB_TABLE_SYMB_TYPE_H__
#define __NUSMV_CORE_COMPILE_SYMB_TABLE_SYMB_TYPE_H__

#include <stdio.h>

#include "nusmv/core/node/node.h"
#include "nusmv/core/utils/utils.h"
#include "nusmv/core/node/printers/MasterPrinter.h"


typedef struct SymbType_TAG* SymbType_ptr;

#define SYMB_TYPE(x)  \
        ((SymbType_ptr) x)

#define SYMB_TYPE_CHECK_INSTANCE(x)  \
        (nusmv_assert(SYMB_TYPE(x) != SYMB_TYPE(NULL)))


#define nullType   SYMB_TYPE(NULL)


typedef enum SymbTypeTag_TAG {
  SYMB_TYPE_NONE, /* no-type and no error. */
  SYMB_TYPE_STATEMENT, /* for statements like assignements, INIT, TRANS etc */
  SYMB_TYPE_BOOLEAN,
  SYMB_TYPE_ENUM,  /* an enumeration of values (includes ranges, i.e. -1..4) */
  SYMB_TYPE_INTEGER,  /* (infinite-precision) integer */
  SYMB_TYPE_REAL, /* (infinite-precision) rational */
  SYMB_TYPE_NFUNCTION,
  SYMB_TYPE_CONTINUOUS,
  SYMB_TYPE_SIGNED_WORD, /* word is like an arrary of booleans + signed arithmetic */
  SYMB_TYPE_UNSIGNED_WORD, /* word is like an arrary of booleans + unsigned arithmetic */
  SYMB_TYPE_WORDARRAY, /* an array of words */
  SYMB_TYPE_ARRAY, /* an array */
  SYMB_TYPE_SET_BOOL,  /* a set of boolean values */
  SYMB_TYPE_SET_INT,  /* a set of integer values */
  SYMB_TYPE_SET_SYMB, /* a set of symbolic values */
  SYMB_TYPE_SET_INT_SYMB, /* a set of symbolic and integer values */
  SYMB_TYPE_INTARRAY, /* unbounded array with integer index */
  SYMB_TYPE_ERROR, /* indicates an error */
  /* SYMB_TYPE_NONE must be the first and SYMB_TYPE_ERROR must be
     the last in the list
  */
} SymbTypeTag;


/* a set of constants to identify different enum-types */
enum Enum_types{ ENUM_TYPE_PURE_INT,
                 ENUM_TYPE_PURE_SYMBOLIC,
                 ENUM_TYPE_INT_SYMBOLIC,
};

/* Forward declaration */
#ifdef DEFINED_NFunction_ptr
#else
typedef struct NFunction_TAG*  NFunction_ptr;
#define DEFINED_NFunction_ptr 1
#endif

/* ---------------------------------------------------------------------- */
/*     Public methods                                                     */
/* ---------------------------------------------------------------------- */

/* Constructors, Destructors, Copiers and Cleaners ****************************/

SymbType_ptr SymbType_create(const NuSMVEnv_ptr env,
                             SymbTypeTag tag, node_ptr body);

SymbType_ptr SymbType_create_array(SymbType_ptr subtype,
                                          int lower_bound,
                                          int upper_bound);

SymbType_ptr SymbType_create_nfunction(const NuSMVEnv_ptr env,
                                       NFunction_ptr nfunction);

/* SymbType_create_from_node: use Compile_InstantiateType */

SymbType_ptr SymbType_copy(const SymbType_ptr self);

void SymbType_destroy(SymbType_ptr self);


/* Getters and Setters ********************************************************/

SymbTypeTag SymbType_get_tag(const SymbType_ptr self);

/* a enum of useful auxiliary functions */

boolean SymbType_is_intarray(const SymbType_ptr self);

boolean SymbType_is_enum(const SymbType_ptr self);

boolean SymbType_is_boolean(const SymbType_ptr self);

boolean SymbType_is_integer(const SymbType_ptr self);

boolean SymbType_is_real(const SymbType_ptr self);

boolean SymbType_is_continuous(const SymbType_ptr self);

boolean SymbType_is_pure_int_enum(const SymbType_ptr self);

boolean SymbType_is_pure_symbolic_enum(const SymbType_ptr self);

boolean SymbType_is_int_symbolic_enum(const SymbType_ptr self);

boolean SymbType_is_word_1(const SymbType_ptr self);

boolean SymbType_is_unsigned_word(const SymbType_ptr self);

boolean SymbType_is_signed_word(const SymbType_ptr self);

boolean SymbType_is_word(const SymbType_ptr self);

boolean SymbType_is_set(const SymbType_ptr self);

boolean SymbType_is_function(const SymbType_ptr self);


boolean SymbType_is_error(const SymbType_ptr self);

boolean SymbType_is_statement(const SymbType_ptr self);

boolean SymbType_is_infinite_precision(const SymbType_ptr self);

boolean SymbType_is_array(const SymbType_ptr self);

boolean SymbType_is_wordarray(const SymbType_ptr self);

int SymbType_calculate_type_size(const SymbType_ptr self);

node_ptr
SymbType_generate_all_word_values(const SymbType_ptr self);

int SymbType_get_word_width(const SymbType_ptr self);

int SymbType_get_word_line_number(const SymbType_ptr self);

int SymbType_get_wordarray_awidth(const SymbType_ptr self);

SymbType_ptr SymbType_get_wordarray_subtype(const SymbType_ptr self);

node_ptr SymbType_get_enum_type_values(const SymbType_ptr self);

NFunction_ptr SymbType_get_nfunction_type(const SymbType_ptr self);

SymbType_ptr SymbType_get_array_subtype(const SymbType_ptr self);

int SymbType_get_array_lower_bound(const SymbType_ptr self);

int SymbType_get_array_upper_bound(const SymbType_ptr self);

SymbType_ptr SymbType_get_intarray_subtype(const SymbType_ptr self);

void SymbType_print(const SymbType_ptr self,
                           MasterPrinter_ptr printer,
                           FILE* output_stream);

char* SymbType_sprint(const SymbType_ptr self,
                             MasterPrinter_ptr printer);

boolean SymbType_is_back_comp(const SymbType_ptr type);

SymbType_ptr
SymbType_get_greater(const SymbType_ptr type1, const SymbType_ptr type2);

SymbType_ptr SymbType_make_set_type(const SymbType_ptr self);

SymbType_ptr SymbType_make_from_set_type(const SymbType_ptr self);

SymbType_ptr SymbType_make_memory_shared(const SymbType_ptr self);

/* functions: */

SymbType_ptr
SymbType_convert_right_to_left(SymbType_ptr leftType,
                               SymbType_ptr rightType);

SymbType_ptr
SymbType_get_minimal_common(SymbType_ptr type1, SymbType_ptr type2);

boolean
SymbType_is_memory_shared(SymbType_ptr self);

boolean
SymbType_equals(SymbType_ptr self, SymbType_ptr oth);

boolean SymbType_is_single_value_enum(const SymbType_ptr self);


/* Conversion *****************************************************************/

node_ptr SymbType_to_node(const SymbType_ptr self,
                          NodeMgr_ptr nodemgr);



#endif /* __NUSMV_CORE_COMPILE_SYMB_TABLE_SYMB_TYPE_H__ */

---