Private and protected interface of class 'BeEnc'. More...
#include <BeEnc_private.h>
Public Member Functions | |
| INHERITS_FROM (BoolEncClient) | |
Data Fields | |
| NodeList_ptr | avail_phy_idx_queue |
| Be_Manager_ptr | be_mgr |
| int | frozen_vars_num |
| int | grow_excess |
| node_ptr * | index2name |
| int | index2name_size |
| int | input_vars_num |
| int * | log2phy |
| int | log_idx_capacity |
| int | max_allocated_time |
| int | max_used_phy_idx |
| hash_ptr | name2be |
| int * | phy2log |
| int | phy_idx_capacity |
| st_table * | shift_hash |
| int | state_vars_num |
| int * | subst_array |
| int | subst_array_size |
Related Functions | |
(Note that these are not member functions.) | |
| void | be_enc_deinit (BeEnc_ptr self) |
| void | be_enc_init (BeEnc_ptr self, SymbTable_ptr symb_table, BoolEnc_ptr bool_enc) |
| BeEnc_ptr | BeEnc_create (SymbTable_ptr symb_table, BoolEnc_ptr bool_enc) |
| The BeEnc class constructor. | |
| VIRTUAL void | BeEnc_destroy (BeEnc_ptr self) |
| The BeEnc class destructor. | |
| Be_Manager_ptr | BeEnc_get_be_manager (const BeEnc_ptr self) |
Returns the Boolean Expressions manager contained into the variable manager, to be used by any operation on BEs | |
| int | BeEnc_get_first_untimed_var_index (const BeEnc_ptr self, BeVarType type) |
| Call this to begin an iteration between a given category of variables. | |
| int | BeEnc_get_frozen_vars_num (const BeEnc_ptr self) |
Returns the number of frozen variables currently handled by the encoder. | |
| int | BeEnc_get_input_vars_num (const BeEnc_ptr self) |
Returns the number of input variables currently handled by the encoder. | |
| int | BeEnc_get_max_time (const BeEnc_ptr self) |
Returns the maximum allocated time | |
| int | BeEnc_get_next_var_index (const BeEnc_ptr self, int var_index, BeVarType type) |
| Use to sequentially iterate over a selected category of variables. | |
| int | BeEnc_get_state_vars_num (const BeEnc_ptr self) |
Returns the number of state variables currently handled by the encoder. | |
| int | BeEnc_get_var_index_with_offset (const BeEnc_ptr self, int from_index, int offset, BeVarType type) |
| Use to randomly iterate over a selected category of variables within the untimed block. | |
| int | BeEnc_get_vars_num (const BeEnc_ptr self) |
Returns the number of input and state variables currently handled by the encoder. | |
| node_ptr | BeEnc_index_to_name (const BeEnc_ptr self, const int index) |
| Given the index of a be var, returns the symbolic variable name. | |
| int | BeEnc_index_to_time (const BeEnc_ptr self, const int index) |
| Given a state or input variable index this returns the time the variable is allocated. | |
| be_ptr | BeEnc_index_to_timed (const BeEnc_ptr self, const int index, const int time) |
| Given an untimed variable index, returns the corresponding BE variable at the given time. | |
| int | BeEnc_index_to_untimed_index (const BeEnc_ptr self, const int index) |
| Given a timed variable index, returns the corresponding untimed BE variable index. | |
| be_ptr | BeEnc_index_to_var (const BeEnc_ptr self, const int index) |
| Given a variable index, returns the corresponding be variable. | |
| boolean | BeEnc_is_index_frozen_var (const BeEnc_ptr self, const int index) |
| Checks whether given index corresponds to a frozen variable. | |
| boolean | BeEnc_is_index_input_var (const BeEnc_ptr self, const int index) |
| Checks whether given index corresponds to an input variable. | |
| boolean | BeEnc_is_index_state_var (const BeEnc_ptr self, const int index) |
| Checks whether given index corresponds to a state variable. | |
| boolean | BeEnc_is_index_untimed (const BeEnc_ptr self, const int index) |
| Checks whether given index corresponds to an untimed variable. | |
| boolean | BeEnc_is_index_untimed_curr (const BeEnc_ptr self, const int index) |
| Checks whether given index corresponds to an untimed current state variable. | |
| boolean | BeEnc_is_index_untimed_curr_frozen_input (const BeEnc_ptr self, const int index) |
| Checks whether given index corresponds to an untimed current state variable, or an untimed frozen, or an untimed input variable. | |
| boolean | BeEnc_is_index_untimed_frozen (const BeEnc_ptr self, const int index) |
| Checks whether given index corresponds to an untimed frozen variable. | |
| boolean | BeEnc_is_index_untimed_input (const BeEnc_ptr self, const int index) |
| Checks whether given index corresponds to an untimed input variable. | |
| boolean | BeEnc_is_index_untimed_next (const BeEnc_ptr self, const int index) |
| Checks whether given index corresponds to an untimed next state variable. | |
| boolean | BeEnc_is_var_index_valid (const BeEnc_ptr self, int var_index) |
| Use to check whether an iteration over a set of variables is over. | |
| int | BeEnc_name_to_index (const BeEnc_ptr self, const node_ptr name) |
| Given the name of a be var, returns the untimed index that variable is allocated at. | |
| be_ptr | BeEnc_name_to_timed (const BeEnc_ptr self, const node_ptr name, const int time) |
| Given the name of an untimed variable, returns the corresponding BE variable at the given time. | |
| be_ptr | BeEnc_name_to_untimed (const BeEnc_ptr self, const node_ptr var_name) |
| Given the variable name, returns the corresponding BE untimed variable. | |
| be_ptr | BeEnc_shift_curr_to_next (BeEnc_ptr self, const be_ptr exp) |
| Shifts given current expression at next time | |
| be_ptr | BeEnc_untimed_expr_to_timed (BeEnc_ptr self, const be_ptr exp, const int time) |
| Shifts given untimed expression at the given time | |
| be_ptr | BeEnc_untimed_expr_to_times (BeEnc_ptr self, const be_ptr exp, const int ctime, const int ftime, const int itime, const int ntime) |
| Given an untimed expression, shifts current, frozen, input and next variables to given times. | |
| be_ptr | BeEnc_untimed_to_timed_and_interval (BeEnc_ptr self, const be_ptr exp, const int from, const int to) |
Makes an AND interval of given expression using range \[from, to\] | |
| be_ptr | BeEnc_untimed_to_timed_or_interval (BeEnc_ptr self, const be_ptr exp, const int from, const int to) |
Makes an OR interval of given expression using range \[from, to\] | |
| be_ptr | BeEnc_var_curr_to_next (const BeEnc_ptr self, const be_ptr curr) |
| Converts an untimed current state variable to the corresponding untimed variable in the next state untimed block. | |
| be_ptr | BeEnc_var_next_to_curr (const BeEnc_ptr self, const be_ptr next) |
| Converts an untimed next state variable to the corresponding untimed variable in the current state untimed block. | |
| int | BeEnc_var_to_index (const BeEnc_ptr self, const be_ptr var) |
| Given a be variable, returns the corresponding be index. | |
| node_ptr | BeEnc_var_to_name (const BeEnc_ptr self, be_ptr be_var) |
| Given a be variable, returns the correponding variable name. | |
| be_ptr | BeEnc_var_to_timed (const BeEnc_ptr self, const be_ptr var, const int time) |
| Given an untimed variable, returns the corresponding BE variable at the given time. | |
| be_ptr | BeEnc_var_to_untimed (const BeEnc_ptr self, const be_ptr var) |
| Given a timed or untimed variable, returns the corresponding BE variable in the current state untimed block (current state, frozen and input vars). | |
Private and protected interface of class 'BeEnc'.
Public interface of class 'BeEnc'.
BeEnc class definition derived from class BoolEncClient. This is the variables encoder for BMC. This class implements the boolean encoding for BMC, by providing variables groups and time-related functions. If the Boolean Expression (BE) layer provides actual access to variables, such as creation, shifting, substitution, expressions, etc., the BeEnc class provides the right semantics for those variables. The idea is to provide: 1. A structured layer for variables (encoding) 2. A set of functionalities to manage the variables.
The encoding is internally organized to provide efficient operations on generic BEs, like variables shifting and substitutions, and conversions between symbolic variables to BE variables, BE indices, etc.
The class BeEnc keeps and manages a set of encoded input, state and frozen variables that are committed as bunches within SymbLayers. The encoder keeps the relation between:
The management of the untimed and timed variables is allowed by the use of two separated levels, called the Physical Level and the Logical Level.
Physical Level
This level holds the actual BE variables, that are instantitated to represent both untimed and timed variables. The order the variables are organized must be considered as random and not directly controllable from outside the class BeEnc, but it is the physical level that will be seen when the indices of BE variables are manipulated. Since there is not visible structure which BE variables within the physical level are organized with, the user cannot assume anything about the indices. For this reason, special iterators are provided to iterate over a set of variables (for example, the set of state untimed vars).
Logical Level
This level provides the necessary structure to the physical level, and it is visible only from within the class BeEnc. Every operation that operates on BE variables will pass through the physical level at first, and then through the logical level. The class BeEnc provides the necessary support to pass from one level to the other, but it is necessary to remember that the logical level is NOT visible and accessible from outside the class.
The logical level is splitted into two distinct parts: 1.1 Untimed variables block. 1.2 Timed variables block.
1.1 Untimed variables block
Keeps the set of untimed (logical) BE variables, such that any (untimed) expression in term of BE will contain references to variables located in this logical block. This block is splitted into 4 sub-blocks, that group respectively untimed current state variables, frozen variables, input variables, and next state variables.
: current state variable @ : frozen variable = : input variable # : next state variable
--- -- -- --- @ == ### --- -- -- --- 012 34 56 789 : BE variable logical index 143 52 87 690 : BE variable physical index
The picture shows an example of a logical untimed variables block. The model contains 7 boolean variables (logical indices from 0..6), where logical indices 0..2 refer the state variables, indices 3 and 4 refer to frozen variables, and logical indices 5 and 6 refer the input variables. The set of state variables is than replicated to represent the next state variables, referred by logical indices 7..9 that constitutes the forth sub-block in the picture.
Notice that logical indices 0..9 refer a boolean variable allocated by the BE layer, that does not distinguish between state, input, frozen or next variables.
Also notice that BE variables are physically allocated at indices that can be completely different from the corresponding indices within the logical level. The class BeEnc keeps the relation between the logical and the physical level, and viceversa.
state frozen input next UNTIMED BLOCK |-------| |---| |---| |-------| 0 1 2 3 4 5 6 7 8 9 LOGICAL INDEX _______________________________________ | 1 | 4 | 3 | 5 | 2 | 8 | 7 | 6 | 9 | 0 | LOG->PHY LEVEL MAP --------------------------------------- | 9 | 0 | 4 | 2 | 1 | 3 | 7 | 6 | 5 | 8 | PHY->LOG LEVEL MAP ---------------------------------------
1.2 Timed variables block
Following the untimed logical variables block, the timed logical variables block holds the set of frozen, state and input variables that are instantiated at a given time. A BE expression instantiated at time t, will contain BE logical variables that belong to this block.
Timed vars block is logically splitted into separate frames, each of one corresponding to a given time t. The structure of each frame depends on the specific time t and on the number of transitions the model has. When the problem length k is 0, only frame from time 0 is allocated, and this frame is constituted by only state and frozen variables. In this condition the encoding structure (with untimed and timed blocks) would be this:
Untimed block Timed block |--------------------------------| |---------------| current frozen input next state 0 frozen 0 -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- | | | || | || | || | | | | | | || | | -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- 00 01 02 03 04 05 06 07 08 09 10 11 12 13 14 : logical indices 01 04 03 05 02 08 07 06 09 00 13 11 17 05 02 : physical indices
In the example BE logical indices 10..12 are allocated to keep current state variables and logical indices 13..14 to keep frozen variables at the initial state (time 0). Since there are no transitions, input variables are not allocated for this value of problem length k.
Frozen variables keep their values constant at all times. Thus to encode a frozen variable at any time it is enough to have just one (untimed) index. As result, new PHYSICAL indexes for frozen variables are introduced only in the untimed block. To enable more efficient time shifting, LOGICAL timed frames include frozen variables, but the corresponding physical indexes are the same as in the untimed block (see indexes 13..14 and 03..04, respectively, in the example). Thus just one BE variable is created for a given frozen variable at any time.
When problem length k=1, the encoding becomes:
Untimed block Timed block |--------------------------------| |---------------------------------------| current frozen input next state0 frozen0 input0 state1 frozen1 -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- | | | || | || | || | | | | | | || | || | || | | || | | -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- -- 00 01 02 03 04 05 06 07 08 09 10 11 12 13 14 15 16 17 18 19 20 21
Here 00..21 are logical indices, and the corresponding physical indices are not shown.
When k>0 the timed block is a sequence of state-frozen (input-state-frozen)+ timed sub-blocks. In the example above BE logical variables 15 and 16 have been added to encode input variables at time 0 (since there is a transition leading to time 1), and logical variables 17..19 and 20..21 have been added to encode state and frozen variables, respectively, at time 1.
When a generic, untimed BE expressions E is instantiated at time t (i.e. is shifted to time t), each current state variable occurring in E will be replaced by the corresponding BE logical variable in the timed sub-block t, as well any occurring input variable. Each next state variable will be replaced by the corresponding state variable located in the timed sub-block (t+1). Frozen variables during shifting always stay untimed.
It is important to notice that the problem length k must be strictly taken into account when shifting operations are performed. In particular, as there are not transitions outgoing the last state at time t=k, neither inputs nor next states can be shifted at time t=k.
From the logics point of view, when t=k inputs variables at time t do not exist at all (and the encoding directly maps this idea). Because of this, the logic value of input variables at time t=k is false.
See the class interface for further details on the provided features.
Definition of the public accessor for class BeEnc
| BeEnc::INHERITS_FROM | ( | BoolEncClient | ) |
| void be_enc_init | ( | BeEnc_ptr | self, | |
| SymbTable_ptr | symb_table, | |||
| BoolEnc_ptr | bool_enc | |||
| ) | [related] |
| BeEnc_ptr BeEnc_create | ( | SymbTable_ptr | symb_table, | |
| BoolEnc_ptr | bool_enc | |||
| ) | [related] |
| VIRTUAL void BeEnc_destroy | ( | BeEnc_ptr | self | ) | [related] |
| Be_Manager_ptr BeEnc_get_be_manager | ( | const BeEnc_ptr | self | ) | [related] |
Returns the Boolean Expressions manager contained into the variable manager, to be used by any operation on BEs
Warning: do not delete the returned instance of Be_Manager class, it belongs to self
None
Call this to begin an iteration between a given category of variables.
Use this method to begin an iteration between a given category of variables, for example the set of input variables, or the set of current and next state variables. The type is a bitwise OR combination of types. When the first index is obtained, following indices can be obtained by calling get_next_var_index, until is_var_index_valid returns false, that means that the iteration is over and must be given up.
None
| int BeEnc_get_frozen_vars_num | ( | const BeEnc_ptr | self | ) | [related] |
Returns the number of frozen variables currently handled by the encoder.
None
| int BeEnc_get_input_vars_num | ( | const BeEnc_ptr | self | ) | [related] |
Returns the number of input variables currently handled by the encoder.
None
| int BeEnc_get_max_time | ( | const BeEnc_ptr | self | ) | [related] |
Returns the maximum allocated time
None
Use to sequentially iterate over a selected category of variables.
Use this method to obtain the index of the variable that follows the variable whose index is provided. If the iteration is over, an invalid index will be returned. Use the method is_var_index_valid to check the validity of the returned index.
None
| int BeEnc_get_state_vars_num | ( | const BeEnc_ptr | self | ) | [related] |
Returns the number of state variables currently handled by the encoder.
None
| int BeEnc_get_var_index_with_offset | ( | const BeEnc_ptr | self, | |
| int | from_index, | |||
| int | offset, | |||
| BeVarType | type | |||
| ) | [related] |
Use to randomly iterate over a selected category of variables within the untimed block.
Use this method to obtain the index of the variable that follows the variable whose index is provided, after offset positions. If the iteration is over, an invalid index will be returned. Use the method is_var_index_valid to check the validity of the returned index.
None
| int BeEnc_get_vars_num | ( | const BeEnc_ptr | self | ) | [related] |
Returns the number of input and state variables currently handled by the encoder.
None
| node_ptr BeEnc_index_to_name | ( | const BeEnc_ptr | self, | |
| const int | index | |||
| ) | [related] |
Given the index of a be var, returns the symbolic variable name.
Current implementation requires that the variable belongs to the untimed block
None
| int BeEnc_index_to_time | ( | const BeEnc_ptr | self, | |
| const int | index | |||
| ) | [related] |
Given a state or input variable index this returns the time the variable is allocated.
The given state or input variable index must refer a timed variable.
If the given index refer to a frozen variable then BE_CURRENT_UNTIMED constant is returned (frozen variables are only allocated in the untimed block).
None
Given an untimed variable index, returns the corresponding BE variable at the given time.
This method expands the maximum allocated time if necessary.
WARNING: If the given index corresponds to an untimed next state var, the returned timed var will be instantitated at time+1
NOTE: Frozen variables are returned untimed as timed frozen variables are never instantiated.
None
| int BeEnc_index_to_untimed_index | ( | const BeEnc_ptr | self, | |
| const int | index | |||
| ) | [related] |
Given a timed variable index, returns the corresponding untimed BE variable index.
Returned index will refer either to an untimed current state variable, an untimed frozen variable or an untimed input variable.
None
Given a variable index, returns the corresponding be variable.
Current implementation requires that the variable index belongs to the untimed block
None
Checks whether given index corresponds to a frozen variable.
Checks whether given index corresponds to an input variable.
Input variables are in the input untimed block, or in timed input areas.
Checks whether given index corresponds to a state variable.
Valid state variables are in current and next state blocks, and in timed state areas.
Checks whether given index corresponds to an untimed variable.
Note: frozen variables are always untimed.
Checks whether given index corresponds to an untimed current state variable.
| boolean BeEnc_is_index_untimed_curr_frozen_input | ( | const BeEnc_ptr | self, | |
| const int | index | |||
| ) | [related] |
Checks whether given index corresponds to an untimed current state variable, or an untimed frozen, or an untimed input variable.
Checks whether given index corresponds to an untimed frozen variable.
Frozen variables are always untimed. So this function is exactly the same as BeEnc_is_index_frozen_var
Checks whether given index corresponds to an untimed input variable.
Checks whether given index corresponds to an untimed next state variable.
Use to check whether an iteration over a set of variables is over.
This method returns true whether the index returned by methods get_first_untimed_var_index, get_next_var_index and get_var_index_with_offset is valid and can be used later in the iteration. If false is returned, then the iteration is over.
None
| int BeEnc_name_to_index | ( | const BeEnc_ptr | self, | |
| const node_ptr | name | |||
| ) | [related] |
Given the name of a be var, returns the untimed index that variable is allocated at.
None
Given the name of an untimed variable, returns the corresponding BE variable at the given time.
This method expands the maximum allocated time if necessary.
WARNING: If the given variable name corresponds to an untimed next state var, the returned index will be instantitated at time+1
NOTE: Frozen variables are returned untimed as they are never allocated as timed variables.
None
Given the variable name, returns the corresponding BE untimed variable.
None
Shifts given current expression at next time
Warning: argument 'exp' must contain only untimed current state variables and untimed frozen variables, otherwise results will be unpredictible
Shifts given untimed expression at the given time
All next state variables will be shifted to time+1. Maximum time is extended if necessary. WARNING: argument 'exp' must contain only untimed variables, otherwise results will be unpredictible
| be_ptr BeEnc_untimed_expr_to_times | ( | BeEnc_ptr | self, | |
| const be_ptr | exp, | |||
| const int | ctime, | |||
| const int | ftime, | |||
| const int | itime, | |||
| const int | ntime | |||
| ) | [related] |
Given an untimed expression, shifts current, frozen, input and next variables to given times.
Shifts untimed current state vars to time ctime, frozen untimed vars to ftime, input untimed vars to itime, and untimed next state vars to ntime.
| be_ptr BeEnc_untimed_to_timed_and_interval | ( | BeEnc_ptr | self, | |
| const be_ptr | exp, | |||
| const int | from, | |||
| const int | to | |||
| ) | [related] |
Makes an AND interval of given expression using range \[from, to\]
Maximum time is extended if necessary.
| be_ptr BeEnc_untimed_to_timed_or_interval | ( | BeEnc_ptr | self, | |
| const be_ptr | exp, | |||
| const int | from, | |||
| const int | to | |||
| ) | [related] |
Makes an OR interval of given expression using range \[from, to\]
Maximum time is extended if necessary.
Converts an untimed current state variable to the corresponding untimed variable in the next state untimed block.
Given variable must be a current state untimed variable
None
Converts an untimed next state variable to the corresponding untimed variable in the current state untimed block.
Given variable must be a next state untimed variable
None
Given a be variable, returns the corresponding be index.
None
Given a be variable, returns the correponding variable name.
Current implementation requires the given be variable to be untimed
None
Given an untimed variable, returns the corresponding BE variable at the given time.
This method expands the maximum allocated time if necessary.
WARNING: If the given variable is an untimed next state, the returned index will be instantitated at time+1
NOTE: Frozen variables are returned untimed as they are always untimed.
None
Given a timed or untimed variable, returns the corresponding BE variable in the current state untimed block (current state, frozen and input vars).
None
| node_ptr* BeEnc::index2name |
| int* BeEnc::log2phy |
| hash_ptr BeEnc::name2be |
| int* BeEnc::phy2log |
| int* BeEnc::subst_array |
1.6.1
