#include "nusmv/core/rbc/rbc.h"#include <limits.h>#include "nusmv/core/be/beRbcManager.h"#include "nusmv/core/utils/Slist.h"#include "nusmv/core/cinit/NuSMVEnv.h"Go to the source code of this file.
Defines | |
| #define | BE_INVALID_SUBST_VALUE RBC_INVALID_SUBST_VALUE |
| Represents an invalid value possibly used when substituting. | |
Typedefs | |
| typedef void *(* | Be_Be2Spec_fun )(Be_Manager_ptr self, be_ptr be) |
| Generic to specific BE conversion gateway type. | |
| typedef struct Be_Cnf_TAG * | Be_Cnf_ptr |
| A Boolean Expression represented in Conjunctive Normal Form. | |
| typedef Rbc_2CnfAlgorithm | Be_CnfAlgorithm |
| BE equivalent of RBC CNF conversion algorithm. | |
| typedef struct Be_Manager_TAG * | Be_Manager_ptr |
The header file for the be package. | |
| typedef void * | be_ptr |
| The Boolean Expression type. | |
| typedef be_ptr(* | Be_Spec2Be_fun )(Be_Manager_ptr self, void *spec_be) |
| Specific to generic BE conversion gateway type. | |
Functions | |
| be_ptr | Be_And (Be_Manager_ptr manager, be_ptr arg1, be_ptr arg2) |
| Builds a new be which is the conjunction between its two arguments. | |
| be_ptr | Be_apply_inlining (Be_Manager_ptr self, be_ptr f, boolean add_conj) |
| Performs the inlining of f, either including or not the conjuction set. | |
| int | Be_BeIndex2BeLiteral (const Be_Manager_ptr self, int beIndex) |
| Converts a BE index into a BE literal (always positive). | |
| int | Be_BeIndex2CnfLiteral (const Be_Manager_ptr self, int beIndex) |
| Returns a CNF literal (always positive) associated with a given BE index. | |
| int | Be_BeLiteral2BeIndex (const Be_Manager_ptr self, int beLiteral) |
| Converts a BE literal into a CNF literal. | |
| int | Be_BeLiteral2CnfLiteral (const Be_Manager_ptr self, int beLiteral) |
| Converts a BE literal into a CNF literal (sign is taken into account). | |
| boolean | Be_BeLiteral_IsSignPositive (const Be_Manager_ptr self, int beLiteral) |
| Returns true iff sign of literal is positive. | |
| int | Be_BeLiteral_Negate (const Be_Manager_ptr self, int beLiteral) |
| Returns negated literal. | |
| int | Be_CnfLiteral2BeLiteral (const Be_Manager_ptr self, int cnfLiteral) |
| Converts a CNF literal into a BE literal. | |
| boolean | Be_CnfLiteral_IsSignPositive (const Be_Manager_ptr self, int cnfLiteral) |
| Returns true iff sign of literal is positive. | |
| int | Be_CnfLiteral_Negate (const Be_Manager_ptr self, int cnfLiteral) |
| Returns negated literal. | |
| Slist_ptr | Be_CnfModelToBeModel (Be_Manager_ptr manager, const Slist_ptr cnfModel) |
| Converts the given CNF model into BE model. | |
| Be_Cnf_ptr | Be_ConvertToCnf (Be_Manager_ptr manager, be_ptr f, int polarity, Be_CnfAlgorithm alg) |
| Converts the given be into the corresponding CNF-ed be. | |
| void | Be_DumpDavinci (Be_Manager_ptr manager, be_ptr f, FILE *outFile) |
| Dumps the given be into a file with Davinci format. | |
| void | Be_DumpGdl (Be_Manager_ptr manager, be_ptr f, FILE *outFile) |
| Dumps the given be into a file with Davinci format. | |
| void | Be_DumpSexpr (Be_Manager_ptr manager, be_ptr f, FILE *outFile) |
| Dumps the given be into a file. | |
| be_ptr | Be_Falsity (Be_Manager_ptr manager) |
| Builds a 'false' constant value. | |
| be_ptr | Be_Iff (Be_Manager_ptr manager, be_ptr arg1, be_ptr arg2) |
| Builds a new be which is the logical equivalence between its two arguments. | |
| be_ptr | Be_Implies (Be_Manager_ptr manager, be_ptr arg1, be_ptr arg2) |
| Builds a new be which is the implication between its two arguments. | |
| be_ptr | Be_Index2Var (Be_Manager_ptr manager, int varIndex) |
| Converts the given variable index into the corresponding be. | |
| void | Be_Init (void) |
| Initializes the module. | |
| boolean | Be_IsConstant (Be_Manager_ptr manager, be_ptr arg) |
| Returns true if the given be is a constant value, such as either False or True. | |
| boolean | Be_IsFalse (Be_Manager_ptr manager, be_ptr arg) |
| Returns true if the given be is the false value, otherwise returns false. | |
| boolean | Be_IsTrue (Be_Manager_ptr manager, be_ptr arg) |
| Returns true if the given be is the true value, otherwise returns false. | |
| be_ptr | Be_Ite (Be_Manager_ptr manager, be_ptr arg_if, be_ptr arg_then, be_ptr arg_else) |
| Builds an if-then-else operation be. | |
| be_ptr | Be_LogicalShiftVar (Be_Manager_ptr manager, be_ptr f, int shift, const int *log2phy, const int *phy2log) |
| Creates a fresh copy G(X') of the be F(X) by shifting each variable index of a given amount. | |
| be_ptr | Be_LogicalVarSubst (Be_Manager_ptr manager, be_ptr f, int *subst, const int *log2phy, const int *phy2log) |
| Replaces all variables in f with other variables, taking them at logical level. | |
| be_ptr | Be_Not (Be_Manager_ptr manager, be_ptr arg) |
| Negates its argument. | |
| be_ptr | Be_Or (Be_Manager_ptr manager, be_ptr arg1, be_ptr arg2) |
| Builds a new be which is the disjunction of its two arguments. | |
| void | Be_Quit (void) |
| De-initializes the module. | |
| be_ptr | Be_Truth (Be_Manager_ptr manager) |
| Builds a 'true' constant value. | |
| int | Be_Var2Index (Be_Manager_ptr manager, be_ptr var) |
| Converts the given variable (as boolean expression) into the corresponding index. | |
| be_ptr | Be_Xor (Be_Manager_ptr manager, be_ptr arg1, be_ptr arg2) |
| Builds a new be which is the exclusive-disjunction of its two arguments. | |
| #define BE_INVALID_SUBST_VALUE RBC_INVALID_SUBST_VALUE |
Represents an invalid value possibly used when substituting.
If during substitution this value is found, an error is raised. This is used for runtime checking of those expressions that are not expected to contain variables that cannot be substituted.
| typedef void*(* Be_Be2Spec_fun)(Be_Manager_ptr self, be_ptr be) |
Generic to specific BE conversion gateway type.
This is the function type for the Be_Manager gateway that provides conversion functionality from generic boolean expression types to specific Boolean Expression type (for example from be_ptr to rbc).
| typedef struct Be_Cnf_TAG* Be_Cnf_ptr |
A Boolean Expression represented in Conjunctive Normal Form.
Special case -- A CONSTANT: If the formula is a constant, Be_Cnf_GetFormulaLiteral() will be INT_MAX, if formula is true then: GetClausesList() will be empty list. if formula is false then: GetClausesList() will contain a single empty clause.
| typedef Rbc_2CnfAlgorithm Be_CnfAlgorithm |
BE equivalent of RBC CNF conversion algorithm.
| typedef struct Be_Manager_TAG* Be_Manager_ptr |
The header file for the be package.
Be_Manager is a generic manager required when you must operate on Boolean Expressions Any instance of Be_Manager can only be accessed via Be_Manager_ptr
| typedef be_ptr(* Be_Spec2Be_fun)(Be_Manager_ptr self, void *spec_be) |
Specific to generic BE conversion gateway type.
This is the function type for the Be_Manager gateway that provides conversion functionality from specific boolean expression types to generic Boolean Expression type (for example from rbc to be_ptr).
| be_ptr Be_And | ( | Be_Manager_ptr | manager, | |
| be_ptr | arg1, | |||
| be_ptr | arg2 | |||
| ) |
Builds a new be which is the conjunction between its two arguments.
| be_ptr Be_apply_inlining | ( | Be_Manager_ptr | self, | |
| be_ptr | f, | |||
| boolean | add_conj | |||
| ) |
Performs the inlining of f, either including or not the conjuction set.
If add_conj is true, the conjuction set is included, otherwise only the inlined formula is returned for a lazy SAT solving.
| int Be_BeIndex2BeLiteral | ( | const Be_Manager_ptr | self, | |
| int | beIndex | |||
| ) |
Converts a BE index into a BE literal (always positive).
| int Be_BeIndex2CnfLiteral | ( | const Be_Manager_ptr | self, | |
| int | beIndex | |||
| ) |
Returns a CNF literal (always positive) associated with a given BE index.
If no CNF index is associated with a given BE index, 0 is returned. BE indexes are associated with CNF indexes through function Be_ConvertToCnf.
| int Be_BeLiteral2BeIndex | ( | const Be_Manager_ptr | self, | |
| int | beLiteral | |||
| ) |
Converts a BE literal into a CNF literal.
| int Be_BeLiteral2CnfLiteral | ( | const Be_Manager_ptr | self, | |
| int | beLiteral | |||
| ) |
Converts a BE literal into a CNF literal (sign is taken into account).
| boolean Be_BeLiteral_IsSignPositive | ( | const Be_Manager_ptr | self, | |
| int | beLiteral | |||
| ) |
Returns true iff sign of literal is positive.
| int Be_BeLiteral_Negate | ( | const Be_Manager_ptr | self, | |
| int | beLiteral | |||
| ) |
Returns negated literal.
| int Be_CnfLiteral2BeLiteral | ( | const Be_Manager_ptr | self, | |
| int | cnfLiteral | |||
| ) |
Converts a CNF literal into a BE literal.
The function returns 0 if there is no BE index associated with the given CNF index. A given CNF literal should be created by given BE manager (through Be_ConvertToCnf).
| boolean Be_CnfLiteral_IsSignPositive | ( | const Be_Manager_ptr | self, | |
| int | cnfLiteral | |||
| ) |
Returns true iff sign of literal is positive.
| int Be_CnfLiteral_Negate | ( | const Be_Manager_ptr | self, | |
| int | cnfLiteral | |||
| ) |
Returns negated literal.
| Slist_ptr Be_CnfModelToBeModel | ( | Be_Manager_ptr | manager, | |
| const Slist_ptr | cnfModel | |||
| ) |
Converts the given CNF model into BE model.
Since it creates a new lsit , the caller is responsible for deleting it when it is no longer used (via lsDestroy)
| Be_Cnf_ptr Be_ConvertToCnf | ( | Be_Manager_ptr | manager, | |
| be_ptr | f, | |||
| int | polarity, | |||
| Be_CnfAlgorithm | alg | |||
| ) |
Converts the given be into the corresponding CNF-ed be.
Since it creates a new Be_Cnf structure, the caller is responsible for deleting it when it is no longer used (via Be_Cnf_Delete).
'alg' can be one value in (RBC_TSEITIN_CONVERSION, RBC_SHERIDAN_CONVERSION) Option "rbc_rbc2cnf_algorithm" (RBC_CNF_ALGORITHM) holds the user preferred value.
'polarity' is used to determine if the clauses generated should represent the RBC positively, negatively, or both (1, -1 or 0 respectively). For an RBC that is known to be true, the clauses that represent it being false are not needed (they would be removed anyway by propogating the unit literal which states that the RBC is true). Similarly for when the RBC is known to be false. This parameter is only used with the compact cnf conversion algorithm, and is ignored if the simple algorithm is used.
| void Be_DumpDavinci | ( | Be_Manager_ptr | manager, | |
| be_ptr | f, | |||
| FILE * | outFile | |||
| ) |
Dumps the given be into a file with Davinci format.
| void Be_DumpGdl | ( | Be_Manager_ptr | manager, | |
| be_ptr | f, | |||
| FILE * | outFile | |||
| ) |
Dumps the given be into a file with Davinci format.
| void Be_DumpSexpr | ( | Be_Manager_ptr | manager, | |
| be_ptr | f, | |||
| FILE * | outFile | |||
| ) |
Dumps the given be into a file.
| be_ptr Be_Falsity | ( | Be_Manager_ptr | manager | ) |
Builds a 'false' constant value.
| be_ptr Be_Iff | ( | Be_Manager_ptr | manager, | |
| be_ptr | arg1, | |||
| be_ptr | arg2 | |||
| ) |
Builds a new be which is the logical equivalence between its two arguments.
| be_ptr Be_Implies | ( | Be_Manager_ptr | manager, | |
| be_ptr | arg1, | |||
| be_ptr | arg2 | |||
| ) |
Builds a new be which is the implication between its two arguments.
| be_ptr Be_Index2Var | ( | Be_Manager_ptr | manager, | |
| int | varIndex | |||
| ) |
Converts the given variable index into the corresponding be.
If corresponding index had not been previously allocated, it will be allocated. If corresponding node does not exist in the dag, it will be inserted.
| void Be_Init | ( | void | ) |
Initializes the module.
Call before any other function contained in this module
Any module structure is allocated and initialized if required
| boolean Be_IsConstant | ( | Be_Manager_ptr | manager, | |
| be_ptr | arg | |||
| ) |
Returns true if the given be is a constant value, such as either False or True.
| boolean Be_IsFalse | ( | Be_Manager_ptr | manager, | |
| be_ptr | arg | |||
| ) |
Returns true if the given be is the false value, otherwise returns false.
| boolean Be_IsTrue | ( | Be_Manager_ptr | manager, | |
| be_ptr | arg | |||
| ) |
Returns true if the given be is the true value, otherwise returns false.
| be_ptr Be_Ite | ( | Be_Manager_ptr | manager, | |
| be_ptr | arg_if, | |||
| be_ptr | arg_then, | |||
| be_ptr | arg_else | |||
| ) |
Builds an if-then-else operation be.
...
| be_ptr Be_LogicalShiftVar | ( | Be_Manager_ptr | manager, | |
| be_ptr | f, | |||
| int | shift, | |||
| const int * | log2phy, | |||
| const int * | phy2log | |||
| ) |
Creates a fresh copy G(X') of the be F(X) by shifting each variable index of a given amount.
Shifting operation replaces each occurence of the variable x_i in `f' with the variable x_(i + shift). A simple lazy mechanism is implemented to optimize that cases which given expression is a constant in.
The two indices arrays log2phy and phy2log map respectively the logical level to the physical level, and the physical level to the logical levels. They allow the be encoder to freely organize the variables into a logical and a physical level. This feature has been introduced with NuSMV-2.4 that ships dynamic encodings.
!!!! WARNING !!!! Since version 2.4 memoizing has been moved to BeEnc, as there is no way of calculating a good hashing key as the time would be requested, but timing information are not available at this stage.
| be_ptr Be_LogicalVarSubst | ( | Be_Manager_ptr | manager, | |
| be_ptr | f, | |||
| int * | subst, | |||
| const int * | log2phy, | |||
| const int * | phy2log | |||
| ) |
Replaces all variables in f with other variables, taking them at logical level.
Replaces every occurence of the variable x_i in in `f' with the variable x_j provided that subst[i] = j.
Notice that in this context, 'i' and 'j' are LOGICAL indices, not physical, i.e. the substitution array is provided in terms of logical indices, and is related only to the logical level.
For a substitution at physical level, see Be_VarSubst.
There is no need for `subst' to contain all the variables, but it should map at least the variables in `f' in order for the substitution to work properly.
The two indices arrays log2phy and phy2log map respectively the logical level to the physical level, and the physical level to the logical levels. They allow the be encoder to freely organize the variables into a logical and a physical level. This feature has been introduced with NuSMV-2.3 that ships dynamic encodings.
| be_ptr Be_Not | ( | Be_Manager_ptr | manager, | |
| be_ptr | arg | |||
| ) |
Negates its argument.
| be_ptr Be_Or | ( | Be_Manager_ptr | manager, | |
| be_ptr | arg1, | |||
| be_ptr | arg2 | |||
| ) |
Builds a new be which is the disjunction of its two arguments.
| void Be_Quit | ( | void | ) |
De-initializes the module.
Call as soon as you finished to use this module services
Any module structure is deleted if required
| be_ptr Be_Truth | ( | Be_Manager_ptr | manager | ) |
Builds a 'true' constant value.
| int Be_Var2Index | ( | Be_Manager_ptr | manager, | |
| be_ptr | var | |||
| ) |
Converts the given variable (as boolean expression) into the corresponding index.
| be_ptr Be_Xor | ( | Be_Manager_ptr | manager, | |
| be_ptr | arg1, | |||
| be_ptr | arg2 | |||
| ) |
Builds a new be which is the exclusive-disjunction of its two arguments.
1.6.1