-
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, Marco Roveri
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 2010/11/03 21h:54