SymbCache_create()
Class constructor
SymbCache_destroy()
Class destructor
SymbCache_get_actual_parameter_context()
Returns the context of the actual parameter associated with the given formal parameter
SymbCache_get_actual_parameter()
Returns the actual param of the given formal parameter
SymbCache_get_constants()
Returns the list of all declared constants
SymbCache_get_define_body()
Returns the body of the given DEFINE name
SymbCache_get_define_context()
Returns the context of the given DEFINE name
SymbCache_get_define_flatten_body()
Returns the flattenized body of the given DEFINE name
SymbCache_get_defines()
Returns the list of all DEFINEs
SymbCache_get_flatten_actual_parameter()
Returns the flattenized actual parameter of the given formal parameter
SymbCache_get_frozen_vars()
Returns the list of all declared frozen variables
SymbCache_get_function_context()
Returns the context of the given NFunction
SymbCache_get_functions()
Returns the list of all NFunctions
SymbCache_get_function()
Returns the NFunction instance of the given function name
SymbCache_get_i_symbols()
Returns the list of all input variables and those DEFINEs whose body refer directly or indirectly to input variables
SymbCache_get_input_vars()
Returns the list of all declared input variables
SymbCache_get_matrix_define_body()
Returns the body of the given MDEFINE name
SymbCache_get_matrix_define_context()
Returns the context of the given MDEFINE name
SymbCache_get_matrix_defines()
Returns the list of all MDEFINEs
SymbCache_get_parameters()
Returns the list of all formal parameters
SymbCache_get_sf_i_symbols()
Returns the list of those DEFINEs whose body refer directly or indirectly to both state(OR frozen) AND input variables
SymbCache_get_sf_symbols()
Returns the list of all state and frozen variables and those DEFINEs whose body refer directly or indirectly to that variables
SymbCache_get_state_frozen_vars()
Returns the list of all declared frozen and state variables
SymbCache_get_state_vars()
Returns the list of all declared state variables (this does not include the frozen variables)
SymbCache_get_symbol_type_type()
Returns the type of array variable, i.e. of symbol_type
SymbCache_get_symbol_types()
Returns the list of all ARRAY vars
SymbCache_get_var_type()
Returns the type of a given variable
SymbCache_get_vars()
Returns the list of all declared variables
SymbCache_is_symbol_constant()
Returns true if the given symbol is a declared constant
SymbCache_is_symbol_declared()
Returns true if the given symbol is declared
SymbCache_is_symbol_define()
Returns true if the given symbol is a declared DEFINE
SymbCache_is_symbol_frozen_var()
Returns true if the variable is frozen
SymbCache_is_symbol_function()
Returns true if the given symbol is a declared NFunction
SymbCache_is_symbol_input_var()
Returns true if the given symbol is an input variable.
SymbCache_is_symbol_matrix_define()
Returns true if the given symbol is a declared MDEFINE
SymbCache_is_symbol_parameter()
Returns true if the given symbol is a declared formal parameter
SymbCache_is_symbol_state_frozen_var()
Returns true if the variable is a frozen or a state variable
SymbCache_is_symbol_state_var()
Returns true if the given symbol is a state variable.
SymbCache_is_symbol_symbol_type()
Returns true if the given symbol is a declared array variable, i.e symbol type
SymbCache_is_symbol_var()
Returns true if the given symbol is either a state, a frozen or an input variable.
SymbCache_list_contains_input_var()
Returns true if var_list contains at least one input variable
SymbCache_list_contains_state_frozen_var()
Returns true if var_list contains at least one state or frozen variable
SymbCache_list_contains_undef_var()
Returns true if the given symbols list contains one or more undeclared variable names
SymbCache_new_constant()
Declares a new constant.
SymbCache_new_define()
Declares a new DEFINE.
SymbCache_new_frozen_var()
Declares a new frozen variable.
SymbCache_new_function()
Declares a new NFunction.
SymbCache_new_input_var()
Declares a new input variable.
SymbCache_new_matrix_define()
Declares a new MDEFINE.
SymbCache_new_parameter()
Declares a new module parameter.
SymbCache_new_state_var()
Declares a new state variable.
SymbCache_new_symbol_type()
Declares a new ARRAY var.
SymbCache_redeclare_state_as_frozen_var()
Redeclare a state variable as a frozen variable
SymbCache_remove_constant()
Removes a constant from the cache of symbols, and from the flattener module
SymbCache_remove_define()
Removes a DEFINE from the cache of symbols, and from the flattener define hash
SymbCache_remove_function()
Removes an NFunction from the cache of symbols
SymbCache_remove_parameter()
Removes a parameter from the cache of symbols
SymbCache_remove_var()
Removes a variable from the cache of symbols, and from the flattener module
SymbCache_resolve_define_chain()
Returns the last non atomic element of a chain of defines
SymbLayer_can_declare_constant()
Call this method to know if a new constant can be declared within this layer.
SymbLayer_can_declare_define()
Call this method to know if a new DEFINE can be declared within this layer.
SymbLayer_can_declare_function()
Call this method to know if a new NFunction can be declared within this layer.
SymbLayer_can_declare_matrix_define()
Call this method to know if a new MDEFINE can be declared within this layer.
SymbLayer_can_declare_parameter()
Call this method to know if a new parameter can be declared within this layer.
SymbLayer_can_declare_symbol_type()
Call this method to know if a new symbol_type can be declared within this layer.
SymbLayer_can_declare_var()
Call this method to know if a new variable can be declared within this layer.
SymbLayer_committed_to_enc()
Called every time an instance is committed within an encoding.
SymbLayer_create()
Class SymbLayer constructor
SymbLayer_declare_constant()
Insert a new constant
SymbLayer_declare_define()
Insert a new DEFINE
SymbLayer_declare_frozen_var()
Insert a new frozen variable
SymbLayer_declare_function()
Insert a new NFunction
SymbLayer_declare_input_var()
Insert a new input variable
SymbLayer_declare_matrix_define()
Insert a new matrix MDEFINE
SymbLayer_declare_parameter()
Insert a new formal parameters
SymbLayer_declare_state_var()
Insert a new state variable
SymbLayer_declare_symbol_type()
Insert a new symbol-type association, i.e. array var
SymbLayer_destroy()
Class SymbLayer destructor
SymbLayer_get_all_symbols()
Returns the entire list of symbols (constants, variables, etc.) declared in this layer
SymbLayer_get_all_vars()
Returns the entire list of variables declared in this layer
SymbLayer_get_bool_frozen_vars_num()
Returns the number of declared boolean frozen variables
SymbLayer_get_bool_frozen_vars()
Returns the list of declared boolean frozen variables declared in this layer
SymbLayer_get_bool_input_vars_num()
Returns the number of declared boolean input variables
SymbLayer_get_bool_input_vars()
Returns the list of declared boolean input variables declared in this layer
SymbLayer_get_bool_state_vars_num()
Returns the number of declared boolean state variables
SymbLayer_get_bool_state_vars()
Returns the list of declared boolean state variables declared in this layer
SymbLayer_get_bool_vars()
Returns the list of boolean variables declared in this layer
SymbLayer_get_constants_num()
Returns the number of declared contants
SymbLayer_get_constants()
Returns the list of declared contants
SymbLayer_get_defines_num()
Returns the number of DEFINEs.
SymbLayer_get_defines()
Returns the list of DEFINEs.
SymbLayer_get_frozen_vars_num()
Returns the number of declared frozen variables.
SymbLayer_get_frozen_vars()
Returns the list of frozen variables declared in this layer
SymbLayer_get_functions_num()
Returns the number of NFunctions.
SymbLayer_get_functions()
Returns the list of NFunctions.
SymbLayer_get_input_vars_num()
Returns the number of declared input variables
SymbLayer_get_input_vars()
Returns the list of input variables declared in this layer
SymbLayer_get_insert_policy()
Returns the policy that must be adopted to stack this layer into a layers stack, within a SymbTable instance
SymbLayer_get_matrix_defines_num()
Returns the number of MDEFINEs.
SymbLayer_get_matrix_defines()
Returns the list of MDEFINEs.
SymbLayer_get_name()
Returns the name self had been registered with.
SymbLayer_get_parameters_num()
Returns the number of parameters.
SymbLayer_get_parameters()
Returns the list of parameters.
SymbLayer_get_state_frozen_vars()
Returns the list of frozen and state variables declared in this layer
SymbLayer_get_state_vars_num()
Returns the number of declared state variables.
SymbLayer_get_state_vars()
Returns the list of state variables declared in this layer
SymbLayer_get_symbol_types_num()
Returns the number of Symbol Types.
SymbLayer_get_symbol_types()
Returns the list of the symbol types declared in this layer
SymbLayer_is_symbol_in_layer()
Returns true if the symbol is defined in the layer.
SymbLayer_is_variable_in_layer()
Returns true if the variable is defined in the layer.
SymbLayer_must_insert_before()
Compares the insertion policies of self and other, and returns true if self must be inserted *before* other
SymbLayer_redeclare_state_as_frozen_var()
Redeclare a state variable as a frozen variable
SymbLayer_remove_define()
Removes a previously declared DEFINE
SymbLayer_remove_function()
Removes a previously declared NFunction
SymbLayer_remove_var()
Removes a variable previously delcared
SymbLayer_removed_from_enc()
Called every time an instance is removed from an encoding.
SymbLayer_set_name()
Sets the layer name.
SymbTablePkg_array_type()
returns an array type.
SymbTablePkg_boolean_enum_type()
returns a boolean enum type
SymbTablePkg_boolean_set_type()
returns a boolean-set type.
SymbTablePkg_error_type()
returns an Error-type.
SymbTablePkg_init()
Initialises the class package.
SymbTablePkg_int_symbolic_enum_type()
returns a enum type containing integers AND symbolic constants
SymbTablePkg_integer_set_type()
returns a integer-set type.
SymbTablePkg_integer_symbolic_set_type()
returns a integer-symbolic-set type.
SymbTablePkg_integer_type()
returns an Integer type.
SymbTablePkg_no_type()
returns a no-type
SymbTablePkg_pure_int_enum_type()
returns a pure integer enum type
SymbTablePkg_pure_symbolic_enum_type()
returns a pure symbolic enum type.
SymbTablePkg_quit()
Shut down the package.
SymbTablePkg_real_type()
returns a Real type.
SymbTablePkg_signed_word_type()
returns a signed Word type (with a given width)
SymbTablePkg_statement_type()
returns a no-type
SymbTablePkg_string_type()
returns a String type.
SymbTablePkg_symbolic_set_type()
returns a symbolic-set type.
SymbTablePkg_unsigned_word_type()
returns an unsigned Word type (with a given width)
SymbTablePkg_wordarray_type()
Returns a WordArray type (given array width and value width)
SymbTable_copy()
Create a new SymbolTable which contains the same info as the given one except the specified symbols in blacklist
SymbTable_create_layer_class()
Declares a new class of layers
SymbTable_create_layer()
Creates and adds a new layer
SymbTable_create()
Class constructor
SymbTable_define_get_layer()
Returns the layer a DEFINE is defined in.
SymbTable_destroy()
Class destructor
SymbTable_function_get_layer()
Returns the layer a NFunction is defined in.
SymbTable_get_actual_parameter_context()
Returns the context of the actual parameter associated with the given formal one
SymbTable_get_actual_parameter()
Returns the actual param of the given formal parameter
SymbTable_get_class_layer_names()
Returns an array of layer names that belong to the given class name. If class_name is NULL, default class name will be taken (must be set before).
SymbTable_get_class_of_layer()
Returns the name of the class in which the given layer is declared or NULL if there is no such a class.
SymbTable_get_constants_num()
Returns the number of all declared constants
SymbTable_get_constants()
Returns the list of all declared constants
SymbTable_get_default_layers_class_name()
Returns the default layers class name that has been previously set. The default layers class name is the class of layers that is taken when the system needs a default set of layers to work with. Typically the default class is the class of model layers, that is used for example when dumping the hierarchy by command write_bool_model.
SymbTable_get_define_body()
Returns the body of the given DEFINE
SymbTable_get_define_context()
Returns the context of the given DEFINE name
SymbTable_get_define_flatten_body()
Returns the flattenized body of the given define
SymbTable_get_defines()
Returns the list of all DEFINEs
SymbTable_get_determinization_var_name()
Returns a valid name for a new determinization variable
SymbTable_get_flatten_actual_parameter()
Returns the flattenized actual parameter of the given formal parameter
SymbTable_get_fresh_symbol_name()
Given a tplate, returns a fresh symbol name. This function NEVER returns the same symbol twice and NEVER returns a declared name
SymbTable_get_frozen_vars_num()
Returns the number of all declared frozen variables
SymbTable_get_frozen_vars()
Returns the list of all declared frozen variables
SymbTable_get_function_context()
Returns the context of the NFunction with the given name
SymbTable_get_functions_num()
Returns the number of all NFunctions
SymbTable_get_functions()
Returns the list of all NFunctions
SymbTable_get_function()
Returns the NFunction with the given name
SymbTable_get_i_symbols()
Returns the list of all input variables and those DEFINEs whose body refer directly or indirectly to input variables
SymbTable_get_input_vars_num()
Returns the number of all declared input variables
SymbTable_get_input_vars()
Returns the list of all declared input variables
SymbTable_get_layers_i_symbols()
Returns the list of input symbols that belong to the given layers
SymbTable_get_layers_i_vars()
Returns the list of input variables that belong to the given layers
SymbTable_get_layers_sf_i_symbols()
Returns the list of state and input symbols that belong to the given layers, meaning those DEFINES whose body contain both state (or frozen) and input variables. This methods does _NOT_ return the state symbols plus the input symbols.
SymbTable_get_layers_sf_i_vars()
Returns the list of variables that belong to the given layers
SymbTable_get_layers_sf_symbols()
Returns the list of state and frozen symbols that belong to the given layers
SymbTable_get_layers_sf_vars()
Returns the list of state and frozen variables that belong to the given layers
SymbTable_get_layers()
Returns the list of owned layers.
SymbTable_get_layer()
Given its name, returns a layer
SymbTable_get_matrix_define_body()
Returns the body of the given MDEFINE name
SymbTable_get_matrix_define_context()
Returns the context of the given MDEFINE name
SymbTable_get_matrix_define_flatten_body()
Returns the flattened body of the given MDEFINE name
SymbTable_get_matrix_defines()
Returns the list of all MDEFINEs
SymbTable_get_parameters_num()
Returns the number of all parameters
SymbTable_get_parameters()
Returns the list of all parameters
SymbTable_get_sf_i_symbols()
Returns the list of those DEFINEs whose body refer directly or indirectly to both state (or frozen) and input variables
SymbTable_get_sf_symbols()
Returns the list of all state and frozen variables and those DEFINEs whose body refer directly or indirectly to state and frozen variables
SymbTable_get_simplification_hash()
Returns a hash which can be used only in Expr_simplify.
SymbTable_get_state_frozen_vars()
Returns the list of all declared frozen and state variables
SymbTable_get_state_vars_num()
Returns the number of all declared state variables
SymbTable_get_state_vars()
Returns the list of all declared state variables
SymbTable_get_symbol_category()
This function returns the category of an identifier
SymbTable_get_symbol_type_type()
Returns the body of the given MDEFINE name
SymbTable_get_symbol_types()
Returns the list of all SymbolTypes
SymbTable_get_type_checker()
Returns the internally stored type checker
SymbTable_get_var_type()
Returns the type of a given variable
SymbTable_get_vars_num()
Returns the number of all declared variables
SymbTable_get_vars()
Returns the list of all declared variables
SymbTable_is_layer_in_class()
Returns true if given layer name belongs to the given class
SymbTable_is_symbol_bool_var()
Returns true if the given symbol is a variable of enum type with the values 0 and 1 (boolean)
SymbTable_is_symbol_constant()
Returns true if the given symbol is a declared constant
SymbTable_is_symbol_declared()
Returns true if the given symbol is declared
SymbTable_is_symbol_define()
Returns true if the given symbol is a declared DEFINE
SymbTable_is_symbol_frozen_var()
Returns true if the given symbol is a frozen variable.
SymbTable_is_symbol_function()
Returns true if the given symbol is a declared NFunction
SymbTable_is_symbol_input_var()
Returns true if the given symbol is an input variable.
SymbTable_is_symbol_matrix_define()
Returns true if the given symbol is a declared MDEFINE
SymbTable_is_symbol_parameter()
Returns true if the given symbol is a declared parameter
SymbTable_is_symbol_state_frozen_var()
Returns true if the given symbol is a frozen or a state variable.
SymbTable_is_symbol_state_var()
Returns true if the given symbol is a state variable.
SymbTable_is_symbol_symbol_type()
Returns true if the given symbol is a declared Symbol Type
SymbTable_is_symbol_var()
Returns true if the given symbol is either a state, frozen or an input variable.
SymbTable_is_var_finite()
Returns true if the given variable has a finite domain
SymbTable_layer_add_to_class()
Adds a given layer (that must exist into self already) to a class of layers. Classes are used to group layers into possibly overlapping sets. For example the class of layers containing the set of symbols that belongs to the SMV model. If class_name is NULL, the default class name will be taken (must be set before)
SymbTable_layer_class_exists()
Checks if a class of layers exists
SymbTable_layer_remove_from_class()
Removes a given layer (that must exist into self already) from a given class of layers. If class_name is NULL, the default class is taken (must be set before)
SymbTable_list_contains_input_var()
Returns true if var_list contains at least one input variable, false otherwise
SymbTable_list_contains_state_frozen_var()
Returns true if var_list contains at least one state or frozen variable, false otherwise
SymbTable_list_contains_undef_var()
Returns true if the given symbols list contains one or more undeclared variable names, false otherwise
SymbTable_remove_layer()
Removes and destroys a layer
SymbTable_rename_layer()
Renames an existing layer
SymbTable_resolve_define_chain()
Returns the last element of a chain of define
SymbTable_set_default_layers_class_name()
Returns the default layers class name that has been previously set. The default layers class name is the class of layers that is taken when the system needs a default set of layers to work with. Typically the default class is the class of model layers, that is used for example when dumping the hierarchy by command write_bool_model.
SymbTable_symbol_get_layer()
Returns the layer a symbol is defined in.
SymbTable_variable_get_layer()
Returns the layer a variable is defined in.
SymbType_calculate_type_size()
The function calculate how many bits is required to store a value of a given type
SymbType_convert_right_to_left()
Returns the left type, if the right one can be implicitly converted to the left one. NULL - otherwise
SymbType_copy()
Class SymbType copy-constructor
SymbType_create_array()
Class SymbType constructor for array types only
SymbType_create_memory_sharing_array_type()
Private class SymbType constructor for memory sharing array type instances
SymbType_create_memory_sharing_type()
Private class SymbType constructor for memory sharing type instances
SymbType_create()
Class SymbType constructor
SymbType_destroy_memory_sharing_type()
Private Class SymbType destructor for memory sharing instances of types.
SymbType_destroy()
Class SymbType destructor
SymbType_equals()
True if and only if the given types are equal, the given types can be memory-sharing or not.
SymbType_generate_all_word_values()
Generates and returns a list of all possible values of a particular Unsigned Word type
SymbType_get_array_lower_bound()
Get array lower bound
SymbType_get_array_subtype()
Get inner type of an array
SymbType_get_array_upper_bound()
Get array upper bound
SymbType_get_enum_type_values()
Returns the list of values of an enum type
SymbType_get_greater()
Returns one of the given types, if the other one can be implicitly converted to the former one. Otherwise - Nil.
SymbType_get_minimal_common()
Returns the minimal type to which the both given types can be converted, or Nil if there is none.
SymbType_get_tag()
Returns the tag (the kind) of the type
SymbType_get_word_line_number()
Returns the line number where the type was declared.
SymbType_get_word_width()
Returns the width of a Word type
SymbType_get_wordarray_awidth()
Returns the width of the address in a WordArray type
SymbType_get_wordarray_vwidth()
Returns the width of the value in a WordArray type
SymbType_is_array()
Returns true if the type is an array-type, or else returns false
SymbType_is_back_comp()
returns true if the given type is "backward compatible", i.e. a enum or integer type.
SymbType_is_boolean_enum()
Returns true, if the type is a enum-type and its values are from boolean range. Otherwise - returns false.
SymbType_is_enum()
Returns true if the type is a enum-type, or else returns false
SymbType_is_error()
Returns true, if the type is a error-type, and false otherwise.
SymbType_is_infinite_precision()
Returns true, if the type is one of infinite-precision types
SymbType_is_int_symbolic_enum()
Returns true, if the type is a enum-type and its value are symbolic AND integer constants. Otherwise - returns false.
SymbType_is_integer()
Returns true if the type is a integer-type, or else returns false
SymbType_is_memory_shared()
True if and only if the given type is memory shared
SymbType_is_pure_int_enum()
Returns true, if the type is a enum-type and its value are integers only. Otherwise - returns false.
SymbType_is_pure_symbolic_enum()
Returns true, if the type is a enum-type and its value are symbolic constants only. Otherwise - returns false.
SymbType_is_real()
Returns true if the type is a real-type, or else returns false
SymbType_is_set()
Returns true, if the type is one of the set-types, i.e. boolean-set, integer-set, symbolic-set, integer-symbolic-set, and false otherwise.
SymbType_is_signed_word()
Returns true, if the type is a signed Word type
SymbType_is_statement()
Returns true, if the type is a statement-type, and false otherwise.
SymbType_is_string()
Returns true, if the type is a String type
SymbType_is_unsigned_word()
Returns true, if the type is an unsigned Word type
SymbType_is_word_1()
Returns true, if the type is a Unsigned Word type and the width of the word is 1. Otherwise - returns false.
SymbType_is_wordarray()
Returns true if the given type is a wordarray
SymbType_is_word()
Returns true, if the type is a Word type (signed or unsigned)
SymbType_make_from_set_type()
This function is opposite to SymbType_make_set_type, i.e. if the given type is one of the set-types, then the type without "set" suffix is returned. Otherwise the type is returned without change.
SymbType_make_memory_shared()
This function takes a NOT memory shared type and returns a memory shared one.
SymbType_make_set_type()
Returns a minimal set-type which the given type can be implicitly converted to, or NULL if this is impossible.
SymbType_print()
Prints the type structure to the output stream.
_resolve_define_chain_is_constant()
Returns true if the expression is a constant, otherwise it returns false
_resolve_define_chain()
Recursively get rid of chain of defines.
class_layers_hash_free()
Private destructor used by clas destroyer
node_equal()
Equality function for node_ptr, used to compare bodies of types in SymbType_equal.
symb_cache_define_to_symbols_lists()
Used to update symbols lists when a DEFINE is declared. The given DEFINE will be added to one of state, input or state-input symbols lists.
symb_cache_deinit()
Private deinitializer
symb_cache_init()
Private initializer
symb_cache_lookup_symbol()
Returns the definition of the given symbol
symb_cache_new_symbol()
Insert a new value in the symbol hash
symb_cache_remove_symbol()
Removes any reference of the given symbol from the cache, and from the flattener internal hashes as well
symb_cache_resolve_pending_defines()
If there are pending DEFINEs that wait for an assignment within the lists of state, input and state-input symbols list, they are resolved and assigned.
symb_layer_deinit()
Private method called by the destructor
symb_layer_init()
Private method called by the constructor
symb_table_create_layers_class()
Internal service used by methods that handle layer classes
symb_table_deinit()
Private deinitializer
symb_table_detect_expr_category()
Returns the type of a define.
symb_table_filter_layer_symbols()
Given a list of symbols, returns a new list that contains only those symbols that have been declared within the model layer
symb_table_filter_layers_symbols()
Given a list of symbols and a list of layers names, returns a new list that contains only those symbols that have been declared within the given layers
symb_table_get_layers_class()
Internal service used by methods that handle layer classes
symb_table_get_layers_from_class()
Internal service used by methods that handle layer classes
symb_table_init()
Private initializer
symb_table_layer_exists()
Returns true if the given name corresponds to an already registered layer.
symb_table_layer_rename_in_class()
Removes or rename a given layer inside the given layers class. If class_name is NULL, then default class is taken (must be set before)
symb_table_types_hash_cleaner()
The function is used to free the memory from memory-sharing Word/WordArray/Array types stored in the hash table symb_table_..._type_hash. Used in the SymbTablePkg_quit only
()
Internal service used by SymbTable_get_matrix_define_flatten_body

Last updated on 2010/05/19 15h:56