const char * 
Rbc_CnfConversionAlgorithm2Str(
  Rbc_2CnfAlgorithm  algo 
)
Conversion from CNF conversion algorithm enumerative to string


Rbc_2CnfAlgorithm 
Rbc_CnfConversionAlgorithmFromStr(
  const char * str 
)
Conversion from string to CNF conversion algorithm enumerative


const char * 
Rbc_CnfGetValidRbc2CnfAlgorithms(
    
)
String of valid conversion algorithms


int 
Rbc_CnfVar2RbcIndex(
  Rbc_Manager_t* rbcManager, 
  int  cnfVar 
)
Returns -1, if there is no original RBC variable corresponding to CNF variable, this may be the case if CNF variable corresponds to an internal node (not leaf) of RBC tree. Input CNF variable should be a correct variable generated by RBC manager.


int 
Rbc_Convert2CnfCompact(
  Rbc_Manager_t* rbcManager, 
  Rbc_t* f, 
  int  polarity, 
  Slist_ptr  clauses, 
  Slist_ptr  vars, 
  int* literalAssignedToWholeFormula 
)
Given `rbcManager' and `f', `clauses' is filled with the disjunctions corresponding to the rbc nodes according to the 'compact' algorithm by Dan Sheridan. `vars' is filled with the variables that occurred in `f' (original or model variables). It is user's responsibility to create `clauses' and `vars' *before* calling the function. New variables are added by the conversion: the maximum index (the last added variable) is returned by the function. The function returns 0 when `f' is true or false. 'polarity' defines whether 'f' has to be true, false, or either (1, -1 or 0 respectively). If 'polarity' is 1/-1 then only the clauses representing the true/false RBC are returned. Otherwise, both sets are returned.

Side Effects `clauses' and `vars' are filled up. `clauses' is the empty list if `f' was true, and contains a single empty clause if `f' was false.


int 
Rbc_Convert2CnfSimple(
  Rbc_Manager_t* rbcManager, 
  Rbc_t* f, 
  Slist_ptr  clauses, 
  Slist_ptr  vars, 
  int* literalAssignedToWholeFormula 
)
Given `rbcManager' and `f', `clauses' is filled with the disjunctions corresponding to the rbc nodes according to the rules: f = A & B => -f A f = A <-> B => f A B -f B f -A -B f -A -B -f -A B -f A -B f = if A then B else C => f A -C f -A -B -f A C -f -A B `vars' is filled with the variables that occurred in `f' (original or model variables converted into corresponding CNF variables). It is user's responsibility to create `clauses' and `vars' *before* calling the function. New variables are added by the conversion: the maximum index is returned by the function. The literal associated to 'f' is assigned to parameter *literalAssignedToWholeFormula (it may be negative). Special case - A CONSTANT (this is consistent with description of Be_Cnf_ptr): if the formula is a constant then *literalAssignedToWholeFormula will be INT_MAX and the return value will 0. if formula is true, `clauses' is the empty list, if formula is false, `clauses' contains a single empty clause.

Side Effects `clauses', `vars' and '*literalAssignedToWholeFormula' are filled up. Fields inside rbcManager might change


int 
Rbc_Convert2Cnf(
  Rbc_Manager_t* rbcManager, 
  Rbc_t* f, 
  int  polarity, 
  Slist_ptr  clauses, 
  Slist_ptr  vars, 
  int* literalAssignedToWholeFormula 
)
This calls the user's choice of translation procedure

Side Effects `clauses' and `vars' are filled up. `clauses' is the empty list if `f' was true, and contains a single empty clause if `f' was false. '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.


Rbc_t * 
Rbc_GetIthVar(
  Rbc_Manager_t * rbcManager, 
  int  varIndex 
)
Returns a pointer to an rbc node containing the requested variable. Works in three steps:

Side Effects none


Rbc_t * 
Rbc_GetLeftOpnd(
  Rbc_t * f 
)
Gets the left operand.

Side Effects none


Rbc_t * 
Rbc_GetOne(
  Rbc_Manager_t * rbcManager 
)
Returns the rbc that stands for logical truth.

Side Effects none


Rbc_t * 
Rbc_GetRightOpnd(
  Rbc_t * f 
)
Gets the right operand.

Side Effects none


