Internal functions and data structures of the rbc package.

static void 
CnfBack(
  Rbc_t* f, 
  char* cnfData, 
  nusmv_ptrint  sign 
)
Dfs BackVisit for CNF conversion.

Side Effects None

Defined in rbcCnfSimple.c

static void 
CnfCompactBack(
  Rbc_t* f, 
  char* cnfData, 
  nusmv_ptrint  sign 
)
Dfs BackVisit for CNF conversion.

Side Effects None

Defined in rbcCnfCompact.c

static void 
CnfCompactCleanFirst(
  Dag_Vertex_t* f, 
  char* cleanData, 
  nusmv_ptrint  sign 
)
Dfs FirstVisit for cleaning.

Side Effects None

Defined in rbcCnfCompact.c

static int 
CnfCompactCleanSet(
  Dag_Vertex_t* f, 
  char* cleanData, 
  nusmv_ptrint  sign 
)
Dfs Set for cleaning.

Side Effects None

Defined in rbcCnfCompact.c

static void 
CnfCompactCommit(
  void* data, 
  int* cl, 
  int  size 
)
Extracts the cnf from the CLG

Side Effects None

Defined in rbcCnfCompact.c

static void 
CnfCompactFirst(
  Rbc_t* f, 
  char* cnfData, 
  nusmv_ptrint  sign 
)
Dfs FirstVisit for CNF conversion.

Side Effects None

Defined in rbcCnfCompact.c

static void 
CnfCompactLast(
  Rbc_t* f, 
  char* cnfData, 
  nusmv_ptrint  sign 
)
Dfs LastVisit for CNF conversion.

Side Effects None

Defined in rbcCnfCompact.c

static void 
CnfCompactPolFirstBack(
  Rbc_t* f, 
  char* cnfData, 
  nusmv_ptrint  sign 
)
Dfs FirstVisit and BackVisit for CNF conversion polarity computation.

Side Effects None

Defined in rbcCnfCompact.c

static int 
CnfCompactPolSet(
  Rbc_t* f, 
  char* cnfData, 
  nusmv_ptrint  sign 
)
Dfs Set for CNF conversion polarity computation.

Side Effects None

Defined in rbcCnfCompact.c

static int 
CnfCompactSet(
  Rbc_t* f, 
  char* cnfData, 
  nusmv_ptrint  sign 
)
Dfs Set for CNF conversion.

Side Effects None

Defined in rbcCnfCompact.c

static void 
CnfEmpty(
  Rbc_t* f, 
  char* cnfData, 
  nusmv_ptrint  sign 
)
Empty function as null operation during DFS

Side Effects None

Defined in rbcCnfCompact.c

static void 
CnfFirst(
  Rbc_t* f, 
  char* cnfData, 
  nusmv_ptrint  sign 
)
Dfs FirstVisit for CNF conversion.

Side Effects None

Defined in rbcCnfSimple.c

static void 
CnfLast(
  Rbc_t* f, 
  char* cnfData, 
  nusmv_ptrint  sign 
)
Dfs LastVisit for CNF conversion.

Side Effects None

Defined in rbcCnfSimple.c

static int 
CnfSet(
  Rbc_t* f, 
  char* cnfData, 
  nusmv_ptrint  sign 
)
Dfs Set for CNF conversion.

Side Effects None

Defined in rbcCnfSimple.c

static void 
DaVinciBack(
  Rbc_t * f, 
  char * daVinciData, 
  nusmv_ptrint  sign 
)
Dfs BackVisit for DaVinci output.

Side Effects None

Defined in rbcOutput.c

static void 
DaVinciFirst(
  Rbc_t * f, 
  char * DaVinciData, 
  nusmv_ptrint  sign 
)
Dfs FirstVisit for DaVinci output.

Side Effects None

Defined in rbcOutput.c

