NuSMV/code/nusmv/core/enc/be/BeEnc_private.h
Go to the documentation of this file.00001 00002 /* --------------------------------------------------------------------------- 00003 00004 00005 This file is part of the ``enc.be'' package of NuSMV version 2. 00006 Copyright (C) 2004 by FBK-irst. 00007 00008 NuSMV version 2 is free software; you can redistribute it and/or 00009 modify it under the terms of the GNU Lesser General Public 00010 License as published by the Free Software Foundation; either 00011 version 2 of the License, or (at your option) any later version. 00012 00013 NuSMV version 2 is distributed in the hope that it will be useful, 00014 but WITHOUT ANY WARRANTY; without even the implied warranty of 00015 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU 00016 Lesser General Public License for more details. 00017 00018 You should have received a copy of the GNU Lesser General Public 00019 License along with this library; if not, write to the Free Software 00020 Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA. 00021 00022 For more information on NuSMV see <http://nusmv.fbk.eu> 00023 or email to <nusmv-users@fbk.eu>. 00024 Please report bugs to <nusmv-users@fbk.eu>. 00025 00026 To contact the NuSMV development board, email to <nusmv@fbk.eu>. 00027 00028 -----------------------------------------------------------------------------*/ 00029 00040 #ifndef __NUSMV_CORE_ENC_BE_BE_ENC_PRIVATE_H__ 00041 #define __NUSMV_CORE_ENC_BE_BE_ENC_PRIVATE_H__ 00042 00043 00044 #include "nusmv/core/enc/be/BeEnc.h" 00045 #include "nusmv/core/enc/base/BoolEncClient.h" 00046 #include "nusmv/core/enc/base/BoolEncClient_private.h" 00047 00048 #include "nusmv/core/be/be.h" 00049 #include "nusmv/core/utils/NodeList.h" 00050 #include "nusmv/core/utils/assoc.h" 00051 #include "nusmv/core/utils/utils.h" 00052 00053 00251 typedef struct BeEnc_TAG 00252 { 00253 /* this MUST stay on the top */ 00254 INHERITS_FROM(BoolEncClient); 00255 00256 /* -------------------------------------------------- */ 00257 /* Private members */ 00258 /* -------------------------------------------------- */ 00259 00260 /* the boolean expr manager, that is in charge of actually allocate 00261 be variables: */ 00262 Be_Manager_ptr be_mgr; 00263 00264 /* the number of physical indices allocated from BE manager 00265 (which may be different from number of used physical index 00266 and number of logical indices) */ 00267 int phy_idx_capacity; 00268 00269 /* the maximum physical index already in the use. */ 00270 int max_used_phy_idx; 00271 00272 /* the number of logical indices which enough memory has been 00273 allocated for. The number of logical indices in use equals 00274 the total size of untimed and all timed frames and is always 00275 less than this fields. Number of logical and physical indices 00276 may be different because every frozen var requires one 00277 physical and many logical indices. */ 00278 int log_idx_capacity; 00279 00280 /* the amount of memory should be requested as an excess to 00281 optimize memory handling */ 00282 int grow_excess; 00283 00284 /* max time reached until now for the variables environment: */ 00285 int max_allocated_time; 00286 00287 /* number of variables occurring in the untimed logical block */ 00288 int state_vars_num; 00289 int frozen_vars_num; 00290 int input_vars_num; 00291 00292 /* queue of physical indices that can be reused after a layer is 00293 removed: */ 00294 NodeList_ptr avail_phy_idx_queue; 00295 00296 /* var name to corresponding be: */ 00297 hash_ptr name2be; 00298 00299 /* var logical index to name: */ 00300 node_ptr* index2name; 00301 int index2name_size; 00302 00303 /* logical to physical indices map and viceversa: 00304 the size of phy2log is phy_idx_capacity. 00305 the size of log2phy is log_idx_capacity. 00306 */ 00307 int* log2phy; 00308 int* phy2log; 00309 00310 int* subst_array; /* Used by substitution operations */ 00311 int subst_array_size; 00312 00313 st_table* shift_hash; /* used to memoize shifting operations */ 00314 00315 /* -------------------------------------------------- */ 00316 /* Virtual methods */ 00317 /* -------------------------------------------------- */ 00318 00319 } BeEnc; 00320 00321 00322 00323 /* ---------------------------------------------------------------------- */ 00324 /* Private methods to be used by derivate and friend classes only */ 00325 /* ---------------------------------------------------------------------- */ 00330 void be_enc_init(BeEnc_ptr self, 00331 SymbTable_ptr symb_table, 00332 BoolEnc_ptr bool_enc); 00333 00338 void be_enc_deinit(BeEnc_ptr self); 00339 00340 void be_enc_commit_layer(BaseEnc_ptr enc_base, const char* layer_name); 00341 void be_enc_remove_layer(BaseEnc_ptr enc_base, const char* layer_name); 00342 00343 00344 #endif /* __NUSMV_CORE_ENC_BE_BE_ENC_PRIVATE_H__ */
