#include "nusmv/core/trace/Trace.h"#include "nusmv/core/trace/TraceMgr.h"#include "nusmv/core/utils/utils.h"#include "nusmv/core/utils/ucmd.h"Go to the source code of this file.
Defines | |
| #define | CONSTANT_EXPR 0 |
| #define | getOpClass(op) |
| #define | isBinaryOp(op) |
| #define | isConstantExpr(op) ((op)==TRUEEXP) || ((op)==FALSEEXP) |
| #define | isPastOp(op) |
| #define | isVariable(op) (((op)==DOT) || ((op) == BIT)) |
| #define | LITERAL 1 |
| #define | PROP_CONNECTIVE 2 |
| #define | TIME_OPERATOR 3 |
| #define | UNKNOWN_OP -1 |
| The public interface to the bmc utilities. | |
Functions | |
| void | Bmc_Utils_add_be_into_inc_solver_positively (SatIncSolver_ptr solver, SatSolverGroup group, be_ptr prob, BeEnc_ptr be_enc, Be_CnfAlgorithm cnf_alg) |
| Converts Be into CNF, and adds it into a group of a incremental solver, sets polarity to 1, and then destroys the CNF. | |
| void | Bmc_Utils_add_be_into_non_inc_solver_positively (SatSolver_ptr solver, be_ptr prob, BeEnc_ptr be_enc, Be_CnfAlgorithm cnf_alg) |
| Converts Be into CNF, and adds it into a group of a non-incremental solver, sets polarity to 1, and then destroys the CNF. | |
| be_ptr | Bmc_Utils_apply_inlining (Be_Manager_ptr be_mgr, be_ptr f) |
| Applies inlining taking into account of current user settings. | |
| be_ptr | Bmc_Utils_apply_inlining4inc (Be_Manager_ptr be_mgr, be_ptr f) |
| Applies inlining forcing inclusion of the conjunct set. Useful in the incremental SAT applications to guarantee soundness. | |
| Outcome | Bmc_Utils_Check_k_l (const int k, const int l) |
| Checks the (k,l) couple. l must be absolute. | |
| void | Bmc_Utils_ConvertLoopFromInteger (const int iLoopback, char *szLoopback, const int _bufsize) |
| Given an integer containing the inner representation of the loopback value, returns as parameter the corresponding user-side value as string. | |
| int | Bmc_Utils_ConvertLoopFromString (const char *strValue, Outcome *result) |
| Given a string representing a loopback possible value, returns the corresponding integer. The (optional) parameter result will be assigned to OUTCOME_SUCCESS if the conversion has been successfully performed, otherwise to OUTCOME_GENERIC_ERROR is the conversion failed. If result is NULL, OUTCOME_SUCCESS is the aspected value, and an assertion is implicitly performed to check the conversion outcome. | |
| void | Bmc_Utils_ExpandMacrosInFilename (const char *filename_to_be_expanded, const SubstString *table_ptr, const size_t table_len, char *filename_expanded, size_t buf_len) |
| Search into a given string any symbol which belongs to a determined set of symbols, and expand each found symbol, finally returning the resulting string. | |
| Trace_ptr | Bmc_Utils_fill_cntexample (BeEnc_ptr be_enc, SatSolver_ptr solver, const int k, Trace_ptr trace) |
| Given a solver containing a model for a problem, fills the given counter-example correspondingly. | |
| Trace_ptr | Bmc_Utils_generate_and_print_cntexample (BeEnc_ptr be_enc, TraceMgr_ptr tm, SatSolver_ptr solver, be_ptr be_prob, const int k, const char *trace_name, NodeList_ptr symbols) |
| Given a problem, and a solver containing a model for that problem, generates and prints a counter-example. | |
| Trace_ptr | Bmc_Utils_generate_cntexample (BeEnc_ptr be_enc, SatSolver_ptr solver, be_ptr be_prob, const int k, const char *trace_name, NodeList_ptr symbols) |
| Given a problem, and a solver containing a model for that problem, generates a counter-example. | |
| int | Bmc_Utils_GetAllLoopbacks (void) |
| Returns the integer value which represents the "all loops" semantic. | |
| const char * | Bmc_Utils_GetAllLoopbacksString (void) |
| Returns a constant string which represents the "all loops" semantic. | |
| int | Bmc_Utils_GetNoLoopback (void) |
| Returns the integer value which represents the "no loop" semantic. | |
| int | Bmc_Utils_GetSuccTime (const int time, const int k, const int l) |
| Given time<=k and a \[l, k\] interval, returns next time, or BMC_NO_LOOP if time is equal to k and there is no loop. | |
| boolean | Bmc_Utils_IsAllLoopbacks (const int l) |
| Returns true if the given loop value represents the "all
possible loopbacks" semantic. | |
| boolean | Bmc_Utils_IsAllLoopbacksString (const char *str) |
| Returns true if the given string represents the "all
possible loops" value. | |
| boolean | Bmc_Utils_IsNoLoopback (const int l) |
| Returns true if l has the internally encoded "no loop" value. | |
| boolean | Bmc_Utils_IsNoLoopbackString (const char *str) |
| Returns true if the given string represents the no loopback value. | |
| boolean | Bmc_Utils_IsSingleLoopback (const int l) |
| Returns true if the given loop value represents a single (relative or absolute) loopback. | |
| be_ptr | Bmc_Utils_next_costraint_from_string (BeEnc_ptr be_enc, BddEnc_ptr bdd_enc, const char *str, Expr_ptr *node_expr) |
| Reads a next expression and builds the corresponding BE formula. | |
| int | Bmc_Utils_RelLoop2AbsLoop (const int loop, const int k) |
| Converts a relative loop value (wich can also be an absolute loop value) to an absolute loop value. | |
| be_ptr | Bmc_Utils_simple_costraint_from_string (BeEnc_ptr be_enc, BddEnc_ptr bdd_enc, const char *str, Expr_ptr *node_expr) |
| Reads a simple expression and builds the corresponding BE formula. | |
| #define getOpClass | ( | op | ) |
((op)==TRUEEXP) || ((op)==FALSEEXP) ? CONSTANT_EXPR \ : \ ((op)==DOT) || ((op) == BIT) || ((op)==NOT) ? LITERAL \ : \ ((op)==AND) || ((op)==OR) || \ ((op)==IFF) ? PROP_CONNECTIVE \ : \ ((op)==OP_PREC) || ((op)==OP_NEXT) || \ ((op)==OP_NOTPRECNOT) || \ ((op)==OP_ONCE) || ((op)==OP_FUTURE) || \ ((op)==OP_HISTORICAL) || ((op)==OP_GLOBAL) || \ ((op)==SINCE) || ((op)==UNTIL) || \ ((op)==TRIGGERED) || ((op)==RELEASES) ? TIME_OPERATOR \ : \ UNKNOWN_OP
| #define isBinaryOp | ( | op | ) |
| #define isConstantExpr | ( | op | ) | ((op)==TRUEEXP) || ((op)==FALSEEXP) |
| #define isPastOp | ( | op | ) |
((op)==OP_PREC) || ((op)==OP_NOTPRECNOT) || \ ((op)==OP_ONCE) || ((op)==OP_HISTORICAL) || \ ((op)==SINCE) || ((op)==TRIGGERED)
| #define isVariable | ( | op | ) | (((op)==DOT) || ((op) == BIT)) |
| #define UNKNOWN_OP -1 |
| void Bmc_Utils_add_be_into_inc_solver_positively | ( | SatIncSolver_ptr | solver, | |
| SatSolverGroup | group, | |||
| be_ptr | prob, | |||
| BeEnc_ptr | be_enc, | |||
| Be_CnfAlgorithm | cnf_alg | |||
| ) |
Converts Be into CNF, and adds it into a group of a incremental solver, sets polarity to 1, and then destroys the CNF.
Outputs into outstream the total time of conversion, adding, setting polarity and destroying BE.
| void Bmc_Utils_add_be_into_non_inc_solver_positively | ( | SatSolver_ptr | solver, | |
| be_ptr | prob, | |||
| BeEnc_ptr | be_enc, | |||
| Be_CnfAlgorithm | cnf_alg | |||
| ) |
Converts Be into CNF, and adds it into a group of a non-incremental solver, sets polarity to 1, and then destroys the CNF.
Outputs into outstream the total time of conversion, adding, setting polarity and destroying BE.
| be_ptr Bmc_Utils_apply_inlining | ( | Be_Manager_ptr | be_mgr, | |
| be_ptr | f | |||
| ) |
Applies inlining taking into account of current user settings.
| be_ptr Bmc_Utils_apply_inlining4inc | ( | Be_Manager_ptr | be_mgr, | |
| be_ptr | f | |||
| ) |
Applies inlining forcing inclusion of the conjunct set. Useful in the incremental SAT applications to guarantee soundness.
| Outcome Bmc_Utils_Check_k_l | ( | const int | k, | |
| const int | l | |||
| ) |
Checks the (k,l) couple. l must be absolute.
Returns OUTCOME_SUCCESS if k and l are compatible, otherwise return OUTCOME_GENERIC_ERROR
| void Bmc_Utils_ConvertLoopFromInteger | ( | const int | iLoopback, | |
| char * | szLoopback, | |||
| const int | _bufsize | |||
| ) |
Given an integer containing the inner representation of the loopback value, returns as parameter the corresponding user-side value as string.
Inverse semantic of Bmc_Utils_ConvertLoopFromString. bufsize is the maximum buffer size
String buffer passed as argument will change
| int Bmc_Utils_ConvertLoopFromString | ( | const char * | strValue, | |
| Outcome * | result | |||
| ) |
Given a string representing a loopback possible value, returns the corresponding integer. The (optional) parameter result will be assigned to OUTCOME_SUCCESS if the conversion has been successfully performed, otherwise to OUTCOME_GENERIC_ERROR is the conversion failed. If result is NULL, OUTCOME_SUCCESS is the aspected value, and an assertion is implicitly performed to check the conversion outcome.
Use this function to correctly convert a string containing a loopback user-side value to the internal representation of the same loopback value
result will change if supplied
| void Bmc_Utils_ExpandMacrosInFilename | ( | const char * | filename_to_be_expanded, | |
| const SubstString * | table_ptr, | |||
| const size_t | table_len, | |||
| char * | filename_expanded, | |||
| size_t | buf_len | |||
| ) |
Search into a given string any symbol which belongs to a determined set of symbols, and expand each found symbol, finally returning the resulting string.
This function is used in order to perform the macro expansion of filenames. table_ptr is the pointer to a previously prepared table which fixes any corrispondence from symbol to strings to be substituited from. table_len is the number of rows in the table (i.e. the number of symbols to search for.)
filename_expanded string data will change
| Trace_ptr Bmc_Utils_fill_cntexample | ( | BeEnc_ptr | be_enc, | |
| SatSolver_ptr | solver, | |||
| const int | k, | |||
| Trace_ptr | trace | |||
| ) |
Given a solver containing a model for a problem, fills the given counter-example correspondingly.
The filled trace is returned. The given trace must be empty
| Trace_ptr Bmc_Utils_generate_and_print_cntexample | ( | BeEnc_ptr | be_enc, | |
| TraceMgr_ptr | tm, | |||
| SatSolver_ptr | solver, | |||
| be_ptr | be_prob, | |||
| const int | k, | |||
| const char * | trace_name, | |||
| NodeList_ptr | symbols | |||
| ) |
Given a problem, and a solver containing a model for that problem, generates and prints a counter-example.
AutomaticStart
A trace is generated and printed using the currently selected plugin. Generated trace is returned, in order to make possible for the caller to do some other operation, like association with the checked property. Returned trace object *cannot* be destroyed by the caller.
| Trace_ptr Bmc_Utils_generate_cntexample | ( | BeEnc_ptr | be_enc, | |
| SatSolver_ptr | solver, | |||
| be_ptr | be_prob, | |||
| const int | k, | |||
| const char * | trace_name, | |||
| NodeList_ptr | symbols | |||
| ) |
Given a problem, and a solver containing a model for that problem, generates a counter-example.
Generated trace is returned, in order to make possible for the caller to do some other operation, like association with the checked property. Returned trace is non-volatile
| int Bmc_Utils_GetAllLoopbacks | ( | void | ) |
Returns the integer value which represents the "all loops" semantic.
| const char* Bmc_Utils_GetAllLoopbacksString | ( | void | ) |
Returns a constant string which represents the "all loops" semantic.
| int Bmc_Utils_GetNoLoopback | ( | void | ) |
Returns the integer value which represents the "no loop" semantic.
| int Bmc_Utils_GetSuccTime | ( | const int | time, | |
| const int | k, | |||
| const int | l | |||
| ) |
Given time<=k and a \[l, k\] interval, returns next time, or BMC_NO_LOOP if time is equal to k and there is no loop.
| boolean Bmc_Utils_IsAllLoopbacks | ( | const int | l | ) |
Returns true if the given loop value represents the "all possible loopbacks" semantic.
This is supplied in order to hide the internal value of loopback which corresponds to the "all loops" semantic.
| boolean Bmc_Utils_IsAllLoopbacksString | ( | const char * | str | ) |
Returns true if the given string represents the "all possible loops" value.
This is supplied in order to hide the internal value of loopback which corresponds to the "all loops" semantic.
| boolean Bmc_Utils_IsNoLoopback | ( | const int | l | ) |
Returns true if l has the internally encoded "no loop" value.
This is supplied in order to hide the internal value of loopback which corresponds to the "no loop" semantic.
| boolean Bmc_Utils_IsNoLoopbackString | ( | const char * | str | ) |
Returns true if the given string represents the no loopback value.
This is supplied in order to hide the internal value of loopback which corresponds to the "no loop" semantic.
| boolean Bmc_Utils_IsSingleLoopback | ( | const int | l | ) |
Returns true if the given loop value represents a single (relative or absolute) loopback.
Both cases "no loop" and "all loops" make this function returning false, since these values are not single loops.
| be_ptr Bmc_Utils_next_costraint_from_string | ( | BeEnc_ptr | be_enc, | |
| BddEnc_ptr | bdd_enc, | |||
| const char * | str, | |||
| Expr_ptr * | node_expr | |||
| ) |
Reads a next expression and builds the corresponding BE formula.
Reads a next expression and builds the corresponding BE formula. Exceptions are raised if the expression cannot be parsed or has type errors. If node_expr is not NULL, it will be set to the parsed expression.
None
| int Bmc_Utils_RelLoop2AbsLoop | ( | const int | loop, | |
| const int | k | |||
| ) |
Converts a relative loop value (wich can also be an absolute loop value) to an absolute loop value.
For example the -4 value when k is 10 is the value 6, but the value 4 (absolute loop value) is still 4
| be_ptr Bmc_Utils_simple_costraint_from_string | ( | BeEnc_ptr | be_enc, | |
| BddEnc_ptr | bdd_enc, | |||
| const char * | str, | |||
| Expr_ptr * | node_expr | |||
| ) |
Reads a simple expression and builds the corresponding BE formula.
Reads a simple expression and builds the corresponding BE formula. Exceptions are raised if the expression cannot be parsed or has type errors.
None
1.6.1