NuSMV Developers Manual: NuSMV/code/nusmv/core/compile/compileUtil.h Source File

00001 /* ---------------------------------------------------------------------------
00002 
00003 
00004   This file is part of the ``compile'' package.
00005   %COPYRIGHT%
00006 
00007 
00008 -----------------------------------------------------------------------------*/
00009 
00019 #ifndef __NUSMV_CORE_COMPILE_COMPILE_UTIL_H__
00020 #define __NUSMV_CORE_COMPILE_COMPILE_UTIL_H__
00021 
00022 #include "nusmv/core/compile/symb_table/SymbTable.h"
00023 #include "nusmv/core/cinit/NuSMVEnv.h"
00024 #include "nusmv/core/utils/NodeList.h"
00025 #include "nusmv/core/node/NodeMgr.h"
00026 #include "nusmv/core/node/node.h"
00027 
00028 /*---------------------------------------------------------------------------*/
00029 /* Constant declarations                                                     */
00030 /*---------------------------------------------------------------------------*/
00031 
00032 
00033 /*---------------------------------------------------------------------------*/
00034 /* Type declarations                                                         */
00035 /*---------------------------------------------------------------------------*/
00036 
00037 
00038 /*---------------------------------------------------------------------------*/
00039 /* Structure declarations                                                    */
00040 /*---------------------------------------------------------------------------*/
00041 
00042 
00043 /*---------------------------------------------------------------------------*/
00044 /* Variable declarations                                                     */
00045 /*---------------------------------------------------------------------------*/
00046 
00047 
00048 /*---------------------------------------------------------------------------*/
00049 /* Macro declarations                                                        */
00050 /*---------------------------------------------------------------------------*/
00051 
00052 
00055 /*---------------------------------------------------------------------------*/
00056 /* Function prototypes                                                       */
00057 /*---------------------------------------------------------------------------*/
00058 
00083 node_ptr Compile_Util_symbol_from_expr(NuSMVEnv_ptr const env,
00084                                               node_ptr const var,
00085                                               const char* prefix,
00086                                               const char* suffix);
00087 
00115 node_ptr sym_intern(const NuSMVEnv_ptr env, const char*);
00116 
00122 node_ptr sym_intern_from_ustring(const NuSMVEnv_ptr env,
00123                                  const string_ptr _string);
00124 
00133 boolean
00134 sym_names_are_equal(const NuSMVEnv_ptr env,
00135                     node_ptr name1, node_ptr name2);
00136 
00156 node_ptr Compile_pop_distrib_ops(const NuSMVEnv_ptr env,
00157                                         node_ptr prop);
00158 
00159 
00172 node_ptr Compile_remove_ltl_bop(const NuSMVEnv_ptr env, node_ptr prop);
00173 
00189 Set_t
00190 Compile_make_sorted_vars_list_from_order(const SymbTable_ptr st,
00191 const NodeList_ptr vars, const NodeList_ptr vars_order);
00192 
00193 
00196 #endif /* __NUSMV_CORE_COMPILE_COMPILE_UTIL_H__ */