int 
Rbc_GetVarIndex(
  Rbc_t* f 
)
Returns the variable index, -1 if the rbc is not a variable.

Side Effects none


Rbc_t * 
Rbc_GetZero(
  Rbc_Manager_t * rbcManager 
)
Returns the rbc that stands for logical falsity.

Side Effects none


boolean 
Rbc_IsConstant(
  Rbc_Manager_t* manager, 
  Rbc_t* f 
)
Returns true if the given rbc is a constant value, such as either False or True


Rbc_t* 
Rbc_LogicalShift(
  Rbc_Manager_t* rbcManager, 
  Rbc_t* f, 
  int  shift, 
  const int* log2phy, 
  const int* phy2log 
)
Given `rbcManager', the rbc `f', and the integer `shift', replaces every occurence of the variable x_i in in `f' with the variable x_(i + shift). Notice that in this context, 'i' is a LOGICAL index, not physical, i.e. the substitution array is provided in terms of logical indices, and is related only to the logical level. For a substitution at physical level, see Rbc_SubstRbc. 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.

Side Effects none


Rbc_t* 
Rbc_LogicalSubstRbc(
  Rbc_Manager_t* rbcManager, 
  Rbc_t* f, 
  Rbc_t** substRbc, 
  int* phy2log 
)
Given `rbcManager', the rbc `f', and the array of rbcs `substRbc', replaces every occurence of the variable x_i in in `f' with the rbc r_i provided that substRbc[i

Side Effects none


Rbc_t* 
Rbc_LogicalSubst(
  Rbc_Manager_t* rbcManager, 
  Rbc_t* f, 
  int* subst, 
  const int* log2phy, 
  const int* phy2log 
)
Given `rbcManager', the rbc `f', and the array of integers `subst', replaces every occurence of the variable x_i in in `f' with the variable x_j provided that subst[i

Side Effects none

See Also Rbc_Subst

Rbc_t * 
Rbc_MakeAnd(
  Rbc_Manager_t * rbcManager, 
  Rbc_t * left, 
  Rbc_t * right, 
  Rbc_Bool_c  sign 
)
Makes the conjunction of two rbcs. Works in three steps:

Side Effects none


Rbc_t * 
Rbc_MakeIff(
  Rbc_Manager_t * rbcManager, 
  Rbc_t * left, 
  Rbc_t * right, 
  Rbc_Bool_c  sign 
)
Makes the coimplication of two rbcs. Works in four steps:

Side Effects none


Rbc_t * 
Rbc_MakeIte(
  Rbc_Manager_t * rbcManager, 
  Rbc_t * i, 
  Rbc_t * t, 
  Rbc_t * e, 
  Rbc_Bool_c  sign 
)
Makes the if-then-else of three rbcs: expands the connective into the corresponding product-of-sums.

Side Effects none


Rbc_t* 
Rbc_MakeNot(
  Rbc_Manager_t* rbcManager, 
  Rbc_t* left 
)
Returns the complement of an rbc.

Side Effects none


Rbc_t * 
Rbc_MakeOr(
  Rbc_Manager_t * rbcManager, 
  Rbc_t * left, 
  Rbc_t * right, 
  Rbc_Bool_c  sign 
)
Makes the disjunction of two rbcs: casts the connective to the negation of a conjunction using De Morgan's law.

Side Effects none


Rbc_t * 
Rbc_MakeXor(
  Rbc_Manager_t * rbcManager, 
  Rbc_t * left, 
  Rbc_t * right, 
  Rbc_Bool_c  sign 
)
Makes the exclusive disjunction of two rbcs: casts the connective as the negation of a coimplication.

Side Effects none


Rbc_Manager_t * 
Rbc_ManagerAlloc(
  int  varCapacity 
)
Creates a new RBC manager: Returns the allocated manager if varCapacity is greater than 0, and NIL(Rbc_Manager_t) otherwise.

Side Effects none

See Also Rbc_ManagerFree

int 
Rbc_ManagerCapacity(
  Rbc_Manager_t * rbcManager 
)
This number is the maximum number of variables (starting from 0) that can be requested without causing any memory allocation.

Side Effects none


void 
Rbc_ManagerFree(
  Rbc_Manager_t * rbcManager 
)
Frees the variable index and the internal dag manager.

Side Effects none


void 
Rbc_ManagerGC(
  Rbc_Manager_t * rbcManager 
)
Relies on the internal DAG garbage collector.

Side Effects None


void 
Rbc_ManagerReserve(
  Rbc_Manager_t * rbcManager, 
  int  newVarCapacity 
)
If the requested space is bigger than the current one makes room for more variables in the varTable.

Side Effects none


void 
Rbc_Mark(
  Rbc_Manager_t * rbc, 
  Rbc_t * f 
)
Marks the vertex in the internal dag. This saves the rbc from being wiped out during garbage collection.

Side Effects none


void 
Rbc_OutputDaVinci(
  Rbc_Manager_t * rbcManager, 
  Rbc_t * f, 
  FILE * outFile 
)
Print out an rbc using DaVinci graph format.

Side Effects None


void 
Rbc_OutputGdl(
  Rbc_Manager_t * rbcManager, 
  Rbc_t * f, 
  FILE * outFile 
)
Print out an rbc using Gdl graph format.

Side Effects None


void 
Rbc_OutputSexpr(
  Rbc_Manager_t * rbcManager, 
  Rbc_t * f, 
  FILE * outFile 
)
Print out an rbc using LISP S-exrpressions.

Side Effects None


void 
Rbc_PrintStats(
  Rbc_Manager_t * rbcManager, 
  int  clustSz, 
  FILE * outFile 
)
Prints various statistics.

Side Effects None


int 
Rbc_RbcIndex2CnfVar(
  Rbc_Manager_t* rbcManager, 
  int  rbcIndex 
)
Returns 0, if there is no original RBC variable corresponding to CNF variable. This may be the case if particular RBC node (of the given variable) has never been converted into CNF


Rbc_t* 
Rbc_Shift(
  Rbc_Manager_t* rbcManager, 
  Rbc_t* f, 
  int  shift 
)
Given `rbcManager', the rbc `f', and the integer `shift', replaces every occurence of the variable x_i in in `f' with the variable x_(i + shift). !!!!!! WARNING WARNING WARNING WARNING WARNING WARNING !!!!! !! !! !! This function cannot be used with the new encoding BeEnc, !! !! with NuSMV-2.4. 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 Rbc_LogicalShiftVar instead. !! !! !! !!!!!! WARNING WARNING WARNING WARNING WARNING WARNING !!!!!

