be.h
External header file
beInt.h
Internal header file
beCnf.c
Conjunctive Normal Form of boolean extpressions
beManager.c
The generic Boolean Expressions Manager implementation
bePkg.c
Contains initialization and deinitialization code for this module
beRbcManager.c
Implementation for the RBC-based Boolean Expressions module.

be.h

External header file

By: Roberto Cavada


beInt.h

Internal header file

By: Roberto Cavada


beCnf.c

Conjunctive Normal Form of boolean extpressions

By: Roberto Cavada

This module defines the Be_Cnf structure and any related method. When converting a be into cnf form the Be_ConvertToCnf function returns a Be_Cnf structure. The Be_Cnf structure is a base class for the structure Bmc_Problem.

See AlsoBe_ConvertToCnf, Bmc_Problem


beManager.c

The generic Boolean Expressions Manager implementation

By: Roberto Cavada

This implementation is independent on the low-level structure is being used.

Be_Manager_Create()
Creates a generic Be_Manager
Be_Manager_Delete()
Be_Manager destroyer
Be_Manager_Spec2Be()
Converts a specific-format boolean expression (for example in rbc format) into a generic BE
Be_Manager_Be2Spec()
Converts a generic BE into a specific-format boolean expression (for example in rbc format)
Be_Manager_GetData()
Derived classes data can be retrieved by this method
Be_Manager_SetData()
Sets specific structure manager data into the generic manager

bePkg.c

Contains initialization and deinitialization code for this module

By: Roberto Cavada

Contains code to be called when entering and exiting the module

Be_Init()
Initializes the module
Be_Quit()
De-initializes the module
be_shiftHashInit()
Initializes private hast table member for shifting operations
be_shiftHash_Quit()
Deletes private hast table member for shifting operations

beRbcManager.c

Implementation for the RBC-based Boolean Expressions module.

By: Roberto Cavada

This implementation is a wrapper for the RBC structure.

()
Given a be_manager returns the contained rbc manager.
()
Converts a rbc into a be
()
Converts a be into a rbc
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_IsTrue()
Returns true if the given be is the true value, otherwise returns false
Be_IsFalse()
Returns true if the given be is the false value, otherwise returns false
Be_IsConstant()
Returns true if the given be is a constant value, such as either False or True
Be_Truth()
Builds a 'true' constant value
Be_Falsity()
Builds a 'false' constant value
Be_Not()
Negates its argument
Be_And()
Builds a new be which is the conjunction between its two arguments
Be_Or()
Builds a new be which is the disjunction of its two arguments
Be_Xor()
Builds a new be which is the exclusive-disjunction of its two arguments
Be_Implies()
Builds a new be which is the implication between its two arguments
Be_Iff()
Builds a new be which is the logical equivalence between its two arguments
Be_Ite()
Builds an if-then-else operation be
Be_ShiftVar()
Creates a fresh copy G(X') of the be F(X) by shifting each variable index of a given amount
Be_LogicalShiftVar()
Creates a fresh copy G(X') of the be F(X) by shifting each variable index of a given amount
Be_VarSubst()
Replaces all variables in f with other variables
Be_LogicalVarSubst()
Replaces all variables in f with other variables, taking them at logical level
Be_ConvertToCnf()
Converts the given be into the corresponding CNF-ed be
Be_CnfModelToBeModel()
Converts the given CNF model into BE model
Be_CnfLiteral2BeLiteral()
Converts a CNF literal into a BE literal
Be_BeLiteral2CnfLiteral()
Converts a BE literal into a CNF literal (sign is taken into account)
Be_BeLiteral2BeIndex()
Converts a BE literal into a CNF literal
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_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_Index2Var()
Converts the given variable index into the corresponding be
Be_Var2Index()
Converts the given variable (as boolean expression) into the corresponding index
Be_PrintStats()
Prints out some statistical data about the underlying rbc structure
Be_CnfLiteral_IsSignPositive()
Returns true iff sign of literal is positive.
Be_CnfLiteral_Negate()
Returns negated literal.
Be_BeLiteral_IsSignPositive()
Returns true iff sign of literal is positive.
Be_BeLiteral_Negate()
Returns negated literal.
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

Last updated on 2007/04/06 14h:44