static void 
DaVinciLast(
  Rbc_t * f, 
  char * daVinciData, 
  nusmv_ptrint  sign 
)
Dfs LastVisit for DaVinci outputon.

Side Effects None

Defined in rbcOutput.c

static int 
DaVinciSet(
  Rbc_t * f, 
  char * daVinciData, 
  nusmv_ptrint  sign 
)
Dfs Set for DaVinci output.

Side Effects None

Defined in rbcOutput.c

static void 
GdlBack(
  Rbc_t * f, 
  char * GdlData, 
  nusmv_ptrint  sign 
)
Dfs BackVisit for Gdl output.

Side Effects None

Defined in rbcOutput.c

static void 
GdlFirst(
  Rbc_t * f, 
  char * GdlData, 
  nusmv_ptrint  sign 
)
Dfs FirstVisit for Gdl output.

Side Effects None

Defined in rbcOutput.c

static void 
GdlLast(
  Rbc_t * f, 
  char * GdlData, 
  nusmv_ptrint  sign 
)
Dfs LastVisit for Gdl outputon.

Side Effects None

Defined in rbcOutput.c

static int 
GdlSet(
  Rbc_t * f, 
  char * GdlData, 
  nusmv_ptrint  sign 
)
Dfs Set for Gdl output.

Side Effects None

Defined in rbcOutput.c

static void 
LogicalShiftLast(
  Rbc_t* f, 
  char* shiftData, 
  nusmv_ptrint  sign 
)
Dfs LastVisit for logical shifting.

Side Effects None

Defined in rbcSubst.c

static void 
LogicalSubstLast(
  Rbc_t* f, 
  char* SubstData, 
  nusmv_ptrint  sign 
)
Dfs LastVisit for logical Substitution.

Side Effects None

Defined in rbcSubst.c

static void 
LogicalSubstRbcLast(
  Rbc_t* f, 
  char* SubstRbcData, 
  nusmv_ptrint  sign 
)
Dfs LastVisit for logical Rbc Substitution.

Side Effects None

Defined in rbcSubst.c

InlineResult_ptr 
RbcInline_apply_inlining(
  Rbc_Manager_t* rbcm, 
  Rbc_t* f 
)
Returned InlineResult instance is cached and must be _NOT_ destroyed by the caller

Side Effects None

See Also InlineResult
Defined in rbcInline.c

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

Defined in rbcCnf.c

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

Defined in rbcCnf.c

const char * 
Rbc_CnfGetValidRbc2CnfAlgorithms(
    
)
String of valid conversion algorithms

Defined in rbcCnf.c

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.

Defined in rbcCnf.c

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.

Defined in rbcCnfCompact.c

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

Defined in rbcCnfSimple.c

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.

Defined in rbcCnf.c

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

Defined in rbcFormula.c

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

Side Effects none

Defined in rbcFormula.c

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

Side Effects none

Defined in rbcFormula.c

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

Side Effects none

Defined in rbcFormula.c

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

Side Effects none

Defined in rbcFormula.c

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

Side Effects none

Defined in rbcFormula.c

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

Defined in rbcFormula.c

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

Defined in rbcSubst.c

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

Defined in rbcSubst.c

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
Defined in rbcSubst.c

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: If RBC_ENABLE_LOCAL_MINIMIZATION_WITHOUT_BLOWUP is defined, applies all the rules proposed in "R. Brummayer and A. Biere. Local Two-Level And-Inverter Graph Minimization without Blowup". In Proc. MEMICS 2006. The expressions o1, o2, o3, o4 refers to the four level of optimization proposed in the paper. The rules are implemented as macros in order to avoid repetitions

Side Effects none

Defined in rbcFormula.c

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

Defined in rbcFormula.c

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. If the if-then-else mode is disable, expands the connective in three AND nodes

Side Effects none

Defined in rbcFormula.c

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

Side Effects none

Defined in rbcFormula.c

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

Defined in rbcFormula.c

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

