#include "nusmv/core/utils/utils.h"#include "nusmv/core/enc/bool/BoolEnc.h"#include "nusmv/core/enc/bdd/BddEnc.h"#include "nusmv/core/enc/be/BeEnc.h"#include "nusmv/core/utils/StreamMgr.h"Go to the source code of this file.
Enumerations | |
| enum | BddSohEnum { BDD_STATIC_ORDER_HEURISTICS_NONE, BDD_STATIC_ORDER_HEURISTICS_BASIC, BDD_STATIC_ORDER_HEURISTICS_ERROR } |
| enum | VarsOrdType { VARS_ORD_INPUTS_BEFORE, VARS_ORD_INPUTS_AFTER, VARS_ORD_TOPOLOGICAL, VARS_ORD_INPUTS_BEFORE_BI, VARS_ORD_INPUTS_AFTER_BI, VARS_ORD_TOPOLOGICAL_BI, VARS_ORD_UNKNOWN } |
Public API for the enc package. Basically methods for accessing global encodings are provided here. More... | |
Functions | |
| const char * | Enc_bdd_static_order_heuristics_to_string (BddSohEnum) |
| Returns the string corresponding to give parameter. | |
| int | Enc_clean_evaluation_cache (NuSMVEnv_ptr env, BddEnc_ptr enc) |
| Top level function for resetting the evaluation self of the bdd encoder. | |
| const char * | Enc_get_valid_bdd_static_order_heuristics (void) |
| Returns a string of all possible values for bdd_static_order_heuristics. | |
| const char * | Enc_get_valid_vars_ord_types (void) |
| Returns a string of all possible values for vars_ord_type. | |
| void | Enc_init_bdd_encoding (NuSMVEnv_ptr env, const char *input_order_file_name) |
| Initializes the bdd enc for the given environment. | |
| void | Enc_init_be_encoding (NuSMVEnv_ptr env) |
| Initializes the be enc for this session. | |
| void | Enc_init_bool_encoding (NuSMVEnv_ptr env) |
| Initializes the boolean encoding for this session. | |
| void | Enc_init_encodings (NuSMVEnv_ptr env) |
| Initializes the encoding package. | |
| void | Enc_quit_encodings (NuSMVEnv_ptr env) |
| Call to destroy all encodings, when session ends. | |
| BddSohEnum | Enc_string_to_bdd_static_order_heuristics (const char *) |
| Converts a string to the corresponding BDD Static Order Heuristics. | |
| VarsOrdType | Enc_string_to_vars_ord (const char *, StreamMgr_ptr) |
| Converts a string to the corresponding var order type. | |
| const char * | Enc_vars_ord_to_string (VarsOrdType) |
| Returns the string corresponding to give parameter. | |
| enum BddSohEnum |
| enum VarsOrdType |
Public API for the enc package. Basically methods for accessing global encodings are provided here.
| const char* Enc_bdd_static_order_heuristics_to_string | ( | BddSohEnum | ) |
Returns the string corresponding to give parameter.
Returned string does not have to be freed
| int Enc_clean_evaluation_cache | ( | NuSMVEnv_ptr | env, | |
| BddEnc_ptr | enc | |||
| ) |
Top level function for resetting the evaluation self of the bdd encoder.
| const char* Enc_get_valid_bdd_static_order_heuristics | ( | void | ) |
Returns a string of all possible values for bdd_static_order_heuristics.
Returned string does not have to be freed
| const char* Enc_get_valid_vars_ord_types | ( | void | ) |
Returns a string of all possible values for vars_ord_type.
Returned string does not have to be freed
| void Enc_init_bdd_encoding | ( | NuSMVEnv_ptr | env, | |
| const char * | input_order_file_name | |||
| ) |
Initializes the bdd enc for the given environment.
| void Enc_init_be_encoding | ( | NuSMVEnv_ptr | env | ) |
Initializes the be enc for this session.
| void Enc_init_bool_encoding | ( | NuSMVEnv_ptr | env | ) |
Initializes the boolean encoding for this session.
Call it to initialize for the current session the encoding, before flattening. In the current implementation, you must call this *before* the flattening phase. After the flattening, you must initialize the bdd encoding as well. Don't forget to call Enc_quit_encodings when the session ends.
| void Enc_init_encodings | ( | NuSMVEnv_ptr | env | ) |
Initializes the encoding package.
This function initializes only data-structures global to all encoding. To initialize particular incoding, you have to invoke corresponding init-functions, such as Enc_init_bool_encoding, etc.
| void Enc_quit_encodings | ( | NuSMVEnv_ptr | env | ) |
Call to destroy all encodings, when session ends.
Call to destroy encodings, when session ends. Enc_init_encodings had to be called before calling this function.
| BddSohEnum Enc_string_to_bdd_static_order_heuristics | ( | const char * | ) |
Converts a string to the corresponding BDD Static Order Heuristics.
BDD_STATIC_ORDER_HEURISTICS_ERROR is returned when the string does not match the given string
| VarsOrdType Enc_string_to_vars_ord | ( | const char * | , | |
| StreamMgr_ptr | ||||
| ) |
Converts a string to the corresponding var order type.
VARS_ORD_UNKNOWN is returned when the string does not match the given string. If the streams argument is not NULL, and VARS_ORD_STR_LEXICOGRAPHIC is given as str argument, a warning will be printed
| const char* Enc_vars_ord_to_string | ( | VarsOrdType | ) |
Returns the string corresponding to give parameter.
Returned string does not have to be freed
1.6.1