Be_And()
Builds a new be which is the conjunction between its two arguments
Be_BeIndex2BeLiteral()
Converts a BE index into a BE literal (always positive)
Be_BeIndex2CnfLiteral()
Returns a CNF literal (always positive) associated with a given BE index
Be_BeLiteral2BeIndex()
Converts a BE literal into a CNF literal
Be_BeLiteral2CnfLiteral()
Converts a BE literal into a CNF literal (sign is taken into account)
Be_BeLiteral_IsSignPositive()
Returns true iff sign of literal is positive.
Be_BeLiteral_Negate()
Returns negated literal.
Be_CnfLiteral2BeLiteral()
Converts a CNF literal into a BE literal
Be_CnfLiteral_IsSignPositive()
Returns true iff sign of literal is positive.
Be_CnfLiteral_Negate()
Returns negated literal.
Be_CnfModelToBeModel()
Converts the given CNF model into BE model
Be_ConvertToCnf()
Converts the given be into the corresponding CNF-ed be
Be_DumpDavinci()
Dumps the given be into a file with Davinci format
Be_DumpGdl()
Dumps the given be into a file with Davinci format
Be_DumpSexpr()
Dumps the given be into a file
Be_Falsity()
Builds a 'false' constant value
Be_Iff()
Builds a new be which is the logical equivalence between its two arguments
Be_Implies()
Builds a new be which is the implication between its two arguments
Be_Index2Var()
Converts the given variable index into the corresponding be
Be_Init()
Initializes the module
Be_IsConstant()
Returns true if the given be is a constant value, such as either False or True
Be_IsFalse()
Returns true if the given be is the false value, otherwise returns false
Be_IsTrue()
Returns true if the given be is the true value, otherwise returns false
Be_Ite()
Builds an if-then-else operation be
Be_LogicalShiftVar()
Creates a fresh copy G(X') of the be F(X) by shifting each variable index of a given amount
Be_LogicalVarSubst()
Replaces all variables in f with other variables, taking them at logical level
Be_Manager_Be2Spec()
Converts a generic BE into a specific-format boolean expression (for example in rbc format)
Be_Manager_Create()
Creates a generic Be_Manager
Be_Manager_Delete()
Be_Manager destroyer
Be_Manager_GetData()
Derived classes data can be retrieved by this method
Be_Manager_SetData()
Sets specific structure manager data into the generic manager
Be_Manager_Spec2Be()
Converts a specific-format boolean expression (for example in rbc format) into a generic BE
Be_Not()
Negates its argument
Be_Or()
Builds a new be which is the disjunction of its two arguments
Be_PrintStats()
Prints out some statistical data about the underlying rbc structure
Be_Quit()
De-initializes the module
Be_RbcManager_Create()
Creates a rbc-specific Be_Manager
Be_RbcManager_Delete()
Destroys the given Be_MAnager instance you previously created by using Be_RbcManager_Create
Be_RbcManager_Reserve()
Changes the maximum number of variables the rbc manager can handle
Be_ShiftVar()
Creates a fresh copy G(X') of the be F(X) by shifting each variable index of a given amount
Be_Truth()
Builds a 'true' constant value
Be_Var2Index()
Converts the given variable (as boolean expression) into the corresponding index
Be_VarSubst()
Replaces all variables in f with other variables
Be_Xor()
Builds a new be which is the exclusive-disjunction of its two arguments
Be_apply_inlining()
Performs the inlining of f, either including or not the conjuction set.
beRbc_Be2Rbc()
Converts a be into a rbc
beRbc_Rbc2Be()
Converts a rbc into a be
be_shiftHashInit()
Initializes private hast table member for shifting operations
be_shiftHash_Quit()
Deletes private hast table member for shifting operations
()
Converts a be into a rbc
()
Converts a rbc into a be
()
Given a be_manager returns the contained rbc manager.

Last updated on 2011/04/06 21h:13