Defined in rbcFormula.c

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
Defined in rbcManager.c

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

Defined in rbcManager.c

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

Side Effects none

Defined in rbcManager.c

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

Side Effects None

Defined in rbcManager.c

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

Defined in rbcManager.c

void 
Rbc_ManagerReset(
  Rbc_Manager_t * rbcManager 
)
Resets RBC manager

Side Effects none

Defined in rbcManager.c

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

Defined in rbcFormula.c

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

Side Effects None

Defined in rbcOutput.c

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

Side Effects None

Defined in rbcOutput.c

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

Side Effects None

Defined in rbcOutput.c

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

Side Effects None

Defined in rbcStat.c

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

Defined in rbcCnf.c

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

Defined in rbcSubst.c

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

Defined in rbcSubst.c

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
Defined in rbcSubst.c

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

Defined in rbcFormula.c

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 if 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)

Defined in rbcCnf.c

boolean 
Rbc_is_and(
  Rbc_t* rbc 
)
Check if a rbc type is RBCAND

Defined in rbcFormula.c

boolean 
Rbc_is_iff(
  Rbc_t* rbc 
)
Check if a rbc type is RBCIFF

Defined in rbcFormula.c

boolean 
Rbc_is_ite(
  Rbc_t* rbc 
)
Check if a rbc type is RBCITE

Defined in rbcFormula.c

boolean 
Rbc_is_top(
  Rbc_t* rbc 
)
Check if a rbc type is RBCTOP

Defined in rbcFormula.c

boolean 
Rbc_is_var(
  Rbc_t* rbc 
)
Check if a rbc type is RBCVAR

Defined in rbcFormula.c

static Rbc_t* 
Reduce(
  Rbc_Manager_t* rbcManager, 
  int  op, 
  Rbc_t* left, 
  Rbc_t* right 
)
Reduction (simplification) of rbcs.

Side Effects none

Defined in rbcFormula.c

static void 
SexprBack(
  Rbc_t * f, 
  char * SexprData, 
  nusmv_ptrint  sign 
)
Dfs BackVisit for Sexpr output.

Side Effects None

Defined in rbcOutput.c

static void 
SexprFirst(
  Rbc_t * f, 
  char * SexprData, 
  nusmv_ptrint  sign 
)
Dfs FirstVisit for Sexpr output.

Side Effects None

Defined in rbcOutput.c

static void 
SexprLast(
  Rbc_t * f, 
  char * SexprData, 
  nusmv_ptrint  sign 
)
Dfs LastVisit for Sexpr outputon.

Side Effects None

Defined in rbcOutput.c

static int 
SexprSet(
  Rbc_t * f, 
  char * SexprData, 
  nusmv_ptrint  sign 
)
Dfs Set for Sexpr output.

Side Effects None

Defined in rbcOutput.c

static void 
ShiftBack(
  Rbc_t * f, 
  char * shiftData, 
  nusmv_ptrint  sign 
)
Dfs BackVisit for shifting.

Side Effects None

Defined in rbcSubst.c

static void 
ShiftFirst(
  Rbc_t * f, 
  char * shiftData, 
  nusmv_ptrint  sign 
)
Dfs FirstVisit for shifting.

Side Effects None

Defined in rbcSubst.c

static void 
ShiftLast(
  Rbc_t * f, 
  char * shiftData, 
  nusmv_ptrint  sign 
)
Dfs LastVisit for shifting.

Side Effects None

Defined in rbcSubst.c

static int 
ShiftSet(
  Rbc_t * f, 
  char * shiftData, 
  nusmv_ptrint  sign 
)
Dfs Set for shifting.

Side Effects None

Defined in rbcSubst.c

static void 
SubstBack(
  Rbc_t * f, 
  char * SubstData, 
  nusmv_ptrint  sign 
)
Dfs BackVisit for substitution.

Side Effects None

Defined in rbcSubst.c

