Private and protected interface of class 'BoolEnc'. More...
#include <BoolEnc_private.h>
Public Member Functions | |
| INHERITS_FROM (BaseEnc) | |
Data Fields | |
| hash_ptr | var2enc |
| hash_ptr | var2mask |
Related Functions | |
(Note that these are not member functions.) | |
| void | bool_enc_deinit (BoolEnc_ptr self) |
| void | bool_enc_init (BoolEnc_ptr self, SymbTable_ptr symb_table) |
| BoolEnc_ptr | BoolEnc_create (SymbTable_ptr symb_table) |
| The BoolEnc class constructor. | |
| VIRTUAL void | BoolEnc_destroy (BoolEnc_ptr self) |
| The BoolEnc class destructor. | |
| int | BoolEnc_get_index_from_bit (const BoolEnc_ptr self, node_ptr name) |
| Returns the index of given bit. | |
| node_ptr | BoolEnc_get_scalar_var_from_bit (const BoolEnc_ptr self, node_ptr name) |
| Returns the name of the scalar variable whose the given bit belongs. | |
| node_ptr | BoolEnc_get_value_from_var_bits (const BoolEnc_ptr self, const BitValues_ptr bit_values) |
| Given a BitValues instance already set with an assigments for its bits, returns the corresponding value for the scalar or word variable whose bits are contained into the BitValues instance. | |
| node_ptr | BoolEnc_get_values_bool_encoding (const BoolEnc_ptr self, node_ptr values, Set_t *bits) |
| Given a set of constants values (for example, the domain of a scalar variable), calculates its boolean encoding by introducing boolean symbols that are returned along with the resulting encoding. | |
| NodeList_ptr | BoolEnc_get_var_bits (const BoolEnc_ptr self, node_ptr name) |
| Returns the list of boolean vars used in the encoding of given scalar var. | |
| node_ptr | BoolEnc_get_var_encoding (const BoolEnc_ptr self, node_ptr name) |
| Given a variable, returns its boolean encoding. | |
| node_ptr | BoolEnc_get_var_mask (const BoolEnc_ptr self, node_ptr name) |
| Given a variable, it returns the mask of its encoding. | |
| boolean | BoolEnc_is_var_bit (const BoolEnc_ptr self, node_ptr name) |
| Returns true if the given symbol is the name of a bit variable that is part of a scalar var. | |
| boolean | BoolEnc_is_var_scalar (const BoolEnc_ptr self, node_ptr name) |
| Returns true if the given symbol is the name of a scalar (non-boolean) variable. | |
| node_ptr | BoolEnc_make_var_bit (const BoolEnc_ptr self, node_ptr name, int index) |
| Given a scalar variable name, construct the name for the nth-indexed bit. | |
| const char * | BoolEnc_scalar_layer_to_bool_layer (const BoolEnc_ptr self, const char *layer_name) |
| Given the name of a scalar layer, a name of the corresponding boolean layer is returned. | |
Private and protected interface of class 'BoolEnc'.
Public interface of class 'BoolEnc'.
BoolEnc class definition derived from class BaseEnc
Definition of the public accessor for class BoolEnc
| BoolEnc::INHERITS_FROM | ( | BaseEnc | ) |
| void bool_enc_deinit | ( | BoolEnc_ptr | self | ) | [related] |
| void bool_enc_init | ( | BoolEnc_ptr | self, | |
| SymbTable_ptr | symb_table | |||
| ) | [related] |
| BoolEnc_ptr BoolEnc_create | ( | SymbTable_ptr | symb_table | ) | [related] |
The BoolEnc class constructor.
AutomaticStart
The BoolEnc class constructor
| VIRTUAL void BoolEnc_destroy | ( | BoolEnc_ptr | self | ) | [related] |
| int BoolEnc_get_index_from_bit | ( | const BoolEnc_ptr | self, | |
| node_ptr | name | |||
| ) | [related] |
Returns the index of given bit.
The given var MUST be a bit
| node_ptr BoolEnc_get_scalar_var_from_bit | ( | const BoolEnc_ptr | self, | |
| node_ptr | name | |||
| ) | [related] |
Returns the name of the scalar variable whose the given bit belongs.
Returns the name of the scalar variable whose the given bit belongs. The given var MUST be a bit
| node_ptr BoolEnc_get_value_from_var_bits | ( | const BoolEnc_ptr | self, | |
| const BitValues_ptr | bit_values | |||
| ) | [related] |
| node_ptr BoolEnc_get_values_bool_encoding | ( | const BoolEnc_ptr | self, | |
| node_ptr | values, | |||
| Set_t * | bits | |||
| ) | [related] |
Given a set of constants values (for example, the domain of a scalar variable), calculates its boolean encoding by introducing boolean symbols that are returned along with the resulting encoding.
This method can be used to retrieve the boolean encoding of a given set of symbols.
For example, it may be used to calculate the boolean encoding representing the domain of a scalar variable which has not been added to any layer. It returns the boolean encoding (typically a ITE node) and the set of boolean symbols (bits) that have been introduced in the encoding. Important: the introduced boolean symbols are not variables, as they are not declared into the symbol table. It is up to the caller later to declare them if needed.
The introduced symbol names are guaranteed to be not among the currently declared symbols.
To retrieve the boolean encoding of an existing (and committed) variable, use method get_var_encoding instead.
Passed set is filled with symbol bits occurring in the encoding. No memoization or change is performed.
| NodeList_ptr BoolEnc_get_var_bits | ( | const BoolEnc_ptr | self, | |
| node_ptr | name | |||
| ) | [related] |
Returns the list of boolean vars used in the encoding of given scalar var.
Returned list must be destroyed by the caller
| node_ptr BoolEnc_get_var_encoding | ( | const BoolEnc_ptr | self, | |
| node_ptr | name | |||
| ) | [related] |
Given a variable, returns its boolean encoding.
Given variable must have been encoded by self
| node_ptr BoolEnc_get_var_mask | ( | const BoolEnc_ptr | self, | |
| node_ptr | name | |||
| ) | [related] |
Given a variable, it returns the mask of its encoding.
Returns an expression representing the mask that removes repetitions of leaves in a variable encoding by assigning value false to don't care boolean variables.Forr Boolean variables it returns the expression TRUE. Similarly for Word variables (since for words there are non redundant assignments).
As an example of what this function does, let us consider a variable x having range 0..4. It can be encoded with 3 bits are needed to encode it: x0, x1, x2. The encodeding performed by NuSMV is
ITE(x0, ITE(x1, 1, 3), ITE(x1, 2, ITE(x2, 4, 0))).
Thus x=2 corresponds to assignment !x0&x1 where x2 is a dont'care. Similarly for x=1 and x=3 (for x=0 and x=4) there is a unique complete assignment to the x0, x1, x2 variables that represent the respective encoding). This function fixes a value for x2 in the assignments representing x=2, x=1 and x=3 respectively (it force x2 to be false). Thus it builds the formula in this case:
ITE(x0, ITE(x2, 0, 1), ITE(x1, 1, ITE(x2, 0, 1)))
that removes the redundant assignments where needed.
Result is memoized. See issue 0925 for further details.
| boolean BoolEnc_is_var_bit | ( | const BoolEnc_ptr | self, | |
| node_ptr | name | |||
| ) | [related] |
Returns true if the given symbol is the name of a bit variable that is part of a scalar var.
| boolean BoolEnc_is_var_scalar | ( | const BoolEnc_ptr | self, | |
| node_ptr | name | |||
| ) | [related] |
Returns true if the given symbol is the name of a scalar (non-boolean) variable.
| node_ptr BoolEnc_make_var_bit | ( | const BoolEnc_ptr | self, | |
| node_ptr | name, | |||
| int | index | |||
| ) | [related] |
Given a scalar variable name, construct the name for the nth-indexed bit.
Constructs and returns the name of the nth-indexed bit of the given scalar variable
| const char * BoolEnc_scalar_layer_to_bool_layer | ( | const BoolEnc_ptr | self, | |
| const char * | layer_name | |||
| ) | [related] |
Given the name of a scalar layer, a name of the corresponding boolean layer is returned.
Returned string should NOT be modified or freed.
| hash_ptr BoolEnc::var2enc |
| hash_ptr BoolEnc::var2mask |
1.6.1
