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:
- the requested variable index exceeds the current capacity:
allocated more room up to the requested index;
- the variable node does not exists: inserts it in the dag
and makes it permanent;
- returns the variable node.
- 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:
- performs boolean simplification: if successfull, returns
the result of the simplification;
- orders left and right son pointers;
- looks up the formula in the dag and returns it.
- 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:
- performs boolean simplification: if successfull, returns
the result of the simplification;
- orders left and right son pointers;
- re-encodes the negation
- looks up the formula in the dag and returns it.
- 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.
- 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:
- varCapacity how big is the variable index
(this number must be strictly greater than 0)
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_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 'f', 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
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
(
)
- Control the way compact CNF conversion is performed
- Side Effects none
- Defined in
rbcInt.h
(
)
- The pointer is filtered by a bitwise-xor with either RBC_FALSE
or RBC_TRUE. The pointer is not altered, but the leftmost bit
is complemented when s==RBC_FALSE and goes unchanged when
s == RBC_TRUE.
- Side Effects none
- Defined in
rbcInt.h