NuSMV/code/nusmv/core/compile/compileInt.h

Go to the documentation of this file.

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


  This file is part of the ``compile'' package of NuSMV version 2.
  Copyright (C) 1998-2004 by CMU and 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_COMPILE_INT_H__
#define __NUSMV_CORE_COMPILE_COMPILE_INT_H__


#include "nusmv/core/compile/compile.h"

#include "nusmv/core/compile/symb_table/symb_table_int.h"
#include "nusmv/core/compile/symb_table/SymbTable.h"
#include "nusmv/core/compile/symb_table/SymbLayer.h"

#include "nusmv/core/fsm/FsmBuilder.h"

#include "nusmv/core/utils/utils.h"
#include "nusmv/core/utils/NodeList.h"
#include "nusmv/core/utils/assoc.h"

#include "nusmv/core/opt/opt.h"
#include "nusmv/core/dd/dd.h"
#include "nusmv/core/node/node.h"
#include "nusmv/core/set/set.h"

#include "nusmv/core/hrc/HrcNode.h"

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

/* The hash table for Compile_check_next memoization */

#define ST_CHECK_NEXT_HASH "ccnh"

#define ST_CHECK_INPUTS_HASH "ccih"

#define ST_BEVAL_EXPR2BEXPR_HASH "cbeh"

/* This hash associates to a variable the corresponding complete cone of
   influence, once it has been computes.
   (node_ptr)var --> (Set_t)complete_cone_of_influence */

#define ST_CONE_COI_HASH "ccch"

/* This hash associates to each formula the corresponding set of
   dependencies. The formula is fully traversed and symbols are resolved.
   (node_ptr)formula --> (Set_t)dependencies */

#define ST_CONE_DEPENDENCIES_HASH "ccdh"

/* This hash associates to each formula the corresponding set of constants
   (node_ptr)formula --> (Set_t)constants */

#define ST_CONE_CONSTS_HASH "cccoh"

/* This hash associates to a variable the corresponding cone of influence at
   depth 0, once it has been computes.
   (node_ptr)var --> (Set_t)cone_of_influence_at_depth_0 */

#define ST_CONE_COI0_HASH "cc0h"

#define ST_CHECK_NESTED_ATTIME_HASH "ccnah"

extern int nusmv_yylineno;

extern cmp_struct_ptr cmps;

/*---------------------------------------------------------------------------*/
/* Function prototypes                                                       */
/*---------------------------------------------------------------------------*/

int CommandIwls95PrintOption(NuSMVEnv_ptr env, int argc, char** argv);

int CommandCPPrintClusterInfo(NuSMVEnv_ptr env, int argc, char** argv);

cmp_struct_ptr cmp_struct_init(void);

void cmp_struct_quit(cmp_struct_ptr);

void Compile_ConstructHierarchy(const NuSMVEnv_ptr env, SymbTable_ptr symb_table,
SymbLayer_ptr, node_ptr, node_ptr,
node_ptr, FlatHierarchy_ptr, HrcNode_ptr, hash_ptr, boolean);

void compile_make_params_hrc(const NuSMVEnv_ptr env,
                                    node_ptr basename,
                                    node_ptr actual_list,
                                    node_ptr formal_list,
                                    HrcNode_ptr hrc_result);

void compile_add_assign_hrc(NodeMgr_ptr nodemgr,
                                   HrcNode_ptr hrc_result,
                                   node_ptr assign_list);

/* This will be removed when assignment of bit selection is implemented */

/* WARNING: (MR) This will be removed when assignment of bit selection is
   implemented */

void error_bit_selection_assignment_not_supported(NuSMVEnv_ptr env,
                                                         node_ptr name);

node_ptr
compile_flatten_rewrite_word_toint_cast(const NuSMVEnv_ptr env,
                                        node_ptr body,
                                        SymbType_ptr type);



#endif /* __NUSMV_CORE_COMPILE_COMPILE_INT_H__ */

---