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,
lsList clauses,
lsList 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,
lsList clauses,
lsList 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,
lsList clauses,
lsList 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:
- 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
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:
- 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
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
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:
- 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
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