static void 
SubstFirst(
  Rbc_t * f, 
  char * SubstData, 
  nusmv_ptrint  sign 
)
Dfs FirstVisit for substitution.

Side Effects None

Defined in rbcSubst.c

static void 
SubstLast(
  Rbc_t* f, 
  char* SubstData, 
  nusmv_ptrint  sign 
)
Dfs LastVisit for Substitution.

Side Effects None

Defined in rbcSubst.c

static void 
SubstRbcBack(
  Rbc_t * f, 
  char * SubstRbcData, 
  nusmv_ptrint  sign 
)
Dfs BackVisit for substRbcitution.

Side Effects None

Defined in rbcSubst.c

static void 
SubstRbcFirst(
  Rbc_t * f, 
  char * SubstRbcData, 
  nusmv_ptrint  sign 
)
Dfs FirstVisit for substitution (variables to formulas).

Side Effects None

Defined in rbcSubst.c

static void 
SubstRbcLast(
  Rbc_t * f, 
  char * SubstRbcData, 
  nusmv_ptrint  sign 
)
Dfs LastVisit for SubstRbcitution.

Side Effects None

Defined in rbcSubst.c

static int 
SubstRbcSet(
  Rbc_t * f, 
  char * SubstRbcData, 
  nusmv_ptrint  sign 
)
Dfs Set for substitution (variables to formulas).

Side Effects None

Defined in rbcSubst.c

static int 
SubstSet(
  Rbc_t * f, 
  char * SubstData, 
  nusmv_ptrint  sign 
)
Dfs Set for substitution.

Side Effects None

Defined in rbcSubst.c

static lsGeneric 
SwapSign(
  lsGeneric  data 
)
Swaps the sign of the argument.

Side Effects None

Defined in rbcCnfSimple.c

static inline void 
disjunction2(
  clause_graph* Left1, 
  clause_graph* Right1, 
  clause_graph* Left2, 
  clause_graph* Right2, 
  int* maxVar, 
  clause_graph* clauses, 
  Rbc_Manager_t* rbcm 
)
Compute the disjunction of two clause sets

Side Effects None

Defined in rbcCnfCompact.c

static inline void 
disjunction(
  clause_graph* Left, 
  clause_graph* Right, 
  int* maxVar, 
  clause_graph* clauses, 
  Rbc_Manager_t* rbcm 
)
Compute the disjunction of two clause sets

Side Effects None

Defined in rbcCnfCompact.c

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

Defined in rbcInline.c

void 
rbc_inlining_cache_init(
    
)
Inline caching private service

Defined in rbcInline.c

InlineResult_ptr 
rbc_inlining_cache_lookup_result(
  Rbc_t* f 
)
Inline caching private service

Defined in rbcInline.c

void 
rbc_inlining_cache_quit(
    
)
Inline caching private service

Defined in rbcInline.c

static void 
rename_clauses(
  clause_graph* clauses, 
  int  var, 
  clause_graph* saved 
)
Renames a set of clauses by adding -var to each clause and adding each clause to the list of saved clauses. Allocates a new variable if var==0. Returns var or the new variable. Refuses to rename a single clause; returns 0 in this case

Side Effects clauses refers to the singleton clause set referring to the renamed clauses

Defined in rbcCnfCompact.c

static inline int 
testSizes(
  clause_graph  left, 
  clause_graph  right 
)
Check whether two clause sets are big enough to require renaming

Side Effects None

Defined in rbcCnfCompact.c

 
(
    
)
Works in two steps:

Side Effects If RBC_ENABLE_LOCAL_MINIMIZATION_WITHOUT_BLOWUP is not 1: "a" is modified; "changed" is modified, the enclosing while loop will be rerun when finished; all the rules will be checked again

See Also Rbc_MakeAnd()
Defined in rbcFormula.c

 
(
    
)
Works in two steps: "changed" is passed to those minimization rules which could modify a or b, the parent rbcs