Side Effects none


Rbc_t * 
Rbc_SubstRbc(
  Rbc_Manager_t * rbcManager, 
  Rbc_t * f, 
  Rbc_t ** substRbc 
)
Given `rbcManager', the rbc `f', and the array of rbcs `substRbc', replaces every occurence of the variable x_i in in `f' with the rbc r_i provided that substRbc[i

Side Effects none


Rbc_t * 
Rbc_Subst(
  Rbc_Manager_t * rbcManager, 
  Rbc_t * f, 
  int * subst 
)
Given `rbcManager', the rbc `f', and the array of integers `subst', replaces every occurence of the variable x_i in in `f' with the variable x_j provided that subst[i

Side Effects none

See Also Rbc_LogicalSubst

void 
Rbc_Unmark(
  Rbc_Manager_t * rbc, 
  Rbc_t * f 
)
Unmarks the vertex in the internal dag. This exposes the rbc to garbage collection.

Side Effects none


int 
Rbc_get_node_cnf(
  Rbc_Manager_t* rbcm, 
  Rbc_t* f, 
  int* maxvar 
)
Given a rbc node, this function returns the corrensponding CNF var it had been already allocated one. Otherwise it will allocate a new CNF var and will increment given maxvar value. If f is RBCDUMMY, a new variable will be always allocated (intended to be a non-terminal var, but a corresponding RBC var will be not allocated)


void 
rbc_inlining_cache_add_result(
  Rbc_t* f, 
  InlineResult_ptr  res 
)
Inline caching private service


void 
rbc_inlining_cache_init(
    
)
Inline caching private service


InlineResult_ptr 
rbc_inlining_cache_lookup_result(
  Rbc_t* f 
)
Inline caching private service


void 
rbc_inlining_cache_quit(
    
)
Inline caching private service


Last updated on 2010/11/03 21h:54