
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 RBCbased 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 lowlevel structure is
being used.

Be_Manager_Create()
 Creates a generic Be_Manager

Be_Manager_Delete()
 Be_Manager destroyer

Be_Manager_Spec2Be()
 Converts a specificformat boolean expression
(for example in rbc format) into a generic BE

Be_Manager_Be2Spec()
 Converts a generic BE into a specificformat 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()
 Deinitializes 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 RBCbased 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 rbcspecific 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 exclusivedisjunction
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 ifthenelse 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 CNFed 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