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

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