Side Effects none

See Also Rbc_MakeAnd()
Defined in rbcFormula.c

 
(
    
)
Works in two steps: "changed" is passed to those minimization rules which could modify a or b, the parent rbcs

Side Effects none

See Also Rbc_MakeAnd()
Defined in rbcFormula.c

 
(
    
)
Control the way compact CNF conversion is performed

Side Effects none

Defined in rbcInt.h

 
(
    
)
Get the right children.

Defined in rbcInt.h

 
(
    
)
Gets the children only of the non-NIL passed rbcs between left or right and makes all the needed assertions

Side Effects To l1, l2, r1 and r2 are assigned the pointers of the children of the non-NIL passed rbcs

See Also Rbc_MakeAnd()
Defined in rbcFormula.c

 
(
    
)
Rbc interface to underlying package

Defined in rbcInt.h

 
(
    
)
If the rule is satisfied, returns the false or true rbc, based on sign: (s)AND(AND(a,b),c) = (s)F if c = ~a. The rule is applied in all its commutative variants.

Side Effects None

See Also Rbc_MakeAnd()
Defined in rbcFormula.c

 
(
    
)
If the rule is satisfied, substitute d, the parent of a and b, with the negation of one of its children: (s)AND(d,c) = (s)AND(~AND(a,b),c) = (s)AND(~b,c) if a = c then d = ~b. The rule is applied in all its commutative variants.

Side Effects If the rule is satisfied: "d" is modified; "changed" is modified, the enclosing while loop will be rerun when finished; all the rules will be checked again

See Also Rbc_MakeAnd()
Defined in rbcFormula.c

 
(
    
)
If the rule is satisfied, return the passed rbc: (s)AND(~AND(a,b),c) = (s)c if a = ~c. The rule is applied in all its commutative variants.

Side Effects None

See Also Rbc_MakeAnd()
Defined in rbcFormula.c

 
(
    
)
If the rule is satisfied, returns d, the parent of a and b: (s)AND(AND(a,b),c) = (s)AND(a,b) = (s)d if c = a The rule is applied in all its commutative variants.

Side Effects none

See Also Rbc_MakeAnd()
Defined in rbcFormula.c

 
(
    
)
If the rule is satisfied, substitute e, the parent of c and d, with one of its children. (s)AND(AND(a,b),e) = (s)AND(AND(a,b),AND(c,d)) = = (s)AND(AND(a,b),d) if c = a then e = d The rule is applied in all its commutative variants.

Side Effects If the rule is satisfied: "e" is modified; "changed" is modified, the enclosing while loop will be rerun when finished; all the rules will be checked again

See Also Rbc_MakeAnd()
Defined in rbcFormula.c

 
(
    
)
If the rule is satisfied, return the negation of one of the children passed: (s)AND(~AND(a,b),~AND(c,d)) = (s)~a if c = ~b & d = a. The rule is applied in all its commutative variants.

Side Effects None

See Also Rbc_MakeAnd()
Defined in rbcFormula.c

 
(
    
)
If the rule is satisfied, substitute e, the parent of a and b, with the negation of one of its children. (s)AND(e,AND(c,d)) = = (s)AND(~AND(a,b),AND(c,d)) = = (s)AND(~a,AND(c,d)) if b = c. The rule is applied in all its commutative variants.

Side Effects If the rule is satisfied: "e" is modified; "changed" is modified, the enclosing while loop will be rerun when finished; all the rules will be checked again

See Also Rbc_MakeAnd()
Defined in rbcFormula.c

 
(
    
)
If the rule is satisfied, returns e, the parent of c and d: (s)AND(~AND(a,b),e) = (s)AND(~AND(a,b),AND(c,d)) = (s)e if a = ~c The rule is applied in all its commutative variants.

Side Effects None

See Also Rbc_MakeAnd()
Defined in rbcFormula.c

Last updated on 2011/06/16 12h:15