be_ptr
Be_And(
Be_Manager_ptr manager,
be_ptr left,
be_ptr right
)
- Builds a new be which is the conjunction between
its two arguments
- Defined in
beRbcManager.c
int
Be_BeIndex2BeLiteral(
const Be_Manager_ptr self,
int beIndex
)
- Converts a BE index into a BE literal (always positive)
- See Also
Be_ConvertToCnf
- Defined in
beRbcManager.c
int
Be_BeIndex2CnfLiteral(
const Be_Manager_ptr self,
int beIndex
)
- 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.
- See Also
Be_ConvertToCnf
- Defined in
beRbcManager.c
int
Be_BeLiteral2BeIndex(
const Be_Manager_ptr self,
int beLiteral
)
- Converts a BE literal into a CNF literal
- See Also
Be_ConvertToCnf
- Defined in
beRbcManager.c
int
Be_BeLiteral2CnfLiteral(
const Be_Manager_ptr self,
int beLiteral
)
- Converts a BE literal into a CNF literal (sign is taken into
account)
- See Also
Be_ConvertToCnf
- Defined in
beRbcManager.c
boolean
Be_BeLiteral_IsSignPositive(
const Be_Manager_ptr self,
int beLiteral
)
- Returns true iff sign of literal is positive.
- See Also
Be_BeLiteral_Negate
Be_CnfLiteral_IsSignPositive
- Defined in
beRbcManager.c
int
Be_BeLiteral_Negate(
const Be_Manager_ptr self,
int beLiteral
)
- Returns negated literal.
- See Also
Be_BeLiteral_IsSignPositive
Be_CnfLiteral_Negate
- Defined in
beRbcManager.c
int
Be_CnfLiteral2BeLiteral(
const Be_Manager_ptr self,
int cnfLiteral
)
- 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).
- See Also
Be_ConvertToCnf
- Defined in
beRbcManager.c
boolean
Be_CnfLiteral_IsSignPositive(
const Be_Manager_ptr self,
int cnfLiteral
)
- Returns true iff sign of literal is positive.
- See Also
Be_CnfLiteral_Negate
Be_BeLiteral_IsSignPositive
- Defined in
beRbcManager.c
int
Be_CnfLiteral_Negate(
const Be_Manager_ptr self,
int cnfLiteral
)
- Returns negated literal.
- See Also
Be_CnfLiteral_IsSignPositive
Be_BeLiteral_Negate
- Defined in
beRbcManager.c
lsList
Be_CnfModelToBeModel(
Be_Manager_ptr manager,
lsList cnfModel
)
- Since it creates a new lsit , the caller
is responsible for deleting it when it is no longer used
(via lsDestroy)
- Defined in
beRbcManager.c
Be_Cnf_ptr
Be_ConvertToCnf(
Be_Manager_ptr manager,
be_ptr f,
int polarity
)
- 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).
'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.
- See Also
Be_Cnf_Delete
- Defined in
beRbcManager.c
void
Be_DumpDavinci(
Be_Manager_ptr manager,
be_ptr f,
FILE* outFile
)
- Dumps the given be into a file with Davinci format
- Defined in
beRbcManager.c
void
Be_DumpGdl(
Be_Manager_ptr manager,
be_ptr f,
FILE* outFile
)
- Dumps the given be into a file with Davinci format
- Defined in
beRbcManager.c
void
Be_DumpSexpr(
Be_Manager_ptr manager,
be_ptr f,
FILE* outFile
)
- Dumps the given be into a file
- Defined in
beRbcManager.c
be_ptr
Be_Falsity(
Be_Manager_ptr manager
)
- Builds a 'false' constant value
- Defined in
beRbcManager.c
be_ptr
Be_Iff(
Be_Manager_ptr manager,
be_ptr left,
be_ptr right
)
- Builds a new be which is the logical equivalence
between its two arguments
- Defined in
beRbcManager.c
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
- Defined in
beRbcManager.c
be_ptr
Be_Index2Var(
Be_Manager_ptr manager,
int varIndex
)
- 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.
- Defined in
beRbcManager.c
void
Be_Init(
)
- Call before any other function contained in this module
- Side Effects Any module structure is allocated and initialized if required
- See Also
Be_Quit
- Defined in
bePkg.c
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
- Defined in
beRbcManager.c
boolean
Be_IsFalse(
Be_Manager_ptr manager,
be_ptr arg
)
- Returns true if the given be is the false value,
otherwise returns false
- Defined in
beRbcManager.c
boolean
Be_IsTrue(
Be_Manager_ptr manager,
be_ptr arg
)
- Returns true if the given be is the true value,
otherwise returns false
- Defined in
beRbcManager.c
be_ptr
Be_Ite(
Be_Manager_ptr manager,
be_ptr c,
be_ptr t,
be_ptr e
)
- Builds an if-then-else operation be
- Side Effects ...
- Defined in
beRbcManager.c
be_ptr
Be_LogicalShiftVar(
Be_Manager_ptr manager,
be_ptr f,
int shift,
const int* log2phy,
const int* phy2log
)
- 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.
- Defined in
beRbcManager.c
be_ptr
Be_LogicalVarSubst(
Be_Manager_ptr manager,
be_ptr f,
int* subst,
const int* log2phy,
const int* phy2log
)
- Replaces every occurence of the variable x_i in in `f'
with the variable x_j provided that subst[i
- Defined in
beRbcManager.c
void*
Be_Manager_Be2Spec(
const Be_Manager_ptr self,
be_ptr be
)
- Converts a generic BE into a specific-format boolean expression
(for example in rbc format)
- See Also
Be_Manager_Spec2Be
- Defined in
beManager.c
Be_Manager_ptr
Be_Manager_Create(
void* spec_manager,
Be_Spec2Be_fun spec2be_converter,
Be_Be2Spec_fun be2spec_converter
)
- spec_manager is the specific structure which is used to manage
the low-level structure. For example the RbcManager class in the
RBC dependant implementation.
This does not assume the ownership of 'spec_manager'. If you have dynamically
created the spec_manager instance, you are responsible for deleting it after
you deleted the Be_manager instance.
This "virtual" function is supplied in order to be called by any
specific class derived from Be_Manager, in its constructor code.
spec2be and be2spec converters are gateways in order to polymorphically
convert the low level support structure (for example a rbc pointer) to
the generic be_ptr and viceversa.
- See Also
Be_RbcManager_Create
Be_Manager_Delete
- Defined in
beManager.c
void
Be_Manager_Delete(
Be_Manager_ptr self
)
- Call this function from the destructor of the derived class
that implements the Be_Manager class. Any other use is to be considered
unusual.
- Side Effects self will be deleted from memory.
- See Also
Be_RbcManager_Delete
Be_Manager_Create
- Defined in
beManager.c
void*
Be_Manager_GetData(
const Be_Manager_ptr self
)
- When you instantiate a derived BE manager (for example the
rbc manager) you can store any useful specific data by using
Be_Manager_SetData. Those data can be lately retrieved by Be_Manager_GetData
which gets a generic, structure-independent Be_Manager.
- See Also
Be_Manager_SetData
- Defined in
beManager.c
void
Be_Manager_SetData(
Be_Manager_ptr self,
void* data
)
- You can retieve saved data by using the method
Be_Manager_GetData. This implements a kind of inheritance mechanism.
- Side Effects self will change its internal state.
- See Also
Be_Manager_GetData
- Defined in
beManager.c
be_ptr
Be_Manager_Spec2Be(
const Be_Manager_ptr self,
void* spec_expr
)
- Calls self->spec2be_converter in order to implement the
polymorphism mechanism
- Side Effects Calls self->be2spec_converter in order to implement the
polymorphism mechanism
- See Also
Be_Manager_Be2Spec
- Defined in
beManager.c
be_ptr
Be_Not(
Be_Manager_ptr manager,
be_ptr left
)
- Negates its argument
- Defined in
beRbcManager.c
be_ptr
Be_Or(
Be_Manager_ptr manager,
be_ptr left,
be_ptr right
)
- Builds a new be which is the disjunction of
its two arguments
- Defined in
beRbcManager.c
void
Be_PrintStats(
Be_Manager_ptr manager,
int clustSize,
FILE* outFile
)
- Prints out some statistical data about the underlying
rbc structure
- Defined in
beRbcManager.c
void
Be_Quit(
)
- Call as soon as you finished to use this module services
- Side Effects Any module structure is deleted if required
- See Also
Be_Init
- Defined in
bePkg.c
Be_Manager_ptr
Be_RbcManager_Create(
const size_t capacity
)
- You must call Be_RbcManager_Delete when the created instance
is no longer used.
- See Also
Be_RbcManager_Delete
- Defined in
beRbcManager.c
void
Be_RbcManager_Delete(
Be_Manager_ptr self
)
- Destroys the given Be_MAnager instance you previously
created by using Be_RbcManager_Create
- See Also
Be_RbcManager_Create
- Defined in
beRbcManager.c
void
Be_RbcManager_Reserve(
Be_Manager_ptr self,
const size_t size
)
- Changes the maximum number of variables the rbc manager can
handle
- Side Effects The given rbc manager will possibly change
- Defined in
beRbcManager.c
be_ptr
Be_ShiftVar(
Be_Manager_ptr manager,
be_ptr f,
int shift
)
- 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.
!!!!!! WARNING WARNING WARNING WARNING WARNING WARNING !!!!!
!! !!
!! This function cannot be used with the new encoding BeEnc. As !!
!! shifting involves the traversal of the logical layer within the !!
!! BeEnc, simple shifting is no longer usable, and will produce !!
!! unpredictable results if used on variables handled by a BeEnc !!
!! instance. !!
!! !!
!! Use Be_LogicalShiftVar instead. !!
!! !!
!!!!!! WARNING WARNING WARNING WARNING WARNING WARNING !!!!!
- See Also
Be_LogicalShiftVar
- Defined in
beRbcManager.c
be_ptr
Be_Truth(
Be_Manager_ptr manager
)
- Builds a 'true' constant value
- Defined in
beRbcManager.c
int
Be_Var2Index(
Be_Manager_ptr manager,
be_ptr var
)
- Converts the given variable (as boolean expression) into
the corresponding index
- Defined in
beRbcManager.c
be_ptr
Be_VarSubst(
Be_Manager_ptr manager,
be_ptr f,
int* subst
)
- Replaces every occurence of the variable x_i in in `f'
with the variable x_j provided that subst[i
- See Also
Be_LogicalSubst
- Defined in
beRbcManager.c
be_ptr
Be_Xor(
Be_Manager_ptr manager,
be_ptr left,
be_ptr right
)
- Builds a new be which is the exclusive-disjunction
of its two arguments
- Defined in
beRbcManager.c
be_ptr
Be_apply_inlining(
Be_Manager_ptr mgr,
be_ptr f,
boolean add_conj
)
- If add_conj is true, the conjuction set is included, otherwise
only the inlined formula is returned for a lazy SAT solving.
- See Also
InlineResult
- Defined in
beRbcManager.c
static void*
beRbc_Be2Rbc(
Be_Manager_ptr mgr,
be_ptr be
)
- The current implementation is really a simple type renaming.
Internally used by Be_Manager via the inheritance mechanism.
- Defined in
beRbcManager.c
static be_ptr
beRbc_Rbc2Be(
Be_Manager_ptr mgr,
void* rbc
)
- The current implementation is really a simple type renaming.
Internally used by Be_Manager via the inheritance mechanism.
- Defined in
beRbcManager.c
void
be_shiftHashInit(
)
- Call be_shiftHash_Quit() before quit from the be
module
- Side Effects Private global vars htShift_ptr will change
- See Also
Be_ShiftVar
Be_LogicalShiftVar
Hash_Quit
- Defined in
bePkg.c
void
be_shiftHash_Quit(
)
- Call be_shiftHash_Quit() before quit from BMC module
- Side Effects Private global vars htShift_ptr will be put to NULL
- See Also
Be_ShiftVar
be_shiftHashInit
- Defined in
bePkg.c
(
)
- This is a macro which can be used to simplify the code.
- See Also
BE
- Defined in
beRbcManager.c
(
)
- This is a macro which can be used to simplify the code.
- See Also
RBC
- Defined in
beRbcManager.c
(
)
- This is a macro which can be used to simplify the code.
- Defined in
beRbcManager.c